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

continuous_measureEntropy_probabilityMeasure

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:42 to 52

Mathematical statement

Exact Lean statement

lemma continuous_measureEntropy_probabilityMeasure {Ω : Type*} [Finite Ω]
    [TopologicalSpace Ω] [DiscreteTopology Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] :
    Continuous (fun (μ : ProbabilityMeasure Ω) ↦ measureEntropy (S := Ω) μ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma continuous_measureEntropy_probabilityMeasure {Ω : Type*} [Finite Ω]    [TopologicalSpace Ω] [DiscreteTopology Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] :    Continuous (fun (μ : ProbabilityMeasure Ω) ↦ measureEntropy (S := Ω) μ) := by  cases nonempty_fintype Ω  unfold measureEntropy  simp_rw [tsum_fintype]  apply continuous_finsetSum  intro ω _  apply Real.continuous_negMulLog.comp  simp only [measure_univ, inv_one, one_smul]  exact continuous_probabilityMeasure_apply_of_isClopen (s := {ω}) <| isClopen_discrete _