OAI/Geometry/RCD/Coordinates/PositiveBilinearIntegralLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An integrated lower bound for positive quadratic forms

Weak mixed-pairing convergence and a uniform norm bound suffice. Strong convergence of vectors or convergence of pointwise energies is not needed.

  1. theorem OAI.RegularPointCoordinates.positive_bilinear_integral_lower line 18