English
A refined pigeonhole bound for fibers ensures there is a fiber achieving the lower bound with respect to b.
Русский
Утверждается существование волокна, достигающего нижнюю границу по b.
LaTeX
$$$\\exists y ∈ t, b ≤ \\sum_{x∈s, f(x)=y} w(x)$$$
Lean4
/-- The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version:
if the total weight of a finite set of pigeons is less than `n • b`, they are sorted into some
pigeonholes, and for all but `n` pigeonholes the total weight of the pigeons there is nonnegative,
then for at least one of these `n` pigeonholes, the total weight of the pigeons in this pigeonhole
is less than `b`. -/
theorem exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul (ht : ∀ y ∉ t, (0 : M) ≤ ∑ x ∈ s with f x = y, w x)
(hb : ∑ x ∈ s, w x < #t • b) : ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b :=
exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum (M := Mᵒᵈ) ht hb
