OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialSourcePromise.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial promise of the actual emitted lattice packet from the fixed spatial graph, using its uniform coefficient and geometric bounds.

  1. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatial_polynomialPromise line 15