OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialPortBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coefficient and edge-count bounds for the actual port schedule tape.

  1. theorem OAI.ContinuumCoulomb.QuantumPackedSchedule.state_coefficientBound line 13
  2. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.initial_count line 36
  3. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.initial_coefficientBound line 44
  4. theorem OAI.ContinuumCoulomb.QuantumSpatialPortProgram.value_bounds line 57