Skip to main content
therefore
Sign inSign up
Open navigation
teorth/PFR
Source indexedlemma · leanprover/lean4:v4.33.0-rc1

construct_good_improved'

PFR.ImprovedPFR · PFR/ImprovedPFR.lean:378 to 401

Source documentation

In fact kk is at most

(d[X^0_i;T_j|T_l] - d[X^0_i; X_i]).$$

Exact Lean statement

lemma construct_good_improved' :
    k ≤ δ + (p.η / 6) *
     ((d[p.X₀₁ # T₁ | T₂] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁])
    + (d[p.X₀₁ # T₂ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₂ | T₃] - d[p.X₀₁ # X₁])
    + (d[p.X₀₁ # T₃ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₃ | T₂] - d[p.X₀₁ # X₁])
    + (d[p.X₀₂ # T₁ | T₂] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₁ | T₃] - d[p.X₀₂ # X₂])
    + (d[p.X₀₂ # T₂ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂])
    + (d[p.X₀₂ # T₃ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₃ | T₂] - d[p.X₀₂ # X₂]))

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma construct_good_improved' :    k ≤ δ + (p.η / 6) *     ((d[p.X₀₁ # T₁ | T₂] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁])    + (d[p.X₀₁ # T₂ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₂ | T₃] - d[p.X₀₁ # X₁])    + (d[p.X₀₁ # T₃ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₃ | T₂] - d[p.X₀₁ # X₁])    + (d[p.X₀₂ # T₁ | T₂] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₁ | T₃] - d[p.X₀₂ # X₂])    + (d[p.X₀₂ # T₂ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂])    + (d[p.X₀₂ # T₃ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₃ | T₂] - d[p.X₀₂ # X₂])) := by  have I1 : I[T₂ : T₁] = I[T₁ : T₂] := mutualInfo_comm hT₂ hT₁ _  have I2 : I[T₃ : T₁] = I[T₁ : T₃] := mutualInfo_comm hT₃ hT₁ _  have I3 : I[T₃ : T₂] = I[T₂ : T₃] := mutualInfo_comm hT₃ hT₂ _  have Z123 := construct_good_prelim' h_min hT hT₁ hT₂ hT₃  have h132 : T₁ + T₃ + T₂ = 0 := by rw [← hT]; abel  have Z132 := construct_good_prelim' h_min h132 hT₁ hT₃ hT₂  have h213 : T₂ + T₁ + T₃ = 0 := by rw [← hT]; abel  have Z213 := construct_good_prelim' h_min h213 hT₂ hT₁ hT₃  have h231 : T₂ + T₃ + T₁ = 0 := by rw [← hT]; abel  have Z231 := construct_good_prelim' h_min h231 hT₂ hT₃ hT₁  have h312 : T₃ + T₁ + T₂ = 0 := by rw [← hT]; abel  have Z312 := construct_good_prelim' h_min h312 hT₃ hT₁ hT₂  have h321 : T₃ + T₂ + T₁ = 0 := by rw [← hT]; abel  have Z321 := construct_good_prelim' h_min h321 hT₃ hT₂ hT₁  simp only [I1, I2, I3] at Z123 Z132 Z213 Z231 Z312 Z321  linarith