internlm/Lean-Github huggingface dataset:
Theorem: tendsto_potential
Proof state before:
case h
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
r : ℝ
rp : r > 0
n : ℕ
h : ∀ n_1 ≥ n, dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) n_1) 1 < min (1 / 2) (r / 4)
⊢ ∀ n_1 ≥ n, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n_1] z) * (f' d c)^[n_1] z) ^ (-(↑(d ^ n_1))⁻¹)) 1 < r
Tactic:
intro k nk
Proof state after:
case h
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
r : ℝ
rp : r > 0
n : ℕ
h : ∀ n_1 ≥ n, dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) n_1) 1 < min (1 / 2) (r / 4)
k : ℕ
nk : k ≥ n
⊢ dist (Complex.abs (s.bottcher c ↑((f' d c)^[k] z) * (f' d c)^[k] z) ^ (-(↑(d ^ k))⁻¹)) 1 < r
Theorem: tendsto_potential
Proof state before:
case h
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
r : ℝ
rp : r > 0
n : ℕ
h : ∀ n_1 ≥ n, dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) n_1) 1 < min (1 / 2) (r / 4)
k : ℕ
nk : k ≥ n
⊢ dist (Complex.abs (s.bottcher c ↑((f' d c)^[k] z) * (f' d c)^[k] z) ^ (-(↑(d ^ k))⁻¹)) 1 < r
Tactic:
specialize h k nk
Proof state after:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
h : dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) k) 1 < min (1 / 2) (r / 4)
⊢ dist (Complex.abs (s.bottcher c ↑((f' d c)^[k] z) * (f' d c)^[k] z) ^ (-(↑(d ^ k))⁻¹)) 1 < r
Theorem: tendsto_potential
Proof state before:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
h : dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) k) 1 < min (1 / 2) (r / 4)
⊢ dist (Complex.abs (s.bottcher c ↑((f' d c)^[k] z) * (f' d c)^[k] z) ^ (-(↑(d ^ k))⁻¹)) 1 < r
Tactic:
generalize hw : (f' d c)^[k] z = w
Proof state after:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
h : dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) k) 1 < min (1 / 2) (r / 4)
w : ℂ
hw : (f' d c)^[k] z = w
⊢ dist (Complex.abs (s.bottcher c ↑w * w) ^ (-(↑(d ^ k))⁻¹)) 1 < r
Theorem: tendsto_potential
Proof state before:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
h : dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) k) 1 < min (1 / 2) (r / 4)
w : ℂ
hw : (f' d c)^[k] z = w
⊢ dist (Complex.abs (s.bottcher c ↑w * w) ^ (-(↑(d ^ k))⁻¹)) 1 < r
Tactic:
generalize hp : s.bottcher c w * w = p
Proof state after:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
h : dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) k) 1 < min (1 / 2) (r / 4)
w : ℂ
hw : (f' d c)^[k] z = w
p : ℂ
hp : s.bottcher c ↑w * w = p
⊢ dist (Complex.abs p ^ (-(↑(d ^ k))⁻¹)) 1 < r
Theorem: tendsto_potential
Proof state before:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
h : dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) k) 1 < min (1 / 2) (r / 4)
w : ℂ
hw : (f' d c)^[k] z = w
p : ℂ
hp : s.bottcher c ↑w * w = p
⊢ dist (Complex.abs p ^ (-(↑(d ^ k))⁻¹)) 1 < r
Tactic:
simp only [hw, hp, Function.comp, Complex.dist_eq, Real.dist_eq] at h ⊢
Proof state after:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
w : ℂ
hw : (f' d c)^[k] z = w
p : ℂ
hp : s.bottcher c ↑w * w = p
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
⊢ |Complex.abs p ^ (-(↑(d ^ k))⁻¹) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
r : ℝ
rp : r > 0
n k : ℕ
nk : k ≥ n
w : ℂ
hw : (f' d c)^[k] z = w
p : ℂ
hp : s.bottcher c ↑w * w = p
h : Complex.abs (p - 1) < min (1 / 2) (r / 4)
⊢ |Complex.abs p ^ (-(↑(d ^ k))⁻¹) - 1| < r
Tactic:
clear hp w hw nk n s cz z3
Proof state after:
case h
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)
⊢ |Complex.abs p ^ (-(↑(d ^ k))⁻¹) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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)
⊢ |Complex.abs p ^ (-(↑(d ^ k))⁻¹) - 1| < r
Tactic:
generalize ha : abs p = a
Proof state after:
case h
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
⊢ |a ^ (-(↑(d ^ k))⁻¹) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
⊢ |a ^ (-(↑(d ^ k))⁻¹) - 1| < r
Tactic:
generalize hb : ((d ^ k : ℕ) : ℝ)⁻¹ = b
Proof state after:
case h
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
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
⊢ |a ^ (-b) - 1| < r
Tactic:
have a1 : |a - 1| < min (1 / 2) (r / 4) := by
  rw [← ha]; refine lt_of_le_of_lt ?_ h
  rw [← Complex.abs.map_one]; apply Complex.abs.abs_abv_sub_le_abv_sub
Proof state after:
case h
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)
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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)
⊢ |a ^ (-b) - 1| < r
Tactic:
have am : a ∈ ball (1 : ℝ) (1 / 2) := by
  simp only [mem_ball, Real.dist_eq]; exact (lt_min_iff.mp a1).1
