N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i in filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ ∑ i in filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
have cpos : 0 < c := zero_lt_one.trans hc
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i in filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i in filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
have A : 0 < 1 - c⁻¹ := sub_pos.2 (inv_lt_one hc)
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N) ⊆ filter (fun x => j < c ^ x) (range N)

case hf
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∀ (i : ℕ),
    i ∈ filter (fun x => j < c ^ x) (range N) → ¬i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N) → 0 ≤ 1 / ↑⌊c ^ i⌋₊ ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i in filter (fun x => j < ↑⌊c ^ x⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤
    ∑ i in filter (fun x => j < c ^ x) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2
apply sum_le_sum_of_subset_of_nonneg
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
hi : i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N)
⊢ i ∈ filter (fun x => j < c ^ x) (range N)
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N) ⊆ filter (fun x => j < c ^ x) (range N)
intro i hi
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
hi : i < N ∧ j < ↑⌊c ^ i⌋₊
⊢ i ∈ filter (fun x => j < c ^ x) (range N)
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
hi : i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N)
⊢ i ∈ filter (fun x => j < c ^ x) (range N)
simp only [mem_filter, mem_range] at hi
no goals
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
hi : i < N ∧ j < ↑⌊c ^ i⌋₊
⊢ i ∈ filter (fun x => j < c ^ x) (range N)
simpa only [hi.1, mem_filter, mem_range, true_and_iff] using
  hi.2.trans_le (Nat.floor_le (pow_nonneg cpos.le _))
case hf
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
_hident : ¬i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N)
⊢ 0 ≤ 1 / ↑⌊c ^ i⌋₊ ^ 2
case hf
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∀ (i : ℕ),
    i ∈ filter (fun x => j < c ^ x) (range N) → ¬i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N) → 0 ≤ 1 / ↑⌊c ^ i⌋₊ ^ 2
intro i _hi _hident
no goals
case hf
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
_hident : ¬i ∈ filter (fun x => j < ↑⌊c ^ x⌋₊) (range N)
⊢ 0 ≤ 1 / ↑⌊c ^ i⌋₊ ^ 2
exact div_nonneg zero_le_one (sq_nonneg _)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i in filter (fun x => j < c ^ x) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤
    ∑ i in filter (fun x => j < c ^ x) (range N), (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)
refine' sum_le_sum fun i _hi => _
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

case b0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

case d0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < (c ^ i) ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)
rw [mul_div_assoc', mul_one, div_le_div_iff]
case b0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

case d0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < (c ^ i) ^ 2

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

case b0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

case d0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < (c ^ i) ^ 2
rotate_left
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ (c ^ i) ^ 2 ≤ ((1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊) ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2
rw [one_mul, ← mul_pow]
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ c ^ i ≤ (1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ (c ^ i) ^ 2 ≤ ((1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊) ^ 2
apply pow_le_pow_of_le_left (pow_nonneg cpos.le _)
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ c ^ i ≤ (1 - c⁻¹)⁻¹ * ↑⌊c ^ i⌋₊
rw [← div_eq_inv_mul, le_div_iff A, mul_comm]
no goals
case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
exact mul_pow_le_nat_floor_pow hc i
case b0.ha
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < ↑⌊c ^ i⌋₊
case b0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2
apply sq_pos_of_pos
case b0.ha
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 ≤ ↑⌊c ^ i⌋₊
case b0.ha
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < ↑⌊c ^ i⌋₊
refine' zero_lt_one.trans_le _
no goals
case b0.ha
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 1 ≤ ↑⌊c ^ i⌋₊
simp only [Nat.le_floor, one_le_pow_of_one_le, hc.le, Nat.one_le_cast, Nat.cast_one]
no goals
case d0
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun x => j < c ^ x) (range N)
⊢ 0 < (c ^ i) ^ 2
exact sq_pos_of_pos (pow_pos cpos _)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ x in filter (fun x => j < c ^ x) (range N), 1 / (c ^ x) ^ 2 ≤
    (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i in filter (fun x => j < c ^ x) (range N), (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2) ≤
    (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2
rw [← mul_sum, ← mul_div_assoc']
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ x in filter (fun x => j < c ^ x) (range N), 1 / (c ^ x) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ x in filter (fun x => j < c ^ x) (range N), 1 / (c ^ x) ^ 2 ≤
    (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)
refine' mul_le_mul_of_nonneg_left _ (sq_nonneg _)
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ x in filter (fun x => j < c ^ x) (range N), 1 / (c ^ x) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
exact sum_div_pow_sq_le_div_sq N hj hc
case e_a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) = c ^ 5 * (c - 1)⁻¹ ^ 3
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
congr 1
case e_a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ c ^ 2 * c ^ 3 * (c - 1) ^ 3 = c ^ 5 * ((c - 1) ^ 2 * (c - 1))
case e_a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) = c ^ 5 * (c - 1)⁻¹ ^ 3
field_simp [cpos.ne', (sub_pos.2 hc).ne']
no goals
case e_a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ c ^ 2 * c ^ 3 * (c - 1) ^ 3 = c ^ 5 * ((c - 1) ^ 2 * (c - 1))
ring!