OAI/Geometry/RCD/Heat/HeatParabolicSmall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small space-time heat mass gives a local upper bound

Dyadic decay first gives a zero upper-level mass on a fixed later cylinder. Continuity in time includes its final slice in the estimate.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_small_parabolic_mass_bound line 19