OAI/Geometry/RCD/Metric/ScaledCompactPotentialMeasurable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Measurability of actual heat potentials on interior time cylinders

Clipping at a positive time margin gives a globally defined measurable function and agrees with the original potential throughout the cylinder.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_potential_continuous_time line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_potential_continuous_space line 42
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_potential_measurable line 50