isBigO_im_sub_im — Mathlib

English

For any z ∈ ℂ, the function w ↦ Im w − Im z is Big-O of w − z near w = z; i.e., the imaginary part difference is controlled by the distance to z.

Русский

Для любого z ∈ ℂ функция w ↦ Im w − Im z является ограниченной сверху той же функцией по мере удаления от z; точнее, Im(w) − Im(z) = O(|w−z|) при w → z.

LaTeX

$$$ (\\lambda w: w_{\\text{im}} - z_{\\text{im}}) =O[𝓝 z] (\\lambda w: w - z) $$$

Lean4

theorem isBigO_im_sub_im {z : ℂ} : (fun (w : ℂ) ↦ w.im - z.im) =O[𝓝 z] fun w ↦ w - z :=
  Asymptotics.isBigO_of_le _ fun w ↦ abs_im_le_norm (w - z)

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