OAI/Geometry/RCD/Sobolev/CutoffLevelVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the localized upper-level square

The positive part need not be differentiable at the level. Its squared L² norm has a quadratic remainder, including at that level. This supplies the nonlinear time test used in the heat level-set iteration.

  1. theorem OAI.RegularPointCoordinates.upperLevelPart_square_remainder line 18
  2. theorem OAI.RegularPointCoordinates.cutoff_level_square_remainder line 40
  3. theorem OAI.RegularPointCoordinates.cutoff_level_square_hasFDerivAt line 111