English
The partial sum of 1/(c^i)^2 beyond a threshold j is bounded by a constant times 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^3 (c - 1)^{-1} / 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_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 ^ 3 * (c - 1)⁻¹ / j ^ 2 :=
by
have cpos : 0 < c := zero_lt_one.trans hc
have A : (0 : ℝ) < c⁻¹ ^ 2 := sq_pos_of_pos (inv_pos.2 cpos)
have B : c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹ :=
by
rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]
swap
· exact sub_pos.2 (pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero)
have : c ^ 3 = c ^ 2 * c := by ring
simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]
rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel₀ (sq_pos_of_pos cpos).ne', one_mul]
simpa using pow_right_mono₀ hc.le one_le_two
have C : c⁻¹ ^ 2 < 1 := pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero
calc
(∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 :=
by
gcongr
intro i hi
simp only [mem_filter, mem_range] at hi
simp only [hi.1, mem_Ico, and_true]
apply Nat.floor_le_of_le
apply le_of_lt
rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
exact Real.log_lt_log hj hi.2
_ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by simp [← pow_mul, mul_comm]
_ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) := (geom_sum_Ico_le_of_lt_one (sq_nonneg _) C)
_ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) :=
by
gcongr
· exact sub_nonneg.2 C.le
· rw [← Real.rpow_natCast]
exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
_ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 :=
by
have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 :=
by
apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
· rw [Set.mem_Ioi]; positivity
rw [Real.log_rpow A]
simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
field_simp [(Real.log_pos hc).ne']
rw [Real.rpow_sub A, I]
simp
ring
_ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr
