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

dist_le_of_sum_zero'

PFR.RhoFunctional · PFR/RhoFunctional.lean:1532 to 1544

Source documentation

If $G$ -valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$ , then

+ \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$

Exact Lean statement

lemma dist_le_of_sum_zero' {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ : Ω' → G} (hsum : T₁ + T₂ + T₃ = 0)
    (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :
    k ≤ I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]
      + (η / 3) * ((ρ[T₁ | T₂ # A] + ρ[T₂ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₁ | T₃ # A] + ρ[T₃ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₂ | T₃ # A] + ρ[T₃ | T₂ # A] - ρ[X₁ # A] - ρ[X₂ # A]))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dist_le_of_sum_zero' {Ω' : Type*} [MeasureSpace Ω']    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ : Ω' → G} (hsum : T₁ + T₂ + T₃ = 0)    (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :    k ≤ I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]      + (η / 3) * ((ρ[T₁ | T₂ # A] + ρ[T₂ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])                 + (ρ[T₁ | T₃ # A] + ρ[T₃ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])                 + (ρ[T₂ | T₃ # A] + ρ[T₃ | T₂ # A] - ρ[X₁ # A] - ρ[X₂ # A])) := by  have := dist_le_of_sum_zero h_min hsum hT₁ hT₂ hT₃ (μ := ℙ)  have : T₁ + T₃ + T₂ = 0 := by convert hsum using 1; abel  have := dist_le_of_sum_zero h_min this hT₁ hT₃ hT₂ (μ := ℙ)  have : T₂ + T₃ + T₁ = 0 := by convert hsum using 1; abel  have := dist_le_of_sum_zero h_min this hT₂ hT₃ hT₁ (μ := ℙ)  linarith