English
interpStrip z equals (sSupNormIm f 0)^{1−z}(sSupNormIm f 1)^z when both edges are nonzero; otherwise it is 0.
Русский
interpStrip z равно (sSupNormIm f 0)^{1−z}(sSupNormIm f 1)^z, если обе границы ненулевые; иначе 0.
LaTeX
$$$\mathrm{interpStrip}(f,z) = \begin{cases}0, & sSupNormIm f 0 = 0 \lor sSupNormIm f 1 = 0,\\ (sSupNormIm f 0)^{1-z} (sSupNormIm f 1)^{z}, & \text{иначе}.\end{cases}$$$
Lean4
/-- The interpolation of `sSupNormIm` on the two boundaries.
In other words, this is the right side of the target inequality:
`|f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|`.
Note that if `sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0` then the power is not continuous
since `0 ^ 0 = 1`. Hence the use of `ite`. -/
noncomputable def interpStrip (z : ℂ) : ℂ :=
if sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0 then 0 else sSupNormIm f 0 ^ (1 - z) * sSupNormIm f 1 ^ z
