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

continuous_rdist_restrict_probabilityMeasure₁

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:107 to 117

Mathematical statement

Exact Lean statement

lemma continuous_rdist_restrict_probabilityMeasure₁ [Finite G]
    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G]
    (X : Ω → G) (P : Measure Ω := by volume_tac) [IsProbabilityMeasure P] (X_mble : Measurable X) :
    Continuous
      (fun (μ : ProbabilityMeasure G) ↦ d[id ; P.map X # id ; μ.toMeasure])

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma continuous_rdist_restrict_probabilityMeasure₁ [Finite G]    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G]    (X : Ω → G) (P : Measure Ω := by volume_tac) [IsProbabilityMeasure P] (X_mble : Measurable X) :    Continuous      (fun (μ : ProbabilityMeasure G) ↦ d[id ; P.map X # id ; μ.toMeasure]) := by  have obs : IsProbabilityMeasure (P.map X) := by    refine ⟨by simp [Measure.map_apply X_mble MeasurableSet.univ]⟩  let ι : ProbabilityMeasure G → ProbabilityMeasure G × ProbabilityMeasure G :=      fun ν ↦ ⟨⟨P.map X, obs⟩, ν⟩  have ι_cont : Continuous ι := Continuous.prodMk_right _  convert! continuous_rdist_restrict_probabilityMeasure.comp ι_cont