OAI/Analysis/Mahler/SourceFullExterior.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.sourceComplexBoundaryForm line 13
2. lemma OAI.Mahler.contDiffAt_dcLinear_source line 17
3. lemma OAI.Mahler.sourceComplexBoundaryForm_raw line 22
4. theorem OAI.Mahler.extDeriv_sourceComplexBoundaryForm line 35

   Source documentation

   The exterior derivative identity in every degree. C3 of the potential supplies all product rules and the symmetric second jet of dc; neither closedness nor a Stokes identity is assumed.

   theorem extDeriv_sourceComplexBoundaryForm {u : E → ℂ} {x : E}
       (hu : ContDiffAt ℝ 3 u x) (k : ℕ) :
       (extDeriv (sourceComplexBoundaryForm u k) x).toAlternatingMap =
         (wedgePower (extDeriv (oneForm (dcLinear u)) x).toAlternatingMap (k+1)).domDomCongr
           (sourceTopSlots k) := by
   …

   Mentions: OAI.Mahler.sourceComplexBoundaryForm, OAI.Mahler.wedgePower, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.sourceTopSlots