Theorems · Theorem · real analysis

Complex.norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le

∀ {a b : ℝ},
  a ≤ 0 →
    ∀ {z : ℂ},
      |z.im| ≤ b →
        b ≤ Real.pi / 2 →
          ‖Complex.exp (↑a * (Complex.exp z + Complex.exp (-z)))‖ ≤ Real.exp (a * Real.cos b * Real.exp |z.re|)

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|}}.$$

Defined in

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Cited by

1 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound