Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.condMutual_comp_comp_le

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:1167 to 1181

Source documentation

Let X, Y, Z. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ].

Exact Lean statement

lemma condMutual_comp_comp_le (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X)
    (hY : Measurable Y) (hZ : Measurable Z) (f : S → V) (g : T → W) (hg : Measurable g)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condMutual_comp_comp_le (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X)    (hY : Measurable Y) (hZ : Measurable Z) (f : S → V) (g : T → W) (hg : Measurable g)    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :    I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ] := by  rw [condMutualInfo_eq_sum hZ, condMutualInfo_eq_sum hZ]  apply Finset.sum_le_sum  intro i _  rcases eq_or_lt_of_le (measureReal_nonneg (μ := μ) (s := (Z ⁻¹' {i}))) with h | h  · simp [← h]  · gcongr    have : IsProbabilityMeasure (μ[|Z ← i]) := by      apply cond_isProbabilityMeasure_of_finite      · exact (ENNReal.toReal_ne_zero.mp (ne_of_gt h)).left      · exact (ENNReal.toReal_ne_zero.mp (ne_of_gt h)).right    apply mutual_comp_comp_le _ hX hY f g hg