English
For a distinguished pair x from distinctPairs, under certain bounds, the density inequality holds comparing the local piece to the full sum over distinct pairs.
Русский
Для отмеченной пары x из distinctPairs при заданных ограничениях выполняется неравенство плотности по сравнению с полной суммой по различным парам.
LaTeX
$$$(G.edgeDensity(x.1,x.2))^2 + (\\text{if } G.IsUniform(\\varepsilon, x.1, x.2) \\text{ then } 0 \\text{ else } \\varepsilon^4/3 - \\varepsilon^5/25) \\leq \\dfrac{ \\sum_{i\\in distinctPairs\\, hP\\, G\\, \\varepsilon\\, x} (G.edgeDensity(i.1,i.2))^2 }{16^{\\#P.parts}}$$$
Lean4
/-- The increment partition has a prescribed (very big) size in terms of the original partition. -/
theorem card_increment (hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPG : ¬P.IsUniform G ε) :
#(increment hP G ε).parts = stepBound #P.parts :=
by
have hPα' : stepBound #P.parts ≤ card α := (mul_le_mul_left' (pow_le_pow_left' (by simp) _) _).trans hPα
have hPpos : 0 < stepBound #P.parts := stepBound_pos (nonempty_of_not_uniform hPG).card_pos
rw [increment, card_bind]
simp_rw [chunk, apply_dite Finpartition.parts, apply_dite card, sum_dite]
rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]
any_goals exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'
rw [Nat.sub_add_cancel a_add_one_le_four_pow_parts_card,
Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), ← add_mul]
congr
rw [filter_card_add_filter_neg_card_eq_card, card_attach]
