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

condRuzsaDist_eq_sum'

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:499 to 523

Source documentation

Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ in a fintype.

Exact Lean statement

lemma condRuzsaDist_eq_sum' {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}
    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) [IsFiniteMeasure μ] (μ' : Measure Ω') [IsFiniteMeasure μ']
    [Fintype S] [Fintype T] :
    d[X | Z ; μ # Y | W ; μ']
      = ∑ z, ∑ w, μ.real (Z ⁻¹' {z}) * μ'.real (W ⁻¹' {w})
          * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist_eq_sum' {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)    (μ : Measure Ω) [IsFiniteMeasure μ] (μ' : Measure Ω') [IsFiniteMeasure μ']    [Fintype S] [Fintype T] :    d[X | Z ; μ # Y | W ; μ']      = ∑ z, ∑ w, μ.real (Z ⁻¹' {z}) * μ'.real (W ⁻¹' {w})          * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])] := by  rw [condRuzsaDist_def, Kernel.rdist, integral_fintype .of_finite]  simp_rw [Measure.prod_real_singleton, smul_eq_mul, Fintype.sum_prod_type,    map_measureReal_apply hZ (.singleton _), map_measureReal_apply hW (.singleton _)]  congr with z  congr with w  by_cases hz : μ.real (Z ⁻¹' {z}) = 0  · simp only [mul_eq_mul_left_iff, mul_eq_zero]    refine .inr <| .inl ?_    simp [hz]  by_cases hw : μ'.real (W ⁻¹' {w}) = 0  · simp only [mul_eq_mul_left_iff, mul_eq_zero]    refine .inr <| .inr ?_    simp [hw]  congr 1  simp only [Measure.real, ENNReal.toReal_eq_zero_iff, measure_ne_top μ, or_false,    measure_ne_top] at hz hw  rw [rdist_eq_rdistm]  rw [condDistrib_apply hX hZ _ _ hz, condDistrib_apply hY hW _ _ hw]