OAI/Analysis/Mahler/BoundaryJet.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.dcOperator line 14

   Source documentation

   The linear operation taking a real derivative to d^c.

   noncomputable def dcOperator : (E →L[ℝ] ℂ) →L[ℝ] (E →L[ℝ] ℂ) :=
   …

2. def OAI.Mahler.dcOneOperator line 17
3. lemma OAI.Mahler.dcOneOperator_fderiv line 21
4. def OAI.Mahler.ddcTwoJet line 25

   Source documentation

   The second derivative determines the actual exterior derivative of d^c.

   noncomputable def ddcTwoJet (B : E →L[ℝ] (E →L[ℝ] ℂ)) :
       E [⋀^Fin 2]→L[ℝ] ℂ :=
   …

5. theorem OAI.Mahler.extDeriv_dc_eq_twoJet line 29
6. lemma OAI.Mahler.continuous_dcOneOperator line 37
7. lemma OAI.Mahler.continuous_ddcTwoJet line 40
8. lemma OAI.Mahler.continuous_wedge_eval line 46
9. lemma OAI.Mahler.continuous_wedgePower_eval line 62
10. abbrev OAI.Mahler.RealComplexTwoJet line 70
11. def OAI.Mahler.boundaryJet line 73
12. lemma OAI.Mahler.continuous_boundaryJet_eval line 78
13. theorem OAI.Mahler.boundaryForm_eq_jet line 90