internlm/Lean-Github huggingface dataset:
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
⊢ ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (1 * -b * x ^ (-b - 1) + 0 * x ^ (-b) * x.log) x
Tactic:
intro x m
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ HasDerivAt (fun x => x ^ (-b)) (1 * -b * x ^ (-b - 1) + 0 * x ^ (-b) * x.log) x
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ HasDerivAt (fun x => x ^ (-b)) (1 * -b * x ^ (-b - 1) + 0 * x ^ (-b) * x.log) x
Tactic:
apply HasDerivAt.rpow (hasDerivAt_id _) (hasDerivAt_const _ _)
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ 0 < id x
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ 0 < id x
Tactic:
simp only [mem_ball, Real.dist_eq, id] at m ⊢
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
x : ℝ
m : |x - 1| < 1 / 2
⊢ 0 < x
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
x : ℝ
m : |x - 1| < 1 / 2
⊢ 0 < x
Tactic:
linarith [abs_lt.mp m]
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
⊢ ∀ x ∈ ball 1 (1 / 2), ‖deriv (fun x => x ^ (-b)) x‖ ≤ 4
Tactic:
intro x m
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ ‖deriv (fun x => x ^ (-b)) x‖ ≤ 4
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ ‖deriv (fun x => x ^ (-b)) x‖ ≤ 4
Tactic:
simp only [(hd x m).deriv, Real.norm_eq_abs, abs_mul, abs_neg, abs_of_nonneg b0]
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ b * |x ^ (-b - 1)| ≤ 4
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : x ∈ ball 1 (1 / 2)
⊢ b * |x ^ (-b - 1)| ≤ 4
Tactic:
simp only [mem_ball, Real.dist_eq, abs_lt, lt_sub_iff_add_lt, sub_lt_iff_lt_add] at m
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : -(1 / 2) + 1 < x ∧ x < 1 / 2 + 1
⊢ b * |x ^ (-b - 1)| ≤ 4
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : -(1 / 2) + 1 < x ∧ x < 1 / 2 + 1
⊢ b * |x ^ (-b - 1)| ≤ 4
Tactic:
norm_num at m
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
⊢ b * |x ^ (-b - 1)| ≤ 4
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
⊢ b * |x ^ (-b - 1)| ≤ 4
Tactic:
have x0 : 0 < x := by linarith
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ b * |x ^ (-b - 1)| ≤ 4
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ b * |x ^ (-b - 1)| ≤ 4
Tactic:
calc b * |x ^ (-b - 1)|
  _ ≤ 1 * |x| ^ (-b - 1) := by bound
  _ = (x ^ (b + 1))⁻¹ := by rw [← Real.rpow_neg x0.le, neg_add', one_mul, abs_of_pos x0]
  _ ≤ ((1 / 2 : ℝ) ^ (b + 1))⁻¹ := by bound
  _ = 2 ^ (b + 1) := by rw [one_div, Real.inv_rpow zero_le_two, inv_inv]
  _ ≤ 2 ^ (1 + 1 : ℝ) := by bound
  _ ≤ 4 := by norm_num
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ b * |x ^ (-b - 1)| ≤ 1 * |x| ^ (-b - 1)
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ 1 * |x| ^ (-b - 1) = (x ^ (b + 1))⁻¹
Tactic:
rw [← Real.rpow_neg x0.le, neg_add', one_mul, abs_of_pos x0]
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ (x ^ (b + 1))⁻¹ ≤ ((1 / 2) ^ (b + 1))⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ ((1 / 2) ^ (b + 1))⁻¹ = 2 ^ (b + 1)
Tactic:
rw [one_div, Real.inv_rpow zero_le_two, inv_inv]
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ 2 ^ (b + 1) ≤ 2 ^ (1 + 1)
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
x : ℝ
m : 1 / 2 < x ∧ x < 3 / 2
x0 : 0 < x
⊢ 2 ^ (1 + 1) ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
bound : ∀ x ∈ ball 1 (1 / 2), ‖deriv (fun x => x ^ (-b)) x‖ ≤ 4
⊢ 0 < 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
bound : ∀ x ∈ ball 1 (1 / 2), ‖deriv (fun x => x ^ (-b)) x‖ ≤ 4
le : |a ^ (-b) - 1| ≤ 4 * |a - 1|
⊢ 4 * |a - 1| < 4 * (r / 4)
Tactic:
linarith [(lt_min_iff.mp a1).2]
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
k : ℕ
p : ℂ
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
a : ℝ
ha : Complex.abs p = a
b : ℝ
hb : (↑(d ^ k))⁻¹ = b
a1 : |a - 1| < min (1 / 2) (r / 4)
am : a ∈ ball 1 (1 / 2)
b0 : 0 ≤ b
b1 : b ≤ 1
hd : ∀ x ∈ ball 1 (1 / 2), HasDerivAt (fun x => x ^ (-b)) (-b * x ^ (-b - 1)) x
bound : ∀ x ∈ ball 1 (1 / 2), ‖deriv (fun x => x ^ (-b)) x‖ ≤ 4
le : |a ^ (-b) - 1| ≤ 4 * |a - 1|
⊢ 4 * (r / 4) = r
Tactic:
ring
Proof state after:
no goals
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(⋯.potential c ↑z).log).log)
Tactic:
set s := superF d
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have zn1 : ∀ {n}, 1 < abs ((f' d c)^[n] z) := by
  intro n; exact lt_of_lt_of_le (by norm_num) (le_trans z3 (le_self_iter d z3 cz _))
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have zn0 : ∀ {n}, 0 < abs ((f' d c)^[n] z) := fun {_} ↦ lt_trans zero_lt_one zn1
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have ln0 : ∀ {n}, 0 < log (abs ((f' d c)^[n] z)) := fun {_} ↦ Real.log_pos zn1
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have dn0 : ∀ {n}, (d:ℝ)^n ≠ 0 := fun {_} ↦ pow_ne_zero _ (Nat.cast_ne_zero.mpr (d_ne_zero d))
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have p0 : 0 < s.potential c z := potential_pos
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have p1 : s.potential c z < 1 := potential_lt_one_of_two_lt (by linarith) cz
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
set f := fun x ↦ log (log x⁻¹)
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Theorem: tendsto_log_neg_log_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)
Tactic:
have fc : ContinuousAt f ((superF d).potential c z) := by
  refine ((NormedField.continuousAt_inv.mpr p0.ne').log (inv_ne_zero p0.ne')).log ?_
  exact Real.log_ne_zero_of_pos_of_ne_one (inv_pos.mpr p0) (inv_ne_one.mpr p1.ne)
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (_root_.f d) d OnePoint.infty := superF d
zn1 : ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
zn0 : ∀ {n : ℕ}, 0 < Complex.abs ((f' d c)^[n] z)
ln0 : ∀ {n : ℕ}, 0 < (Complex.abs ((f' d c)^[n] z)).log
dn0 : ∀ {n : ℕ}, ↑d ^ n ≠ 0
p0 : 0 < s.potential c ↑z
p1 : s.potential c ↑z < 1
f : ℝ → ℝ := fun x => x⁻¹.log.log
fc : ContinuousAt f (⋯.potential c ↑z)
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) atTop (𝓝 (-(s.potential c ↑z).log).log)