English
The map interpStrip f is DiffContOnCl on the open vertical strip, i.e., differentiable with continuous linearization there.
Русский
Функция interpStrip f дифференцируема с непрерывной линейной аппроксимацией на открытой вертикальной полосе.
LaTeX
$$$\\text{DiffContOnCl }\\mathbb{C}\\; (\\interpStrip\\, f)\\; (\\text{verticalStrip } 0 1).$$$
Lean4
theorem diffContOnCl_interpStrip : DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1) :=
by
by_cases h :
sSupNormIm f 0 = 0 ∨
sSupNormIm f 1 =
0
-- Case everywhere 0
· eta_expand; simp_rw [interpStrip_eq_of_zero f _ h]; exact diffContOnCl_const
· push_neg at h
rcases h with ⟨h0, h1⟩
rw [ne_comm] at h0 h1
apply Differentiable.diffContOnCl
intro z
eta_expand
simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
(lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]
refine DifferentiableAt.mul ?_ ?_
· apply DifferentiableAt.const_cpow (DifferentiableAt.const_sub differentiableAt_id 1) _
left; simp only [Ne, ofReal_eq_zero]; rwa [eq_comm]
· refine DifferentiableAt.const_cpow ?_ ?_
· apply differentiableAt_id
· left; simp only [Ne, ofReal_eq_zero]; rwa [eq_comm]
