English
If a nonempty finite sum has each summand with norm at most t, then the sum has norm at most t.
Русский
Если каждая члена суммы имеет норму не более t, тогда норма суммы не превышает t.
LaTeX
$$$ s.Nonempty \rightarrow (\forall i \in s,\ padicNorm\ p\ (F i) \le t) \rightarrow padicNorm\ p\ (\sum i \in s, F i) \le t $$$
Lean4
theorem sum_le {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} :
s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t := by
classical
refine s.induction_on (by rintro ⟨-, ⟨⟩⟩) ?_
rintro a S haS IH - ht
by_cases hs : S.Nonempty
· rw [Finset.sum_insert haS]
exact
padicNorm.nonarchimedean.trans
(max_le (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
· simp_all
