isBigO_re_sub_re — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isBigO_re_sub_re {z : ℂ} : (fun (w : ℂ) ↦ w.re - z.re) =O[𝓝 z] fun w ↦ w - z :=
  Asymptotics.isBigO_of_le _ fun w ↦ abs_re_le_norm (w - z)

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