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

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

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have L := Complex.locally_lipschitz_exp hr (by bound) 0 z
  (by simpa only [sub_zero, Complex.norm_eq_abs])
State after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : ‖z.exp - exp 0‖ ≤ (1 + 1) * ‖exp 0‖ * ‖z - 0‖
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : ‖z.exp - exp 0‖ ≤ (1 + 1) * ‖exp 0‖ * ‖z - 0‖
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
simp only [Complex.exp_zero, Complex.norm_eq_abs, norm_one, mul_one, sub_zero] at L
State after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have t : 1 + 1 = (2 : ℝ) := by norm_num
State after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
rw [t] at L
State after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
assumption
State after:
no goals

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

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ 1 ≤ 1
Tactic:
bound
State after:
no goals

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ ‖z - 0‖ < 1
Tactic:
simpa only [sub_zero, Complex.norm_eq_abs]
State after:
no goals

State before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
⊢ 1 + 1 = 2
Tactic:
norm_num
State after:
no goals