English
The sum of 1/⌊c^i⌋^2 beyond threshold j is bounded by a multiple of 1/j^2.
Русский
Сумма 1/⌊c^i⌋^2 после порога j ограничена множителем от 1/j^2.
LaTeX
$$$$ (\\\\sum i ∈ range N with j < ⌊c^i⌋_+, 1/⌊c^i⌋^2) ≤ c^5 (c - 1)^{-1}^3 / j^2 $$$$
Lean4
/-- The sum of `1/⌊c^i⌋₊^2` above a threshold `j` is comparable to `1/j^2`, up to a multiplicative
constant. -/
theorem sum_div_nat_floor_pow_sq_le_div_sq (N : ℕ) {j : ℝ} (hj : 0 < j) {c : ℝ} (hc : 1 < c) :
(∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 :=
by
have cpos : 0 < c := zero_lt_one.trans hc
have A : 0 < 1 - c⁻¹ := sub_pos.2 (inv_lt_one_of_one_lt₀ hc)
calc
(∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2 :=
by
gcongr
exact fun k hk ↦ hk.trans_le <| Nat.floor_le (by positivity)
_ ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * ((1 : ℝ) / (c ^ i) ^ 2) :=
by
gcongr with i
rw [mul_div_assoc', mul_one, div_le_div_iff₀]; rotate_left
· apply sq_pos_of_pos
refine zero_lt_one.trans_le ?_
simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]
· exact sq_pos_of_pos (pow_pos cpos _)
rw [one_mul, ← mul_pow]
gcongr
rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
exact mul_pow_le_nat_floor_pow hc i
_ ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 :=
by
rw [← mul_sum, ← mul_div_assoc']
gcongr
exact sum_div_pow_sq_le_div_sq N hj hc
_ = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 := by
congr 1
field_simp
