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

condRuzsaDist'_eq_integral

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:703 to 714

Source documentation

Explicit formula for conditional Ruzsa distance d[X ; Y | W], in integral form.

Exact Lean statement

lemma condRuzsaDist'_eq_integral (X : Ω → G) {Y : Ω' → G} {W : Ω' → T}
    (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) (μ' : Measure Ω') [IsFiniteMeasure μ'] [FiniteRange W] :
    d[X ; μ # Y | W ; μ']
      = (μ'.map W)[fun w ↦ d[X ; μ # Y ; (μ'[|W ← w])]]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist'_eq_integral (X : Ω → G) {Y : Ω' → G} {W : Ω' → T}    (hY : Measurable Y) (hW : Measurable W)    (μ : Measure Ω) (μ' : Measure Ω') [IsFiniteMeasure μ'] [FiniteRange W] :    d[X ; μ # Y | W ; μ']      = (μ'.map W)[fun w ↦ d[X ; μ # Y ; (μ'[|W ← w])]] := by  rw [condRuzsaDist'_eq_sum hY hW]  simp_rw [← smul_eq_mul]  have : ∀ᵐ x ∂(μ'.map W), x ∈ (FiniteRange.toFinset W : Set T) := by    rw [ae_map_iff (by measurability) (by exact Finset.measurableSet _)]    simp [← FiniteRange.range]  rw [integral_eq_setIntegral this,  setIntegral_finset _ .finset]  simp [map_measureReal_apply hW (MeasurableSet.singleton _),]