feat: Ixx summation filters (#30380)

We prove some results about sums over intervals of the form Ixx which are needed for defining the Eisenstein series E2 (see #26014). We also define these as summation filters.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: CBirkbeck

Mathlib.lean

@@ -60,6 +60,7 @@ import Mathlib.Algebra.BigOperators.Finsupp.Fin
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 import Mathlib.Algebra.BigOperators.Group.Finset.Indicator
+import Mathlib.Algebra.BigOperators.Group.Finset.Interval
 import Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
 import Mathlib.Algebra.BigOperators.Group.Finset.Pi
 import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
@@ -5202,6 +5203,7 @@ import Mathlib.Order.Filter.AtTopBot.Finite
 import Mathlib.Order.Filter.AtTopBot.Finset
 import Mathlib.Order.Filter.AtTopBot.Floor
 import Mathlib.Order.Filter.AtTopBot.Group
+import Mathlib.Order.Filter.AtTopBot.Interval
 import Mathlib.Order.Filter.AtTopBot.Map
 import Mathlib.Order.Filter.AtTopBot.ModEq
 import Mathlib.Order.Filter.AtTopBot.Monoid
@@ -6524,6 +6526,7 @@ import Mathlib.Topology.Algebra.GroupCompletion
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Indicator
 import Mathlib.Topology.Algebra.InfiniteSum.Basic
+import Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
 import Mathlib.Topology.Algebra.InfiniteSum.Constructions
 import Mathlib.Topology.Algebra.InfiniteSum.Defs
 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+
+import Mathlib.Algebra.CharP.Defs
+import Mathlib.Algebra.Group.EvenFunction
+import Mathlib.Data.Int.Interval
+import Mathlib.Tactic.Zify
+
+/-!
+# Sums/products over integer intervals
+
+This file contains some lemmas about sums and products over integer intervals `Ixx`.
+
+-/
+
+namespace Finset
+
+@[to_additive]
+lemma prod_Icc_of_even_eq_range {α : Type*} [CommGroup α] {f : ℤ → α} (hf : f.Even) (N : ℕ) :
+    ∏ m ∈ Icc (-N : ℤ) N, f m = (∏ m ∈ range (N + 1), f m) ^ 2 / f 0 := by
+  induction N with
+  | zero => simp [sq]
+  | succ N ih =>
+    rw [Nat.cast_add, Nat.cast_one, Icc_succ_succ, prod_union (by simp), prod_pair (by omega), ih,
+      prod_range_succ _ (N + 1), hf, ← pow_two, div_mul_eq_mul_div, ← mul_pow, Nat.cast_succ]
+
+@[to_additive]
+lemma prod_Icc_eq_prod_Ico_mul {α : Type*} [CommMonoid α] (f : ℤ → α) {l u : ℤ}
+    (h : l ≤ u) : ∏ m ∈ Icc l u, f m = (∏ m ∈ Ico l u, f m) * f u := by
+  simp [Icc_eq_cons_Ico h, mul_comm]
+
+@[to_additive]
+lemma prod_Icc_succ_eq_mul_endpoints {R : Type*} [CommGroup R] (f : ℤ → R) {N : ℕ} :
+    ∏ m ∈ Icc (-(N + 1) : ℤ) (N + 1), f m =
+    f (N + 1) * f (-(N + 1) : ℤ) * ∏ m ∈ Icc (-N : ℤ) N, f m := by
+  induction N
+  · rw [Icc_succ_succ]
+    simp only [CharP.cast_eq_zero, neg_zero, Icc_self, zero_add, Int.reduceNeg, union_insert,
+      union_singleton, mem_insert, reduceCtorEq, mem_singleton, neg_eq_zero, one_ne_zero, or_self,
+      not_false_eq_true, prod_insert, prod_singleton]
+    grind
+  · rw [Icc_succ_succ, prod_union (by simp)]
+    grind
+
+end Finset

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -233,4 +233,8 @@ lemma one_sub_le_one_add_mul_one_sub (h : c + b * c ≤ a + b) : 1 - a ≤ (1 +
   rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]
   gcongr
 
+instance [Nontrivial R] : NoMaxOrder R := ⟨fun a ↦ ⟨a + 1, by simp⟩⟩
+
+instance [Nontrivial R] : NoMinOrder R := ⟨fun a ↦ ⟨a - 1, by simp⟩⟩
+
 end OrderedRing

Mathlib/Data/Int/Interval.lean

@@ -164,3 +164,31 @@ theorem image_Ico_emod (n a : ℤ) (h : 0 ≤ a) : (Ico n (n + a)).image (· % a
     · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hia.left hia.right]
 
 end Int
+
+section Nat
+
+lemma Finset.Icc_succ_succ (m n : ℕ) :
+    Icc (-(m + 1) : ℤ) (n + 1) = Icc (-m : ℤ) n ∪ {(-(m + 1) : ℤ), (n + 1 : ℤ)} := by
+  ext
+  simp only [mem_Icc, union_insert, union_singleton, mem_insert]
+  omega
+
+lemma Finset.Ico_succ_succ (m n : ℕ) :
+    Ico (-(m + 1) : ℤ) (n + 1) = Ico (-m : ℤ) n ∪ {(-(m + 1) : ℤ), (n : ℤ)} := by
+  ext
+  simp only [mem_Ico, union_insert, union_singleton, mem_insert]
+  omega
+
+lemma Finset.Ioc_succ_succ (m n : ℕ) :
+    Ioc (-(m + 1) : ℤ) (n + 1) = Ioc (-m : ℤ) n ∪ {-(m : ℤ), (n + 1 : ℤ)} := by
+  ext
+  simp only [mem_Ioc, union_insert, union_singleton, mem_insert]
+  omega
+
+lemma Finset.Ioo_succ_succ (m n : ℕ) :
+    Ioo (-(m + 1) : ℤ) (n + 1) = Ioo (-m : ℤ) n ∪ {-(m : ℤ), (n : ℤ)} := by
+  ext
+  simp only [mem_Ioo, union_insert, union_singleton, mem_insert]
+  omega
+
+end Nat

Mathlib/Order/Filter/AtTopBot/Finset.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
 -/
 import Mathlib.Data.Finset.Order
-import Mathlib.Data.Finset.Preimage
-import Mathlib.Order.Filter.AtTopBot.Tendsto
 import Mathlib.Order.Filter.AtTopBot.Basic
 import Mathlib.Order.Filter.Finite
 import Mathlib.Order.Interval.Finset.Defs

Mathlib/Order/Filter/AtTopBot/Interval.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck, David Loeffler
+-/
+
+import Mathlib.Order.Filter.AtTopBot.Archimedean
+import Mathlib.Order.Filter.Prod
+import Mathlib.Order.Interval.Finset.Defs
+
+/-!
+# Limits of intervals along filters
+
+This file contains some lemmas about how filters `Ixx` behave as the endpoints tend to `±∞`.
+
+-/
+
+namespace Finset
+
+open Filter
+
+section Asymmetric
+
+variable {α : Type*} [Preorder α] [LocallyFiniteOrder α]
+
+lemma tendsto_Icc_atBot_prod_atTop :
+    Tendsto (fun p : α × α ↦ Icc p.1 p.2) (atBot ×ˢ atTop) atTop := by
+  simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
+    using fun b i _ ↦ (eventually_le_atBot i).prod_mk (eventually_ge_atTop i)
+
+lemma tendsto_Ioc_atBot_prod_atTop [NoBotOrder α] :
+    Tendsto (fun p : α × α ↦ Ioc p.1 p.2) (atBot ×ˢ atTop) atTop := by
+  simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
+    using fun b i _ ↦ (eventually_lt_atBot i).prod_mk (eventually_ge_atTop i)
+
+lemma tendsto_Ico_atBot_prod_atTop [NoTopOrder α] :
+    Tendsto (fun p : α × α ↦ Finset.Ico p.1 p.2) (atBot ×ˢ atTop) atTop := by
+  simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
+    using fun b i _ ↦ (eventually_le_atBot i).prod_mk (eventually_gt_atTop i)
+
+lemma tendsto_Ioo_atBot_prod_atTop [NoBotOrder α] [NoTopOrder α] :
+    Tendsto (fun p : α × α ↦ Finset.Ioo p.1 p.2) (atBot ×ˢ atTop) atTop := by
+  simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
+    using fun b i _ ↦ (eventually_lt_atBot i).prod_mk (eventually_gt_atTop i)
+
+end Asymmetric
+
+section Symmetric
+
+variable {α : Type*} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α]
+  [LocallyFiniteOrder α]
+
+lemma tendsto_Icc_neg_atTop_atTop :
+    Tendsto (fun a : α ↦ Icc (-a) a) atTop atTop :=
+  tendsto_Icc_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)
+
+lemma tendsto_Ioc_neg_atTop_atTop [NoBotOrder α] :
+    Tendsto (fun a : α ↦ Ioc (-a) a) atTop atTop :=
+  tendsto_Ioc_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)
+
+lemma tendsto_Ico_neg_atTop_atTop [NoTopOrder α] :
+    Tendsto (fun a : α ↦ Ico (-a) a) atTop atTop :=
+  tendsto_Ico_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)
+
+lemma tendsto_Ioo_neg_atTop_atTop [NoBotOrder α] [NoTopOrder α] :
+    Tendsto (fun a : α ↦ Ioo (-a) a) atTop atTop :=
+  tendsto_Ioo_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)
+
+end Symmetric
+
+section NatCast
+
+variable {R : Type*} [Ring R] [PartialOrder R] [IsOrderedRing R] [LocallyFiniteOrder R]
+  [Archimedean R]
+
+lemma tendsto_Icc_neg :
+    Tendsto (fun n : ℕ ↦ Icc (-n : R) n) atTop atTop :=
+  tendsto_Icc_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop
+
+variable [Nontrivial R]
+
+lemma tendsto_Ioc_neg : Tendsto (fun n : ℕ ↦ Ioc (-n : R) n) atTop atTop :=
+  tendsto_Ioc_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop
+
+lemma tendsto_Ico_neg : Tendsto (fun n : ℕ ↦ Ico (-n : R) n) atTop atTop :=
+  tendsto_Ico_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop
+
+lemma tendsto_Ioo_neg : Tendsto (fun n : ℕ ↦ Ioo (-n : R) n) atTop atTop :=
+  tendsto_Ioo_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop
+
+end NatCast
+
+end Finset

Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+
+import Mathlib.Algebra.BigOperators.Group.Finset.Interval
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Order.Filter.AtTopBot.Interval
+import Mathlib.Topology.Algebra.InfiniteSum.Defs
+import Mathlib.Topology.Algebra.Monoid.Defs
+import Mathlib.Tactic.FinCases
+
+
+/-!
+# Sums over symmetric integer intervals
+
+This file contains some lemmas about sums over symmetric integer intervals `Ixx -N N` used, for
+example in the definition of the Eisenstein series `E2`.
+In particular we define `symmetricIcc`, `symmetricIco`, `symmetricIoc` and `symmetricIoo` as
+`SummationFilter`s corresponding to the intervals `Icc -N N`, `Ico -N N`, `Ioc -N N` respectively.
+We also prove that these filters are all `NeBot` and `LeAtTop`.
+
+-/
+
+open Finset Topology Function Filter SummationFilter
+
+namespace SummationFilter
+
+section IntervalFilters
+
+variable (G : Type*) [Neg G] [Preorder G] [LocallyFiniteOrder G]
+
+/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
+intervals `Icc (-N) N`· -/
+@[simps]
+def symmetricIcc : SummationFilter G where
+  filter := atTop.map (fun g ↦ Icc (-g) g)
+
+/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
+intervals `Ioo (-N) N`· Note that for `G = ℤ` this coincides with
+`symmetricIcc` so one should use that. See `symmetricIcc_eq_symmetricIoo_int`. -/
+@[simps]
+def symmetricIoo : SummationFilter G where
+  filter := atTop.map (fun g ↦ Ioo (-g) g)
+
+/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
+intervals `Ico (-N) N`· -/
+@[simps]
+def symmetricIco : SummationFilter G where
+  filter := atTop.map (fun N ↦ Ico (-N) N)
+
+/-- The SummationFilter on a locally finite order `G` corresponding to the symmetric
+intervals `Ioc (-N) N`· -/
+@[simps]
+def symmetricIoc : SummationFilter G where
+  filter := atTop.map (fun N ↦ Ioc (-N) N)
+
+variable [(atTop : Filter G).NeBot]
+
+instance : (symmetricIcc G).NeBot where
+  ne_bot := by simp [symmetricIcc, Filter.NeBot.map]
+
+instance : (symmetricIco G).NeBot where
+  ne_bot := by simp [symmetricIco, Filter.NeBot.map]
+
+instance : (symmetricIoc G).NeBot where
+  ne_bot := by simp [symmetricIoc, Filter.NeBot.map]
+
+instance : (symmetricIoo G).NeBot where
+  ne_bot := by simp [symmetricIoo, Filter.NeBot.map]
+
+section LeAtTop
+
+variable {G : Type*} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G]
+
+lemma symmetricIcc_le_Conditional :
+    (symmetricIcc G).filter ≤ (conditional G).filter :=
+  Filter.map_mono (tendsto_neg_atTop_atBot.prodMk tendsto_id)
+
+instance : (symmetricIcc G).LeAtTop where
+  le_atTop := le_trans symmetricIcc_le_Conditional (conditional G).le_atTop
+
+variable [NoTopOrder G] [NoBotOrder G]
+
+instance : (symmetricIco G).LeAtTop where
+  le_atTop := by
+    rw [symmetricIco, map_le_iff_le_comap, ← @tendsto_iff_comap]
+    exact tendsto_Ico_neg_atTop_atTop
+
+instance : (symmetricIoc G).LeAtTop where
+  le_atTop := by
+    rw [symmetricIoc, map_le_iff_le_comap, ← @tendsto_iff_comap]
+    exact tendsto_Ioc_neg_atTop_atTop
+
+instance : (symmetricIoo G).LeAtTop where
+  le_atTop := by
+    rw [symmetricIoo, map_le_iff_le_comap, ← @tendsto_iff_comap]
+    exact tendsto_Ioo_neg_atTop_atTop
+
+end LeAtTop
+
+end IntervalFilters
+section Int
+
+variable {α : Type*} {f : ℤ → α} [CommGroup α] [TopologicalSpace α] [ContinuousMul α]
+
+lemma symmetricIcc_eq_map_Icc_nat :
+    (symmetricIcc ℤ).filter = atTop.map (fun N : ℕ ↦ Icc (-(N : ℤ)) N) := by
+  simp [← Nat.map_cast_int_atTop, Function.comp_def]
+
+lemma symmetricIcc_eq_symmetricIoo_int : symmetricIcc ℤ = symmetricIoo ℤ := by
+  simp only [symmetricIcc, symmetricIoo, mk.injEq]
+  ext s
+  simp only [← Nat.map_cast_int_atTop, Filter.map_map, Filter.mem_map, mem_atTop_sets, ge_iff_le,
+    Set.mem_preimage, comp_apply]
+  refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩ <;>
+  [ convert ha (b - 1) (by grind) using 1; convert ha (b + 1) (by grind) using 1 ] <;>
+  simpa [Finset.ext_iff] using by grind
+
+@[to_additive]
+lemma HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc {a : α}
+    (hf : HasProd f a (symmetricIcc ℤ)) (hf2 : Tendsto (fun N : ℕ ↦ (f N)⁻¹) atTop (𝓝 1)) :
+    HasProd f a (symmetricIco ℤ) := by
+  simp only [HasProd, tendsto_map'_iff, symmetricIcc_eq_map_Icc_nat,
+    ← Nat.map_cast_int_atTop, symmetricIco] at *
+  apply tendsto_of_div_tendsto_one _ hf
+  simpa [Pi.div_def, fun N : ℕ ↦ prod_Icc_eq_prod_Ico_mul f (show (-N : ℤ) ≤ N by omega)]
+    using hf2
+
+@[to_additive]
+lemma multipliable_symmetricIco_of_multiplible_symmetricIcc
+    (hf : Multipliable f (symmetricIcc ℤ)) (hf2 : Tendsto (fun N : ℕ ↦ (f N)⁻¹) atTop (𝓝 1)) :
+    Multipliable f (symmetricIco ℤ) :=
+  (hf.hasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc hf2).multipliable
+
+@[to_additive]
+lemma tprod_symmetricIcc_eq_tprod_symmetricIco [T2Space α]
+    (hf : Multipliable f (symmetricIcc ℤ)) (hf2 : Tendsto (fun N : ℕ ↦ (f N)⁻¹) atTop (𝓝 1)) :
+    ∏'[symmetricIco ℤ] b, f b = ∏'[symmetricIcc ℤ] b, f b :=
+  (hf.hasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc hf2).tprod_eq
+
+@[to_additive]
+lemma hasProd_symmetricIcc_iff {α : Type*} [CommMonoid α] [TopologicalSpace α]
+    {f : ℤ → α} {a : α} : HasProd f a (symmetricIcc ℤ) ↔
+    Tendsto (fun N : ℕ ↦ ∏ n ∈ Icc (-(N : ℤ)) N, f n) atTop (𝓝 a) := by
+  simp [HasProd, symmetricIcc, ← Nat.map_cast_int_atTop, comp_def]
+
+@[to_additive]
+lemma hasProd_symmetricIco_int_iff {α : Type*} [CommMonoid α] [TopologicalSpace α]
+    {f : ℤ → α} {a : α} : HasProd f a (symmetricIco ℤ) ↔
+    Tendsto (fun N : ℕ ↦ ∏ n ∈ Ico (-(N : ℤ)) (N : ℤ), f n) atTop (𝓝 a) := by
+  simp [HasProd, symmetricIco, ← Nat.map_cast_int_atTop, comp_def]
+
+@[to_additive]
+lemma hasProd_symmetricIoc_int_iff {α : Type*} [CommMonoid α] [TopologicalSpace α]
+    {f : ℤ → α} {a : α} : HasProd f a (symmetricIoc ℤ) ↔
+    Tendsto (fun N : ℕ ↦ ∏ n ∈ Ioc (-(N : ℤ)) (N : ℤ), f n) atTop (𝓝 a) := by
+  simp [HasProd, symmetricIoc, ← Nat.map_cast_int_atTop, comp_def]
+
+end Int
+
+end SummationFilter

Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

@@ -334,4 +334,14 @@ theorem Multipliable.hasProd_iff (h : Multipliable f L) :
     HasProd f a L ↔ ∏'[L] b, f b = a :=
   Iff.intro HasProd.tprod_eq fun eq ↦ eq ▸ h.hasProd
 
+@[to_additive]
+theorem tprod_eq_of_filter_le {L₁ L₂ : SummationFilter β} [L₁.NeBot]
+    (h : L₁.filter ≤ L₂.filter) (hf : Multipliable f L₂) : ∏'[L₁] b, f b = ∏'[L₂] b, f b :=
+  (hf.mono_filter h).hasProd_iff.mp (hf.hasProd.mono_left h)
+
+@[to_additive]
+theorem tprod_eq_of_multipliable_unconditional [L.LeAtTop] (hf : Multipliable f) :
+     ∏'[L] b, f b = ∏' b, f b :=
+  tprod_eq_of_filter_le L.le_atTop hf
+
 end HasProd