awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))
B : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))
h :
  ∀ (n : ℕ) (hn : HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ) < a),
    (↑⌊c k ^ (n + 1)⌋₊ : ℝ) ≤ a * (↑⌊c k ^ n⌋₊ : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) (n + 1)) : ℝ) ≤ a * (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) n) : ℝ)

Tactic:
filter_upwards [(tendsto_order.1 B).2 a hk] with n hn

Premises used: tendsto_order, And.right, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))
B : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))
n : ℕ
hn : HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ) < a
⊢ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) ≤ a * (↑⌊c k ^ n⌋₊ : ℝ)

Tactic:
(div_le_iff₀ (H n)).1 hn.le

Premises used: div_le_iff₀, LT.lt.le, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))
B : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))
n : ℕ
hn : HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ) < a
⊢ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) ≤ a * (↑⌊c k ^ n⌋₊ : ℝ)

Tactic:
exact (div_le_iff₀ (H n)).1 hn.le

Premises used: div_le_iff₀, LT.lt.le, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ 0 < c

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ 0 < HPow.hPow (β := ℕ) c⁻¹ 2

Tactic:
have A : (0 : ℝ) < c⁻¹ ^ 2 := sq_pos_of_pos (inv_pos.2 cpos)
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
rw : HPow.hPow (β := ℕ) c 2 * (c - 1) ≤ HPow.hPow (β := ℕ) c 3 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
rw₁ : 0 < 1 - HPow.hPow (β := ℕ) c⁻¹ 2
⊢ HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹

Tactic:
rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]

Premises used: Iff.mpr, sub_pos, div_eq_mul_inv, div_le_div_iff₀
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) c⁻¹ 2

Tactic:
sub_pos.2 (pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero)

Premises used: Iff.mpr, sub_pos, LT.lt.le, inv_lt_one_of_one_lt₀, two_ne_zero, inv_nonneg, pow_lt_one₀
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) c⁻¹ 2

Tactic:
exact sub_pos.2 (pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero)

Premises used: Iff.mpr, sub_pos, LT.lt.le, inv_lt_one_of_one_lt₀, two_ne_zero, inv_nonneg, pow_lt_one₀
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c

Tactic:
have : c ^ 3 = c ^ 2 * c := by ring
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
this : HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c
simp : HPow.hPow (β := ℕ) c 2 * c * (HPow.hPow (β := ℕ) c 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 2
⊢ HPow.hPow (β := ℕ) c 2 * (c - 1) ≤ HPow.hPow (β := ℕ) c 3 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)

Tactic:
simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]

Premises used: mul_sub, sub_le_sub_iff_left, inv_pow, mul_one
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
this : HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c
rw : c ≤ HPow.hPow (β := ℕ) c 2
⊢ HPow.hPow (β := ℕ) c 2 * c * (HPow.hPow (β := ℕ) c 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 2

Tactic:
rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel₀ (sq_pos_of_pos cpos).ne', one_mul]

Premises used: mul_inv_cancel₀, mul_assoc, sq_pos_of_pos, LT.lt.ne', mul_comm, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
this : HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c
⊢ c ≤ HPow.hPow (β := ℕ) c 2

Tactic:
simpa using pow_right_mono₀ hc.le one_le_two

Premises used: LT.lt.le, pow_right_mono₀, one_le_two
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹

Tactic:
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
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 < 1

Tactic:
have C : c⁻¹ ^ 2 < 1 := pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
h : {i ∈ range N | j < c ^ i} ⊆ Ico ⌊Real.log j / Real.log c⌋₊ N
⊢ LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i ∈ {i ∈ range N | j < c ^ i}
⊢ i < N ∧ j < c ^ i

Tactic:
simp only [mem_filter, mem_range] at hi

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
h : ⌊Real.log j / Real.log c⌋₊ ≤ i
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N

Tactic:
simp only [hi.1, mem_Ico, and_true]

Premises used: and_true, And.left, Finset.mem_Ico
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
h : Real.log j / Real.log c ≤ (↑i : ℝ)
⊢ ⌊Real.log j / Real.log c⌋₊ ≤ i

Tactic:
apply Nat.floor_le_of_le

Premises used: Nat.floor_le_of_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
h : Real.log j / Real.log c < (↑i : ℝ)
⊢ Real.log j / Real.log c ≤ (↑i : ℝ)

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
h : Real.log j < Real.log (c ^ i)
⊢ Real.log j / Real.log c < (↑i : ℝ)

Tactic:
rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]

Premises used: Real.log_pos, div_lt_iff₀, Real.log_pow
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)

Tactic:
Real.log_lt_log hj hi.2

Premises used: Real.log_lt_log, And.right
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)

Tactic:
exact Real.log_lt_log hj hi.2

Premises used: Real.log_lt_log, And.right
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ Eq (α := ℝ) (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, HPow.hPow (β := ℕ) c⁻¹ 2 ^ i)

Tactic:
simp [← pow_mul, mul_comm]

Premises used: pow_mul, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, HPow.hPow (β := ℕ) c⁻¹ 2 ^ i ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ / (1 - HPow.hPow (β := ℕ) c⁻¹ 2)

