English
If the norm of f is bounded above on the closed strip [l,u], then the norm of scale f l u is bounded above on the closed strip [0,1].
Русский
Если норма f ограничена на замкнутой полосе [l,u], то норма scale f l u ограничена на замкнутой полосе [0,1].
LaTeX
$$$\\text{If } \\sup \\|f(z)\\| \\text{ on } \\text{verticalClosedStrip } l u < \\infty, \\; \\text{then } \\sup \\|\\scale f l u(z)\\| \\text{ on } \\text{verticalClosedStrip } 0 1 < \\infty.$$$
Lean4
/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`. -/
theorem scale_bddAbove {f : ℂ → E} {l u : ℝ} (hul : l < u) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip l u)) :
BddAbove ((norm ∘ scale f l u) '' verticalClosedStrip 0 1) :=
by
obtain ⟨R, hR⟩ := bddAbove_def.mp hB
rw [bddAbove_def]
use R
intro r hr
obtain ⟨w, hw₁, hw₂, _⟩ := hr
simp only [comp_apply, scale, smul_eq_mul]
have : ‖f (↑l + w * (↑u - ↑l))‖ ∈ norm ∘ f '' verticalClosedStrip l u :=
by
simp only [comp_apply, mem_image]
use ↑l + w * (↑u - ↑l)
simp only [and_true]
exact scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hw₁
exact hR ‖f (↑l + w * (↑u - ↑l))‖ this
