English
The complex exponential is uniformly continuous on any left half-plane {x ∈ ℂ | x.re ≤ a} for any real a.
Русский
Комплексная экспонента равномерно непрерывна на любой левой полуплоскости {x ∈ ℂ | Re x ≤ a} при любом действительном a.
LaTeX
$$$$ \\operatorname{UniformContinuousOn}(\\exp, \\{x \\in \\mathbb{C} \\mid \\operatorname{Re}(x) \\le a\\}). $$$$
Lean4
/-- The complex exponential function is uniformly continuous on left half planes. -/
theorem «cexp» (a : ℝ) : UniformContinuousOn exp {x : ℂ | x.re ≤ a} :=
by
have : Continuous (cexp - 1) := Continuous.sub (Continuous.cexp continuous_id') continuous_one
rw [Metric.uniformContinuousOn_iff, Metric.continuous_iff'] at *
intro ε hε
simp only [gt_iff_lt, Pi.sub_apply, Pi.one_apply, dist_sub_eq_dist_add_right, sub_add_cancel] at this
have ha : 0 < ε / (2 * Real.exp a) := by positivity
have H := this 0 (ε / (2 * Real.exp a)) ha
rw [Metric.eventually_nhds_iff] at H
obtain ⟨δ, hδ⟩ := H
refine ⟨δ, hδ.1, ?_⟩
intro x _ y hy hxy
have h3 := hδ.2 (y := x - y) (by simpa only [dist_zero_right] using hxy)
rw [dist_eq_norm, exp_zero] at *
have : cexp x - cexp y = cexp y * (cexp (x - y) - 1) :=
by
rw [mul_sub_one, ← exp_add]
ring_nf
rw [this, mul_comm]
have hya : ‖cexp y‖ ≤ Real.exp a := by
simp only [norm_exp, Real.exp_le_exp]
exact hy
simp only [gt_iff_lt, dist_zero_right, Set.mem_setOf_eq, norm_mul, Complex.norm_exp] at *
apply lt_of_le_of_lt (mul_le_mul h3.le hya (Real.exp_nonneg y.re) (le_of_lt ha))
have hrr : ε / (2 * a.exp) * a.exp = ε / 2 := by
nth_rw 2 [mul_comm]
field_simp
rw [hrr]
exact div_two_lt_of_pos hε