Tactic:
geom_sum_Ico_le_of_lt_one (sq_nonneg _) C

Premises used: sq_nonneg, geom_sum_Ico_le_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
hab : HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ ≤ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
hab :
  HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) (↑⌊Real.log j / Real.log c⌋₊ : ℝ) ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ ≤ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)

Tactic:
rw [← Real.rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) (↑⌊Real.log j / Real.log c⌋₊ : ℝ) ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)

Tactic:
Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le

Premises used: LT.lt.le, Nat.sub_one_lt_floor, Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) (↑⌊Real.log j / Real.log c⌋₊ : ℝ) ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)

Tactic:
exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le

Premises used: LT.lt.le, Nat.sub_one_lt_floor, Real.rpow_le_rpow_of_exponent_ge
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
a : Membership.mem (γ := Set ℝ) (Set.Ioi 0) (1 / HPow.hPow (β := ℕ) j 2)
a₁ : Real.log (HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c)) = Real.log (1 / HPow.hPow (β := ℕ) j 2)
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2

Tactic:
apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)

Premises used: Real.rpow_pos_of_pos, Real.log_injOn_pos
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ 0 < 1 / HPow.hPow (β := ℕ) j 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
a : Real.log j / Real.log c * Real.log (HPow.hPow (β := ℕ) c⁻¹ 2) = Real.log (1 / HPow.hPow (β := ℕ) j 2)
⊢ Real.log (HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c)) = Real.log (1 / HPow.hPow (β := ℕ) j 2)

Tactic:
rw [Real.log_rpow A]

Premises used: Real.log_rpow
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
a : Real.log j / Real.log c * ((↑2 : ℝ) * Real.log c) = (↑2 : ℝ) * Real.log j
⊢ Real.log j / Real.log c * Real.log (HPow.hPow (β := ℕ) c⁻¹ 2) = Real.log (1 / HPow.hPow (β := ℕ) j 2)

Tactic:
simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]

Premises used: one_div, neg_inj, Real.log_pow, Real.log_inv, mul_neg
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ Real.log j / Real.log c * ((↑2 : ℝ) * Real.log c) = (↑2 : ℝ) * Real.log j

Tactic:
field [(Real.log_pos hc).ne']

Premises used: Real.log_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2

Tactic:
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 [(Real.log_pos hc).ne']
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
I : HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
rw :
  1 / HPow.hPow (β := ℕ) j 2 / HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) 1 / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
rw [Real.rpow_sub A, I]

Premises used: Real.rpow_sub
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
I : HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
simp :
  (HPow.hPow (β := ℕ) j 2)⁻¹ * HPow.hPow (β := ℕ) c 2 / (1 - (HPow.hPow (β := ℕ) c 2)⁻¹) =
    HPow.hPow (β := ℕ) c 2 * (1 - (HPow.hPow (β := ℕ) c 2)⁻¹)⁻¹ / HPow.hPow (β := ℕ) j 2
⊢ 1 / HPow.hPow (β := ℕ) j 2 / HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) 1 / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
I : HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
⊢ (HPow.hPow (β := ℕ) j 2)⁻¹ * HPow.hPow (β := ℕ) c 2 / (1 - (HPow.hPow (β := ℕ) c 2)⁻¹) =
    HPow.hPow (β := ℕ) c 2 * (1 - (HPow.hPow (β := ℕ) c 2)⁻¹)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
hc₁ : 0 ≤ HPow.hPow (β := ℕ) j 2
⊢ HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
i₁ :
  Eq (α := ℝ) (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, HPow.hPow (β := ℕ) c⁻¹ 2 ^ i)
i₂ :
  HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
i₃ :
  HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2
i₄ :
  HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2

Tactic:
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
      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 [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr

Premises used: HSub.hSub, Finset.Ico, HDiv.hDiv, Real.log, Finset.range, Inv.inv, HPow.hPow, sq_nonneg, LT.lt, Nat.floor, OfNat.ofNat, Finset.filter, Finset.sum, geom_sum_Ico_le_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
⊢ 0 < c

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
inl : (1 - c⁻¹) * HPow.hPow (β := ℕ) c 0 ≤ (↑⌊HPow.hPow (β := ℕ) c 0⌋₊ : ℝ)
inr : ∀ (hi : i ≠ 0), (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)

Tactic:
rcases eq_or_ne i 0 with (rfl | hi)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * HPow.hPow (β := ℕ) c 0 ≤ (↑⌊HPow.hPow (β := ℕ) c 0⌋₊ : ℝ)

Tactic:
simp only [pow_zero, Nat.floor_one, Nat.cast_one, mul_one, sub_le_self_iff, inv_nonneg, cpos.le]

Premises used: LT.lt.le, pow_zero, inv_nonneg, mul_one, Nat.floor_one, Nat.cast_one, sub_le_self_iff
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
h : 1 ≤ c ^ i * c⁻¹
⊢ c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ 1 ≤ c ^ i * c⁻¹

Tactic:
simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi

Premises used: LT.lt.le, div_eq_mul_inv, pow_one, le_self_pow₀, one_le_div