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

rdist_of_sums_ge'

PFR.SecondEstimate · PFR/SecondEstimate.lean:62 to 72

Source documentation

$d[X_1+\tilde X_1; X_2+\tilde X_2] \geq k - \frac{\eta}{2} ( d[X_1; X_1] + d[X_2;X_2] ).$

Exact Lean statement

lemma rdist_of_sums_ge' : d[X₁ + X₁' # X₂ + X₂'] ≥ k - p.η * (d[X₁ # X₁] + d[X₂ # X₂]) / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rdist_of_sums_ge' : d[X₁ + X₁' # X₂ + X₂'] ≥ k - p.η * (d[X₁ # X₁] + d[X₂ # X₂]) / 2 := by  refine LE.le.ge (LE.le.trans ?_ (distance_ge_of_min p h_min (hX₁.add hX₁') (hX₂.add hX₂')))  rw [sub_sub, sub_le_sub_iff_left k, ← mul_add,mul_div_assoc]  refine mul_le_mul_of_nonneg_left ?_ (by linarith [p.hη])  have h₁' := condRuzsaDist_diff_le' ℙ p.hmeas1 hX₁ hX₁' (h_indep.indepFun (show 0 ≠ 2 by decide))  have h₂' := condRuzsaDist_diff_le' ℙ p.hmeas2 hX₂ hX₂' (h_indep.indepFun (show 1 ≠ 3 by decide))  rw [h₁.entropy_congr, add_sub_cancel_right,    ← (IdentDistrib.refl hX₁.aemeasurable).rdist_congr h₁] at h₁'  rw [h₂.entropy_congr, add_sub_cancel_right,    ← (IdentDistrib.refl hX₂.aemeasurable).rdist_congr h₂] at h₂'  linarith