English
For a finite set S, EquitableOn(s,f) is equivalent to the two-sided bound: for every a ∈ S, the average of f over S lies between f(a) and f(a) − 1, etc.
Русский
Для конечного множества S равномерность по f эквивалентна неким двухсторонним границам относительно среднего значения; для каждого a ∈ S f(a) находится между средним значением и его на единицу выше.
LaTeX
$$$$ \\mathrm{EquitableOn}(s,f) \\iff \\forall a \\in s,\\ \\frac{\\sum_{i\\in s} f(i)}{|s|} \\le f(a) \\land f(a) \\le \\frac{\\sum_{i\\in s} f(i)}{|s|} + 1. $$$$
Lean4
theorem equitableOn_iff_le_le_add_one :
EquitableOn (s : Set α) f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / s.card + 1 :=
by
rw [Set.equitableOn_iff_exists_le_le_add_one]
refine ⟨?_, fun h => ⟨_, h⟩⟩
rintro ⟨b, hb⟩
by_cases h : ∀ a ∈ s, f a = b + 1
· intro a ha
rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]
exact ⟨le_rfl, Nat.le_succ _⟩
push_neg at h
obtain ⟨x, hx₁, hx₂⟩ := h
suffices h : b = (∑ i ∈ s, f i) / s.card by
simp_rw [← h]
apply hb
symm
refine
Nat.div_eq_of_lt_le (le_trans (by simp [mul_comm]) (sum_le_sum fun a ha => (hb a ha).1))
((sum_lt_sum (fun a ha => (hb a ha).2) ⟨_, hx₁, (hb _ hx₁).2.lt_of_ne hx₂⟩).trans_le ?_)
rw [mul_comm, sum_const_nat]
exact fun _ _ => rfl
