Theorems · Theorem · number theory

ZLattice.tsum_norm_rpow_le

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

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

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopology