norm_le_sSupNormIm — Mathlib

English

On the boundary edges Re z = 0 or Re z = 1, the norm of F f ε z is bounded by 1.

Русский

На границах, где Re z = 0 или Re z = 1, нормa F f ε z не превышает 1.

LaTeX

$$$\|F(f,\varepsilon)(z)\| \le 1$ whenever z lies on the edges Re z \in \{0,1\} and ε > 0.$$

Lean4

/-- If `f` is bounded on the unit vertical strip, then `f` is bounded by `sSupNormIm` there. -/
theorem norm_le_sSupNormIm (f : ℂ → E) (z : ℂ) (hD : z ∈ verticalClosedStrip 0 1)
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) : ‖f z‖ ≤ sSupNormIm f (z.re) :=
  by
  refine le_csSup ?_ ?_
  · revert hB; gcongr
    exact preimage_mono (singleton_subset_iff.mpr hD)
  · apply mem_image_of_mem (norm ∘ f)
    simp only [mem_preimage, mem_singleton]

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