OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorGraph.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Explicit ordinary-spin coordinates for a simultaneous mediator stage. The new sites are the two actual members of every fresh pair.

  1. theorem OAI.ContinuumCoulomb.MediatorGraph.submatrix_sum line 14
  2. theorem OAI.ContinuumCoulomb.MediatorGraph.submatrix_add_apply line 20
  3. theorem OAI.ContinuumCoulomb.MediatorGraph.submatrix_smul_apply line 23
  4. theorem OAI.ContinuumCoulomb.MediatorGraph.sum_kronecker line 26
  5. theorem OAI.ContinuumCoulomb.MediatorGraph.kronecker_sum line 34
  6. def OAI.ContinuumCoulomb.MediatorGraph.vertexEquiv line 42
  7. def OAI.ContinuumCoulomb.MediatorGraph.old line 45
  8. def OAI.ContinuumCoulomb.MediatorGraph.fresh line 47
  9. def OAI.ContinuumCoulomb.MediatorGraph.pairEquiv line 50
  10. def OAI.ContinuumCoulomb.MediatorGraph.basisEquiv line 53
  11. theorem OAI.ContinuumCoulomb.MediatorGraph.basisEquiv_old line 71
  12. theorem OAI.ContinuumCoulomb.MediatorGraph.basisEquiv_fresh line 75
  13. theorem OAI.ContinuumCoulomb.MediatorGraph.old_ne_fresh line 80
  14. theorem OAI.ContinuumCoulomb.MediatorGraph.fresh_injective line 86
  15. theorem OAI.ContinuumCoulomb.MediatorGraph.old_injective line 91
  16. theorem OAI.ContinuumCoulomb.MediatorGraph.pairTensor_entry line 95
  17. def OAI.ContinuumCoulomb.MediatorGraph.joinedMatrices line 101
  18. theorem OAI.ContinuumCoulomb.MediatorGraph.sourceTensor_joined line 108

    Source documentation

    Splitting the ordinary spin tensor into old spins and actual two-spin mediator pairs is an exact basis permutation.

    theorem sourceTensor_joined (n r : ℕ) (A : Fin n → Matrix (Fin 2) (Fin 2) ℂ)
    (B : Fin r → Fin 2 → Matrix (Fin 2) (Fin 2) ℂ) :
    (sourceTensor (n + r * 2) (joinedMatrices n r A B)).submatrix
      (basisEquiv n r) (basisEquiv n r) =
        sourceTensor n A ⊗ₖ mediatorTensor r (fun e => twoSpinTensor (B e 0) (B e 1)) := by
