OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFixedPauli.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Fixed-arity Pauli traces evaluated entirely in rational registers. The interpretation is the actual complex Pauli coefficient, not an assumed list of Hamiltonian coefficients.

  1. def OAI.ContinuumCoulomb.QuantumFixedPauli.enumerate line 15
  2. def OAI.ContinuumCoulomb.QuantumFixedPauli.finiteSum line 18
  3. def OAI.ContinuumCoulomb.QuantumFixedPauli.finiteProduct line 21
  4. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.value_finiteSum line 24
  5. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.value_finiteProduct line 29
  6. def OAI.ContinuumCoulomb.QuantumFixedPauli.pauli line 34
  7. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.value_pauli line 40
  8. def OAI.ContinuumCoulomb.QuantumFixedPauli.word line 45
  9. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.value_word line 48
  10. def OAI.ContinuumCoulomb.QuantumFixedPauli.coefficient line 54
  11. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.value_coefficient line 59
  12. def OAI.ContinuumCoulomb.QuantumFixedPauli.realCoefficient line 71
  13. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.realCoefficient_eq line 75
  14. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.realCoefficient_expansion line 82
  15. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.coefficient_of_entries line 92

    Source documentation

    This entrywise attachment applies to the actual local core of an ordered history term once its six-site table has been constructed.

    theorem coefficient_of_entries {ι : Type} [Fintype ι] [DecidableEq ι]
    (A : Matrix (ι → Fin 2) (ι → Fin 2) Scalar)
    (H : Matrix (ι → Fin 2) (ι → Fin 2) ℂ)
    (hA : ∀ s t, value (A s t) = H s t) (w : ι → Fin 4) :
    realValue (realCoefficient A w) = (qmaPauliCoefficient H w).re := by
…

    Mentions: OAI.ContinuumCoulomb.QuantumFixedPauli.realCoefficient, OAI.ContinuumCoulomb.qmaPauliCoefficient

  16. theorem OAI.ContinuumCoulomb.QuantumFixedPauli.sample_error line 101