OAI/Geometry/RCD/Metric/BoundedPositiveMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite measure from a bounded local positive functional

The one-sided bound by the positive part preserves positivity under the Hahn--Banach extension. Riesz--Markov then gives a finite positive measure.

  1. theorem OAI.RegularPointCoordinates.exists_finite_measure_of_positive_bound line 21