internlm/Lean-Github huggingface dataset:
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
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)
Tactic:
have t := Tendsto.comp fc (tendsto_potential 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 (_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)
t : Tendsto (f ∘ fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (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)
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
fc : ContinuousAt f (⋯.potential c ↑z)
t : Tendsto (f ∘ fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (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)
Tactic:
simpa only [Real.log_inv, Real.log_neg_eq_log, Nat.cast_pow, Function.comp_def, Real.log_rpow zn0,
  neg_mul, ← div_eq_inv_mul, Real.log_div ln0.ne' dn0, Real.log_pow, f] using t
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
s : Super (f d) d OnePoint.infty := superF d
⊢ ∀ {n : ℕ}, 1 < Complex.abs ((f' d c)^[n] z)
Tactic:
intro n
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
n : ℕ
⊢ 1 < Complex.abs ((f' d c)^[n] z)
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
n : ℕ
⊢ 1 < Complex.abs ((f' d c)^[n] z)
Tactic:
exact lt_of_lt_of_le (by norm_num) (le_trans z3 (le_self_iter d z3 cz _))
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
s : Super (f d) d OnePoint.infty := superF d
n : ℕ
⊢ 1 < 3
Tactic:
norm_num
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
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
⊢ 2 < Complex.abs z
Tactic:
linarith
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
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
⊢ ContinuousAt f (⋯.potential c ↑z)
Tactic:
refine ((NormedField.continuousAt_inv.mpr p0.ne').log (inv_ne_zero p0.ne')).log ?_
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
⊢ (s.potential c ↑z)⁻¹.log ≠ 0
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
⊢ (s.potential c ↑z)⁻¹.log ≠ 0
Tactic:
exact Real.log_ne_zero_of_pos_of_ne_one (inv_pos.mpr p0) (inv_ne_one.mpr p1.ne)
Proof state after:
no goals
Theorem: log_neg_log_potential_approx
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
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| ≤ iter_error d c z
Tactic:
apply le_of_forall_pos_lt_add
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
⊢ ∀ (ε : ℝ), 0 < ε → |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + ε
Theorem: log_neg_log_potential_approx
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
⊢ ∀ (ε : ℝ), 0 < ε → |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + ε
Tactic:
intro e ep
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
e : ℝ
ep : 0 < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
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
e : ℝ
ep : 0 < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
rcases (Metric.tendsto_nhds.mp (tendsto_log_neg_log_potential d z3 cz) e ep).exists with ⟨n,t⟩
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
have ie := iter_approx d z3 cz n
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) (-(⋯.potential c ↑z).log).log < e
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |(-(⋯.potential c ↑z).log).log - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
generalize log (-log ((superF d).potential c z)) = p at ie t
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
p : ℝ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
ie : |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
p : ℝ
t : dist ((Complex.abs ((f' d c)^[n] z)).log.log - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
generalize log (log (Complex.abs ((f' d c)^[n] z))) = x at ie t
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
ie : |x - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
t : dist (x - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
ie : |x - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
t : dist (x - ↑n * (↑d).log) p < e
⊢ |p - (Complex.abs z).log.log| < iter_error d c z + e
Tactic:
generalize log (log (Complex.abs z)) = y at ie t
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : dist (x - ↑n * (↑d).log) p < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : dist (x - ↑n * (↑d).log) p < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e
Tactic:
rw [Real.dist_eq, abs_sub_comm] at t
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < iter_error d c z + e
Tactic:
rw [add_comm]
Proof state after:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < e + iter_error d c z
Theorem: log_neg_log_potential_approx
Proof state before:
case h.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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| < e + iter_error d c z
Tactic:
calc |p - y|
    _ = |(p - (x - n * log d)) + (x - y - n * log d)| := by ring_nf
    _ ≤ |p - (x - n * log d)| + |x - y - n * log d| := abs_add _ _
    _ < e + _ := add_lt_add_of_lt_of_le t ie
Proof state after:
no goals
Theorem: log_neg_log_potential_approx
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
e : ℝ
ep : 0 < e
n : ℕ
p x : ℝ
t : |p - (x - ↑n * (↑d).log)| < e
y : ℝ
ie : |x - y - ↑n * (↑d).log| ≤ iter_error d c z
⊢ |p - y| = |p - (x - ↑n * (↑d).log) + (x - y - ↑n * (↑d).log)|
Tactic:
ring_nf
Proof state after:
no goals
Theorem: hasDerivAt_ene
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
⊢ HasDerivAt ene (-dene x) x
Tactic:
have h : HasDerivAt (fun x ↦ exp (-exp x)) (exp (-exp x) * -exp x) x :=
  HasDerivAt.exp (Real.hasDerivAt_exp x).neg
Proof state after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) ((-x.exp).exp * -x.exp) x
⊢ HasDerivAt ene (-dene x) x
Theorem: hasDerivAt_ene
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) ((-x.exp).exp * -x.exp) x
⊢ HasDerivAt ene (-dene x) x
Tactic:
simp only [mul_neg, ← Real.exp_add, neg_add_eq_sub] at h
Proof state after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) (-(x - x.exp).exp) x
⊢ HasDerivAt ene (-dene x) x
Theorem: hasDerivAt_ene
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
h : HasDerivAt (fun x => (-x.exp).exp) (-(x - x.exp).exp) x
⊢ HasDerivAt ene (-dene x) x
Tactic:
exact h
Proof state after:
no goals
Theorem: dene_anti
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
⊢ dene x ≥ dene y
Tactic:
refine Real.exp_le_exp.mpr ?_
Proof state after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
⊢ y - y.exp ≤ x - x.exp
Theorem: dene_anti
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
a : AntitoneOn (fun x => x - x.exp) (Ici 0)
⊢ y - y.exp ≤ x - x.exp
Tactic:
exact a x0 (le_trans x0 xy) xy
Proof state after:
no goals
Theorem: dene_anti
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Tactic:
have hd : ∀ x, HasDerivAt (fun x ↦ x - exp x) (1 - exp x) x :=
  fun x ↦ (hasDerivAt_id x).sub (Real.hasDerivAt_exp x)
Proof state after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Theorem: dene_anti
Proof state before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Tactic:
have d : Differentiable ℝ (fun x ↦ x - exp x) := fun x ↦ (hd x).differentiableAt
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Theorem: dene_anti
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici _)
Proof state after:
case hf
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ContinuousOn (fun x => x - x.exp) (Ici 0)

case hf'
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ DifferentiableOn ℝ (fun x => x - x.exp) (interior (Ici 0))

case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ∀ x ∈ interior (Ici 0), deriv (fun x => x - x.exp) x ≤ 0
Theorem: dene_anti
Proof state before:
case hf
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ContinuousOn (fun x => x - x.exp) (Ici 0)
Tactic:
exact d.continuous.continuousOn
Proof state after:
no goals
Theorem: dene_anti
Proof state before:
case hf'
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ DifferentiableOn ℝ (fun x => x - x.exp) (interior (Ici 0))
Tactic:
exact d.differentiableOn
Proof state after:
no goals
Theorem: dene_anti
Proof state before:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ∀ x ∈ interior (Ici 0), deriv (fun x => x - x.exp) x ≤ 0
Tactic:
intro x m
Proof state after:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : x ∈ interior (Ici 0)
⊢ deriv (fun x => x - x.exp) x ≤ 0
Theorem: dene_anti
Proof state before:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : x ∈ interior (Ici 0)
⊢ deriv (fun x => x - x.exp) x ≤ 0
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at m
Proof state after:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : 0 < x
⊢ deriv (fun x => x - x.exp) x ≤ 0
Theorem: dene_anti
Proof state before:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : 0 < x
⊢ deriv (fun x => x - x.exp) x ≤ 0
Tactic:
simp only [(hd x).deriv, sub_nonpos, Real.one_le_exp m.le]
Proof state after:
no goals
Theorem: dene_eq
Proof state before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
⊢ dene (z.log.log - k) = (-k).exp * z.log * z ^ (-(-k).exp)
Tactic:
have l0 : 0 < log z := Real.log_pos z1
Proof state after:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ dene (z.log.log - k) = (-k).exp * z.log * z ^ (-(-k).exp)
Theorem: dene_eq
Proof state before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ dene (z.log.log - k) = (-k).exp * z.log * z ^ (-(-k).exp)
Tactic:
simp only [dene, sub_eq_add_neg, Real.exp_add, Real.exp_log l0, mul_comm _ (exp (-k)), ←neg_mul]
Proof state after:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-k).exp * z.log * (-(-k).exp * z.log).exp = (-k).exp * z.log * z ^ (-(-k).exp)
Theorem: dene_eq
Proof state before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-k).exp * z.log * (-(-k).exp * z.log).exp = (-k).exp * z.log * z ^ (-(-k).exp)
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-(-k).exp * z.log).exp = z ^ (-(-k).exp)
Theorem: dene_eq
Proof state before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ (-(-k).exp * z.log).exp = z ^ (-(-k).exp)
Tactic:
rw [mul_comm, Real.exp_mul, Real.exp_log (by positivity)]
Proof state after:
no goals
Theorem: dene_eq
Proof state before:
c z✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℝ
z1 : 1 < z
k : ℝ
l0 : 0 < z.log
⊢ 0 < z
Tactic:
positivity
Proof state after:
no goals
Theorem: potential_error_le
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have z1 : 1 < abs z := by linarith
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Theorem: potential_error_le
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have z4 : 4 ≤ abs z := by linarith
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Theorem: potential_error_le
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have l1 : 1.386 < log (abs z) := lt_of_lt_of_le lt_log_4 (Real.log_le_log (by linarith) z4)
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Theorem: potential_error_le
Proof state before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have l0 : 0 < log (abs z) := lt_trans (by norm_num) l1
Proof state after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)