English
The cardinality of the biUnion of star is controlled by the star size times m+1.
Русский
Кардинальность биобъединения звезды контролируется размером звезды и m+1.
LaTeX
$$card((star hP G ε hU V).biUnion id) ≤ card(star hP G ε hU V) · (m+1)$$
Lean4
/-- Lower bound on the edge densities between non-uniform parts of `SzemerediRegularity.increment`.
-/
theorem edgeDensity_chunk_not_uniform [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α)
(hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5) (hε₁ : ε ≤ 1) {hU : U ∈ P.parts} {hV : V ∈ P.parts} (hUVne : U ≠ V)
(hUV : ¬G.IsUniform ε U V) :
(G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25 + ε ^ 4 / ↑3 ≤
(∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (G.edgeDensity ab.1 ab.2 : ℝ) ^ 2) /
↑16 ^ #P.parts :=
calc
↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / ↑3 ≤
↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / ↑25 +
#(star hP G ε hU V) * #(star hP G ε hV U) / ↑16 ^ #P.parts * (↑9 / ↑16) * ε ^ 2 :=
by
apply add_le_add_left
have Ul : 4 / 5 * ε ≤ #(star hP G ε hU V) / _ := eps_le_card_star_div hPα hPε hε₁ hU hV hUVne hUV
have Vl : 4 / 5 * ε ≤ #(star hP G ε hV U) / _ :=
eps_le_card_star_div hPα hPε hε₁ hV hU hUVne.symm fun h => hUV h.symm
rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _), ← _root_.div_mul_div_comm, mul_assoc]
have : 0 < ε := by sz_positivity
have UVl := mul_le_mul Ul Vl (by positivity) ?_
swap
· -- This seems faster than `exact div_nonneg (by positivity) (by positivity)` and *much*
-- (tens of seconds) faster than `positivity` on its own.
apply div_nonneg <;> positivity
refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)
· norm_num
nlinarith
· norm_num
positivity
_ ≤
(∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (G.edgeDensity ab.1 ab.2 : ℝ) ^ 2) /
↑16 ^ #P.parts :=
by
have t :
(star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts :=
product_subset_product star_subset_chunk star_subset_chunk
have hε : 0 ≤ ε := by sz_positivity
have sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b := fun a b => rfl
have :=
add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ)) ((G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25)
(show 0 ≤ 3 / 4 * ε by linarith) ?_ ?_
· simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow, cast_pow, mul_pow, div_pow, ←
mul_assoc] at this
norm_num at this
exact this
· simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow]
norm_num
exact edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV
· rw [sp, card_product]
apply (edgeDensity_chunk_aux hP hPα hPε hU hV).trans
· rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
simp
