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·

Equations

• SummationFilter.symmetricIcc G = { filter := Filter.map (fun (g : G) => Finset.Icc (-g) g) Filter.atTop }

@[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.

Equations

• SummationFilter.symmetricIoo G = { filter := Filter.map (fun (g : G) => Finset.Ioo (-g) g) Filter.atTop }

@[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·

Equations

• SummationFilter.symmetricIco G = { filter := Filter.map (fun (N : G) => Finset.Ico (-N) N) Filter.atTop }

@[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·

Equations

• SummationFilter.symmetricIoc G = { filter := Filter.map (fun (N : G) => Finset.Ioc (-N) N) Filter.atTop }

@[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 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 ℤ)

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

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 ℤ)

theorem SummationFilter.summable_symmetricIco_of_multiplible_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 ℤ)

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)