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

ProbabilityTheory.entropy_eq_log_card

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:201 to 211

Source documentation

If X is S-valued random variable, then H[X] = log |S| if and only if X is uniformly distributed.

Exact Lean statement

lemma entropy_eq_log_card {X : Ω → S} [Fintype S] [MeasurableSingletonClass S]
    (hX : Measurable X) (μ : Measure Ω) [hμ : NeZero μ]
    [IsFiniteMeasure μ] :
    entropy X μ = log (Fintype.card S) ↔ ∀ s, μ.map X {s} = μ Set.univ / Fintype.card S

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma entropy_eq_log_card {X : Ω → S} [Fintype S] [MeasurableSingletonClass S]    (hX : Measurable X) (μ : Measure Ω) [hμ : NeZero μ]    [IsFiniteMeasure μ] :    entropy X μ = log (Fintype.card S) ↔ ∀ s, μ.map X {s} = μ Set.univ / Fintype.card S := by  rcases eq_zero_or_neZero (μ.map X) with h | h  · have := Measure.le_map_apply (@Measurable.aemeasurable Ω S _ _ X μ hX) Set.univ    simp [h] at this; simp [this] at hμ  have : IsFiniteMeasure (μ.map X) := by    apply Measure.isFiniteMeasure_map  rw [entropy_def, measureEntropy_eq_card_iff_measure_eq, Measure.map_apply hX MeasurableSet.univ]  simp