English
Let p be a prime and s a finite index set with F : s → ℚ. If for every i ∈ s we have the p-adic norm |F(i)|_p < t for some t > 0, then the p-adic norm of the sum is also less than t, i.e. |∑_{i∈s} F(i)|_p < t.
Русский
Пусть p — простое число и s — конечный индексный набор с F : s → ℚ. Если для каждого i ∈ s выполняется |F(i)|_p < t при t > 0, то p-адическая норма суммы также меньше t: |∑_{i∈s} F(i)|_p < t.
LaTeX
$$$\\displaystyle \\forall \\alpha \\quad \\forall F:\\alpha \\to \\mathbb{Q}, \\quad \\forall s\\in\\mathrm{Finset}(\\alpha),\\quad \\forall t>0,\\quad (\\forall i\\in s,\\ |F(i)|_p < t) \\Rightarrow \\left|\\sum_{i\\in s} F(i)\\right|_p < t$$$
Lean4
theorem sum_lt' {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} (hF : ∀ i ∈ s, padicNorm p (F i) < t) (ht : 0 < t) :
padicNorm p (∑ i ∈ s, F i) < t :=
by
obtain rfl | hs := Finset.eq_empty_or_nonempty s
· simp [ht]
· exact sum_lt hs hF
