OAI/Geometry/RCD/Coordinates/HalfRestrictedMean.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Testing a half-restricted plan detects the absolute mean error

Adding half the original plan keeps the subplan mass at least one half. Its normalization therefore increases compression by at most a factor two.

  1. def OAI.RegularPointCoordinates.halfRestrictedMeasure line 17
  2. theorem OAI.RegularPointCoordinates.halfRestrictedMeasure_le line 20
  3. theorem OAI.RegularPointCoordinates.halfRestrictedMeasure_mass_lower line 33
  4. theorem OAI.RegularPointCoordinates.halfRestrictedMeasure_mass_ne_zero line 39
  5. theorem OAI.RegularPointCoordinates.submeasure_integral_tendsto_zero line 43
  6. theorem OAI.RegularPointCoordinates.halfRestrictedMeasure_abs_integral line 62
  7. theorem OAI.RegularPointCoordinates.integral_abs_tendsto_of_halfRestrictedMeans line 90