OAI/Geometry/EinsteinFour/HodgeTheory06.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Actual chart integral formulas for the L2 and covariant energy pairings against a compactly supported orthonormal-frame test.

  1. theorem OAI.PositiveEinsteinFour.Geometry.twoFormLocalNabla_zero_off line 24
  2. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTest_support line 34
  3. theorem OAI.PositiveEinsteinFour.Geometry.twoFormGramTest_pairing line 41
  4. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormL2Inner_gramTest line 81
  5. theorem OAI.PositiveEinsteinFour.Geometry.smoothTwoFormCovariantEnergy_gramTest line 116
  6. def OAI.PositiveEinsteinFour.Geometry.twoFormValueNorm line 166
  7. def OAI.PositiveEinsteinFour.Geometry.twoFormEnergyRoot line 169
  8. def OAI.PositiveEinsteinFour.Geometry.twoFormControl line 173
  9. theorem OAI.PositiveEinsteinFour.Geometry.twoFormControl_nonneg line 176
  10. def OAI.PositiveEinsteinFour.Geometry.twoFormValueNormL2 line 180
  11. def OAI.PositiveEinsteinFour.Geometry.twoFormEnergyRootL2 line 183
  12. def OAI.PositiveEinsteinFour.Geometry.twoFormControlL2 line 186
  13. theorem OAI.PositiveEinsteinFour.Geometry.twoFormValueNormL2_coe line 189
  14. theorem OAI.PositiveEinsteinFour.Geometry.twoFormValueNormL2_norm_sq line 193
  15. theorem OAI.PositiveEinsteinFour.Geometry.twoFormEnergyRootL2_norm_sq line 204
  16. theorem OAI.PositiveEinsteinFour.Geometry.twoFormControlL2_norm_le line 216
  17. theorem OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureField_bound line 258
  18. def OAI.PositiveEinsteinFour.Geometry.smoothL2CurvatureLinear line 269
  19. theorem OAI.PositiveEinsteinFour.Geometry.twoFormValueNormL2_eq_L2norm line 280
  20. theorem OAI.PositiveEinsteinFour.Geometry.smoothL2CurvatureLinear_bound line 289
  21. def OAI.PositiveEinsteinFour.Geometry.twoFormCurvatureBound line 307
  22. theorem OAI.PositiveEinsteinFour.Geometry.smoothL2CurvatureLinear_norm_le line 310
  23. def OAI.PositiveEinsteinFour.Geometry.smoothL2Curvature line 314
  24. def OAI.PositiveEinsteinFour.Geometry.twoFormL2Curvature line 318
  25. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Curvature_smooth line 321
  26. def OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockPotential line 327

    Source documentation

    The bounded potential in 1 + ∇*∇ = 2 R - 5 for harmonic two-forms when Ricci is normalized to 3g.

    def twoFormWeitzenbockPotential : TwoFormL2 o →L[ℝ] TwoFormL2 o :=
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.TwoFormL2

  27. theorem OAI.PositiveEinsteinFour.Geometry.twoForm_chart_localization_bound line 354
  28. theorem OAI.PositiveEinsteinFour.Geometry.twoFormMetricCurvatureAction_symmetric line 417
  29. theorem OAI.PositiveEinsteinFour.Geometry.smoothL2Curvature_inner line 432
  30. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Curvature_selfAdjoint line 442
  31. theorem OAI.PositiveEinsteinFour.Geometry.smoothL2Curvature_hodge line 483
  32. theorem OAI.PositiveEinsteinFour.Geometry.twoFormL2Curvature_hodge line 489
  33. theorem OAI.PositiveEinsteinFour.Geometry.twoFormWeitzenbockPotential_hodge line 500