OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPrivateCompiler.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete rational X/Z-to-Heisenberg compiler, without a private-pair input assumption.

  1. theorem OAI.ContinuumCoulomb.QuantumPrivate.rawBudget_packed line 13
  2. theorem OAI.ContinuumCoulomb.QuantumPrivate.rawScale_packed line 17
  3. theorem OAI.ContinuumCoulomb.QuantumPrivate.map_range_eq_ofFn line 21
  4. theorem OAI.ContinuumCoulomb.QuantumPrivate.subdivide_packed line 26
  5. theorem OAI.ContinuumCoulomb.QuantumPrivate.output_packed line 51
  6. theorem OAI.ContinuumCoulomb.QuantumPrivate.compile_accuracy line 56
  7. theorem OAI.ContinuumCoulomb.QuantumPrivate.compile_valid line 62