OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceCalibratedGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal rounded source, rather than an arbitrary bounded graph, admits one common polynomial calibration scale and polynomial coordinate extent. The scale exponent may also meet any fixed analytic lower bound.

  1. def OAI.ContinuumCoulomb.SourceMetadataProgram.calibrationSize line 15
  2. abbrev OAI.ContinuumCoulomb.SourceMetadataProgram.geometricWeight line 18
  3. abbrev OAI.ContinuumCoulomb.SourceMetadataProgram.geometricGraph line 22
  4. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.exists_source_calibration line 26