OAI/Geometry/RCD/Heat/RiccatiFiniteInterval.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite-interval bound for a scalar Riccati inequality

A constant barrier keeps the solution above its threshold. The reciprocal then has uniformly negative derivative, giving a bound before the endpoint.

  1. theorem OAI.RegularPointCoordinates.riccati_finite_interval line 17