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 ^ 3 * (c - 1)⁻¹ / 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 ^ 3 * (c - 1)⁻¹ / 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 < c⁻¹ ^ 2
⊢ ∑ i in filter (fun x => j < c ^ x) (range N), 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / 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 ^ 3 * (c - 1)⁻¹ / j ^ 2
have A : (0 : ℝ) < c⁻¹ ^ 2 := sq_pos_of_pos (inv_pos.2 cpos)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff _ (sub_pos.2 hc)]
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2
swap
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)
have : c ^ 3 = c ^ 2 * c := by ring
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * c * (c ^ 2)⁻¹ ≤ c ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)
simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * c * (c ^ 2)⁻¹ ≤ c ^ 2
rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel (sq_pos_of_pos cpos).ne', one_mul]
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2
simpa using pow_le_pow hc.le one_le_two
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2
exact sub_pos.2 (pow_lt_one (inv_nonneg.2 cpos.le) (inv_lt_one hc) two_ne_zero)
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 3 = c ^ 2 * c
ring
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ filter (fun i => j < c ^ i) (range N) ⊆ Ico ⌊Real.log j / Real.log c⌋₊ N
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ ∑ i in filter (fun i => j < c ^ i) (range N), 1 / (c ^ i) ^ 2 ≤
    ∑ i in Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / (c ^ i) ^ 2
refine'
  sum_le_sum_of_subset_of_nonneg _ fun i _hi _hident => div_nonneg zero_le_one (sq_nonneg _)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i ∈ filter (fun i => j < c ^ i) (range N)
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ filter (fun i => j < c ^ i) (range N) ⊆ Ico ⌊Real.log j / Real.log c⌋₊ N
intro i hi
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i ∈ filter (fun i => j < c ^ i) (range N)
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
simp only [mem_filter, mem_range] at hi
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ ⌊Real.log j / Real.log c⌋₊ ≤ i
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
simp only [hi.1, mem_Ico, and_true_iff]
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c ≤ ↑i
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ ⌊Real.log j / Real.log c⌋₊ ≤ i
apply Nat.floor_le_of_le
case h.a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c < ↑i
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c ≤ ↑i
apply le_of_lt
case h.a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)
case h.a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c < ↑i
rw [div_lt_iff (Real.log_pos hc), ← Real.log_pow]
no goals
case h.a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j < Real.log (c ^ i)
exact Real.log_lt_log hj hi.2
case e_f.h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
⊢ 1 / (c ^ i) ^ 2 = (c⁻¹ ^ 2) ^ i
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ ∑ i in Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / (c ^ i) ^ 2 = ∑ i in Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i
congr 1 with i
no goals
case e_f.h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
i : ℕ
⊢ 1 / (c ^ i) ^ 2 = (c⁻¹ ^ 2) ^ i
simp [← pow_mul, mul_comm]
case h'x
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c⁻¹ ^ 2 < 1
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ ∑ i in Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / (1 - c⁻¹ ^ 2)
apply geom_sum_Ico_le_of_lt_one (sq_nonneg _)
case h'x
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c⁻¹ < 1
case h'x
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c⁻¹ ^ 2 < 1
rw [sq_lt_one_iff (inv_nonneg.2 (zero_le_one.trans hc.le))]
no goals
case h'x
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c⁻¹ < 1
exact inv_lt_one hc
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 0 ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 0 < 1 - c⁻¹ ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / (1 - c⁻¹ ^ 2) ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / (1 - c⁻¹ ^ 2)
apply div_le_div _ _ _ le_rfl
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 0 ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)
apply Real.rpow_nonneg_of_nonneg (sq_nonneg _)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (c⁻¹ ^ 2) ^ ↑⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)
rw [← Real.rpow_nat_cast]
case hx1
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c⁻¹ ^ 2 ≤ 1

case hyz
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j / Real.log c - 1 ≤ ↑⌊Real.log j / Real.log c⌋₊
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (c⁻¹ ^ 2) ^ ↑⌊Real.log j / Real.log c⌋₊ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1)
apply Real.rpow_le_rpow_of_exponent_ge A
no goals
case hx1
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c⁻¹ ^ 2 ≤ 1
exact pow_le_one _ (inv_nonneg.2 (zero_le_one.trans hc.le)) (inv_le_one hc.le)
no goals
case hyz
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j / Real.log c - 1 ≤ ↑⌊Real.log j / Real.log c⌋₊
exact (Nat.sub_one_lt_floor _).le
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 0 < 1 - c⁻¹ ^ 2
simpa only [inv_pow, sub_pos] using inv_lt_one (one_lt_pow hc two_ne_zero)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
⊢ 1 / j ^ 2 / (c⁻¹ ^ 2) ^ 1 / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
⊢ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2
rw [Real.rpow_sub A, I]
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
this : c ^ 2 - 1 ≠ 0
⊢ 1 / j ^ 2 / (c⁻¹ ^ 2) ^ 1 / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
⊢ 1 / j ^ 2 / (c⁻¹ ^ 2) ^ 1 / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2
have : c ^ 2 - 1 ≠ 0 := (sub_pos.2 (one_lt_pow hc two_ne_zero)).ne'
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
this : c ^ 2 - 1 ≠ 0
⊢ (c ^ 2 - 1) * j ^ 2 = j ^ 2 * (c ^ 2 - 1)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
this : c ^ 2 - 1 ≠ 0
⊢ 1 / j ^ 2 / (c⁻¹ ^ 2) ^ 1 / (1 - c⁻¹ ^ 2) = c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2
field_simp [hj.ne', (zero_lt_one.trans hc).ne']
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
this : c ^ 2 - 1 ≠ 0
⊢ (c ^ 2 - 1) * j ^ 2 = j ^ 2 * (c ^ 2 - 1)
ring
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 1 / j ^ 2 ∈ Set.Ioi 0

case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log ((c⁻¹ ^ 2) ^ (Real.log j / Real.log c)) = Real.log (1 / j ^ 2)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = 1 / j ^ 2
apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j / Real.log c * Real.log (c⁻¹ ^ 2) = Real.log (1 / j ^ 2)
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log ((c⁻¹ ^ 2) ^ (Real.log j / Real.log c)) = Real.log (1 / j ^ 2)
rw [Real.log_rpow A]
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j / Real.log c * (↑2 * Real.log c) = ↑2 * Real.log j
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j / Real.log c * Real.log (c⁻¹ ^ 2) = Real.log (1 / j ^ 2)
simp only [one_div, Real.log_inv, Real.log_pow, Nat.cast_one, mul_neg,
  neg_inj]
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j * (2 * Real.log c) = 2 * Real.log j * Real.log c
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j / Real.log c * (↑2 * Real.log c) = ↑2 * Real.log j
field_simp [(Real.log_pos hc).ne']
no goals
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ Real.log j * (2 * Real.log c) = 2 * Real.log j * Real.log c
ring
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (j ^ 2)⁻¹ ∈ Set.Ioi 0
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 1 / j ^ 2 ∈ Set.Ioi 0
rw [one_div]
no goals
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ (j ^ 2)⁻¹ ∈ Set.Ioi 0
exact inv_pos.2 (sq_pos_of_pos hj)
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 0 ≤ c ^ 3 * (c - 1)⁻¹
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2
apply div_le_div _ B (sq_pos_of_pos hj) le_rfl
no goals
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
⊢ 0 ≤ c ^ 3 * (c - 1)⁻¹
exact mul_nonneg (pow_nonneg cpos.le _) (inv_nonneg.2 (sub_pos.2 hc).le)