Theorem: tendsto_potential (Ray/Dynamics/Multibrot/Potential.lean)

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) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (⋯.potential c ↑z))
Tactic:
set s := superF d
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) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))

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) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Tactic:
suffices h : Tendsto (fun n ↦ (abs ((f' d c)^[n] z) *
    s.potential c ↑((f' d c)^[n] z)) ^ (-((d ^ n : ℕ) : ℝ)⁻¹))
    atTop (𝓝 1) by
  replace h := h.mul_const (s.potential c z)
  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
  exact h
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) * s.potential c ↑((f' d c)^[n] z)) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)

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) * s.potential c ↑((f' d c)^[n] z)) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
Tactic:
simp only [← s.abs_bottcher, ← Complex.abs.map_mul, mul_comm _ (s.bottcher _ _)]
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 (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)

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 (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
Tactic:
rw [Metric.tendsto_atTop]
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
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < ε

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
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < ε
Tactic:
intro r rp
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
r : ℝ
rp : r > 0
⊢ ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r

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
⊢ ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r
Tactic:
rcases Metric.tendsto_atTop.mp ((bottcher_large_approx d c).comp (tendsto_iter_atInf d z3 cz))
    (min (1 / 2) (r / 4)) (by bound) with ⟨n, h⟩
State after:
case intro
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, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r

State before:
case intro
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, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r
Tactic:
use n
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)
⊢ ∀ 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

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

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

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

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

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 ⊢
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

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

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

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

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

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

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

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

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]
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

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

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

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

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

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
State after:
no goals

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

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

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
State after:
no goals

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
State after:
no goals

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]
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)

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

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]
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)

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
State after:
no goals

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]
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

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
State after:
no goals

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]
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))⁻¹

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
State after:
no goals

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]
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

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
State after:
no goals

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

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 _ _)
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

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 ⊢
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

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]
State after:
no goals

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

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]
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

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

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

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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals