English
If left/right subsets nearly fill their supersets, then the absolute difference of densities is bounded by a function of proportions.
Русский
Если левый/правый множества почти заполняют свои надмножества, то модуль разности плотностей ограничен выражением через пропорции заполнения.
LaTeX
$$$\left|\operatorname{edgeDensity}(r, s_2, t_2) - \operatorname{edgeDensity}(r, s_1, t_1)\right| \le 1 - \frac{|s_2|}{|s_1|} \cdot \frac{|t_2|}{|t_1|}$$$
Lean4
theorem abs_edgeDensity_sub_edgeDensity_le_one_sub_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty)
(ht₂ : t₂.Nonempty) : |edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - #s₂ / #s₁ * (#t₂ / #t₁) :=
by
refine abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, ?_⟩
rw [← add_sub_cancel_right (edgeDensity r s₁ t₁) (edgeDensity (fun x y ↦ ¬r x y) s₁ t₁), ←
add_sub_cancel_right (edgeDensity r s₂ t₂) (edgeDensity (fun x y ↦ ¬r x y) s₂ t₂),
edgeDensity_add_edgeDensity_compl _ (hs₂.mono hs) (ht₂.mono ht), edgeDensity_add_edgeDensity_compl _ hs₂ ht₂,
sub_sub_sub_cancel_left]
exact edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂
