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

ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq

PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:406 to 417

Mathematical statement

Exact Lean statement

lemma measureEntropy_eq_card_iff_measure_eq [Fintype S] [IsFiniteMeasure μ] [NeZero μ] :
    Hm[μ] = log (Fintype.card S) ↔
    (∀ s : S, μ {s} = μ Set.univ / Fintype.card S)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma measureEntropy_eq_card_iff_measure_eq [Fintype S] [IsFiniteMeasure μ] [NeZero μ] :    Hm[μ] = log (Fintype.card S) ↔    (∀ s : S, μ {s} = μ Set.univ / Fintype.card S) := by  obtain h | h := isEmpty_or_nonempty S  · have : μ = 0 := Subsingleton.elim _ _    simp [Fintype.card_eq_zero, this]  rw [div_eq_mul_inv, measureEntropy_eq_card_iff_measureReal_eq]  congr! with s  rw [measureReal_def, ← ENNReal.toReal_eq_toReal_iff' (measure_ne_top μ {s})]  · rw [ENNReal.toReal_mul, ENNReal.toReal_inv]    rfl  · finiteness