OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelTable.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Ordered finite tables and their literal product enumeration. These identities compare the computed lists with the actual finite Pauli family.

  1. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.table line 15
  2. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.nextTerm line 19
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.index line 22
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelTable.nextQubit line 24
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.nextQubit_index line 27
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.lookup_ofFn line 32
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.product_table line 37
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.radius_table line 55
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelTable.family_table line 65

    Source documentation

    A literal stage is the same product-ordered finite table as its supplied word and coefficient formulas. The hypotheses are pointwise identities.

    theorem family_table (e : Fin m ≃ κ) (ix : ι → ℕ) (xs : κ → List ι)
    (w : κ → ι → Fin 4) (J : κ → ℚ) (N n : ℕ)
    (f : ℕ → List Letter → Fin d → List Letter)
    (g : ℚ → ℚ → Fin d → ℚ) :
    family d f g (N,n,table e ix xs w J) =
      List.ofFn (fun i : Fin (m*d) =>
        let p := nextTerm e d i
…

    Mentions: OAI.ContinuumCoulomb.QuantumOrderedLabelTable.table, OAI.ContinuumCoulomb.QuantumOrderedLabelTable.nextTerm