scale_bound_right — Mathlib

English

Analogous bound holds if the bound on Re z = u is given, transferring to Re z = 1 for scale f l u.

Русский

Аналогично, если ограничение на Re z = u существует, то на Re z = 1 для scale f l u выполняется аналогичное ограничение.

LaTeX

$$$\\forall z\\in\\{\\mathrm{Re} z = 1\\}, \\|\\scale f l u z\\| \\le b$ при условии $\\forall z\\in\\{\\mathrm{Re} z = u\\}, \\|f z\\| \\le b.$$$

Lean4

/-- A bound to the norm of `f` on the line `z.re = u` induces a bound to the norm of `scale f l u z`
  on the line `z.re = 1`. -/
theorem scale_bound_right {f : ℂ → E} {l u b : ℝ} (hb : ∀ z ∈ re ⁻¹' { u }, ‖f z‖ ≤ b) :
    ∀ z ∈ re ⁻¹' { 1 }, ‖scale f l u z‖ ≤ b :=
  by
  simp only [scale, mem_preimage, mem_singleton_iff, smul_eq_mul]
  intro z hz
  exact hb (↑l + z * (↑u - ↑l)) (by simp [hz])

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