OAI/Analysis/Mahler/ExteriorDirectional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.extDeriv_directional line 14

   Source documentation

   The actual exterior derivative is the sum of coordinate one-forms wedged with directional derivatives. No Leibniz rule is assumed.

   theorem extDeriv_directional [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] [FiniteDimensional ℝ E] (basis : Module.Basis J ℝ E) {n : ℕ}
       {A : E → E [⋀^Fin n]→L[ℝ] ℂ} {x : E} (hA : DifferentiableAt ℝ A x) :
       (extDeriv A x).toAlternatingMap =
         ∑ j : J, (wedge (covectorVolume (fun _ : Fin 1 => complexCoord basis j))
           (fderiv ℝ A x (basis j)).toAlternatingMap).domDomCongr (prependFinEquiv n) := by
   …

   Mentions: OAI.Mahler.wedge, OAI.Mahler.covectorVolume, OAI.Mahler.complexCoord, OAI.Mahler.prependFinEquiv