English
For z in the open vertical strip, interpStrip f z equals (sSupNormIm f 0)^(1−z) · (sSupNormIm f 1)^z.
Русский
Для z из открытого вертикального полосы выполняется равенство interpStrip f z = (sSupNormIm f 0)^(1−z) · (sSupNormIm f 1)^z.
LaTeX
$$$\\displaystyle \\text{If } z \\in \\text{verticalStrip } 0 1,\\; \\interpStrip f z = sSupNormIm f 0^{\\,1 - z} \\cdot sSupNormIm f 1^{\\,z}.$$$
Lean4
/-- Rewrite for `InterpStrip` on the open vertical strip. -/
theorem interpStrip_eq_of_mem_verticalStrip (z : ℂ) (hz : z ∈ verticalStrip 0 1) :
interpStrip f z = sSupNormIm f 0 ^ (1 - z) * sSupNormIm f 1 ^ z :=
by
by_cases h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
· rw [interpStrip_eq_of_zero _ z h]
rcases h with h0 | h1
· simp only [h0, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ne_eq, true_and, ofReal_eq_zero]
left
rw [sub_eq_zero, eq_comm]
simp only [Complex.ext_iff, one_re, ne_of_lt hz.2, false_and, not_false_eq_true]
· simp only [h1, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq, true_and]
right
rw [eq_comm]
simp only [Complex.ext_iff, zero_re, ne_of_lt hz.1, false_and, not_false_eq_true]
· push_neg at h
replace h : (0 < sSupNormIm f 0) ∧ (0 < sSupNormIm f 1) :=
⟨(lt_of_le_of_ne (sSupNormIm_nonneg f 0) (ne_comm.mp h.1)),
(lt_of_le_of_ne (sSupNormIm_nonneg f 1) (ne_comm.mp h.2))⟩
exact interpStrip_eq_of_pos f z h.1 h.2
