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

gen_ineq_01

PFR.ImprovedPFR · PFR/ImprovedPFR.lean:209 to 222

Source documentation

Other version of gen_ineq_00, in which we switch to the complement in the second term.

Exact Lean statement

lemma gen_ineq_01 : d[Y # Z₁ + Z₂ | ⟨Z₂ + Z₄, Sum⟩] - d[Y # Z₁] ≤
    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4
    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma gen_ineq_01 : d[Y # Z₁ + Z₂ | ⟨Z₂ + Z₄, Sum⟩] - d[Y # Z₁] ≤    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8 := by  convert gen_ineq_00 Y hY Z₁ Z₂ Z₃ Z₄ hZ₁ hZ₂ hZ₃ hZ₄ h_indep using 2  let e : G × G ≃ G × G :=  { toFun p := ⟨p.2 - p.1, p.2⟩    invFun p := ⟨- p.1 + p.2, p.2⟩    left_inv := by intro ⟨a, b⟩; simp    right_inv := by intro ⟨a, b⟩; simp }  convert! (condRuzsaDist_comp_right (ℙ : Measure Ω₀) (ℙ : Measure Ω) Y (Z₁ + Z₂) (⟨Z₁ + Z₃, Sum⟩) e    (by fun_prop) (by fun_prop) (by fun_prop) e.injective) with p  simp only [e, Pi.add_apply, Equiv.coe_fn_mk, Function.comp_apply]  abel