OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedIncidence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Uniform incidence bounds for the actual ordered local reductions. Every new site belongs to one input term, while old sites remain in that term's stored support. The bound counts zero-coefficient terms as well.

  1. def OAI.ContinuumCoulomb.QuantumOrderedIncidence.count line 16
  2. def OAI.ContinuumCoulomb.QuantumOrderedIncidence.Bounded line 19
  3. def OAI.ContinuumCoulomb.QuantumOrderedIncidence.Origin line 21
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.extension_bound line 24
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.append_origin line 65
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.subdivision_origin line 79
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.subdivision_bound line 91
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.yy_origin line 97
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.yy_bound line 108
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.third_origin line 114
  11. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.third_bound line 139
  12. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.xz_bound line 145
  13. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.private_bound line 162
  14. theorem OAI.ContinuumCoulomb.QuantumOrderedIncidence.complete_bound line 167