English
The total derivative of a map into a product is the sum of the partial derivatives along each coordinate, yielding a coprod-like decomposition.
Русский
Полная производная отображения в произведение пространства равна сумме частичных производных по каждой координате.
LaTeX
$$$mfderiv (I.prod I') (f,g) = (mfderiv I I' f) ∘ (fst) + (mfderiv I' I'' g) ∘ (snd)$$$
Lean4
/-- The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
`TangentSpace`. -/
theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'} (hf : MDifferentiableAt (I.prod I') I'' f p) :
mfderiv (I.prod I') I'' f p =
mfderiv (I.prod I') I'' (fun z : M × M' => f (z.1, p.2)) p +
mfderiv (I.prod I') I'' (fun z : M × M' => f (p.1, z.2)) p :=
by
erw [mfderiv_comp_of_eq hf (mdifferentiableAt_fst.prodMk mdifferentiableAt_const) rfl,
mfderiv_comp_of_eq hf (mdifferentiableAt_const.prodMk mdifferentiableAt_snd) rfl, ← ContinuousLinearMap.comp_add,
mdifferentiableAt_fst.mfderiv_prod mdifferentiableAt_const,
mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_snd, mfderiv_fst, mfderiv_snd, mfderiv_const, mfderiv_const]
symm
convert ContinuousLinearMap.comp_id <| mfderiv (.prod I I') I'' f (p.1, p.2)
exact ContinuousLinearMap.coprod_inl_inr
