This file proves lemmas involving the summability of functions that decay in a manner comparable to inverse powers of the norm function on subsets of Euclidean space.

def Inv_Pow_Norm_Summable_Over_Set_Euclidean {d : ℕ} (X : Set (EuclideanSpace ℝ (Fin d))) : Prop

Equations

• Inv_Pow_Norm_Summable_Over_Set_Euclidean X = Summable fun (x : ↑X) => 1 / ‖↑x‖ ^ (d + 1)

def Exists_Inv_Pow_Norm_Summable_Over_Set_Euclidean {d : ℕ} (X : Set (EuclideanSpace ℝ (Fin d))) : Prop

Equations

• Exists_Inv_Pow_Norm_Summable_Over_Set_Euclidean X = ∃ k > 0, Summable fun (x : ↑X) => 1 / ‖↑x‖ ^ k

def IsDecayingMap {d : ℕ} (X : Set (EuclideanSpace ℝ (Fin d))) (f : EuclideanSpace ℝ (Fin d) → ℝ) : Prop

Equations

• IsDecayingMap X f = ∀ (k : ℕ), ∃ (C : ℝ), ∀ x ∈ X, ‖x‖ ^ k * ‖f x‖ ≤ C

theorem DecayingMap.summable_union_disjoint {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {s t : Set β} (hd : Disjoint s t) (hs : Summable (f ∘ Subtype.val)) (ht : Summable (f ∘ Subtype.val)) : Summable (f ∘ Subtype.val)

theorem DecayingMap.IsDecayingMap.subset {d : ℕ} {X X' : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : IsDecayingMap X f) (hX' : X' ⊆ X) : IsDecayingMap X' f

theorem DecayingMap.Summable_of_Inv_Pow_Summable' {d : ℕ} {X : Set (EuclideanSpace ℝ (Fin d))} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : IsDecayingMap X f) (hX : Inv_Pow_Norm_Summable_Over_Set_Euclidean X) (hne_zero : 0 ∉ X) : Summable fun (x : ↑X) => f ↑x

theorem DecayingMap.Summable.subset {α : Type u_1} {β : Type u_2} [AddCommGroup β] [UniformSpace β] [IsUniformAddGroup β] [CompleteSpace β] (f : α → β) {X X' : Set α} (hX : Summable fun (x : ↑X) => f ↑x) (hX' : X' ⊆ X) : Summable fun (x : ↑X') => f ↑x

theorem DecayingMap.Inv_Pow_Norm_Summable_Over_Set_Euclidean.subset {d : ℕ} {X X' : Set (EuclideanSpace ℝ (Fin d))} (hX : Inv_Pow_Norm_Summable_Over_Set_Euclidean X) (hX' : X' ⊆ X) : Inv_Pow_Norm_Summable_Over_Set_Euclidean X'

theorem DecayingMap.Summable_of_Inv_Pow_Summable {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (X : Set (EuclideanSpace ℝ (Fin d))) (hX : Inv_Pow_Norm_Summable_Over_Set_Euclidean X) (hf : IsDecayingMap X f) : Summable fun (x : ↑X) => f ↑x

theorem SchwartzMap.IsDecaying {d : ℕ} (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℝ) : IsDecayingMap Set.univ ⇑f

theorem SchwartzMap.Summable_of_Inv_Pow_Summable' {d : ℕ} (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℝ) {X : Set (EuclideanSpace ℝ (Fin d))} (hX : Inv_Pow_Norm_Summable_Over_Set_Euclidean X) (hne_zero : 0 ∉ X) : Summable fun (x : ↑X) => f ↑x

theorem extracted_1 {d : ℕ} {X : Set (EuclideanSpace ℝ (Fin d))} {Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))} [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] : let bℤ := (Module.Free.chooseBasis ℤ ↥Λ).reindex (ZLattice.basis_index_equiv Λ); let bℝ := Basis.ofZLatticeBasis ℝ Λ bℤ; let D := {m : EuclideanSpace ℝ (Fin d) | ∀ (i : Fin d), (bℝ.repr m) i ∈ Set.Ico (-1) 1}; Finite ↑(X ∩ D)

theorem Summable_Inverse_Powers_of_Finite_Orbits {d : ℕ} {X : Set (EuclideanSpace ℝ (Fin d))} {Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))} [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (ρ : AddAction ↥Λ ↑X) [Fintype (Quotient (AddAction.orbitRel ↥Λ ↑X))] : Inv_Pow_Norm_Summable_Over_Set_Euclidean X