English
For a nonarchimedean f, a function g: β → α, and a multiset s, there exists b ∈ s (if s ≠ 0) such that f(∑_{t∈s} g(t)) ≤ f(g(b)).
Русский
Для ненархимедовой f и отображения g:β→α и мультисета s существует b ∈ s (если s ≠ 0) так, что
LaTeX
$$$\\exists b\\in s\\;\\text{ such that }\\ f\\Big(\\sum_{t\\in s} g(t)\\Big) \\le f(g(b))$$$
Lean4
/-- Given a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, a function `g : β → α`
and a multiset `s : Multiset β`, we can always find `b : β`, belonging to `s` if `s` is nonempty,
such that `f (s.sum g) ≤ f (g b)` . -/
theorem multiset_image_add {F α β : Type*} [AddCommMonoid α] [FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R]
[Nonempty β] {f : F} (hna : IsNonarchimedean f) (g : β → α) (s : Multiset β) :
∃ b : β, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b) := by
induction s using Multiset.induction_on with
| empty => simp
| cons a s
h =>
obtain ⟨b, hb1, hb2⟩ := multiset_image_add_of_nonempty (s := a ::ₘ s) hna g Multiset.cons_ne_zero
exact ⟨b, fun _ ↦ hb1, hb2⟩
