OAI/Geometry/RCD/Coordinates/FrameResidualDefect.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact residual energy and its quantitative Gram-error bound

  1. theorem OAI.RegularPointCoordinates.frame_residual_energy_expansion line 15
  2. theorem OAI.RegularPointCoordinates.frame_residual_energy_le line 41