OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/AutomaticCalibrationParameters.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Input and query bounds for the automatic calibrated-distance program. The unary evaluator range is a fixed polynomial in the source size.

  1. abbrev OAI.ContinuumCoulomb.AutomaticCalibration.Input line 14
  2. def OAI.ContinuumCoulomb.AutomaticCalibration.queryBound line 16
  3. def OAI.ContinuumCoulomb.AutomaticCalibration.environment line 18
  4. def OAI.ContinuumCoulomb.AutomaticCalibration.interval line 21
  5. def OAI.ContinuumCoulomb.AutomaticCalibration.value line 24
  6. theorem OAI.ContinuumCoulomb.AutomaticCalibration.interval_order line 28
  7. theorem OAI.ContinuumCoulomb.AutomaticCalibration.queryBound_coefficients line 35
  8. theorem OAI.ContinuumCoulomb.AutomaticCalibration.interval_query_bound line 41
  9. theorem OAI.ContinuumCoulomb.AutomaticCalibration.value_mem line 65