Theorem: exp_small (Ray/Misc/Bounds.lean)

State before:
z : ℂ
zs : Complex.abs z ≤ 1
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have rp : (1 : ℝ) > 0 := by norm_num
State after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have cp : (2 : ℝ) > 0 := by norm_num
State after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have fc : ContinuousAt (fun z ↦ exp z - 1) z := by
  apply ContinuousAt.sub; apply ContinuousAt.cexp
  exact continuousAt_id; exact continuousAt_const
State after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
apply weak_to_strong_small rp cp zs fc
State after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ ∀ (z : ℂ), Complex.abs z < 1 → Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ ∀ (z : ℂ), Complex.abs z < 1 → Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
intro w wr
State after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
w : ℂ
wr : Complex.abs w < 1
⊢ Complex.abs (w.exp - 1) ≤ 2 * Complex.abs w

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
w : ℂ
wr : Complex.abs w < 1
⊢ Complex.abs (w.exp - 1) ≤ 2 * Complex.abs w
Tactic:
exact weak_exp_small wr
State after:
no goals

State before:
z : ℂ
zs : Complex.abs z ≤ 1
⊢ 1 > 0
Tactic:
norm_num
State after:
no goals

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
⊢ 2 > 0
Tactic:
norm_num
State after:
no goals

State before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun z => z.exp - 1) z
Tactic:
apply ContinuousAt.sub
State after:
case hf
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => x.exp) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z

State before:
case hf
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => x.exp) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Tactic:
apply ContinuousAt.cexp
State after:
case hf.h
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun y => y) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z

State before:
case hf.h
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun y => y) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Tactic:
exact continuousAt_id
State after:
case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z

State before:
case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Tactic:
exact continuousAt_const
State after:
no goals