English
If a finite sum of quantities all have norm less than t and the index set is nonempty, then the norm of the sum is less than t.
Русский
Для конечной суммы чисел, все из которых имеют норму меньше t, и множество индексов непусто, норма суммы тоже меньше t.
LaTeX
$$$ \text{If } s \neq \emptyset \text{ and } \forall i \in s,\ padicNorm\ p\ (F i) < t,\ \ padicNorm\ p\ (\sum i \in s, F i) < t $$$
Lean4
theorem sum_lt {α : 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
lt_of_le_of_lt padicNorm.nonarchimedean
(max_lt (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
· simp_all
