English
If a finite set of rationals has p-adic valuations above a threshold, then the valuation of their sum is above that threshold.
Русский
Если у конечного набора рациональных чисел p-адикальная величина превышает порог, то и сумма имеет величину выше этого порога.
LaTeX
$$$ \\text{If } \\forall i \\in S,\\ v_p(F_i) > t \\text{ and } \\sum_{i\\in S} F_i \\neq 0, \\; v_p\\left(\\sum_{i\\in S} F_i\\right) > t$$$
Lean4
/-- If the p-adic valuation of a finite set of positive rationals is greater than a given rational
number, then the p-adic valuation of their sum is also greater than the same rational number. -/
theorem lt_sum_of_lt {p j : ℕ} [hp : Fact (Nat.Prime p)] {F : ℕ → ℚ} {S : Finset ℕ} (hS : S.Nonempty)
(hF : ∀ i, i ∈ S → padicValRat p (F j) < padicValRat p (F i)) (hn1 : ∀ i : ℕ, 0 < F i) :
padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i) := by
induction hS using Finset.Nonempty.cons_induction with
| singleton k =>
rw [Finset.sum_singleton]
exact hF k (by simp)
| cons s S' Hnot Hne Hind =>
rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]
exact
padicValRat.lt_add_of_lt (ne_of_gt (add_pos (hn1 s) (Finset.sum_pos (fun i _ => hn1 i) Hne)))
(hF _ (by simp [Finset.mem_insert, true_or]))
(Hind (fun i hi => hF _ (by rw [Finset.cons_eq_insert, Finset.mem_insert]; exact Or.inr hi)))
