English
Let r ≥ 0 with r ≤ 1. For any x, y ∈ ℂ with ||y − x|| < r, the exponential map satisfies ||e^y − e^x|| ≤ (1 + r) ||e^x|| ||y − x||.
Русский
Пусть r ≥ 0 и r ≤ 1. Для любых x, y ∈ ℂ такие, что ||y − x|| < r, выполняется неравенство ||e^y − e^x|| ≤ (1 + r) ||e^x|| ||y − x||.
LaTeX
$$$\\\\forall r \\\\ge 0, \\\\forall r \\\\le 1, \\\\forall x,y \\\\in \\\\mathbb{C}, \\\\|y - x\\\\| < r \\\\Rightarrow \\\\|e^y - e^x\\\\| \\\\le (1 + r) \\\\|e^x\\\\| \\\\|y - x\\\\|.$$$
Lean4
theorem locally_lipschitz_exp {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‖ :=
by
have hy_eq : y = x + (y - x) := by abel
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
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
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
-- Porting note: proof by term mode `locally_lipschitz_exp zero_le_one le_rfl x`
-- doesn't work because `‖y - x‖` and `dist y x` don't unify
