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

dist_le_of_sum_zero_cond'

PFR.RhoFunctional · PFR/RhoFunctional.lean:1552 to 1565

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_cond' {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ : Ω' → G} (S : Ω' → G)
    (hsum : T₁ + T₂ + T₃ = 0)
    (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) (hS : Measurable S) :
    k ≤ I[T₁ : T₂ | S] + I[T₁ : T₃| S] + I[T₂ : T₃ | S]
      + (η / 3) * ((ρ[T₁ | ⟨T₂, S⟩ # A] + ρ[T₂ | ⟨T₁, S⟩ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₁, S⟩ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₂ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₂, S⟩ # A] - ρ[X₁ # A] - ρ[X₂ # A]))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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