OAI/Geometry/RCD/Sobolev/CompactScalarPrimitive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two primitives of a compact scalar second derivative

Only continuity and compact support of the prescribed second derivative are needed. Both primitives vanish at zero and have global Lipschitz bounds.

  1. theorem OAI.RegularPointCoordinates.compact_scalar_two_primitives line 18