z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
have hy_eq : y = x + (y - x) := by abel
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
have hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖ := by
  rw [pow_two]
  exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
have h_sq : ∀ z, ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2 := by
  intro z hz
  have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
  rw [← sub_le_iff_le_add', ← norm_smul z]
  exact (norm_sub_norm_le _ _).trans this
no goals
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
calc
  ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖ := by nth_rw 1 [hy_eq]
  _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * ‖y - x‖ ^ 2 := (h_sq (y - x) (hyx.le.trans hr_le))
  _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) :=
    (add_le_add_left (mul_le_mul le_rfl hyx_sq_le (sq_nonneg _) (norm_nonneg _)) _)
  _ = (1 + r) * ‖exp x‖ * ‖y - x‖ := by ring
no goals
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)
abel
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
rw [pow_two]
no goals
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
intro z hz
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ - ‖z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
rw [← sub_le_iff_le_add', ← norm_smul z]
no goals
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ - ‖z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
exact (norm_sub_norm_le _ _).trans this
no goals
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖
nth_rw 1 [hy_eq]
no goals
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) = (1 + r) * ‖exp x‖ * ‖y - x‖
ring