sSupNormIm_eps_pos — Mathlib

English

If ε > 0, then ||invInterpStrip f z ε|| equals (ε + sSupNormIm f 0)^(Re z - 1) (ε + sSupNormIm f 1)^(-Re z).

Русский

Если ε > 0, то ||invInterpStrip f z ε|| равняется (ε + sSupNormIm f 0)^{Re z - 1} (ε + sSupNormIm f 1)^{-Re z}.

LaTeX

$$$\|\mathrm{invInterpStrip}(f,z,\varepsilon)\| = (\varepsilon + \mathrm{sSupNormIm} f 0)^{\Re z - 1} (\varepsilon + \mathrm{sSupNormIm} f 1)^{-\Re z}$$$

Lean4

/-- `sSup` of `norm` translated by `ε > 0` is positive applied to the image of `f` on the
vertical line `re z = x` -/
theorem sSupNormIm_eps_pos {ε : ℝ} (hε : ε > 0) (x : ℝ) : 0 < ε + sSupNormIm f x := by linarith [sSupNormIm_nonneg f x]

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