OAI/Geometry/RCD/Coordinates/PoissonBilinearMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One positive measure-valued form for the finite Poisson span

Polarization of the actual scalar measures gives the coefficient measures. Locality identifies their quadratic tests with each directional scalar measure. Positivity is then retained on the common interior ball, including the singular part.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_bilinear_energy_measure line 25