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

ProbabilityTheory.condEntropy_le_log_card

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:424 to 431

Source documentation

Conditional entropy is at most the logarithm of the cardinality of the range.

Exact Lean statement

lemma condEntropy_le_log_card [MeasurableSingletonClass S] [Fintype S]
    (X : Ω → S) (Y : Ω → T) (hY : Measurable Y) (μ : Measure Ω) [IsProbabilityMeasure μ] :
    H[X | Y ; μ] ≤ log (Fintype.card S)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condEntropy_le_log_card [MeasurableSingletonClass S] [Fintype S]    (X : Ω → S) (Y : Ω → T) (hY : Measurable Y) (μ : Measure Ω) [IsProbabilityMeasure μ] :    H[X | Y ; μ] ≤ log (Fintype.card S) := by  refine (integral_mono_of_nonneg ?_ (integrable_const (log (Fintype.card S))) ?_).trans ?_  · exact ae_of_all _ (fun _ ↦ entropy_nonneg _ _)  · exact ae_of_all _ (fun _ ↦ entropy_le_log_card _ _)  · have : IsProbabilityMeasure (μ.map Y) := isProbabilityMeasure_map hY.aemeasurable    simp