English
A derivative equality for the composition with projection on Icc, matching the derivative of f at w.
Русский
Равенство производной для композиции с проекцией на Icc по отношению к производной f в w.
LaTeX
$$$mfderivWithin 𝓘(ℝ) I (f \circ (Set.projIcc x y h.out.le)) (Icc x y) w 1 = mfderiv (𝓡∂ 1) I f w 1$$$
Lean4
theorem mfderivWithin_comp_projIcc_one {f : Icc x y → M} {w : Icc x y} :
mfderivWithin 𝓘(ℝ) I (f ∘ (projIcc x y h.out.le)) (Icc x y) w 1 = mfderiv (𝓡∂ 1) I f w 1 :=
by
by_cases hw : MDifferentiableAt (𝓡∂ 1) I f w; swap
· rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]
· rfl
· rwa [mdifferentiableWithinAt_comp_projIcc_iff]
rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]; rotate_left
· simp [hw]
· exact (contMDiffOn_projIcc _ w.2).mdifferentiableWithinAt le_rfl
· exact (uniqueDiffOn_Icc h.out _ w.2).uniqueMDiffWithinAt
simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']
have : w = projIcc x y h.out.le (w : ℝ) := by rw [projIcc_of_mem]
rw [projIcc_of_mem _ w.2]
congr 1
convert mfderivWithin_projIcc_one w.2
