English
If f ≤ g pointwise, f(i) < g(i) for some i, 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 \\to \\\\mathbb{R}_{\\\\ge 0∞}, \\\\forall sf sg \\\\in \\\\mathbb{R}_{\\\\ge 0∞}, \\\\Big( \\\\forall a, f(a) \\\\le g(a) \\\\Big) \\\\Rightarrow \\\\Big( \\\\exists a, f(a) < g(a) \\\\Rightarrow HasSum f sf \\\\land HasSum g sg \\\\Rightarrow sf < sg \\\\Big)$$$
Lean4
theorem hasSum_lt {f g : α → ℝ≥0∞} {sf sg : ℝ≥0∞} {i : α} (h : ∀ a : α, f a ≤ g a) (hi : f i < g i) (hsf : sf ≠ ∞)
(hf : HasSum f sf) (hg : HasSum g sg) : sf < sg :=
by
by_cases hsg : sg = ∞
· exact hsg.symm ▸ lt_of_le_of_ne le_top hsf
· have hg' : ∀ x, g x ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)
lift f to α → ℝ≥0 using fun x => ne_of_lt (lt_of_le_of_lt (h x) <| lt_of_le_of_ne le_top (hg' x))
lift g to α → ℝ≥0 using hg'
lift sf to ℝ≥0 using hsf
lift sg to ℝ≥0 using hsg
simp only [coe_le_coe, coe_lt_coe] at h hi ⊢
exact NNReal.hasSum_lt h hi (ENNReal.hasSum_coe.1 hf) (ENNReal.hasSum_coe.1 hg)
