-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
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

Proof state:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ ∑ i ∈ filter (fun i => j < ↑⌊c ^ i⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc

Result:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i ∈ filter (fun i => j < ↑⌊c ^ i⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Proof state:
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))

Tactic:
ring!

Result:
no goals

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

Tactic:
refine zero_lt_one.trans_le ?_

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

Proof state:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i ∈ filter (fun i => j < ↑⌊c ^ i⌋₊) (range N), 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2

Tactic:
have A : 0 < 1 - c⁻¹ := sub_pos.2 (inv_lt_one_of_one_lt₀ hc)

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

Proof state:
case h.h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (fun i => j < ↑⌊c ^ i⌋₊) ≤ fun i => j < c ^ i

Tactic:
exact fun k hk ↦ hk.trans_le <| Nat.floor_le (by positivity)

Result:
no goals

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

Tactic:
rw [one_mul, ← mul_pow]

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

Proof state:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ filter (fun i => j < c ^ i) (range N), (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2) ≤
    (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2

Tactic:
rw [← mul_sum, ← mul_div_assoc']

Result:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ i ∈ filter (fun i => j < c ^ i) (range N), 1 / (c ^ i) ^ 2 ≤
    (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)

Proof state:
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

Tactic:
field_simp [(sub_pos.2 hc).ne']

Result:
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))

Proof state:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
k : ℕ
hk : j < ↑⌊c ^ k⌋₊
⊢ 0 ≤ c ^ k

Tactic:
positivity

Result:
no goals

Proof state:
case hb.ha
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
_hi : i ∈ filter (fun i => j < c ^ i) (range N)
⊢ 1 ≤ ↑⌊c ^ i⌋₊

Tactic:
simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]

Result:
no goals

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

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

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

Tactic:
rotate_left

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

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

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

Tactic:
apply sq_pos_of_pos

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

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

Tactic:
rw [mul_div_assoc', mul_one, div_le_div_iff₀]

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

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

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

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

Tactic:
exact sq_pos_of_pos (pow_pos cpos _)

Result:
no goals

Proof state:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ i ∈ filter (fun i => j < c ^ i) (range N), 1 / (c ^ i) ^ 2 ≤
    (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)

Tactic:
gcongr

Result:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ filter (fun i => j < c ^ i) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

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

Tactic:
refine sum_le_sum fun i _hi => ?_

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

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

Tactic:
gcongr

Result:
case h.h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (fun i => j < ↑⌊c ^ i⌋₊) ≤ fun i => j < c ^ i

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

Tactic:
exact mul_pow_le_nat_floor_pow hc i

Result:
no goals

Proof state:
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

Tactic:
congr 1

Result:
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

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

Tactic:
gcongr

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