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

Q_dist

PFR.TorsionEndgame · PFR/TorsionEndgame.lean:251 to 260

Mathematical statement

Exact Lean statement

lemma Q_dist (j j' : Fin p.m) : d[Q j # -(Q j')] ≤ 2 * k

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Q_dist (j j' : Fin p.m) : d[Q j # -(Q j')] ≤ 2 * k := by  have : IdentDistrib (Q j) (Q j') ℙ ℙ := Q_ident _ h_mes h_indep hident _ _  have hQj_mes : Measurable (-(Q j')) := Q_mes h_mes _  calc    _ = d[Q j' # -(Q j')] := IdentDistrib.rdist_congr_left (by fun_prop) this    _ ≤ _ := by      convert multidist_ruzsa_IV p.hm (fun i ω ↦ Y (i, j') ω) _ (by fun_prop) (inferInstance)        using 2      · apply multiDist_copy; intro i; convert (hident i j').symm      exact indep_yj h_mes h_indep j'