English
For a nonarchimedean f, a function g: β → α, and a Finset s, there exists u ∈ powersetCard(|s|-m) s such that a certain inequality holds comparing sums and products with -b.
Русский
Пусть f ненархимедова, g:β→α и Finset s; существует u ∈ powersetCard(|s|-m) s, для которого выполняется нужное неравенство между суммами и произведениями элементов, отрицательных по отношению к b.
LaTeX
$$$\\exists u \\in \\text{powersetCard}(|s|-m)\\, s,\\ f (\\text{sum over } u) \\le f (\\text{prod over } u)$$$
Lean4
theorem finset_powerset_image_add [IsStrictOrderedRing R] {F α β : Type*} [CommRing α] [FunLike F α R]
[AddGroupSeminormClass F α R] {f : F} (hf_na : IsNonarchimedean f) (s : Finset β) (b : β → α) (m : ℕ) :
∃ u : powersetCard (s.card - m) s,
f ((powersetCard (s.card - m) s).sum fun t : Finset β ↦ t.prod fun i : β ↦ -b i) ≤
f (u.val.prod fun i : β ↦ -b i) :=
by
set g := fun t : Finset β ↦ t.prod fun i : β ↦ -b i
obtain ⟨b, hb_in, hb⟩ := hf_na.finset_image_add g (powersetCard (s.card - m) s)
exact ⟨⟨b, hb_in (powersetCard_nonempty.mpr (Nat.sub_le s.card m))⟩, hb⟩
