OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBufferedDogleg.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The two direct buffered endpoint arms, including their one-step joins.

  1. def OAI.ContinuumCoulomb.qmaBufferedDoglegLength line 9
  2. def OAI.ContinuumCoulomb.qmaBufferedDoglegPoint line 11
  3. def OAI.ContinuumCoulomb.qmaBufferedDoglegSupport line 16
  4. theorem OAI.ContinuumCoulomb.qmaBufferedDogleg_zero line 21
  5. theorem OAI.ContinuumCoulomb.qmaBufferedDogleg_last line 24
  6. theorem OAI.ContinuumCoulomb.qmaBufferedDogleg_support line 29
  7. theorem OAI.ContinuumCoulomb.qmaBufferedDogleg_step line 34
  8. theorem OAI.ContinuumCoulomb.qmaBufferedDogleg_injective line 42
  9. theorem OAI.ContinuumCoulomb.qmaBufferedDogleg_length_bound line 52
  10. theorem OAI.ContinuumCoulomb.qmaBufferedFanout_direct_support line 57