English
The function n ↦ extremalNumber(n,H) / (n choose 2) is nonincreasing for n ≥ 2; more precisely, (extremalNumber n H) / (n choose 2) decreases as n grows, after normalization.
Русский
Функция n ↦ extremalNumber(n,H) / (n choose 2) не возрастает при n ≥ 2; то есть отношение экстремального числа к choose2 падает с ростом n.
LaTeX
$$$\\operatorname{AntitoneOn}\\bigl( n \\mapsto \\frac{\\mathrm{extremalNumber}(n,H)}{\\binom{n}{2}} \\bigr)([2,\\infty)).$$$
Lean4
theorem antitoneOn_extremalNumber_div_choose_two (H : SimpleGraph W) :
AntitoneOn (fun n ↦ (extremalNumber n H / n.choose 2 : ℝ)) (Set.Ici 2) :=
by
apply antitoneOn_nat_Ici_of_succ_le
intro n hn
conv_lhs =>
enter [1, 1]
rw [← Fintype.card_fin (n + 1)]
rw [div_le_iff₀ (mod_cast Nat.choose_pos (by linarith)), extremalNumber_le_iff_of_nonneg H (by positivity)]
intro G _ h
rw [mul_comm, ← mul_div_assoc, le_div_iff₀' (mod_cast Nat.choose_pos hn), Nat.cast_choose_two, Nat.cast_choose_two,
Nat.cast_add_one, add_sub_cancel_right (n : ℝ) 1, mul_comm _ (n - 1 : ℝ), ← mul_div (n - 1 : ℝ),
mul_comm _ (n / 2 : ℝ), mul_assoc, mul_comm (n - 1 : ℝ), ← mul_div (n + 1 : ℝ), mul_comm _ (n / 2 : ℝ), mul_assoc,
mul_le_mul_iff_right₀ (by positivity), ← Nat.cast_pred (by positivity), ← Nat.cast_mul, ← Nat.cast_add_one, ←
Nat.cast_mul, Nat.cast_le]
conv_rhs =>
rw [← Fintype.card_fin (n + 1), ← card_univ]
-- double counting `(v, e) ↦ v ∉ e`
apply
card_nsmul_le_card_nsmul' (r := fun v e ↦ v ∉ e)
-- counting `e`
· intro e he
simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter, ← compl_eq_univ_sdiff,
card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩, Nat.cast_id, Nat.reduceSubDiff, le_refl]
-- counting `v`
· intro v hv
simpa [edgeFinset_deleteIncidenceSet_eq_filter] using card_edgeFinset_deleteIncidenceSet_le_extremalNumber h v
