OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/AutomaticCalibrationNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The very same rational scale used by the search gives the rational near-unit lengths supplied to the contact-coordinate program.

  1. def OAI.ContinuumCoulomb.AutomaticCalibration.spacing line 12
  2. def OAI.ContinuumCoulomb.AutomaticCalibration.normalizedValue line 14
  3. theorem OAI.ContinuumCoulomb.AutomaticCalibration.spacing_positive line 17
  4. theorem OAI.ContinuumCoulomb.AutomaticCalibration.normalizedValue_mem line 24
  5. opaque OAI.ContinuumCoulomb.AutomaticCalibration.spacingProgram line 37
  6. opaque OAI.ContinuumCoulomb.AutomaticCalibration.normalizedProgram line 40
  7. def OAI.ContinuumCoulomb.AutomaticCalibration.normalizedCertificate line 46