OAI/Geometry/EinsteinFour/ScalarAdjointTests.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Test pairing for the adjoint operator arising from the actual density-weighted chart equation.

  1. def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzDirectOperator line 21
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarFormalAdjointOperator_pairing line 27
  3. theorem OAI.PositiveEinsteinFour.Geometry.scalarFormalAdjointOperator_remainder line 38