isTheta_exp_arg_mul_im — Mathlib

English

If the imaginary part of g is bounded along l, then exp(arg f · im g) is Θ_l(1).

Русский

Если мнимая часть g ограничена вдоль l, то exp(arg f · im g) является Θ_l(1).

LaTeX

$$$$ \mathrm{Real.exp} \Bigl( \arg(f) \cdot \mathrm{Im}(g) \Bigr) = \Theta_l(1) $$$$

Lean4

theorem isTheta_exp_arg_mul_im (hl : IsBoundedUnder (· ≤ ·) l fun x => |(g x).im|) :
    (fun x => Real.exp (arg (f x) * im (g x))) =Θ[l] fun _ => (1 : ℝ) :=
  by
  rcases hl with ⟨b, hb⟩
  refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩
  rw [eventually_map] at hb ⊢
  refine hb.mono fun x hx => ?_
  rw [abs_mul]
  exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

Похожие утверждения