∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) {ε : ℝ},
  ε > 0 →
    ‖Complex.HadamardThreeLines.invInterpStrip f z ε‖ =
      (ε + Complex.HadamardThreeLines.sSupNormIm f 0) ^ (z.re - 1) *
        (ε + Complex.HadamardThreeLines.sSupNormIm f 1) ^ (-z.re)