OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryThreeLocal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual circuit-history Hamiltonian is sent to an explicitly specified rational three-local even-Y family. Sampling and the two subdivision stages each have their own inverse-precision error bound.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.historySites line 14
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.historySites_nodup line 18
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.historySites_length line 22
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.historySites_cover line 26
  5. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicHistory.ThreeLocalTerm line 36
  6. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicHistory.ThreeLocalQubit line 39
  7. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocalWord line 42
  8. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocalSites line 47
  9. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocalCoefficient line 51
  10. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocalEnergy line 56
  11. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.sampledHistoryEnergy line 60
  12. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocal_support line 64
  13. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.threeLocal_even line 69