OAI/Geometry/RCD/Coordinates/BilinearIntervalAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted quadratic energy of an actual time average

Positivity of the bilinear form gives Jensen's inequality directly on the finite interval used to smooth the Sobolev time family.

  1. theorem OAI.RegularPointCoordinates.positive_bilinear_interval_average line 17