OAI/Geometry/RCD/Sobolev/MedianLevel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A median level for the local Poincare argument

Only the two half-mass inequalities are needed. The level is the lower endpoint at which the cumulative distribution reaches one half.

  1. theorem OAI.RegularPointCoordinates.exists_probability_median line 17