English
For ε > 0, the map z ↦ invInterpStrip(f,z,ε) is differentiable with continuous extension on the vertical strip Re z ∈ [0,1].
Русский
Для ε > 0 отображение z ↦ invInterpStrip(f,z,ε) является дифференцируемым с непрерывным продолжением на вертикальной полосе Re z ∈ [0,1].
LaTeX
$$$\text{If } \varepsilon > 0,\quad z \mapsto \mathrm{invInterpStrip}(f,z,\varepsilon)\text{ is differentiable on and extends continuously to the vertical strip } \{ z:\Re z \in [0,1]\}$$$
Lean4
/-- Useful rewrite for the absolute value of `invInterpStrip` -/
theorem norm_invInterpStrip {ε : ℝ} (hε : ε > 0) :
‖invInterpStrip f z ε‖ = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) :=
by
simp only [invInterpStrip, norm_mul]
repeat rw [← ofReal_add]
repeat rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]
simp
