isTheta_ofReal — Mathlib

English

For f: α → ℝ, the complex embedding f ↦ f in ℂ yields a Θ relation with f.

Русский

Для f: α → ℝ комплексная инкапсуляция f в ℂ сохраняет отношение Θ по отношению к f.

LaTeX

$$$$ (f · : α \to \mathbb{C}) =_\Theta[l] f.$$$$

Lean4

theorem isTheta_ofReal (f : α → ℝ) (l : Filter α) : (f · : α → ℂ) =Θ[l] f :=
  .of_norm_left <| by simpa using (Asymptotics.isTheta_rfl (f := f)).norm_left

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