…

    Mentions: OAI.ContinuumCoulomb.sourceTensor, OAI.ContinuumCoulomb.MediatorGraph.joinedMatrices, OAI.ContinuumCoulomb.MediatorGraph.basisEquiv, OAI.ContinuumCoulomb.mediatorTensor, OAI.ContinuumCoulomb.twoSpinTensor

  19. def OAI.ContinuumCoulomb.MediatorGraph.normalizedBottom line 127
  20. theorem OAI.ContinuumCoulomb.MediatorGraph.reindex_operator_apply line 130
  21. theorem OAI.ContinuumCoulomb.MediatorGraph.reindex_form line 139
  22. theorem OAI.ContinuumCoulomb.MediatorGraph.normalizedBottom_reindex line 149
  23. theorem OAI.ContinuumCoulomb.MediatorGraph.reindex_operator_norm line 164
  24. theorem OAI.ContinuumCoulomb.MediatorGraph.matrixForm_smul line 187
  25. theorem OAI.ContinuumCoulomb.MediatorGraph.normalizedBottom_eq_rayleigh line 194
  26. theorem OAI.ContinuumCoulomb.MediatorGraph.sourceMatrixBottom_eq_mediator line 211
  27. theorem OAI.ContinuumCoulomb.MediatorGraph.twoSpinTensor_one line 219
  28. theorem OAI.ContinuumCoulomb.MediatorGraph.localPauli_old line 223
  29. theorem OAI.ContinuumCoulomb.MediatorGraph.pairPauli line 238
  30. theorem OAI.ContinuumCoulomb.MediatorGraph.localPauli_fresh line 243
  31. theorem OAI.ContinuumCoulomb.MediatorGraph.heisenberg_old line 269
  32. theorem OAI.ContinuumCoulomb.MediatorGraph.heisenberg_spoke line 278
  33. theorem OAI.ContinuumCoulomb.MediatorGraph.heisenberg_central line 287
  34. abbrev OAI.ContinuumCoulomb.MediatorGraph.EdgeIndex line 308
  35. def OAI.ContinuumCoulomb.MediatorGraph.edgeEquiv line 310
  36. def OAI.ContinuumCoulomb.MediatorGraph.stageLeft line 314
  37. def OAI.ContinuumCoulomb.MediatorGraph.stageRight line 321
  38. def OAI.ContinuumCoulomb.MediatorGraph.stageWeight line 328
  39. def OAI.ContinuumCoulomb.MediatorGraph.stageMatrix line 335
  40. theorem OAI.ContinuumCoulomb.MediatorGraph.stage_no_loops line 343
  41. theorem OAI.ContinuumCoulomb.MediatorGraph.stage_positive line 364
  42. theorem OAI.ContinuumCoulomb.MediatorGraph.stageMatrix_physical line 378

    Source documentation

    The emitted ordinary graph has exactly the physical central and spoke matrices used in the proved simultaneous-mediator estimate.

    theorem stageMatrix_physical (n q r : ℕ) (keepLeft keepRight : Fin q → Fin n)
    (hkeep : ∀ e, keepLeft e ≠ keepRight e) (keepWeight : Fin q → ℚ)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (Delta : ℚ)
    (amplitude : Fin r → ℚ) :
    (stageMatrix n q r keepLeft keepRight keepWeight left right member Delta amplitude).submatrix
      (basisEquiv n r) (basisEquiv n r) =
        physicalRawMediatorHamiltonian n r (Delta : ℝ)
          (sourceGraphMatrix n q keepLeft keepRight (fun e => (keepWeight e : ℝ)))
          left right member (fun e => (amplitude e : ℝ)) := by
…

    Mentions: OAI.ContinuumCoulomb.MediatorGraph.stageMatrix, OAI.ContinuumCoulomb.MediatorGraph.basisEquiv, OAI.ContinuumCoulomb.physicalRawMediatorHamiltonian, OAI.ContinuumCoulomb.sourceGraphMatrix

  43. theorem OAI.ContinuumCoulomb.MediatorGraph.oldGraph_matrix line 400
  44. theorem OAI.ContinuumCoulomb.MediatorGraph.oldGraph_operator_norm line 410
  45. theorem OAI.ContinuumCoulomb.MediatorGraph.graph_star line 418
  46. theorem OAI.ContinuumCoulomb.MediatorGraph.stage_bottom line 428

    Source documentation

    One ordinary, fully enumerated positive graph stage, with explicit scales and rational spoke outputs. The only bounds concern entering weights, unreplaced weights and the entering inverse precision.

    theorem stage_bottom (n q r : ℕ) {W G : ℕ} (hW : 0 < W) (hG : 0 < G)
    (keepLeft keepRight : Fin q → Fin n) (hkeep : ∀ e, keepLeft e ≠ keepRight e)
    (keepWeight : Fin q → ℚ) (hkeepWeight : 3 * ∑ e, |(keepWeight e : ℝ)| ≤ W)
    (left right : Fin r → Fin n) (hneq : ∀ e, left e ≠ right e)
    (J : Fin r → ℚ) (hJ : ∀ e, |(J e : ℝ)| ≤ W)
    (hJlower : ∀ e, 1 / (W : ℝ) ≤ |(J e : ℝ)|) :
    |sourceMatrixBottom (n + r * 2)
        (stageMatrix n q r keepLeft keepRight keepWeight left right
          (fun e => signedMediatorMember (J e)) (MediatorParameters.delta r W G)
          (fun e => MediatorParameters.spoke r W G (J e))) +
      3 * r * MediatorParameters.delta r W G + 3 * ∑ e, |(J e : ℝ)| -
        sourceMatrixBottom n (sourceGraphMatrix n q keepLeft keepRight
…

    Mentions: OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.MediatorGraph.stageMatrix, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.MediatorParameters.delta, OAI.ContinuumCoulomb.MediatorParameters.spoke, OAI.ContinuumCoulomb.sourceGraphMatrix