OAI/Geometry/RCD/Heat/HeatLocalSmoothing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local L²-to-L∞ smoothing without a heat-kernel hypothesis

The parabolic small-mass bound is normalized using L² contraction. Both signs are tested, so the result applies to arbitrary real L² data.

  1. theorem OAI.RegularPointCoordinates.heat_set_time_L2_bound line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_local_L2_smoothing line 37