sSupNormIm_nonneg

Mathlib.Analysis.Complex.Hadamard

URI: https://scilib.ai/kg/mathlib#Complex.HadamardThreeLines.sSupNormIm_nonneg

← MathLib Explorer

English

0 ≤ sSupNormIm f x for every x.

Русский

0 ≤ sSupNormIm f x для каждого x.

LaTeX

$$$0 \leq \mathrm{sSupNormIm}(f,x)$$$

Lean4

/-- `sSup` of `norm` is nonneg applied to the image of `f` on the vertical line `re z = x` -/
theorem sSupNormIm_nonneg (x : ℝ) : 0 ≤ sSupNormIm f x :=
  by
  apply Real.sSup_nonneg
  rintro y ⟨z1, _, hz2⟩
  simp only [← hz2, comp, norm_nonneg]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru