English
If f is bounded on the unit vertical strip, then ||f(z)|| ≤ sSupNormIm f (z.re) for z in the strip.
Русский
Если f ограничена на единичной вертикальной полосе, то ||f(z)|| ≤ sSupNormIm f (Re z) для z внутри полосы.
LaTeX
$$$\|f(z)\| \leq \mathrm{sSupNormIm}(f, z_{\mathrm{re}})$ for appropriate z within the verticalClosedStrip, i.e., when $z \in \mathrm{verticalClosedStrip}(0,1)$.$$
Lean4
/-- The function `invInterpStrip` is `diffContOnCl`. -/
theorem diffContOnCl_invInterpStrip {ε : ℝ} (hε : ε > 0) :
DiffContOnCl ℂ (fun z ↦ invInterpStrip f z ε) (verticalStrip 0 1) :=
by
apply Differentiable.diffContOnCl
apply Differentiable.mul
· apply Differentiable.const_cpow (Differentiable.sub_const differentiable_id 1) _
left
rw [← ofReal_add, ofReal_ne_zero]
simp only [ne_eq, ne_of_gt (sSupNormIm_eps_pos f hε 0), not_false_eq_true]
· apply Differentiable.const_cpow (Differentiable.neg differentiable_id)
apply Or.inl
rw [← ofReal_add, ofReal_ne_zero]
exact (ne_of_gt (sSupNormIm_eps_pos f hε 1))
