OAI/Geometry/EinsteinFour/WeylEstimates07.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual smooth closed and coclosed two-forms. Their inclusion in the finite weak Hodge kernel proves finite-dimensionality without an index input.

  1. def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormExterior line 22
  2. def OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCodifferential line 38
  3. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicTwoForms line 52
  4. theorem OAI.PositiveEinsteinFour.Geometry.mem_smoothHarmonicTwoForms line 55
  5. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicTwoForm_energy_zero line 64
  6. def OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToWeak line 76
  7. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicToWeak_injective line 87
  8. theorem OAI.PositiveEinsteinFour.Geometry.smoothHarmonicTwoForms_finite line 97
  9. def OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian line 121
  10. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_sub line 124
  11. theorem OAI.PositiveEinsteinFour.Geometry.twoFormHodgeForm_smooth_pairing line 129
  12. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_pairing line 146
  13. theorem OAI.PositiveEinsteinFour.Geometry.smoothHodgeLaplacian_selfAdjoint line 157