OAI/Geometry/RCD/Heat/ScaledCompactReferenceBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed-reference amplitude bounds for the actual scaled heat potentials

The additive gauge is fixed once at time ε. All interior times use that same gauge, uniformly over the positive endpoint factor.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_reference_bounds line 22