English
Define interpStrip'(f,l,u,z) as 0 if sSupNormIm f l = 0 or sSupNormIm f u = 0, otherwise sSupNormIm f l^{1 − ((z − l)/(u − l))} · sSupNormIm f u^{((z − l)/(u − l))}. This generalizes interpStrip to a general strip [l,u].
Русский
Определим interpStrip'(f,l,u,z) как 0, если sSupNormIm f l = 0 или sSupNormIm f u = 0, иначе sSupNormIm f l^{1 − ((z − l)/(u − l))} · sSupNormIm f u^{((z − l)/(u − l))}. Это обобщение interpStrip на общий прямоугольник [l,u].
LaTeX
$$$\\displaystyle \\interpStrip'\\,f\\,l\\,u\\,z = \\begin{cases}0, & sSupNormIm f l = 0 \\lor sSupNormIm f u = 0, \\\\ sSupNormIm f l^{\,1 - \\frac{z-l}{u-l}} \\cdot sSupNormIm f u^{\,\\frac{z-l}{u-l}}, & \\text{else}.\\end{cases}$$$
Lean4
/-- The correct generalization of `interpStrip` to produce bounds in the general case. -/
noncomputable def interpStrip' (f : ℂ → E) (l u : ℝ) (z : ℂ) : ℂ :=
if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
else sSupNormIm f l ^ (1 - ((z - l) / (u - l))) * sSupNormIm f u ^ ((z - l) / (u - l))
