English
For ε>0, z in verticalClosedStrip 0 1, and BddAbove bound on norm f on verticalClosedStrip 0 1, a bound holds: ‖f z‖ ≤ ‖((ε + sSupNormIm f 0)^(1−z) (ε + sSupNormIm f 1)^z)‖.
Русский
Для ε>0, z на вертикальной закрытой полосе 0 1 и ограничение нормы f на вертикальной закрытой полосе 0 1 выполняется неравенство: ‖f(z)‖ ≤ ‖((ε + sSupNormIm f 0)^(1−z) (ε + sSupNormIm f 1)^z)‖.
LaTeX
$$$\\|f(z)\\| \\le \\|\\bigl(\\varepsilon + sSupNormIm f 0\\bigr)^{1 - z} \\cdot \\bigl(\\varepsilon + sSupNormIm f 1\\bigr)^{z}\\|.$$$
Lean4
theorem norm_le_interpStrip_of_mem_verticalClosedStrip_eps (ε : ℝ) (hε : ε > 0) (z : ℂ)
(hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
(hz : z ∈ verticalClosedStrip 0 1) : ‖f z‖ ≤ ‖((ε + sSupNormIm f 0) ^ (1 - z) * (ε + sSupNormIm f 1) ^ z : ℂ)‖ :=
by
simp only [norm_mul, ← ofReal_add, norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _, sub_re, one_re]
rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀, ← Real.rpow_neg_one, ←
Real.rpow_neg_one]
· simp only [← Real.rpow_mul (le_of_lt (sSupNormIm_eps_pos f hε _)), mul_neg, mul_one, neg_sub, mul_assoc]
simpa [F, norm_invInterpStrip _ _ hε, norm_smul, mul_comm] using
norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip f ε hε z hd hB hz
· simp only [Real.rpow_pos_of_pos (sSupNormIm_eps_pos f hε _) z.re]
· simp only [Real.rpow_pos_of_pos (sSupNormIm_eps_pos f hε _) (1 - z.re)]
