English
Under suitable regularity, the norm of f on the closed vertical strip is bounded by the norm of interpStrip composed with f on that strip.
Русский
При надлежащей гладкости норма f на закрытой вертикальной полосе ограничена нормой interpStrip(f) на той же полосе.
LaTeX
$$$\\|f z\\| ≤ \\|\\interpStrip f z\\| \\quad \\text{ для всех } z \\in \\text{verticalClosedStrip } 0 1.$$$
Lean4
/-- **Hadamard three-line theorem**: If `f` is a bounded function, continuous on the
closed strip `re ⁻¹' [l, u]` and differentiable on open strip `re ⁻¹' (l, u)`, then for
`M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x}))` we have that for all `z` in the closed strip
`re ⁻¹' [a,b]` the inequality
`‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l))`
holds. -/
theorem norm_le_interpStrip_of_mem_verticalClosedStrip {l u : ℝ} (hul : l < u) {f : ℂ → E} {z : ℂ}
(hz : z ∈ verticalClosedStrip l u) (hd : DiffContOnCl ℂ f (verticalStrip l u))
(hB : BddAbove ((norm ∘ f) '' verticalClosedStrip l u)) : ‖f z‖ ≤ ‖interpStrip' f l u z‖ :=
by
have hgoal :=
norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ (scale f l u)
(mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip hul hz) (scale_diffContOnCl hul hd)
(scale_bddAbove hul hB)
simp only [scale, smul_eq_mul] at hgoal
rw [fun_arg_eq hul, div_sub_div_same, interpStrip_scale f hul z] at hgoal
exact hgoal
