English
The derivative equality with projection at a point reduces to the one in mfderivWithin_projIcc_one.
Русский
Эквивалентность производной с проекцией через Icc сводится к соответствующему результату mfderivWithin_projIcc_one.
LaTeX
$$$\text{mdifferentiableWithinAt } (f) (Icc x y) w \Rightarrow \; mfderivWithin 𝓘(ℝ) (𝓡∂ 1) (Set.projIcc x y h.out.le) (Icc x y) w 1 = 1$$$
Lean4
theorem mdifferentiableWithinAt_comp_projIcc_iff {f : Icc x y → M} {w : Icc x y} :
MDifferentiableWithinAt 𝓘(ℝ) I (f ∘ (Set.projIcc x y h.out.le)) (Icc x y) w ↔ MDifferentiableAt (𝓡∂ 1) I f w :=
by
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
· have A := (contMDiff_subtype_coe_Icc (x := x) (y := y) (n := 1) w).mdifferentiableAt le_rfl
rw [← mdifferentiableWithinAt_univ] at A ⊢
convert hf.comp _ A (fun z hz ↦ z.2)
ext z
simp
· have := (contMDiffOn_projIcc (x := x) (y := y) (n := 1) w w.2).mdifferentiableWithinAt le_rfl
exact MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq (w : ℝ) hf this (by simp)
