OAI/Analysis/Mahler/ExteriorCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.continuousReindex line 12
2. lemma OAI.Mahler.continuousReindex_apply line 24
3. lemma OAI.Mahler.continuousReindex_toAlternatingMap line 28
4. lemma OAI.Mahler.continuous_basis_expansion line 32
5. lemma OAI.Mahler.extDeriv_sum line 44
6. theorem OAI.Mahler.extDeriv_basis_expansion line 61

   Source documentation

   Exact coordinate expression for exterior differentiation; the factorial is the one forced by the actual unnormalized shuffle product.

   theorem extDeriv_basis_expansion (basis : Module.Basis J ℝ E) {n : ℕ}
       {A : E → E [⋀^Fin n]→L[ℝ] ℂ} {x : E} (hA : DifferentiableAt ℝ A x) :
       (extDeriv A x).toAlternatingMap =
         ∑ q : Fin n → J,
           (wedge (covectorVolume (fun _ : Fin 1 =>
             (fderiv ℝ (fun y => A y (basis ∘ q) / (n.factorial : ℂ)) x).toLinearMap))
             (covectorVolume (complexCoord basis ∘ q))).domDomCongr (prependFinEquiv n) := by
   …

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