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

sum_condMutual_le

PFR.Endgame · PFR/Endgame.lean:136 to 145

Source documentation

I[U : V | S] + I[V : W | S] + I[W : U | S] is less than or equal to 6 * η * k - (1 - 5 * η) / (1 - η) * (2 * η * k - I₁).

Exact Lean statement

lemma sum_condMutual_le [Module (ZMod 2) G] [IsProbabilityMeasure (ℙ : Measure Ω)] :
    I[U : V | S] + I[V : W | S] + I[W : U | S]
      ≤ 6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_condMutual_le [Module (ZMod 2) G] [IsProbabilityMeasure (ℙ : Measure Ω)] :    I[U : V | S] + I[V : W | S] + I[W : U | S]      ≤ 6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁) := by  have : I[W : U | S] = I₂ := condMutualInfo_comm (by fun_prop) (by fun_prop) ..  rw [I₃_eq, this]  any_goals simpa  have h₂ := second_estimate p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min  have : 0 < 1 - p.η := by linarith [p.hη']  field_simp at h₂ ⊢  linarith