English
If f and g both have MF-derivatives within at corresponding sets, then their sum has MF-derivative within at with the sum of the derivatives.
Русский
Если у функции f и g есть производные по MF внутри на множестве, то их сумма имеет производную MF внутри со суммой производных.
LaTeX
$$$\text{HasMFDerivWithinAt } I\ 𝓘(\mathbb{K},E')\ f z f' \land \text{HasMFDerivWithinAt } I\ 𝓘(\mathbb{K},E')\ g z g' \Rightarrow \text{HasMFDerivWithinAt } I\ 𝓘(\mathbb{K},E')\ (f+g) z (f'+g')$$$
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`. Version in terms of the one-variable derivatives. -/
theorem mfderiv_prod_eq_add_comp {f : M × M' → M''} {p : M × M'} (hf : MDifferentiableAt (I.prod I') I'' f p) :
mfderiv (I.prod I') I'' f p =
(mfderiv I I'' (fun z : M => f (z, p.2)) p.1) ∘L
(id (ContinuousLinearMap.fst 𝕜 E E') : (TangentSpace (I.prod I') p) →L[𝕜] (TangentSpace I p.1)) +
(mfderiv I' I'' (fun z : M' => f (p.1, z)) p.2) ∘L
(id (ContinuousLinearMap.snd 𝕜 E E') : (TangentSpace (I.prod I') p) →L[𝕜] (TangentSpace I' p.2)) :=
by
rw [mfderiv_prod_eq_add hf]
congr
· have : (fun z : M × M' => f (z.1, p.2)) = (fun z : M => f (z, p.2)) ∘ Prod.fst := rfl
rw [this, mfderiv_comp (I' := I)]
· simp only [mfderiv_fst, id_eq]
rfl
· exact hf.comp _ (mdifferentiableAt_id.prodMk mdifferentiableAt_const)
· exact mdifferentiableAt_fst
· have : (fun z : M × M' => f (p.1, z.2)) = (fun z : M' => f (p.1, z)) ∘ Prod.snd := rfl
rw [this, mfderiv_comp (I' := I')]
· simp only [mfderiv_snd, id_eq]
rfl
· exact hf.comp _ (mdifferentiableAt_const.prodMk mdifferentiableAt_id)
· exact mdifferentiableAt_snd
