OAI/Geometry/RCD/Sobolev/SmoothTimeTestOrder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth nonnegative time tests control interior interval integrals

Only scalar bumps with one inner and one outer radius are needed. Their outer radii decrease to the prescribed closed interval.

  1. theorem OAI.RegularPointCoordinates.integral_closedBall_nonneg_of_smooth_tests line 20