OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceIndexedGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual indexed source array inherits the exact separation and polynomial norm estimates of its rational contact construction.

  1. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.contactSpacing_positive line 13
  2. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.contactLengths_near_one line 18
  3. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.source_coordinate_bound line 29
  4. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.raw_diameter_bound line 40
  5. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.indexed_norm_bound line 59
  6. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.indexed_separation line 73