OAI/Geometry/EinsteinFour/ScalarBoundedPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous test pairings for bounded representatives of local heat output.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalarBoundedTest_integrable line 17
  2. def OAI.PositiveEinsteinFour.Geometry.scalarBoundedTestPairing line 22
  3. theorem OAI.PositiveEinsteinFour.Geometry.scalarBoundedTestPairing_apply line 43
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_eq_bounded_of_tests line 46