Proof state after:
case h
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)
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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)
⊢ |a ^ (-b) - 1| < r
Tactic:
have b0 : 0 ≤ b := by rw [← hb]; bound
Proof state after:
case h
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
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
⊢ |a ^ (-b) - 1| < r
Tactic:
have b1 : b ≤ 1 := by rw [← hb]; bound
Proof state after:
case h
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
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
⊢ |a ^ (-b) - 1| < r
Tactic:
have hd : ∀ x, x ∈ ball (1 : ℝ) (1 / 2) →
    HasDerivAt (fun x ↦ x ^ (-b)) (1 * -b * x ^ (-b - 1) + 0 * x ^ (-b) * log x) x := by
  intro x m; apply HasDerivAt.rpow (hasDerivAt_id _) (hasDerivAt_const _ _)
  simp only [mem_ball, Real.dist_eq, id] at m ⊢; linarith [abs_lt.mp m]
Proof state after:
case h
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)) (1 * -b * x ^ (-b - 1) + 0 * x ^ (-b) * x.log) x
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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)) (1 * -b * x ^ (-b - 1) + 0 * x ^ (-b) * x.log) x
⊢ |a ^ (-b) - 1| < r
Tactic:
simp only [MulZeroClass.zero_mul, add_zero, one_mul] at hd
Proof state after:
case h
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
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
⊢ |a ^ (-b) - 1| < r
Tactic:
have bound : ∀ x, x ∈ ball (1 : ℝ) (1 / 2) → ‖deriv (fun x ↦ x ^ (-b)) x‖ ≤ 4 := by
  intro x m
  simp only [(hd x m).deriv, Real.norm_eq_abs, abs_mul, abs_neg, abs_of_nonneg b0]
  simp only [mem_ball, Real.dist_eq, abs_lt, lt_sub_iff_add_lt, sub_lt_iff_lt_add] at m
  norm_num at m
  have x0 : 0 < x := by linarith
  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:
case h
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
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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
⊢ |a ^ (-b) - 1| < r
Tactic:
have le := Convex.norm_image_sub_le_of_norm_deriv_le (fun x m ↦ (hd x m).differentiableAt) bound
    (convex_ball _ _) (mem_ball_self (by norm_num)) am
