Theorems · Theorem · real analysis

hasStrictFDerivAt_uncurry_coprod

∀ {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₂]
  [inst_4 : NormedSpace 𝕜 E₂] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [IsRCLikeNormedField 𝕜]
  {u : E₁ × E₂} {f : E₁ → E₂ → F} {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F},
  (∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (↿f₁ v) v.1) →
    (∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (↿f₂ v) v.2) →
      ContinuousAt (↿f₁) u → 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.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Partial

Cited by

5 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceIsRCLikeNormedField