Theorems · Theorem · sequences and series

sum_div_pow_sq_le_div_sq

∀ (N : ℕ) {j : ℝ},
  0 < j → ∀ {c : ℝ}, 1 < c → ∑ i ∈ Finset.range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

The sum of 1/(c^i)^2 above a threshold j is comparable to 1/j^2, up to a multiplicative constant.

Defined in

Mathlib.Analysis.SpecificLimits.FloorPow

Cited by

1 results in Mathlib

Foundations

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