OAI/Geometry/RCD/Sobolev/BoundaryTorsionProfile.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A fixed scalar profile for compact interior torsion tests

Only its first two derivatives are used: the profile is zero below one and agrees with the identity above two. No higher-order rate is needed.

  1. def OAI.RegularPointCoordinates.boundaryTorsionProfile line 18
  2. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_smooth line 20
  3. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_zero line 23
  4. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_identity line 26
  5. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_nonneg line 29
  6. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_deriv_zero line 34
  7. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_deriv_one line 42
  8. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_second_zero line 50
  9. theorem OAI.RegularPointCoordinates.boundaryTorsionProfile_two_derivative_bounds line 64