English
Given a nonarchimedean f, a function g: β → α, and a multiset s, there exists a submultiset b with certain size and inclusion properties such that f(map prod (powersetCard (card s - m) s).sum over b) ≤ f(b.prod over s).
Русский
Пусть f ненархимедова, g:β→α, s — мультисет; существует подмножество, удовлетворяющее размерной и включительной коррекции, для которого неравенство выполняется.
LaTeX
$$$\\exists t : \\text{Multiset}(α),\\; \\text{card } t = \\text{card } s - m \\wedge (\\forall x\\in t, x\\in s) \\wedge f\\Big(\\sum_{u\\in \\text{powersetCard}(\\text{card } s - m) s} \\prod_{i\\in u} (-b(i))\\Big) \\le f\\Big(\\prod_{i\\in t} (-b(i))\\Big)$$$
Lean4
theorem multiset_powerset_image_add [IsStrictOrderedRing R] {F α : Type*} [CommRing α] [FunLike F α R]
[AddGroupSeminormClass F α R] {f : F} (hf_na : IsNonarchimedean f) (s : Multiset α) (m : ℕ) :
∃ t : Multiset α,
card t = card s - m ∧ (∀ x : α, x ∈ t → x ∈ s) ∧ f (map prod (powersetCard (card s - m) s)).sum ≤ f t.prod :=
by
set g := fun t : Multiset α ↦ t.prod
obtain ⟨b, hb_in, hb_le⟩ := hf_na.multiset_image_add g (powersetCard (card s - m) s)
have hb : b ≤ s ∧ card b = card s - m := by
rw [← mem_powersetCard]
exact hb_in (card_pos.mp (card_powersetCard (s.card - m) s ▸ Nat.choose_pos ((card s).sub_le m)))
exact ⟨b, hb.2, fun x hx ↦ mem_of_le hb.left hx, hb_le⟩
