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

condRuzsaDistance_ge_of_min

PFR.TauFunctional · PFR/TauFunctional.lean:212 to 254

Source documentation

For any $G$ -valued random variables $X'_1,X'_2$ and random variables $Z,W$ , one can lower bound $d[X'_1|Z;X'_2|W]$ by $k - \eta (d[X^0_1;X'_1|Z] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2|W] - d[X^0_2;X_2] ).$

Exact Lean statement

lemma condRuzsaDistance_ge_of_min [MeasurableSingletonClass G]
    [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S]
    [Finite T] [MeasurableSpace T] [MeasurableSingletonClass T]
    (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂')
    (Z : Ω'₁ → S) (W : Ω'₂ → T) (hZ : Measurable Z) (hW : Measurable W) :
    d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁' | Z] - d[p.X₀₁ # X₁])
      - p.η * (d[p.X₀₂ # X₂' | W] - d[p.X₀₂ # X₂]) ≤ d[X₁' | Z # X₂' | W]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDistance_ge_of_min [MeasurableSingletonClass G]    [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S]    [Finite T] [MeasurableSpace T] [MeasurableSingletonClass T]    (h : tau_minimizes p X₁ X₂) (h1 : Measurable X₁') (h2 : Measurable X₂')    (Z : Ω'₁ → S) (W : Ω'₂ → T) (hZ : Measurable Z) (hW : Measurable W) :    d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁' | Z] - d[p.X₀₁ # X₁])      - p.η * (d[p.X₀₂ # X₂' | W] - d[p.X₀₂ # X₂]) ≤ d[X₁' | Z # X₂' | W] := by  have hz (a : ℝ) : a = ∑ z ∈ FiniteRange.toFinset Z, Measure.real ℙ (Z ⁻¹' {z}) * a := by    simp_rw [← Finset.sum_mul, ← map_measureReal_apply hZ (MeasurableSet.singleton _),      sum_measureReal_singleton]    rw [FiniteRange.real_full hZ]    simp  have hw (a : ℝ) : a = ∑ w ∈ FiniteRange.toFinset W, Measure.real ℙ (W ⁻¹' {w}) * a := by    simp_rw [← Finset.sum_mul, ← map_measureReal_apply hW (MeasurableSet.singleton _),      sum_measureReal_singleton]    rw [FiniteRange.real_full hW]    simp  rw [condRuzsaDist_eq_sum h1 hZ h2 hW, condRuzsaDist'_eq_sum h1 hZ, hz d[X₁ # X₂],    hz d[p.X₀₁ # X₁], hz (p.η * (d[p.X₀₂ # X₂' | W] - d[p.X₀₂ # X₂])),    ← Finset.sum_sub_distrib, Finset.mul_sum, ← Finset.sum_sub_distrib, ← Finset.sum_sub_distrib]  apply Finset.sum_le_sum  intro z _  rw [condRuzsaDist'_eq_sum h2 hW, hw d[p.X₀₂ # X₂],    hw (Measure.real ℙ (Z ⁻¹' {z}) * d[X₁ # X₂] - p.η * (Measure.real ℙ (Z ⁻¹' {z}) *      d[p.X₀₁ ; ℙ # X₁' ; ℙ[|Z ← z]] - Measure.real ℙ (Z ⁻¹' {z}) * d[p.X₀₁ # X₁])),    ← Finset.sum_sub_distrib, Finset.mul_sum, Finset.mul_sum, ← Finset.sum_sub_distrib]  apply Finset.sum_le_sum  intro w _  rcases eq_or_ne (Measure.real ℙ (Z ⁻¹' {z})) 0 with hpz | hpz  · simp [hpz]  rcases eq_or_ne (Measure.real ℙ (W ⁻¹' {w})) 0 with hpw | hpw  · simp [hpw]  set μ := (hΩ₁.volume)[|Z ← z]  have hμ : IsProbabilityMeasure μ := cond_isProbabilityMeasure_of_real hpz  set μ' := ℙ[|W ← w]  have hμ' : IsProbabilityMeasure μ' := cond_isProbabilityMeasure_of_real hpw  suffices d[X₁ # X₂] - p.η * (d[p.X₀₁; volume # X₁'; μ] - d[p.X₀₁ # X₁]) -    p.η * (d[p.X₀₂; volume # X₂'; μ'] - d[p.X₀₂ # X₂]) ≤ d[X₁' ; μ # X₂'; μ'] by    replace this := mul_le_mul_of_nonneg_left this      (show 0 ≤ (Measure.real ℙ (Z ⁻¹' {z})) * (Measure.real ℙ (W ⁻¹' {w})) by positivity)    convert this using 1    ring  exact distance_ge_of_min' p h h1 h2