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

ProbabilityTheory.condEntropy_comp_ge

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:1095 to 1107

Source documentation

Data-processing inequality for the conditional entropy: H[Y|f(X)] ≥ H[Y|X] To upgrade this to equality, see condEntropy_of_injective'

Exact Lean statement

lemma condEntropy_comp_ge
    [FiniteRange X] [FiniteRange Y] (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (f : S → U) : H[Y | f ∘ X ; μ] ≥ H[Y | X; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condEntropy_comp_ge    [FiniteRange X] [FiniteRange Y] (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) (f : S → U) : H[Y | f ∘ X ; μ] ≥ H[Y | X; μ] := by  have h_joint : H[⟨Y, ⟨X, f ∘ X⟩⟩ ; μ] = H[⟨Y, X⟩ ; μ] := by    let g : T × S → T × S × U := fun (y, x) ↦ (y, (x, f x))    change H[g ∘ ⟨Y, X⟩ ; μ] = H[⟨Y, X⟩ ; μ]    refine entropy_comp_of_injective μ (by exact Measurable.prod hY hX) g (fun _ _ h => ?_)    repeat rewrite [Prod.mk.injEq] at h    exact Prod.ext h.1 h.2.1  have hZ : Measurable (f ∘ X) := by fun_prop  rewrite [chain_rule'' μ hY hX, ← entropy_prod_comp hX μ f, ← h_joint,    ← chain_rule'' μ hY (Measurable.prod (by exact hX) (by exact hZ))]  exact entropy_submodular μ hY hX hZ