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

ProbabilityTheory.const_of_nonpos_entropy

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:314 to 324

Source documentation

If X is an S-valued random variable of non-positive entropy, then X is almost surely constant.

Exact Lean statement

lemma const_of_nonpos_entropy [MeasurableSingletonClass S]
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : Ω → S} (hX : Measurable X) [FiniteRange X] (hent : H[X; μ] ≤ 0) :
    ∃ s : S, μ.real (X ⁻¹' {s}) = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma const_of_nonpos_entropy [MeasurableSingletonClass S]    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}    [IsProbabilityMeasure μ] {X : Ω → S} (hX : Measurable X) [FiniteRange X] (hent : H[X; μ] ≤ 0) :    ∃ s : S, μ.real (X ⁻¹' {s}) = 1 := by    rcases prob_ge_exp_neg_entropy' (μ := μ) X hX with ⟨ s, hs ⟩    use s    apply LE.le.antisymm    · rw [← probReal_univ (μ := μ)]      exact measureReal_mono (subset_univ _) (by finiteness)    refine le_trans ?_ hs    simp [hent]