Theorems · Definition · number theory

ZLattice.tsumNormRPowBound

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : 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.

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

3 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopology