OAI/Geometry/EinsteinFour/FourHeatAwayBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian derivative scale is uniformly O(t) away from the center. This is the bound used for the normal-chart cutoff commutator.

  1. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_weighted_inverse_time line 14
  2. theorem OAI.PositiveEinsteinFour.Geometry.fourHeatGaussian_away_inverse_time line 35