OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumAlgebraicHeight.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Rational coefficient-height bounds for the fixed history expressions. These bounds provide a polynomial precision budget before real evaluation.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight line 11
  2. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height line 12
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight_nonnegative line 14
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_nonnegative line 17
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight_rat line 20
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight_neg line 23
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight_add line 26
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight_sub line 33
  9. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realHeight_mul line 37
  10. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_rat line 45
  11. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_neg line 48
  12. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_add line 51
  13. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_sub line 57
  14. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_mul line 60
  15. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_conj line 70
  16. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_sqrtHalf line 73
  17. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_imaginary line 76
  18. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_realPart line 79
  19. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_imagPart line 83
  20. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_sum line 87
  21. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.height_product line 94
  22. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sample_error_height line 102