sSupNormIm — Mathlib

English

sSupNormIm f x equals the supremum of the norms of f on the line Re z = x.

Русский

sSupNormIm f x равен наибольшему верхнему пределу нормы функции f по строке Re z = x.

LaTeX

$$$\mathrm{sSupNormIm}(f,x)=\sup\{ \|f(z)\| : \Re z = x\}$$$

Lean4

/-- The supremum of the norm of `f` on imaginary lines. (Fixed real part)
This is also known as the function `M` -/
noncomputable def sSupNormIm {E : Type*} [NormedAddCommGroup E] (f : ℂ → E) (x : ℝ) : ℝ :=
  sSup ((norm ∘ f) '' (re ⁻¹' { x }))

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