OAI/Geometry/RCD/Sobolev/CutoffIntegralLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing local cutoff integral limits to the whole space

  1. theorem OAI.RegularPointCoordinates.integral_cutoff_error_le_tail line 14
  2. theorem OAI.RegularPointCoordinates.exists_integral_limit_of_cutoffs line 40
  3. theorem OAI.RegularPointCoordinates.integral_tendsto_of_cutoffs line 71