OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePhysicalThreshold.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Literal raw-source assembly of the complete physical threshold pair. The same fixed powers determine the calibration amplification, the centered nuclear mesh, and the rational slab dimensions.

  1. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.mesh line 13
  2. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.horizontalRadius line 14
  3. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.verticalRadius line 15
  4. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.slabHorizontal line 16
  5. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.slabVertical line 18
  6. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.horizontal_product line 21
  7. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.vertical_product line 28
  8. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.mesh_positive line 35
  9. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.slabHorizontal_bounds line 39
  10. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.slabVertical_bounds line 47
  11. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.input line 55
  12. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.value line 67
  13. opaque OAI.ContinuumCoulomb.SourcePhysicalThreshold.tauProgram line 71
  14. opaque OAI.ContinuumCoulomb.SourcePhysicalThreshold.inputProgram line 76
  15. opaque OAI.ContinuumCoulomb.SourcePhysicalThreshold.program line 89
  16. def OAI.ContinuumCoulomb.SourcePhysicalThreshold.certificate line 94
  17. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.actual_error line 98
  18. theorem OAI.ContinuumCoulomb.SourcePhysicalThreshold.gap line 113