internlm/Lean-Github huggingface dataset:
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |⋯.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
set s := superF d
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have z3 : 3 ≤ abs z := le_trans (by norm_num) z4
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have z0 : 0 < abs z := lt_of_lt_of_le (by norm_num) z3
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have l2 : 0 < log (abs z) := Real.log_pos (by linarith)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have h := log_neg_log_potential_approx d z3 cz
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
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)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < s.potential c ↑z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < s.potential c ↑z
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have lp0 : 0 < -log (s.potential c z) :=
  neg_pos.mpr (Real.log_neg p0 (potential_lt_one_of_two_lt (by linarith) cz))
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < s.potential c ↑z
lp0 : 0 < -(s.potential c ↑z).log
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
h : |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < s.potential c ↑z
lp0 : 0 < -(s.potential c ↑z).log
⊢ |s.potential c ↑z - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
generalize s.potential c z = p at h p0 lp0
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
h : |(-p.log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < p
lp0 : 0 < -p.log
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
h : |(-p.log).log - (Complex.abs z).log.log| ≤ iter_error d c z
p0 : 0 < p
lp0 : 0 < -p.log
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
generalize hr : iter_error d c z = r at h
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have r0 : 0 ≤ r := le_trans (abs_nonneg _) h
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
set t := Ici (log (log (abs z)) - r)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have yt : log (-log p) ∈ t := by
  simp only [abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right, add_comm r] at h
  simp only [mem_Ici, tsub_le_iff_right, h, t]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have lt : log (log (abs z)) ∈ t := by
  simp only [mem_Ici, tsub_le_iff_right, le_add_iff_nonneg_right, r0, t]
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
generalize hb : dene (log (log (abs z)) - r) = b
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have b0 : 0 ≤ b := by rw [←hb]; exact dene_nonneg
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have bound : ∀ x, x ∈ t → ‖deriv ene x‖ ≤ b := by
  intro x m
  simp only [Real.dist_eq, mem_Ici, ←hr, t] at m
  simp only [deriv_ene, norm_neg, Real.norm_of_nonneg dene_nonneg, ←hb, ←hr]
  apply dene_anti (sub_nonneg.mpr (iter_error_le_log_log_abs d z4 cz)) m
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
have m := Convex.norm_image_sub_le_of_norm_deriv_le
  (fun x _ ↦ (hasDerivAt_ene x).differentiableAt) bound (convex_Ici _) lt yt
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : ‖ene (-p.log).log - ene (Complex.abs z).log.log‖ ≤ b * ‖(-p.log).log - (Complex.abs z).log.log‖
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : ‖ene (-p.log).log - ene (Complex.abs z).log.log‖ ≤ b * ‖(-p.log).log - (Complex.abs z).log.log‖
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
simp only [Real.norm_eq_abs] at m
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |ene (-p.log).log - ene (Complex.abs z).log.log| ≤ b * |(-p.log).log - (Complex.abs z).log.log|
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |ene (-p.log).log - ene (Complex.abs z).log.log| ≤ b * |(-p.log).log - (Complex.abs z).log.log|
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
replace m := le_trans m (mul_le_mul_of_nonneg_left h (by bound))
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |ene (-p.log).log - ene (Complex.abs z).log.log| ≤ b * r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |ene (-p.log).log - ene (Complex.abs z).log.log| ≤ b * r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
simp only [ene, Real.exp_log lp0, neg_neg, Real.exp_log p0, Real.exp_log l2, Real.exp_neg,
  Real.exp_log z0, inv_eq_one_div] at m
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |p - 1 / Complex.abs z| ≤ b * r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |p - 1 / Complex.abs z| ≤ b * r
⊢ |p - 1 / Complex.abs z| ≤ potential_error d c z
Tactic:
refine le_trans m (le_of_eq ?_)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |p - 1 / Complex.abs z| ≤ b * r
⊢ b * r = potential_error d c z
Theorem: potential_approx
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
l2 : 0 < (Complex.abs z).log
p : ℝ
p0 : 0 < p
lp0 : 0 < -p.log
r : ℝ
hr : iter_error d c z = r
h : |(-p.log).log - (Complex.abs z).log.log| ≤ r
r0 : 0 ≤ r
t : Set ℝ := Ici ((Complex.abs z).log.log - r)
yt : (-p.log).log ∈ t
lt : (Complex.abs z).log.log ∈ t
b : ℝ
hb : dene ((Complex.abs z).log.log - r) = b
b0 : 0 ≤ b
bound : ∀ x ∈ t, ‖deriv ene x‖ ≤ b
m : |p - 1 / Complex.abs z| ≤ b * r
⊢ b * r = potential_error d c z
Tactic:
simp only [←hr, ←hb, potential_error]
Proof state after:
no goals