Convergence of p-series on lattices

Let E be a finite dimensional normed ℝ-space, and L a discrete subgroup of E of rank d. We show that ∑ z ∈ L, ‖z - x‖ʳ is convergent for r < -d.

Main results

• ZLattice.summable_norm_rpow: ∑ z ∈ L, ‖z‖ʳ converges when r < -d.
• ZLattice.summable_norm_sub_rpow: ∑ z ∈ L, ‖z - x‖ʳ converges when r < -d.
• ZLattice.tsum_norm_rpow_le: ∑ z ∈ L, ‖z‖ʳ ≤ Aʳ * ∑ k : ℕ, kᵈ⁺ʳ⁻¹ for some A > 0 depending only on L.

theorem ZLattice.exists_forall_abs_repr_le_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_2} (b : Module.Basis ι ℤ ↥L) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖

def ZLattice.normBound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) : ℝ

Given a basis of a (possibly not full rank) ℤ-lattice, there exists a ε > 0 such that |b.repr x i| < n for all ‖x‖ < n * ε (i.e. b.repr x i = O(x) depending only on b). This is an arbitrary choice of such an ε.

Equations

• ZLattice.normBound b = ⋯.choose

theorem ZLattice.normBound_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) : 0 < normBound b

theorem ZLattice.normBound_spec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι) : normBound b * ↑|(b.repr x) i| ≤ ‖x‖

theorem ZLattice.abs_repr_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (i : ι) : ↑|(b.repr x) i| ≤ (normBound b)⁻¹ * ‖x‖

theorem ZLattice.abs_repr_lt_of_norm_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (n : ℕ) (hxn : ‖x‖ < normBound b * ↑n) (i : ι) : |(b.repr x) i| < ↑n

theorem ZLattice.le_norm_of_le_abs_repr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L) (x : ↥L) (n : ℕ) (i : ι) (hi : ↑n ≤ |(b.repr x) i|) : normBound b * ↑n ≤ ‖x‖

theorem ZLattice.sum_piFinset_Icc_rpow_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) {d : ℕ} (hd : d = Fintype.card ι) (n : ℕ) (r : ℝ) (hr : r < -↑d) : ∑ p ∈ Fintype.piFinset fun (x : ι) => Finset.Icc (-↑n) ↑n, ‖∑ i : ι, p i • b i‖ ^ r ≤ 2 * ↑d * 3 ^ (d - 1) * normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

theorem ZLattice.exists_finsetSum_norm_rpow_le_tsum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : ∃ A > 0, ∀ r < -↑(Module.finrank ℤ ↥L), ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)

def ZLattice.tsumNormRPowBound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : ℝ

Let L be a lattice with (possibly non-full) rank d, and r : ℝ such that d < r. Then ∑ z ∈ L, ‖z‖⁻ʳ ≤ A⁻ʳ * ∑ k : ℕ, kᵈ⁻ʳ⁻¹ for some A > 0 depending only on L. This is an arbitrary choice of A. See ZLattice.tsum_norm_rpow_le.

Equations

• ZLattice.tsumNormRPowBound L = ⋯.choose

theorem ZLattice.tsumNormRPowBound_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : 0 < tsumNormRPowBound L

theorem ZLattice.tsumNormRPowBound_spec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (r : ℝ) (h : r < -↑(Module.finrank ℤ ↥L)) (s : Finset ↥L) : ∑ z ∈ s, ‖z‖ ^ r ≤ tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)

theorem ZLattice.summable_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (r : ℝ) (hr : r < -↑(Module.finrank ℤ ↥L)) : Summable fun (z : ↥L) => ‖z‖ ^ r

If L is a ℤ-lattice with rank d in E, then ∑ z ∈ L, ‖z‖ʳ converges when r < -d.

theorem ZLattice.tsum_norm_rpow_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (r : ℝ) (hr : r < -↑(Module.finrank ℤ ↥L)) : ∑' (z : ↥L), ‖z‖ ^ r ≤ tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)

∑ z ∈ L, ‖z‖⁻ʳ ≤ A⁻ʳ * ∑ k : ℕ, kᵈ⁻ʳ⁻¹ for some A > 0 depending only on L.

theorem ZLattice.summable_norm_sub_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (r : ℝ) (hr : r < -↑(Module.finrank ℤ ↥L)) (x : E) : Summable fun (z : ↥L) => ‖↑z - x‖ ^ r

theorem ZLattice.summable_norm_sub_zpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (n : ℤ) (hn : n < -↑(Module.finrank ℤ ↥L)) (x : E) : Summable fun (z : ↥L) => ‖↑z - x‖ ^ n

theorem ZLattice.summable_norm_zpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (n : ℤ) (hn : n < -↑(Module.finrank ℤ ↥L)) : Summable fun (z : ↥L) => ‖z‖ ^ n

theorem ZLattice.summable_norm_sub_inv_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (n : ℕ) (hn : Module.finrank ℤ ↥L < n) (x : E) : Summable fun (z : ↥L) => ‖↑z - x‖⁻¹ ^ n

theorem ZLattice.summable_norm_pow_inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (n : ℕ) (hn : Module.finrank ℤ ↥L < n) : Summable fun (z : ↥L) => ‖z‖⁻¹ ^ n