OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/SpinMatrixNorm.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Dimension-independent operator bounds for the actual spin matrices.

  1. def OAI.ContinuumCoulomb.spinMatrixOperator line 16

    Source documentation

    The ordinary Euclidean operator represented by a finite spin matrix.

    def spinMatrixOperator (M : Matrix ι ι ℂ) : EuclideanSpace ℂ ι →L[ℂ] EuclideanSpace ℂ ι :=
…
  2. theorem OAI.ContinuumCoulomb.spinMatrixOperator_apply line 19
  3. theorem OAI.ContinuumCoulomb.spinMatrixOperator_add line 22
  4. theorem OAI.ContinuumCoulomb.spinMatrixOperator_smul line 27
  5. theorem OAI.ContinuumCoulomb.spinMatrixOperator_sum line 32
  6. theorem OAI.ContinuumCoulomb.spinMatrixOperator_mul line 37
  7. theorem OAI.ContinuumCoulomb.spinMatrixOperator_one line 44
  8. theorem OAI.ContinuumCoulomb.spinMatrixOperator_star line 48
  9. theorem OAI.ContinuumCoulomb.spinMatrixOperator_unitary_norm_map line 53
  10. theorem OAI.ContinuumCoulomb.spinMatrixOperator_unitary_norm line 63
  11. theorem OAI.ContinuumCoulomb.pauli_star line 70

    Source documentation

    Actual one-site Paulis are Hermitian.

    theorem pauli_star (μ : Fin 3) : (pauli μ).conjTranspose = pauli μ := by
…

    Mentions: OAI.ContinuumCoulomb.pauli

  12. theorem OAI.ContinuumCoulomb.sourceTensor_star line 74
  13. theorem OAI.ContinuumCoulomb.sourceLocalPauli_star line 79
  14. theorem OAI.ContinuumCoulomb.sourceLocalPauli_operator_norm line 87
  15. theorem OAI.ContinuumCoulomb.bellTransform_star line 92
  16. theorem OAI.ContinuumCoulomb.bellTransform_one line 97
  17. theorem OAI.ContinuumCoulomb.firstPauli_star line 100
  18. theorem OAI.ContinuumCoulomb.secondPauli_star line 105
  19. theorem OAI.ContinuumCoulomb.bellMemberPauli_star line 110
  20. theorem OAI.ContinuumCoulomb.bellMemberPauli_sq line 117
  21. theorem OAI.ContinuumCoulomb.mediatorLocal_star line 124
  22. theorem OAI.ContinuumCoulomb.mediatorLocal_one line 132
  23. theorem OAI.ContinuumCoulomb.elementaryMediatorSpoke_star line 137
  24. theorem OAI.ContinuumCoulomb.elementaryMediatorSpoke_sq line 145
  25. theorem OAI.ContinuumCoulomb.elementaryMediatorSpoke_operator_norm line 153
  26. theorem OAI.ContinuumCoulomb.mediatorEdgeSpoke_operator_norm line 160

    Source documentation

    Two three-axis spokes have norm at most six, including all spectators.

    theorem mediatorEdgeSpoke_operator_norm (n r : ℕ) (e : Fin r) (i j : Fin n) (member : Fin 2) :
    ‖spinMatrixOperator (mediatorEdgeSpoke n r e i j member)‖ ≤ 6 := by
…

    Mentions: OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.mediatorEdgeSpoke

  27. theorem OAI.ContinuumCoulomb.totalMediatorSpokes_operator_norm line 179

    Source documentation

    The actual simultaneous hopping norm is polynomial in the edge list.

    theorem totalMediatorSpokes_operator_norm (n r : ℕ) (left right : Fin r → Fin n)
    (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) :
    ‖spinMatrixOperator (totalMediatorSpokes n r left right member amplitude)‖ ≤
      6 * ∑ e, |amplitude e| := by
…

    Mentions: OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.totalMediatorSpokes

  28. theorem OAI.ContinuumCoulomb.mediatorEdgeSpoke_star line 197
  29. theorem OAI.ContinuumCoulomb.totalMediatorSpokes_star line 202
  30. theorem OAI.ContinuumCoulomb.sourceHeisenbergMatrix_star line 211
  31. theorem OAI.ContinuumCoulomb.sourceHeisenbergMatrix_operator_norm line 219
  32. def OAI.ContinuumCoulomb.sourceGraphMatrix line 235
  33. theorem OAI.ContinuumCoulomb.sourceGraphMatrix_operator_norm line 239