OAI/Geometry/RCD/Heat/ScaledHeatActionLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous action limits with convergence at every interior time

  1. structure OAI.RegularPointCoordinates.HeatActionLimit line 13
  2. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatConverges line 27
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatConverges.subsequence line 35
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_action_limit line 45