OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialFinalEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Full-space error of the complete literal routing program. The sum pays for the actual port, crossing, parity and final subdivision stages.

  1. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.planar_energy line 13
  2. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatial_planar_noLoops line 23
  3. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatial_planar_energy line 33
  4. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatial_routed_energy_error line 40
  5. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.sum_error line 51
  6. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatial_energy_error line 60