English
Cardinality of interedges between s and t equals sum over left-partitions.
Русский
Кардинал числа ребер между s и t равно сумме по левой части разбиения.
LaTeX
$$$\#(\operatorname{interedges}(r, s, t)) = \sum_{a \in P.parts} \#(\operatorname{interedges}(r, a, t))$$$
Lean4
theorem 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 (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans ?_
refine le_trans ?_ (mul_le_of_le_one_right ?_ (edgeDensity_le_one r s₂ t₂))
· rw [sub_mul, one_mul]
refine sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)
· exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card hs)) (Nat.cast_nonneg _)
· apply div_nonneg <;> exact mod_cast Nat.zero_le _
· exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card ht)) (Nat.cast_nonneg _)
