OAI/Geometry/RCD/Heat/RiccatiInitialBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The initial bound from a finite positive-time Riccati inequality

The derivative is needed only at positive times. Continuity handles the initial value, and no value or regularity is assumed at the final endpoint.

  1. theorem OAI.RegularPointCoordinates.riccati_initial_bound line 15