OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDistributedGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The distributed history bounds transported to the actual tensor-qubit basis.

  1. theorem OAI.ContinuumCoulomb.qmaDistributedQubit_lower line 12
  2. theorem OAI.ContinuumCoulomb.qmaDistributedQubit_accepting line 34