Theorems · Theorem · global analysis

mfderiv_prod_eq_add_comp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M × M' → M''} {p : M × M'},
  MDiffAt f p →
    mfderiv% f p =
      (mfderiv% fun z => f (z, p.2)) p.1 ∘SL id (ContinuousLinearMap.fst 𝕜 E E') +
        (mfderiv% fun z => f (p.1, z)) p.2 ∘SL id (ContinuousLinearMap.snd 𝕜 E E')

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.

Defined in

Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace