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

dist_le_of_sum_zero_cond

PFR.RhoFunctional · PFR/RhoFunctional.lean:1501 to 1524

Source documentation

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

+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$

Exact Lean statement

lemma dist_le_of_sum_zero_cond {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ S : Ω' → G}
    (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃)
    (hS : Measurable S) :
    k ≤ 3 * I[T₁ : T₂ | S] + (2 * H[T₃ | S] - H[T₁ | S] - H[T₂ | S])
      + η * (ρ[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₃ S : Ω' → G}    (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃)    (hS : Measurable S) :    k ≤ 3 * I[T₁ : T₂ | S] + (2 * H[T₃ | S] - H[T₁ | S] - H[T₂ | S])      + η * (ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₂ | ⟨T₃, S⟩ #  A] - ρ[X₁ # A] - ρ[X₂ # A]) := by  cases nonempty_fintype G  have hw (a : ℝ) : a = ∑ w, (Measure.real ℙ (S ⁻¹' {w})) * a := by    have : IsProbabilityMeasure (map S ℙ) := isProbabilityMeasure_map hS.aemeasurable    simp_rw [← Finset.sum_mul, ← map_measureReal_apply hS (MeasurableSet.singleton _),      sum_measureReal_singleton]    simp  rw [condMutualInfo_eq_sum' hS, condEntropy_eq_sum_fintype _ _ _ hS,    condEntropy_eq_sum_fintype _ _ _ hS, condEntropy_eq_sum_fintype _ _ _ hS,    condRho_prod_eq_sum hT₃ hS, condRho_prod_eq_sum hT₃ hS, hw k, hw ρ[X₁ # A], hw ρ[X₂ # A]]  simp only [Finset.mul_sum, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib, mul_sub, mul_add]  gcongr with g hg  rcases eq_or_ne (Measure.real ℙ (S ⁻¹' {g})) 0 with hpg | hpg  · simp [hpg]  set μ := ℙ[|S ← g]  have hμ : IsProbabilityMeasure μ := cond_isProbabilityMeasure_of_real hpg  have := dist_le_of_sum_zero (μ := μ) h_min hsum hT₁ hT₂ hT₃  have := mul_le_mul_of_nonneg_left this (show 0 ≤ (Measure.real ℙ (S ⁻¹' {g})) by simp)  linarith