OAI/Geometry/EinsteinFour/HeatKernels06.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Change of variables for a compact amplitude in an actual normal chart. The normalization factor of the manifold measure remains explicit.

  1. theorem OAI.PositiveEinsteinFour.Geometry.heatNormalScalarLift_integral_chart line 23