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

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs ((1 + z) ^ w - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have z1 : 1 + z ≠ 0 := by
  rw [←Complex.abs.ne_zero_iff]; apply ne_of_gt
  calc abs (1 + z) ≥ abs (1 : ℂ) - abs z := by bound
    _ ≥ abs (1 : ℂ) - 1/2 := by bound
    _ > 0 := by norm_num
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs ((1 + z) ^ w - 1) ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs ((1 + z) ^ w - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
rw [Complex.cpow_def_of_ne_zero z1]
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have ls := log1p_small zs
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have eas : abs (log (1 + z) * w) ≤ 1 := by
  rw [Complex.abs.map_mul]
  calc abs (log (1 + z)) * abs w ≤ 2 * abs z * abs w := by bound
    _ ≤ 2 * (1/2) * 1 := by bound
    _ = 1 := by norm_num
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have es := exp_small eas
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs ((1 + z).log * w)
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs ((1 + z).log * w)
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
rw [Complex.abs.map_mul, ←mul_assoc] at es
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
trans 2 * abs (log (1 + z)) * abs w
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w

z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w

z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
exact es
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
calc 2 * abs (log (1 + z)) * abs w ≤ 2 * (2 * abs z) * abs w := by bound
  _ = 4 * abs z * abs w := by ring
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ 1 + z ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff]
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (1 + z) ≠ 0

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (1 + z) ≠ 0
Tactic:
apply ne_of_gt
State after:
case h
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ 0 < Complex.abs (1 + z)

State before:
case h
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ 0 < Complex.abs (1 + z)
Tactic:
calc abs (1 + z) ≥ abs (1 : ℂ) - abs z := by bound
  _ ≥ abs (1 : ℂ) - 1/2 := by bound
  _ > 0 := by norm_num
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (1 + z) ≥ Complex.abs 1 - Complex.abs z
Tactic:
bound
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs 1 - Complex.abs z ≥ Complex.abs 1 - 1 / 2
Tactic:
bound
State after:
no goals

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

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs ((1 + z).log * w) ≤ 1
Tactic:
rw [Complex.abs.map_mul]
State after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (1 + z).log * Complex.abs w ≤ 1

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (1 + z).log * Complex.abs w ≤ 1
Tactic:
calc abs (log (1 + z)) * abs w ≤ 2 * abs z * abs w := by bound
  _ ≤ 2 * (1/2) * 1 := by bound
  _ = 1 := by norm_num
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (1 + z).log * Complex.abs w ≤ 2 * Complex.abs z * Complex.abs w
Tactic:
bound
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ 2 * Complex.abs z * Complex.abs w ≤ 2 * (1 / 2) * 1
Tactic:
bound
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ 2 * (1 / 2) * 1 = 1
Tactic:
norm_num
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 2 * (2 * Complex.abs z) * Complex.abs w
Tactic:
bound
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * (2 * Complex.abs z) * Complex.abs w = 4 * Complex.abs z * Complex.abs w
Tactic:
ring
State after:
no goals