OAI/Geometry/RCD/Coordinates/FrameEnergyError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrable quantitative errors for a bounded-gradient probe

  1. def OAI.RegularPointCoordinates.frameEnergyError line 13
  2. theorem OAI.RegularPointCoordinates.frameEnergyError_aestronglyMeasurable line 18
  3. theorem OAI.RegularPointCoordinates.frame_energy_error_sq_integral line 26