English
invInterpStrip f z ε is defined by a two-case rule: either 0 if an edge is zero, otherwise (ε + sSupNormIm f 0)^(z-1) (ε + sSupNormIm f 1)^(-z).
Русский
invInterpStrip f z ε задана по правилу прямого переноса: 0, если одна из крайних величин равна нулю; иначе (ε + sSupNormIm f 0)^(z-1) (ε + sSupNormIm f 1)^(-z).
LaTeX
$$$\mathrm{invInterpStrip}(f,z,\varepsilon)=\begin{cases}0,& sSupNormIm f 0 =0 \lor sSupNormIm f 1 =0,\\[2mm] (\varepsilon + sSupNormIm f 0)^{z-1}(\varepsilon + sSupNormIm f 1)^{-z},& \neg (sSupNormIm f 0 =0 \lor sSupNormIm f 1 =0).\end{cases}$$$
Lean4
/-- The inverse of the interpolation of `sSupNormIm` on the two boundaries.
In other words, this is the inverse of the right side of the target inequality:
`|f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|`.
Shifting this by a positive epsilon allows us to prove the case when either of the boundaries
is zero. -/
noncomputable def invInterpStrip (ε : ℝ) : ℂ :=
(ε + sSupNormIm f 0) ^ (z - 1) * (ε + sSupNormIm f 1) ^ (-z)
