OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGeometryPowers.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

One uniform power bounds all finite geometric inputs of the actual history-to-lattice coefficient program.

  1. def OAI.ContinuumCoulomb.QuantumHistorySpatial.geometryEnvelope line 14
  2. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.geometryEnvelope_parts line 18
  3. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.geometryEnvelope_power line 26
  4. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.crossing_card_bound line 39
  5. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.model_geometry_power line 48
  6. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.outputCoefficientNat_one line 81
  7. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.outputCoefficientNat_of_power line 88
  8. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.latticeBound_of_power line 95