English
Let f: C → E with E a normed additive commutative group. If 0 < sSupNormIm f 0 and 0 < sSupNormIm f 1, then for every z ∈ C, interpStrip f z equals (sSupNormIm f 0)^(1 − z) · (sSupNormIm f 1)^z.
Русский
Пусть f: ℂ → E, где E — нормированная аддитивная коммутативная группа. Если 0 < sSupNormIm f 0 и 0 < sSupNormIm f 1, то для любого z ∈ ℂ верно: interpStrip f z = (sSupNormIm f 0)^(1 − z) · (sSupNormIm f 1)^z.
LaTeX
$$$\\displaystyle \\text{If } f: \\mathbb{C} \\to E,\\; E \\text{ normed additive group, and } 0 < sSupNormIm f 0,\\; 0 < sSupNormIm f 1,\\text{ then } \\\\interpStrip\\,f\\,z = sSupNormIm f 0^{\,1 - z} \\cdot sSupNormIm f 1^{\,z}.$$$
Lean4
/-- Rewrite for `InterpStrip` when `0 < sSupNormIm f 0` and `0 < sSupNormIm f 1`. -/
theorem interpStrip_eq_of_pos (z : ℂ) (h0 : 0 < sSupNormIm f 0) (h1 : 0 < sSupNormIm f 1) :
interpStrip f z = sSupNormIm f 0 ^ (1 - z) * sSupNormIm f 1 ^ z := by
simp only [ne_of_gt h0, ne_of_gt h1, interpStrip, if_false, or_false]
