English
There exists an eventual bound for the norm of f in terms of the three-line bound as ε → 0.
Русский
Существует асимптотически ограничивающее неравенство нормы f в терминах трёхлинейной границы при ε → 0.
LaTeX
$$$\\text{There exists } ε\\to 0^+ : \\|f(z)\\| \\le \\|\\text{bound}(ε)\\|.$$$
Lean4
/-- **Hadamard three-line theorem** on `re ⁻¹' [0, 1]`: If `f` is a bounded function, continuous on the
closed strip `re ⁻¹' [0, 1]` and differentiable on open strip `re ⁻¹' (0, 1)`, then for
`M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x}))` we have that for all `z` in the closed strip
`re ⁻¹' [0, 1]` the inequality `‖f(z)‖ ≤ M(0) ^ (1 - z.re) * M(1) ^ z.re` holds. -/
theorem norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ (f : ℂ → E) {z : ℂ} (hz : z ∈ verticalClosedStrip 0 1)
(hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) :
‖f z‖ ≤ ‖interpStrip f z‖ :=
by
apply
le_on_closure (fun w hw ↦ norm_le_interpStrip_of_mem_verticalStrip_zero f w hd hB hw)
(Continuous.comp_continuousOn' continuous_norm hd.2)
(Continuous.comp_continuousOn' continuous_norm (diffContOnCl_interpStrip f).2)
rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz
