OAI/Geometry/RCD/Sobolev/ContinuousSobolevTestOrder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact Sobolev tests detect the order of continuous functions

Radial Lipschitz cutoffs suffice. Full support turns a positive value into a strictly positive integral against one of these actual tests.

  1. theorem OAI.RegularPointCoordinates.continuous_nonpos_of_sobolev_tests line 20