OAI/Geometry/EinsteinFour/FourHeatGaussianApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gaussian dilation and its actual approximate-identity limit.

  1. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_dilate line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_rescaled_measurable line 27
  3. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_rescaled_bound line 37
  4. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_rescaled_pointwise line 43
  5. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_rescaled_limit line 54
  6. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_integral_dilate line 70
  7. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_approximate_identity line 98