English
A more refined bound using a parameter δ: the absolute density difference is bounded by 2δ when certain fill conditions hold.
Русский
Уточненная граница через параметр δ: модуль разности плотностей не превышает 2δ при условии заполнения.
LaTeX
$$$\left|\operatorname{edgeDensity}(r, s_2, t_2) - \operatorname{edgeDensity}(r, s_1, t_1)\right| \le 2\delta$$
Lean4
/-- If `s₂ ⊆ s₁`, `t₂ ⊆ t₁` and they take up all but a `δ`-proportion, then the difference in edge
densities is at most `2 * δ`. -/
theorem abs_edgeDensity_sub_edgeDensity_le_two_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hδ : 0 ≤ δ)
(hscard : (1 - δ) * #s₁ ≤ #s₂) (htcard : (1 - δ) * #t₁ ≤ #t₂) :
|(edgeDensity r s₂ t₂ : 𝕜) - edgeDensity r s₁ t₁| ≤ 2 * δ :=
by
rcases lt_or_ge δ 1 with h | h
·
exact
(abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq r hs ht hδ h hscard htcard).trans
((sub_le_self_iff _).2 <| sq_nonneg δ)
rw [two_mul]
refine (abs_sub _ _).trans (add_le_add (le_trans ?_ h) (le_trans ?_ h)) <;>
· rw [abs_of_nonneg]
· exact mod_cast edgeDensity_le_one r _ _
· exact mod_cast edgeDensity_nonneg r _ _
