Partial derivatives

Results in this file relate the partial derivatives of a bivariate function to its differentiability in the product space.

Main statements

• hasStrictFDerivAt_uncurry_coprod: establishing strict differentiability at a point u in the product space, this requires that both partial derivatives exist in a neighbourhood of u and be continuous at u.

theorem hasStrictFDerivAt_uncurry_coprod {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IsRCLikeNormedField 𝕜] {u : E₁ × E₂} {f : E₁ → E₂ → F} {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F} (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₁) => f x v.2) (↿f₁ v) v.1) (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun (x : E₂) => f v.1 x) (↿f₂ v) v.2) (cf₁ : ContinuousAt (↿f₁) u) (cf₂ : ContinuousAt (↿f₂) u) : HasStrictFDerivAt (↿f) ((↿f₁ u).coprod (↿f₂ u)) u

If bivariate f : E₁ → E₂ → F has partial derivatives f₁ and f₂ in a neighbourhood of u : E₁ × E₂ and if they are continuous there then the uncurried function ↿f is strictly differentiable at u with its derivative mapping z to f₁ u.1 u.2 z.1 + f₂ u.1 u.2 z.2.