OAI/Geometry/RCD/Metric/WeightedProbabilityRecovery.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded probability cutoffs preserve every integrable moment

The recovery weights are the existing normalized radial cutoffs. In particular their densities are at most two and converge pointwise to one.

  1. theorem OAI.RegularPointCoordinates.integral_weighted_recovery line 18
  2. theorem OAI.RegularPointCoordinates.weighted_probability_recovery line 45