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

condRuzsaDist_of_const

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:721 to 729

Source documentation

Conditioning by a constant does not affect Ruzsa distance.

Exact Lean statement

lemma condRuzsaDist_of_const {X : Ω → G} (hX : Measurable X)
    (Y : Ω' → G) (W : Ω' → T) (c : S)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [FiniteRange W] :
    d[X|(fun _ ↦ c) ; μ # Y | W ; μ'] = d[X ; μ # Y | W ; μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist_of_const {X : Ω → G} (hX : Measurable X)    (Y : Ω' → G) (W : Ω' → T) (c : S)    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [FiniteRange W] :    d[X|(fun _ ↦ c) ; μ # Y | W ; μ'] = d[X ; μ # Y | W ; μ'] := by  rw [condRuzsaDist_def, condRuzsaDist'_def, Measure.map_const, measure_univ, one_smul,    Kernel.rdist, Kernel.rdist, integral_prod _ (integrable_of_finiteSupport _), integral_dirac,    integral_prod _ (integrable_of_finiteSupport _), integral_dirac]  congr!  rw [condDistrib_apply hX measurable_const] <;> simp