OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedTableProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Fixed-width algebraic coefficient tables, with exact normalization of the padded words. Each local arity at most six uses a fixed finite program.

  1. theorem OAI.ContinuumCoulomb.QuantumPaddedTable.coefficient_decision line 17
  2. def OAI.ContinuumCoulomb.QuantumPaddedTable.coefficient line 25
  3. opaque OAI.ContinuumCoulomb.QuantumPaddedTable.coefficientProgram line 32
  4. def OAI.ContinuumCoulomb.QuantumPaddedTable.table line 42
  5. def OAI.ContinuumCoulomb.QuantumPaddedTable.tableProgram line 45
  6. theorem OAI.ContinuumCoulomb.QuantumPaddedTable.coefficient_value line 53
  7. theorem OAI.ContinuumCoulomb.QuantumPaddedTable.table_length line 73
  8. theorem OAI.ContinuumCoulomb.QuantumPaddedTable.six_table_length line 78
  9. def OAI.ContinuumCoulomb.QuantumPaddedTable.certificate line 83
  10. abbrev OAI.ContinuumCoulomb.QuantumPaddedTable.Input line 87
  11. def OAI.ContinuumCoulomb.QuantumPaddedTable.inputCode line 88
  12. def OAI.ContinuumCoulomb.QuantumPaddedTable.uniformTable line 91

    Source documentation

    Total fixed-arity dispatcher. Invalid arities use the six-site branch.

    def uniformTable (x : Input) : List RealScalar :=
…

    Mentions: OAI.ContinuumCoulomb.QuantumPaddedTable.Input

  13. opaque OAI.ContinuumCoulomb.QuantumPaddedTable.uniformProgram line 99
  14. theorem OAI.ContinuumCoulomb.QuantumPaddedTable.uniformTable_eq line 115
  15. theorem OAI.ContinuumCoulomb.QuantumPaddedTable.uniformTable_length line 119
  16. def OAI.ContinuumCoulomb.QuantumPaddedTable.uniformCertificate line 124