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

condRho_sum_le

PFR.RhoFunctional · PFR/RhoFunctional.lean:1711 to 1759

Source documentation

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

\le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]).$$

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) :
    ρ[Y₁ + Y₂ | ⟨Y₁ + Y₃, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] + ρ[Y₁ + Y₃ | ⟨Y₁ + Y₂, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] -
      (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤
        (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 2

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) :    ρ[Y₁ + Y₂ | ⟨Y₁ + Y₃, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] + ρ[Y₁ + Y₃ | ⟨Y₁ + Y₂, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] -      (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤        (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 2 := by  set S := Y₁ + Y₂ + Y₃ + Y₄  set T₁ := Y₁ + Y₂  set T₂ := Y₁ + Y₃  set T₁' := Y₃ + Y₄  set T₂' := Y₂ + Y₄  have J : ρ[T₁ | ⟨T₂, S⟩ # A] ≤    (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4      + (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 8 + (d[Y₁ + Y₂ # Y₃ + Y₄]        + I[Y₁ + Y₂ : Y₁ + Y₃ | Y₁ + Y₂ + Y₃ + Y₄] + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄]) / 4 :=    new_gen_ineq hY₁ hY₂ hY₃ hY₄ h_indep hA  have J' : ρ[T₂ | ⟨T₁, Y₁ + Y₃ + Y₂ + Y₄⟩ # A] ≤    (ρ[Y₁ # A] + ρ[Y₃ # A] + ρ[Y₂ # A] + ρ[Y₄ # A]) / 4      + (d[Y₁ # Y₃] + d[Y₂ # Y₄] + d[Y₁ # Y₂] + d[Y₃ # Y₄]) / 8 + (d[Y₁ + Y₃ # Y₂ + Y₄]        + I[Y₁ + Y₃ : Y₁ + Y₂|Y₁ + Y₃ + Y₂ + Y₄] + d[Y₁ | Y₁ + Y₂ # Y₃ | Y₃ + Y₄]) / 4 :=    new_gen_ineq hY₁ hY₃ hY₂ hY₄ h_indep.reindex_four_acbd hA  have : Y₁ + Y₃ + Y₂ + Y₄ = S := by simp only [S]; abel  rw [this] at J'  have : d[Y₁ + Y₂ # Y₃ + Y₄] + I[Y₁ + Y₂ : Y₁ + Y₃ | Y₁ + Y₂ + Y₃ + Y₄]    + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄] + d[Y₁ + Y₃ # Y₂ + Y₄]    + I[Y₁ + Y₃ : Y₁ + Y₂|S] + d[Y₁ | Y₁ + Y₂ # Y₃ | Y₃ + Y₄]      = (d[Y₁ # Y₂] + d[Y₃ # Y₄]) + (d[Y₁ # Y₃] + d[Y₂ # Y₄]) := by    have K : Y₁ + Y₃ + Y₂ + Y₄ = S := by simp only [S]; abel    have K' : I[Y₁ + Y₃ : Y₁ + Y₂|Y₁ + Y₂ + Y₃ + Y₄] = I[Y₁ + Y₃ : Y₃ + Y₄|Y₁ + Y₂ + Y₃ + Y₄] := by      have : Measurable (Y₁ + Y₃) := by fun_prop      rw [condMutualInfo_comm this (by fun_prop), condMutualInfo_comm this (by fun_prop)]      have B := condMutualInfo_of_inj_map (X := Y₃ + Y₄) (Y := Y₁ + Y₃) (Z := Y₁ + Y₂ + Y₃ + Y₄)        (by fun_prop) (by fun_prop) (by fun_prop) (fun a b ↦ a - b) (fun a ↦ sub_right_injective)        (μ := ℙ)      convert B with g      simp    have K'' : I[Y₁ + Y₂ : Y₁ + Y₃|Y₁ + Y₂ + Y₃ + Y₄] = I[Y₁ + Y₂ : Y₂ + Y₄|Y₁ + Y₂ + Y₃ + Y₄] := by      have : Measurable (Y₁ + Y₂) := by fun_prop      rw [condMutualInfo_comm this (by fun_prop), condMutualInfo_comm this (by fun_prop)]      have B := condMutualInfo_of_inj_map (X := Y₂ + Y₄) (Y := Y₁ + Y₂) (Z := Y₁ + Y₂ + Y₃ + Y₄)        (by fun_prop) (by fun_prop) (by fun_prop) (fun a b ↦ a - b) (fun a ↦ sub_right_injective)        (μ := ℙ)      convert B with g      simp      abel    rw [sum_of_rdist_eq_char_2' Y₁ Y₂ Y₃ Y₄ h_indep hY₁ hY₂ hY₃ hY₄,      sum_of_rdist_eq_char_2' Y₁ Y₃ Y₂ Y₄ h_indep.reindex_four_acbd hY₁ hY₃ hY₂ hY₄, K, K', K'']    abel  linarith