English
A uniform lower bound on the edge density for pairs inside the uniform part of the partition.
Русский
Единое нижнее ограничение на плотность рёбер между парами внутри однородной части разбиения.
LaTeX
$$(G.edgeDensity U V)^2 − ε^5/25 ≤ (sum over chunk hP G ε hU).parts × (chunk hP G ε hV).parts of (G.edgeDensity ab.1 ab.2)^2 / 16^{|P.parts|}$$
Lean4
/-- Lower bound on the edge densities between parts of `SzemerediRegularity.increment`. This is the
blanket lower bound used the uniform parts. -/
theorem edgeDensity_chunk_uniform [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α)
(hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5) (hU : U ∈ P.parts) (hV : V ∈ P.parts) :
(G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25 ≤
(∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (G.edgeDensity ab.1 ab.2 : ℝ) ^ 2) /
↑16 ^ #P.parts :=
by
apply (edgeDensity_chunk_aux (hP := hP) hPα hPε hU hV).trans
have key : (16 : ℝ) ^ #P.parts = #((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts) := by
rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow];
norm_cast
simp_rw [key]
convert sum_div_card_sq_le_sum_sq_div_card (α := ℝ)
