OAI/Geometry/RCD/Sobolev/ContinuousDifferenceSpace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The complete space of continuous differences

A continuous function modulo additive constants is represented by its pairwise differences. The inherited supremum norm is exactly the oscillation norm needed for positive kernel contraction.

  1. def OAI.RegularPointCoordinates.continuousDifferenceSubmodule line 18
  2. instance OAI.RegularPointCoordinates.continuousDifferenceSubmodule_closed line 31
  3. abbrev OAI.RegularPointCoordinates.ContinuousDifference line 38
  4. def OAI.RegularPointCoordinates.continuousDifference line 40
  5. def OAI.RegularPointCoordinates.differenceValue line 45
  6. theorem OAI.RegularPointCoordinates.differenceValue_apply line 48
  7. theorem OAI.RegularPointCoordinates.continuousDifference_diagonal line 51
  8. theorem OAI.RegularPointCoordinates.differenceValue_sub line 55
  9. theorem OAI.RegularPointCoordinates.continuousDifference_value line 61
  10. theorem OAI.RegularPointCoordinates.ContinuousDifference.norm_le line 68