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

rho_of_sum_le

PFR.RhoFunctional · PFR/RhoFunctional.lean:1064 to 1075

Source documentation

If $X,Y$ are independent, then $\rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$

Exact Lean statement

lemma rho_of_sum_le [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ]) / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rho_of_sum_le [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :    ρ[X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ]) / 2 := by  have I : ρ[X + Y ; μ # A] ≤ ρ[X ; μ # A] + (H[X+Y ; μ] - H[X ; μ])/2 :=    rho_of_sum hX hY hA h_indep  have J : ρ[Y + X ; μ # A] ≤ ρ[Y ; μ # A] + (H[Y+X ; μ] - H[Y ; μ ])/2 :=    rho_of_sum hY hX hA h_indep.symm  have : Y + X = X + Y := by abel  rw [this] at J  have : X - Y = X + Y := ZModModule.sub_eq_add _ _  rw [h_indep.rdist_eq hX hY, sub_eq_add_neg, this]  linarith