OAI/Geometry/RCD/Heat/LipschitzTimePairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual time derivatives of Lipschitz compact pairings

Compact spatial pairings of a Lipschitz cylinder are Lipschitz in time. Their absolutely continuous representatives admit integration by parts.

  1. theorem OAI.RegularPointCoordinates.compact_cylinder_pairing_lipschitz line 17
  2. theorem OAI.RegularPointCoordinates.compact_set_pairing_lipschitz line 48
  3. theorem OAI.RegularPointCoordinates.lipschitz_time_pairing_integration_by_parts line 74