OAI/Geometry/EinsteinFour/FourHeatGaussian.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The normalized Euclidean four-dimensional Gaussian used in the local heat construction. All integrals use the actual Euclidean volume measure.

  1. def OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian line 15
  2. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_pos line 18
  3. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_continuous line 23
  4. theorem OAI.PositiveEinsteinFour.Geometry.fourGaussian_integrable line 27
  5. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_integrable line 38
  6. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_mass line 41