English
Given a nonarchimedean f, a function g: β → α, and a nonempty multiset s ⊆ β, there exists b ∈ s such that f(∑_{t∈s} g(t)) ≤ f(g(b)).
Русский
При заданной ненархимедовой функции f, отображении g: β → α и ненулевой мультимножине s, существует элемент b ∈ s, удовлетворяющий неравенству
LaTeX
$$$\\exists b\\in s\\;\\text{ such that }\\ f\\Big(\\sum_{t\\in s} g(t)\\Big) \\le f(g(b))$$$
Lean4
/-- Given a nonarchimedean function `α → R`, a function `g : β → α` and a nonempty multiset
`s : Multiset β`, we can always find `b : β` belonging to `s` such that
`f (t.sum g) ≤ f (g b)` . -/
theorem multiset_image_add_of_nonempty {α β : Type*} [AddCommMonoid α] [Nonempty β] {f : α → R}
(hna : IsNonarchimedean f) (g : β → α) {s : Multiset β} (hs : s ≠ 0) :
∃ b : β, (b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b) := by
induction s using Multiset.induction_on with
| empty => contradiction
| cons a s h =>
simp only [Multiset.mem_cons, Multiset.map_cons, Multiset.sum_cons, exists_eq_or_imp]
by_cases h1 : s = 0
· simp [h1]
· obtain ⟨w, h2, h3⟩ := h h1
rcases le_max_iff.mp <| hna (g a) (Multiset.map g s).sum with h4 | h4
· exact .inl h4
· exact .inr ⟨w, h2, le_trans h4 h3⟩
