English
Let a ≤ 0, b ≥ 0 with |Im z| ≤ b ≤ π/2. Then ||exp(a (e^z + e^{−z}))|| ≤ exp(a cos b · e^{|Re z|}).
Русский
Пусть a ≤ 0, b ≥ 0 и |Im z| ≤ b ≤ π/2. Тогда ||exp(a (e^z + e^{−z}))|| ≤ exp(a cos b · e^{|Re z|}).
LaTeX
$$$$ \\forall a,b \\in \\mathbb{R}, \\ ha \\le 0, \\forall z \\in \\mathbb{C}, \\; |\\mathrm{Im}(z)| \\le b, \\; b \\le \\frac{\\pi}{2} \\Rightarrow \\\\ \\| \\exp\\Big(a \\big( e^{z} + e^{-z} \\big) \\Big) \\| \\le \\exp\\Big(a \\cos b \\exp\\big(|\\mathrm{Re}(z)|\\big)\\Big). $$$$
Lean4
/-- A supporting lemma for the **Phragmen-Lindelöf principle** in a horizontal strip. If `z : ℂ`
belongs to a horizontal strip `|Complex.im z| ≤ b`, `b ≤ π / 2`, and `a ≤ 0`, then
$$\left|exp^{a\left(e^{z}+e^{-z}\right)}\right| \le e^{a\cos b \exp^{|re z|}}.$$
-/
theorem norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le {a b : ℝ} (ha : a ≤ 0) {z : ℂ} (hz : |z.im| ≤ b) (hb : b ≤ π / 2) :
‖exp (a * (exp z + exp (-z)))‖ ≤ Real.exp (a * Real.cos b * Real.exp |z.re|) :=
by
simp only [norm_exp, Real.exp_le_exp, re_ofReal_mul, add_re, exp_re, neg_im, Real.cos_neg, ← add_mul, mul_assoc,
mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]
have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha
· exact Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _) (hb.trans <| half_le_self <| Real.pi_pos.le) hz
· refine Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩
exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)
