From 3c576e7e17abb6c14ee2bb679660064070504b24 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Tue, 14 May 2024 22:42:31 +0200 Subject: [PATCH] Remove unnecessary hypotheses from `mutual_comp_le` and `mutual_comp_comp_le`. Co-authored-by: Lorenzo Luccioli --- PFR/MoreRuzsaDist.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/PFR/MoreRuzsaDist.lean b/PFR/MoreRuzsaDist.lean index 9f95c12f..a81160f2 100644 --- a/PFR/MoreRuzsaDist.lean +++ b/PFR/MoreRuzsaDist.lean @@ -32,11 +32,11 @@ variable {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} {V : Type uV} Let $X,Y$ be random variables. For any function $f, g$ on the range of $X$, we have $I[f(X) : Y] \leq I[X:Y]$. -/ lemma mutual_comp_le (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X) - (hY : Measurable Y) (f : S → U) (hf : Measurable f) [FiniteRange X] [FiniteRange Y] : + (hY : Measurable Y) (f : S → U) [FiniteRange X] [FiniteRange Y] : I[f ∘ X : Y ; μ] ≤ I[X : Y ; μ] := by - rw [mutualInfo_comm (Measurable.comp hf hX) hY, mutualInfo_comm hX hY, - mutualInfo_eq_entropy_sub_condEntropy hY (Measurable.comp hf hX), - mutualInfo_eq_entropy_sub_condEntropy hY hX] + have h_meas : Measurable (f ∘ X) := Measurable.comp (measurable_discrete f) hX + rw [mutualInfo_comm h_meas hY, mutualInfo_comm hX hY, + mutualInfo_eq_entropy_sub_condEntropy hY h_meas, mutualInfo_eq_entropy_sub_condEntropy hY hX] gcongr exact condEntropy_comp_ge μ hX hY f @@ -45,13 +45,13 @@ lemma mutual_comp_le (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurabl have $\bbI[f(X) : g(Y)] \leq \bbI[X : Y]$. -/ lemma mutual_comp_comp_le (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X) - (hY : Measurable Y) (f : S → U) (g : T → V) (hf : Measurable f) (hg : Measurable g) [ - FiniteRange X] [FiniteRange Y]: + (hY : Measurable Y) (f : S → U) (g : T → V) (hg : Measurable g) + [FiniteRange X] [FiniteRange Y] : I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ] := calc - _ ≤ I[X : g ∘ Y ; μ] := mutual_comp_le μ hX (Measurable.comp hg hY) f hf + _ ≤ I[X : g ∘ Y ; μ] := mutual_comp_le μ hX (Measurable.comp hg hY) f _ = I[g ∘ Y : X ; μ] := mutualInfo_comm hX (Measurable.comp hg hY) μ - _ ≤ I[Y : X ; μ] := mutual_comp_le μ hY hX g hg + _ ≤ I[Y : X ; μ] := mutual_comp_le μ hY hX g _ = I[X : Y ; μ] := mutualInfo_comm hY hX μ /--