English
Variant statement of abs bound under subset relations; same content as previous.
Русский
Вариант утверждения о модульной границе при отношениях подмножества; та же идея.
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_two_mul_sub_sq (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hδ₀ : 0 ≤ δ) (hδ₁ : δ < 1)
(hs₂ : (1 - δ) * #s₁ ≤ #s₂) (ht₂ : (1 - δ) * #t₁ ≤ #t₂) :
|(edgeDensity r s₂ t₂ : 𝕜) - edgeDensity r s₁ t₁| ≤ 2 * δ - δ ^ 2 :=
by
have hδ' : 0 ≤ 2 * δ - δ ^ 2 := by
rw [sub_nonneg, sq]
gcongr
exact hδ₁.le.trans (by simp)
rw [← sub_pos] at hδ₁
obtain rfl | hs₂' := s₂.eq_empty_or_nonempty
· rw [Finset.card_empty, Nat.cast_zero] at hs₂
simpa [edgeDensity, (nonpos_of_mul_nonpos_right hs₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
obtain rfl | ht₂' := t₂.eq_empty_or_nonempty
· rw [Finset.card_empty, Nat.cast_zero] at ht₂
simpa [edgeDensity, (nonpos_of_mul_nonpos_right ht₂ hδ₁).antisymm (Nat.cast_nonneg _)] using hδ'
have hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ) := by ring
rw [hr]
norm_cast
refine (Rat.cast_le.2 <| abs_edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂' ht₂').trans ?_
push_cast
have h₁ := hs₂'.mono hs
have h₂ := ht₂'.mono ht
gcongr
· refine (le_div_iff₀ ?_).2 hs₂
exact mod_cast h₁.card_pos
· refine (le_div_iff₀ ?_).2 ht₂
exact mod_cast h₂.card_pos
