feat(Topology/Algebra/InfiniteSum/Order): positivity extension for infinite sums (#21557)

Add a positivity extension for `tsum`. This extension only attempts to prove nonnegativity goals, as proving positivity requires wrestling with convergence.



Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>

Author: FLDutchmann

Mathlib/Topology/Algebra/InfiniteSum/Order.lean

@@ -314,3 +314,29 @@ theorem Summable.tendsto_atTop_of_pos [LinearOrderedField α] [TopologicalSpace
   inv_inv f ▸ Filter.Tendsto.inv_tendsto_nhdsGT_zero <|
     tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf.tendsto_atTop_zero <|
       Eventually.of_forall fun _ ↦ inv_pos.2 (hf' _)
+
+namespace Mathlib.Meta.Positivity
+
+open Qq Lean Meta Finset
+
+attribute [local instance] monadLiftOptionMetaM in
+/-- Positivity extension for infinite sums.
+
+This extension only proves non-negativity, strict positivity is more delicate for infinite sums and
+requires more assumptions. -/
+@[positivity tsum _]
+def evalTsum : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@tsum _ $instCommMonoid $instTopSpace $ι $f) =>
+    lambdaBoundedTelescope f 1 fun args (body : Q($α)) => do
+      let #[(i : Q($ι))] := args | failure
+      let rbody ← core zα pα body
+      let pbody ← rbody.toNonneg
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
+      let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
+      let instOrderClosed ← synthInstanceQ q(OrderClosedTopology $α)
+      assertInstancesCommute
+      return .nonnegative q(@tsum_nonneg $ι $α $pα' $instTopSpace $instOrderClosed $f $pr)
+  | _ => throwError "not tsum"
+
+end Mathlib.Meta.Positivity

MathlibTest/positivity.lean

@@ -5,6 +5,7 @@ import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.Topology.Algebra.InfiniteSum.Order
 
 /-! # Tests for the `positivity` tactic
 
@@ -380,6 +381,19 @@ example (f : D → E) (c : ℝ) (hc : 0 < c): 0 ≤ ∫ x, c * ‖f x‖ ∂μ :
 
 end Integral
 
+/-! ## Infinite Sums -/
+
+example (f : ℕ → ℝ) : 0 ≤ ∑' n, f n ^ 2 := by positivity
+example  (f : ℕ → ℝ≥0) (c : ℝ) (hc : 0 < c) : 0 ≤ ∑' n, c * f n := by positivity
+example [LinearOrderedField α] [TopologicalSpace α] [OrderClosedTopology α] (f : ℚ → α) :
+    0 ≤ ∑' q, (f q)^2 := by
+  positivity
+
+-- Make sure that the extension doesn't produce an invalid term by accidentally unifying `?n` with
+-- `0` because of the `hf` assumption
+set_option linter.unusedVariables false in
+example (f : ℕ → ℕ) (hf : 0 ≤ f 0) : 0 ≤ ∑' n, f n := by positivity
+
 /-! ## Big operators -/
 
 example (n : ℕ) (f : ℕ → ℤ) : 0 ≤ ∑ j ∈ range n, f j ^ 2 := by positivity