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

ProbabilityTheory.prob_ge_exp_neg_entropy'

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:301 to 310

Source documentation

If X is an S-valued random variable, then there exists s ∈ S such that P[X=s] ≥ \exp(-H[X]).

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma prob_ge_exp_neg_entropy' [MeasurableSingletonClass S]    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}    [IsProbabilityMeasure μ] (X : Ω → S) (hX : Measurable X) [FiniteRange X] :    ∃ s : S, rexp (- H[X ; μ]) ≤ μ.real (X ⁻¹' {s}) := by  obtain ⟨s, hs⟩ := prob_ge_exp_neg_entropy X μ hX  use s  rwa [IsProbabilityMeasure.measure_univ, one_mul,    (show ENNReal.ofNNReal _ = ENNReal.ofReal _ from rfl),    ENNReal.ofReal_le_iff_le_toReal (measure_ne_top _ _), ← Measure.real,    map_measureReal_apply hX (MeasurableSet.singleton s)] at hs