OAI/Geometry/RCD/Sobolev/CompactBadAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite Vitali estimate for points with a large ball average

This is the covering step of De Philippis--Gigli (2018), Proposition 3.2, Step 2.1. The containing region and the radius cutoff remain explicit.

  1. theorem OAI.RegularPointCoordinates.compact_bad_average line 18