OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumAlgebraicScalarProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial programs for the exact algebraic history scalars. Each operation uses only rational arithmetic on four registers.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realCode line 13
  2. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.scalarCode line 14
  3. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realRatProgram line 16
  4. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realAddProgram line 19
  5. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realNegProgram line 29
  6. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realSubProgram line 33
  7. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realMulProgram line 38
  8. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.ratProgram line 54
  9. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.addProgram line 57
  10. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.negProgram line 66
  11. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.subProgram line 70
  12. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.mulProgram line 75
  13. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.conjProgram line 87
  14. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realPartProgram line 91
  15. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.imagPartProgram line 94
  16. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.fixedSumProgram line 98

    Source documentation

    Finite sums used by a fixed local matrix are bounded-depth compositions.

    noncomputable def fixedSumProgram {α : Type} (ea : α → List Bool) (m : ℕ)
    (f : Fin m → α → Scalar) (p : ∀ i, Procedure ea scalarCode (f i)) :
    Procedure ea scalarCode (fun x => sum (List.ofFn (fun i => f i x))) := by
…

    Mentions: OAI.ContinuumCoulomb.QuantumAlgebraicScalar.Scalar, OAI.ContinuumCoulomb.QuantumAlgebraicScalar.scalarCode, OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sum

  17. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.fixedProductProgram line 109
  18. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sampleCode line 120
  19. opaque OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sampleProgram line 122
  20. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sampleCertificate line 131