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

averaged_final

PFR.ImprovedPFR · PFR/ImprovedPFR.lean:665 to 672

Mathematical statement

Exact Lean statement

lemma averaged_final : k ≤ (6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁))
    + p.η / 6 * (8 * k + 2 * (d[X₁ # X₁] + d[X₂ # X₂]))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma averaged_final : k ≤ (6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁))    + p.η / 6 * (8 * k + 2 * (d[X₁ # X₁] + d[X₂ # X₂])) := by  apply (averaged_construct_good hX₁ hX₂ hX₁' hX₂' h_min).trans  have : 0 ≤ p.η := p.hη.le  have := sum_condMutual_le p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep.reindex_four_abdc h_min  gcongr ?_ + (p.η / 6) * ?_  linarith [dist_diff_bound_1 p hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep,    dist_diff_bound_2 p hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep]