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

ProbabilityTheory.entropy_comp_le

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:643 to 654

Source documentation

Data-processing inequality for the entropy: H[f(X)] ≤ H[X]. To upgrade this to equality, see entropy_of_comp_eq_of_comp or entropy_comp_of_injective.

Exact Lean statement

lemma entropy_comp_le (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (f : S → U) [FiniteRange X] :
    H[f ∘ X ; μ] ≤ H[X ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma entropy_comp_le (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (f : S → U) [FiniteRange X] :    H[f ∘ X ; μ] ≤ H[X ; μ] := by  have hfX : Measurable (f ∘ X) := by fun_prop  have : H[X ; μ] = H[⟨X, f ∘ X⟩ ; μ] := by    refine (entropy_comp_of_injective μ hX (fun x ↦ (x, f x)) ?_).symm    intro x y hxy    simp only [Prod.mk.injEq] at hxy    exact hxy.1  rw [this, chain_rule _ hX hfX]  simp only [le_add_iff_nonneg_right]  exact condEntropy_nonneg X (f ∘ X) μ