scale_bound_left — Mathlib

English

If a bound a holds on the line Re z = l, then for the scaled function scale f l u there is a bound a on the line Re z = 0.

Русский

Если существует ограничение на прямой Re z = l, то для scale f l u существует ограничение на Re z = 0.

LaTeX

$$$\\forall z\\in\\{\\mathrm{Re} z = 0\\}, \\|\\scale f l u z\\| \\le a$ given $\\forall z\\in\\{\\mathrm{Re} z = l\\}, \\|f z\\| \\le a.$$$

Lean4

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

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