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

condRho_sum_le'

PFR.RhoFunctional · PFR/RhoFunctional.lean:1765 to 1788

Source documentation

For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$ , define $T_1:=Y_1+Y_2, T_2:=Y_1+Y_3, T_3:=Y_2+Y_3$ and $S:=Y_1+Y_2+Y_3+Y_4$ . Then

- \frac{1}{2}\sum_{i} \rho(Y_i))\le \sum_{1\leq i < j \leq 4}d[Y_i;Y_j]$$

Exact Lean statement

lemma condRho_sum_le' {Y₁ Y₂ Y₃ Y₄ : Ω → G}
      (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄)
      (h_indep : iIndepFun ![Y₁, Y₂, Y₃, Y₄]) (hA : A.Nonempty) :
    let S

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRho_sum_le' {Y₁ Y₂ Y₃ Y₄ : Ω → G}      (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄)      (h_indep : iIndepFun ![Y₁, Y₂, Y₃, Y₄]) (hA : A.Nonempty) :    let S := Y₁ + Y₂ + Y₃ + Y₄    let T₁ := Y₁ + Y₂    let T₂ := Y₁ + Y₃    let T₃ := Y₂ + Y₃    ρ[T₁ | ⟨T₂, S⟩ # A] + ρ[T₂ | ⟨T₁, S⟩ # A] + ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₁, S⟩ # A]      + ρ[T₂ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₂, S⟩ # A]      - 3 * (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤    d[Y₁ # Y₂] + d[Y₁ # Y₃] + d[Y₁ # Y₄] + d[Y₂ # Y₃] + d[Y₂ # Y₄] + d[Y₃ # Y₄] := by  have K₁ := condRho_sum_le hY₁ hY₂ hY₃ hY₄ h_indep hA  have K₂ := condRho_sum_le hY₂ hY₁ hY₃ hY₄ h_indep.reindex_four_bacd hA  have Y₂₁ : Y₂ + Y₁ = Y₁ + Y₂ := by abel  have dY₂₁ : d[Y₂ # Y₁] = d[Y₁ # Y₂] := rdist_symm  rw [Y₂₁, dY₂₁] at K₂  have K₃ := condRho_sum_le hY₃ hY₁ hY₂ hY₄ h_indep.reindex_four_cabd hA  have Y₃₁ : Y₃ + Y₁ = Y₁ + Y₃ := by abel  have Y₃₂ : Y₃ + Y₂ = Y₂ + Y₃ := by abel  have S₃ : Y₁ + Y₃ + Y₂ + Y₄ = Y₁ + Y₂ + Y₃ + Y₄ := by abel  have dY₃₁ : d[Y₃ # Y₁] = d[Y₁ # Y₃] := rdist_symm  have dY₃₂ : d[Y₃ # Y₂] = d[Y₂ # Y₃] := rdist_symm  rw [Y₃₁, Y₃₂, S₃, dY₃₁, dY₃₂] at K₃  linarith