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

ProbabilityTheory.measureEntropy_le_log_card_of_mem

PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:359 to 370

Mathematical statement

Exact Lean statement

lemma measureEntropy_le_log_card_of_mem
    {A : Finset S} (μ : Measure S) (hμA : μ Aᶜ = 0) :
    Hm[μ] ≤ log A.card

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma measureEntropy_le_log_card_of_mem    {A : Finset S} (μ : Measure S) (hμA : μ Aᶜ = 0) :    Hm[μ] ≤ log A.card := by  have h_log_card_nonneg : 0 ≤ log (Nat.card A) := log_natCast_nonneg (Nat.card ↑A)  rcases eq_zero_or_neZero μ with rfl|hμ  · simp    positivity  by_cases hμ_fin : IsFiniteMeasure μ  · rw [← measureEntropy_univ_smul]    exact measureEntropy_le_card_aux A <| by simp [hμA]  · rw [measureEntropy_of_not_isFiniteMeasure hμ_fin]    exact log_natCast_nonneg _