OAI/Analysis/Mahler/ExteriorCoefficient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.extDeriv_scalar_const line 13

   Source documentation

   Exterior differentiation of a scalar coefficient times an arbitrary constant continuous form, in every degree and the actual shuffle convention.

   theorem extDeriv_scalar_const [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] (basis : Module.Basis J ℝ E) {n : ℕ}
       (B : E [⋀^Fin n]→L[ℝ] ℂ) {f : E → ℂ} {x : E}
       (hf : DifferentiableAt ℝ f x) :
       (extDeriv (fun y => f y • B) x).toAlternatingMap =
         (wedge (covectorVolume (fun _ : Fin 1 => (fderiv ℝ f x).toLinearMap))
           B.toAlternatingMap).domDomCongr (prependFinEquiv n) := by
   …

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