Proof state after:
case h
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 ^ (-b)‖ ≤ 4 * ‖a - 1‖
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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 ^ (-b)‖ ≤ 4 * ‖a - 1‖
⊢ |a ^ (-b) - 1| < r
Tactic:
simp only [Real.norm_eq_abs, Real.one_rpow] at le
Proof state after:
case h
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|
⊢ |a ^ (-b) - 1| < r
Theorem: tendsto_potential
Proof state before:
case h
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|
⊢ |a ^ (-b) - 1| < r
Tactic:
calc |a ^ (-b) - 1|
  _ ≤ 4 * |a - 1| := le
  _ < 4 * (r / 4) := by linarith [(lt_min_iff.mp a1).2]
  _ = r := by ring
Proof state after:
no goals
Theorem: tendsto_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
h : Tendsto (fun n => (Complex.abs ((f' d c)^[n] z) * s.potential c ↑((f' d c)^[n] z)) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Tactic:
replace h := h.mul_const (s.potential c z)
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
h :
  Tendsto
    (fun k => (Complex.abs ((f' d c)^[k] z) * s.potential c ↑((f' d c)^[k] z)) ^ (-(↑(d ^ k))⁻¹) * s.potential c ↑z)
    atTop (𝓝 (1 * s.potential c ↑z))
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Theorem: tendsto_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
h :
  Tendsto
    (fun k => (Complex.abs ((f' d c)^[k] z) * s.potential c ↑((f' d c)^[k] z)) ^ (-(↑(d ^ k))⁻¹) * s.potential c ↑z)
    atTop (𝓝 (1 * s.potential c ↑z))
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Tactic:
simp only [div_mul_cancel₀ _ potential_pos.ne', one_mul, ← f_f'_iter, s.potential_eqn_iter,
  Real.mul_rpow (Complex.abs.nonneg _) (pow_nonneg s.potential_nonneg _),
  Real.pow_rpow_inv_natCast s.potential_nonneg (pow_ne_zero _ (d_ne_zero d)),
  Real.rpow_neg (pow_nonneg s.potential_nonneg _), ← div_eq_mul_inv] at h
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
h : Tendsto (fun k => Complex.abs ((f' d c)^[k] z) ^ (-(↑(d ^ k))⁻¹)) atTop (𝓝 (s.potential c ↑z))
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Theorem: tendsto_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
h : Tendsto (fun k => Complex.abs ((f' d c)^[k] z) ^ (-(↑(d ^ k))⁻¹)) atTop (𝓝 (s.potential c ↑z))
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Tactic:
exact h
Proof state after:
no goals
Theorem: tendsto_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
r : ℝ
rp : r > 0
⊢ min (1 / 2) (r / 4) > 0
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
⊢ |a - 1| < min (1 / 2) (r / 4)
Tactic:
rw [← ha]
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
⊢ |Complex.abs p - 1| < min (1 / 2) (r / 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
⊢ |Complex.abs p - 1| < min (1 / 2) (r / 4)
Tactic:
refine lt_of_le_of_lt ?_ h
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
⊢ |Complex.abs p - 1| ≤ Complex.abs (p - 1)
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
⊢ |Complex.abs p - 1| ≤ Complex.abs (p - 1)
Tactic:
rw [← Complex.abs.map_one]
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
⊢ |Complex.abs p - Complex.abs 1| ≤ Complex.abs (p - 1)
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
⊢ |Complex.abs p - Complex.abs 1| ≤ Complex.abs (p - 1)
Tactic:
apply Complex.abs.abs_abv_sub_le_abv_sub
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)
⊢ a ∈ ball 1 (1 / 2)
Tactic:
simp only [mem_ball, Real.dist_eq]
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)
⊢ |a - 1| < 1 / 2
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)
⊢ |a - 1| < 1 / 2
Tactic:
exact (lt_min_iff.mp a1).1
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)
⊢ 0 ≤ b
Tactic:
rw [← hb]
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)
⊢ 0 ≤ (↑(d ^ k))⁻¹
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)
⊢ 0 ≤ (↑(d ^ k))⁻¹
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
⊢ b ≤ 1
Tactic:
rw [← hb]
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
⊢ (↑(d ^ k))⁻¹ ≤ 1
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
⊢ (↑(d ^ k))⁻¹ ≤ 1
Tactic:
bound
Proof state after:
no goals