OAI/Geometry/RCD/Heat/SpaceTimeIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Turning the two-time quadratic bound into a spatial increment rate

  1. theorem OAI.RegularPointCoordinates.spaceTimeSlopeRate_increment line 10