English
For z in verticalStrip 0 1, with appropriate differentiability, the norm is bounded by the interpolant: ‖f z‖ ≤ ‖interpStrip f z‖.
Русский
Для z в вертикальной полосе 0 1 при подходящей дифференцируемости выполняется: ‖f z‖ ≤ ‖interpStrip f z‖.
LaTeX
$$$\\|f z\\| ≤ \\|\\interpStrip f z\\| \\quad (z \\in \\text{verticalStrip } 0 1).$$$
Lean4
/-- **Hadamard three-line theorem** (Variant in simpler terms): Let `f` be a
bounded function, continuous on the closed strip `re ⁻¹' [l, u]` and differentiable on open strip
`re ⁻¹' (l, u)`. If, for all `z.re = l`, `‖f z‖ ≤ a` for some `a ∈ ℝ` and, similarly, for all
`z.re = u`, `‖f z‖ ≤ b` for some `b ∈ ℝ` then for all `z` in the closed strip
`re ⁻¹' [l, u]` the inequality
`‖f(z)‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))`
holds. -/
theorem norm_le_interp_of_mem_verticalClosedStrip' {f : ℂ → E} {z : ℂ} {a b l u : ℝ} (hul : l < u)
(hz : z ∈ verticalClosedStrip l u) (hd : DiffContOnCl ℂ f (verticalStrip l u))
(hB : BddAbove ((norm ∘ f) '' verticalClosedStrip l u)) (ha : ∀ z ∈ re ⁻¹' { l }, ‖f z‖ ≤ a)
(hb : ∀ z ∈ re ⁻¹' { u }, ‖f z‖ ≤ b) : ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l)) :=
by
have hgoal :=
norm_le_interp_of_mem_verticalClosedStrip₀₁' (scale f l u)
(mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip hul hz) (scale_diffContOnCl hul hd)
(scale_bddAbove hul hB) (scale_bound_left ha) (scale_bound_right hb)
simp only [scale, smul_eq_mul, sub_re] at hgoal
rw [fun_arg_eq hul, bound_exp_eq hul] at hgoal
exact hgoal
