English
If the norm of f is bounded above on the verticalClosedStrip l u, then the norm of scale f l u is bounded above on verticalClosedStrip 0 1.
Русский
Если норма f ограничена на вертикальной закрытой полосе [l,u], то норма scale f l u ограничена на вертикальной закрытой полосе [0,1].
LaTeX
$$$\\text{If } \\sup_{z \\in \\text{verticalClosedStrip } l u} \\|f z\\| < \\infty, \\text{ then } \\sup_{z \\in \\text{verticalClosedStrip } 0 1} \\|\\scale f l u z\\| < \\infty.$$$
Lean4
/-- **Hadamard three-line theorem** on `re ⁻¹' [0, 1]` (Variant in simpler terms): Let `f` be a
bounded function, continuous on the closed strip `re ⁻¹' [0, 1]` and differentiable on open strip
`re ⁻¹' (0, 1)`. If, for all `z.re = 0`, `‖f z‖ ≤ a` for some `a ∈ ℝ` and, similarly, for all
`z.re = 1`, `‖f z‖ ≤ b` for some `b ∈ ℝ` then for all `z` in the closed strip
`re ⁻¹' [0, 1]` the inequality `‖f(z)‖ ≤ a ^ (1 - z.re) * b ^ z.re` holds. -/
theorem norm_le_interp_of_mem_verticalClosedStrip₀₁' (f : ℂ → E) {z : ℂ} {a b : ℝ} (hz : z ∈ verticalClosedStrip 0 1)
(hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1))
(ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a) (hb : ∀ z ∈ re ⁻¹' { 1 }, ‖f z‖ ≤ b) : ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re :=
by
have : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re :=
by
by_cases h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
· rw [interpStrip_eq_of_zero f z h, norm_zero, mul_nonneg_iff]
left
exact ⟨Real.rpow_nonneg (sSupNormIm_nonneg f _) _, Real.rpow_nonneg (sSupNormIm_nonneg f _) _⟩
· push_neg at h
rcases h with ⟨h0, h1⟩
rw [ne_comm] at h0 h1
simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
(lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]
simp only [norm_mul]
rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h0).mp (sSupNormIm_nonneg f _)) _]
rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h1).mp (sSupNormIm_nonneg f _)) _]
simp only [sub_re, one_re, le_refl]
apply (norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ f hz hd hB).trans (this.trans _)
apply mul_le_mul_of_nonneg _ _ (Real.rpow_nonneg (sSupNormIm_nonneg f _) _)
· apply (Real.rpow_nonneg _ _)
specialize hb 1
simp only [mem_preimage, one_re, mem_singleton_iff, forall_true_left] at hb
exact (norm_nonneg _).trans hb
· apply Real.rpow_le_rpow (sSupNormIm_nonneg f _) _ (sub_nonneg.mpr hz.2)
· rw [sSupNormIm]
apply csSup_le _
· simpa [comp_apply, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] using ha
· use ‖(f 0)‖, 0
simp only [mem_preimage, zero_re, mem_singleton_iff, comp_apply, and_self]
· apply Real.rpow_le_rpow (sSupNormIm_nonneg f _) _ hz.1
· rw [sSupNormIm]
apply csSup_le _
· simpa [comp_apply, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] using hb
· use ‖(f 1)‖, 1
simp only [mem_preimage, one_re, mem_singleton_iff, comp_apply, and_self]
