Theorems · Theorem · number theory

ZLattice.tsumNormRPowBound_spec

∀ {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),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ ZLattice.tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopology