OAI/Geometry/RCD/Coordinates/SobolevFramePathEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An integrable envelope for the variation of the actual Sobolev coefficients

  1. def OAI.RegularPointCoordinates.framePathEnergy line 15
  2. theorem OAI.RegularPointCoordinates.framePathEnergy_nonneg line 19
  3. theorem OAI.RegularPointCoordinates.compressed_frame_path_energy line 23
  4. theorem OAI.RegularPointCoordinates.sobolev_frame_variation_envelope line 46