BoundedHeatSecondVariation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded heat bridge has the exact Hessian second variation

All spatial representatives, mixed Gram entries, and iterated sources are constructed from the three original bounded L2 data. The spatial test is a positive-time heat regularization. No second-order premise is assumed.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_second_variation line 26