English
If f ≤ g pointwise and f(i) < g(i) at some i, and HasSum f sf, HasSum g sg, then sf < sg.
Русский
Если f ≤ g по всем точкам и есть i, где f(i) < g(i), а HasSum для f и g сходится к sf и sg, то sf < sg.
LaTeX
$$$\\\\forall f,g : \\alpha \\rightarrow \\\\mathbb{R}_{\\\\ge 0}, \\\\forall sf sg \\\\in \\\\mathbb{R}_{\\\\ge 0}, \\\\Big(\\\\forall a, f(a) \\\\le g(a)\\\\Big) \\\\Rightarrow \\\\Big(\\\\exists i, f(i) < g(i)\\\\Rightarrow \\\\mathrm{HasSum}(f,sf) \\\\land \\\\mathrm{HasSum}(g,sg) \\\\Rightarrow sf < sg\\\\Big)$$$
Lean4
nonrec theorem hasSum_lt {f g : α → ℝ≥0} {sf sg : ℝ≥0} {i : α} (h : ∀ a : α, f a ≤ g a) (hi : f i < g i)
(hf : HasSum f sf) (hg : HasSum g sg) : sf < sg :=
by
have A : ∀ a : α, (f a : ℝ) ≤ g a := fun a => NNReal.coe_le_coe.2 (h a)
have : (sf : ℝ) < sg := hasSum_lt A (NNReal.coe_lt_coe.2 hi) (hasSum_coe.2 hf) (hasSum_coe.2 hg)
exact NNReal.coe_lt_coe.1 this
