English
Let E_i be normed spaces and consider the map that updates the i-th coordinate of a function x: ι → E_i by replacing it with a new value. The Fréchet derivative at x in direction y is the projection onto the i-th coordinate; i.e., the derivative is the continuous linear map that sends a perturbation to its i-th coordinate.
Русский
Пусть E_i - нормированные пространства и функция обновления x: ι → E_i заменяет i-ю координату на новое значение. Производная по Фрете в направлении y равна проекции на i-ю координату; то есть производная - линейное отображение, отдающее только i-ю координату при векторном возмущении.
LaTeX
$$$\\mathrm{D}(\\mathrm{Function.update}\\, x\\, i) = \\pi_i$, где \\pi_i - проекция на i-ую координату в продукте пространств.$$
Lean4
@[fun_prop]
theorem hasFDerivAt_update (x : ∀ i, E i) {i : ι} (y : E i) :
HasFDerivAt (Function.update x i) (.pi (Pi.single i (.id 𝕜 (E i)))) y :=
by
set l := (ContinuousLinearMap.pi (Pi.single i (.id 𝕜 (E i))))
have update_eq : Function.update x i = (fun _ ↦ x) + l ∘ (· - x i) :=
by
ext t j
dsimp [l, Pi.single, Function.update]
split_ifs with hji
· subst hji
simp
· simp
rw [update_eq]
convert (hasFDerivAt_const _ _).add (l.hasFDerivAt.comp y (hasFDerivAt_sub_const (x i)))
rw [zero_add, ContinuousLinearMap.comp_id]
