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 SummationFilters 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.

def SummationFilter.symmetricIcc (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : SummationFilter G

The SummationFilter on a locally finite order G corresponding to the symmetric intervals Icc (-N) N·

@[simp]

theorem SummationFilter.symmetricIcc_filter (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : (symmetricIcc G).filter = Filter.map (fun (g : G) => Finset.Icc (-g) g) Filter.atTop

def SummationFilter.symmetricIoo (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : SummationFilter 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.

@[simp]

theorem SummationFilter.symmetricIoo_filter (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : (symmetricIoo G).filter = Filter.map (fun (g : G) => Finset.Ioo (-g) g) Filter.atTop

def SummationFilter.symmetricIco (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : SummationFilter G

The SummationFilter on a locally finite order G corresponding to the symmetric intervals Ico (-N) N·

@[simp]

theorem SummationFilter.symmetricIco_filter (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : (symmetricIco G).filter = Filter.map (fun (N : G) => Finset.Ico (-N) N) Filter.atTop

def SummationFilter.symmetricIoc (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : SummationFilter G

The SummationFilter on a locally finite order G corresponding to the symmetric intervals Ioc (-N) N·

@[simp]

theorem SummationFilter.symmetricIoc_filter (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] : (symmetricIoc G).filter = Filter.map (fun (N : G) => Finset.Ioc (-N) N) Filter.atTop

instance SummationFilter.instNeBotSymmetricIcc (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] [Filter.atTop.NeBot] : (symmetricIcc G).NeBot

instance SummationFilter.instNeBotSymmetricIco (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] [Filter.atTop.NeBot] : (symmetricIco G).NeBot

instance SummationFilter.instNeBotSymmetricIoc (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] [Filter.atTop.NeBot] : (symmetricIoc G).NeBot

instance SummationFilter.instNeBotSymmetricIoo (G : Type u_1) [Neg G] [Preorder G] [LocallyFiniteOrder G] [Filter.atTop.NeBot] : (symmetricIoo G).NeBot

theorem SummationFilter.symmetricIcc_le_Conditional {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : (symmetricIcc G).filter ≤ (conditional G).filter

instance SummationFilter.instLeAtTopSymmetricIcc {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : (symmetricIcc G).LeAtTop

instance SummationFilter.instLeAtTopSymmetricIco {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] [NoTopOrder G] : (symmetricIco G).LeAtTop

instance SummationFilter.instLeAtTopSymmetricIoc {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] [NoBotOrder G] : (symmetricIoc G).LeAtTop

instance SummationFilter.instLeAtTopSymmetricIoo {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] [NoTopOrder G] [NoBotOrder G] : (symmetricIoo G).LeAtTop

theorem SummationFilter.symmetricIcc_eq_map_Icc_nat : (symmetricIcc ℤ).filter = Filter.map (fun (N : ℕ) => Finset.Icc (-↑N) ↑N) Filter.atTop

theorem SummationFilter.symmetricIcc_eq_symmetricIoo_int : symmetricIcc ℤ = symmetricIoo ℤ

theorem HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc {α : Type u_1} {f : ℤ → α} [CommGroup α] [TopologicalSpace α] [ContinuousMul α] {a : α} (hf : HasProd f a (SummationFilter.symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => (f ↑N)⁻¹) Filter.atTop (nhds 1)) : HasProd f a (SummationFilter.symmetricIco ℤ)

theorem HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc {α : Type u_1} {f : ℤ → α} [AddCommGroup α] [TopologicalSpace α] [ContinuousAdd α] {a : α} (hf : HasSum f a (SummationFilter.symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => -f ↑N) Filter.atTop (nhds 0)) : HasSum f a (SummationFilter.symmetricIco ℤ)

@[deprecated HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc (since := "2025-12-15")]

theorem SummationFilter.HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc {α : Type u_1} {f : ℤ → α} [CommGroup α] [TopologicalSpace α] [ContinuousMul α] {a : α} (hf : HasProd f a (symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => (f ↑N)⁻¹) Filter.atTop (nhds 1)) : HasProd f a (symmetricIco ℤ)

Alias of HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc.

theorem SummationFilter.multipliable_symmetricIco_of_multipliable_symmetricIcc {α : Type u_1} {f : ℤ → α} [CommGroup α] [TopologicalSpace α] [ContinuousMul α] (hf : Multipliable f (symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => (f ↑N)⁻¹) Filter.atTop (nhds 1)) : Multipliable f (symmetricIco ℤ)

theorem SummationFilter.summable_symmetricIco_of_summable_symmetricIcc {α : Type u_1} {f : ℤ → α} [AddCommGroup α] [TopologicalSpace α] [ContinuousAdd α] (hf : Summable f (symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => -f ↑N) Filter.atTop (nhds 0)) : Summable f (symmetricIco ℤ)

@[deprecated SummationFilter.multipliable_symmetricIco_of_multipliable_symmetricIcc (since := "2025-12-15")]

theorem SummationFilter.multipliable_symmetricIco_of_multiplible_symmetricIcc {α : Type u_1} {f : ℤ → α} [CommGroup α] [TopologicalSpace α] [ContinuousMul α] (hf : Multipliable f (symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => (f ↑N)⁻¹) Filter.atTop (nhds 1)) : Multipliable f (symmetricIco ℤ)

Alias of SummationFilter.multipliable_symmetricIco_of_multipliable_symmetricIcc.

theorem SummationFilter.tprod_symmetricIcc_eq_tprod_symmetricIco {α : Type u_1} {f : ℤ → α} [CommGroup α] [TopologicalSpace α] [ContinuousMul α] [T2Space α] (hf : Multipliable f (symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => (f ↑N)⁻¹) Filter.atTop (nhds 1)) : ∏'[symmetricIco ℤ] (b : ℤ), f b = ∏'[symmetricIcc ℤ] (b : ℤ), f b

theorem SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIco {α : Type u_1} {f : ℤ → α} [AddCommGroup α] [TopologicalSpace α] [ContinuousAdd α] [T2Space α] (hf : Summable f (symmetricIcc ℤ)) (hf2 : Filter.Tendsto (fun (N : ℕ) => -f ↑N) Filter.atTop (nhds 0)) : ∑'[symmetricIco ℤ] (b : ℤ), f b = ∑'[symmetricIcc ℤ] (b : ℤ), f b

theorem SummationFilter.hasProd_symmetricIcc_iff {α : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : ℤ → α} {a : α} : HasProd f a (symmetricIcc ℤ) ↔ Filter.Tendsto (fun (N : ℕ) => ∏ n ∈ Finset.Icc (-↑N) ↑N, f n) Filter.atTop (nhds a)

theorem SummationFilter.hasSum_symmetricIcc_iff {α : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : ℤ → α} {a : α} : HasSum f a (symmetricIcc ℤ) ↔ Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Icc (-↑N) ↑N, f n) Filter.atTop (nhds a)

theorem SummationFilter.hasProd_symmetricIco_int_iff {α : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : ℤ → α} {a : α} : HasProd f a (symmetricIco ℤ) ↔ Filter.Tendsto (fun (N : ℕ) => ∏ n ∈ Finset.Ico (-↑N) ↑N, f n) Filter.atTop (nhds a)

theorem SummationFilter.hasSum_symmetricIco_int_iff {α : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : ℤ → α} {a : α} : HasSum f a (symmetricIco ℤ) ↔ Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, f n) Filter.atTop (nhds a)

theorem SummationFilter.hasProd_symmetricIoc_int_iff {α : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : ℤ → α} {a : α} : HasProd f a (symmetricIoc ℤ) ↔ Filter.Tendsto (fun (N : ℕ) => ∏ n ∈ Finset.Ioc (-↑N) ↑N, f n) Filter.atTop (nhds a)

theorem SummationFilter.hasSum_symmetricIoc_int_iff {α : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : ℤ → α} {a : α} : HasSum f a (symmetricIoc ℤ) ↔ Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.Ioc (-↑N) ↑N, f n) Filter.atTop (nhds a)

theorem Summable.tendsto_zero_of_even_summable_symmetricIcc {F : Type u_2} [NormedAddCommGroup F] [NormSMulClass ℤ F] {f : ℤ → F} (hf : Summable f (SummationFilter.symmetricIcc ℤ)) (hs : Function.Even f) : Filter.Tendsto f Filter.atTop (nhds 0)