OAI/Geometry/RCD/Heat/ScaledCompactSpacetimeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform spacetime amplitude under one fixed additive gauge

The gauge is the factor's value at the fixed center and reference time ε. The bound covers every point and every interior time in a compact cylinder.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_spacetime_bounded line 20