Theorems · Theorem · number theory

ZLattice.sum_piFinset_Icc_rpow_le

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

Defined in

Mathlib.Algebra.Module.ZLattice.Summable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalDiscreteTopologyFintypeDecidableEq