OAI/Geometry/RCD/Heat/HeatExhaustionScales.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A fixed exhaustion of space and strictly positive heat times

  1. def OAI.RegularPointCoordinates.heatCompactRadius line 10
  2. def OAI.RegularPointCoordinates.heatCompactTimeMargin line 11
  3. theorem OAI.RegularPointCoordinates.heatCompactRadius_nonneg line 13
  4. theorem OAI.RegularPointCoordinates.heatCompactTimeMargin_pos line 17
  5. theorem OAI.RegularPointCoordinates.heatCompactTimeMargin_le_one line 21
  6. theorem OAI.RegularPointCoordinates.heat_exhaustion_contains line 27