OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPrivateTerms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Explicit private mediator terms; no support-selection oracle is needed.

  1. def OAI.ContinuumCoulomb.QuantumPrivate.left line 14
  2. def OAI.ContinuumCoulomb.QuantumPrivate.right line 20
  3. theorem OAI.ContinuumCoulomb.QuantumPrivate.factor line 25
  4. theorem OAI.ContinuumCoulomb.QuantumPrivate.disjoint line 34
  5. def OAI.ContinuumCoulomb.QuantumPrivate.old line 45
  6. def OAI.ContinuumCoulomb.QuantumPrivate.fresh line 46
  7. theorem OAI.ContinuumCoulomb.QuantumPrivate.old_ne_fresh line 48
  8. def OAI.ContinuumCoulomb.QuantumPrivate.term line 53
  9. theorem OAI.ContinuumCoulomb.QuantumPrivate.term_word line 64
  10. def OAI.ContinuumCoulomb.QuantumPrivate.weight line 73
  11. theorem OAI.ContinuumCoulomb.QuantumPrivate.weight_cast line 75
  12. def OAI.ContinuumCoulomb.QuantumPrivate.budget line 79
  13. def OAI.ContinuumCoulomb.QuantumPrivate.scale line 80
  14. theorem OAI.ContinuumCoulomb.QuantumPrivate.budget_cast line 82
  15. theorem OAI.ContinuumCoulomb.QuantumPrivate.scale_cast line 86