Theorems · Theorem · number theory

ZLattice.exists_finsetSum_norm_rpow_le_tsum

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

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopology