OAI/Algebra/DepthFive/OperatorTraceBridge.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.toMatrix_eq_pathShiftMatrix line 20

   Source documentation

   An operator action described by weighted basis shifts has exactly the corresponding path-shift matrix. No orthonormal structure is required here.

   theorem toMatrix_eq_pathShiftMatrix
       (b : Basis I K V) (c : Basis J K W) (F : V →ₗ[K] W)
       (shift : I → P → J) (weight : I → P → K)
       (haction : ∀ i, F (b i) = ∑ p, weight i p • c (shift i p)) :
       LinearMap.toMatrix b c F = pathShiftMatrix shift weight := by
   …

   Mentions: OAI.Problem335.pathShiftMatrix

2. theorem OAI.Problem335.operator_first_trace_of_path_action line 37

   Source documentation

   First trace for a finite-basis operator with collision-free path action.

   theorem operator_first_trace_of_path_action
       (b : Basis I ℝ V) (c : Basis J ℝ W) (F : V →ₗ[ℝ] W)
       (shift : I → P → J) (weight : I → P → ℝ)
       (haction : ∀ i, F (b i) = ∑ p, weight i p • c (shift i p))
       (hdisjoint : ∀ i p q, p ≠ q → shift i p = shift i q →
         weight i p * weight i q = 0) :
       let A := LinearMap.toMatrix b c F
   …

3. theorem OAI.Problem335.operator_first_trace_of_sqrt_path_action line 50

   Source documentation

   First trace for the square-root occupation coefficients of the Fock basis.

   theorem operator_first_trace_of_sqrt_path_action
       (b : Basis I ℝ V) (c : Basis J ℝ W) (F : V →ₗ[ℝ] W)
       (shift : I → P → J) (mass : I → P → ℝ)
       (haction : ∀ i, F (b i) = ∑ p, Real.sqrt (mass i p) • c (shift i p))
       (hnonneg : ∀ i p, 0 ≤ mass i p)
       (hdisjoint : ∀ i p q, p ≠ q → shift i p = shift i q →
         mass i p = 0 ∨ mass i q = 0) :
       let A := LinearMap.toMatrix b c F
   …

4. theorem OAI.Problem335.operator_second_trace_of_path_action line 64

   Source documentation

   Exact second trace for an operator described on a finite basis by paths.

   theorem operator_second_trace_of_path_action
       (b : Basis I ℝ V) (c : Basis J ℝ W) (F : V →ₗ[ℝ] W)
       (shift : I → P → J) (weight : I → P → ℝ)
       (haction : ∀ i, F (b i) = ∑ p, weight i p • c (shift i p)) :
       let A := LinearMap.toMatrix b c F
   …

5. theorem OAI.Problem335.path_toMatrix_unitsSMul_apply line 78

   Source documentation

   Coordinates after separate unit rescalings of the source and target bases.

   theorem path_toMatrix_unitsSMul_apply {I : Type u_1} {J : Type u_2}
       {V : Type u_4} {W : Type u_5}
       [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
       [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W]
       (b : Basis I ℝ V) (c : Basis J ℝ W) (F : V →ₗ[ℝ] W)
       (sourceScale : I → ℝˣ) (targetScale : J → ℝˣ) (j : J) (i : I) :
       LinearMap.toMatrix (b.unitsSMul sourceScale) (c.unitsSMul targetScale) F j i =
         (targetScale j : ℝ)⁻¹ * (sourceScale i : ℝ) * LinearMap.toMatrix b c F j i := by
   …

6. theorem OAI.Problem335.toMatrix_normalized_path_action line 91

   Source documentation

   The path coefficient changes by the source/target normalization ratio. This applies in particular to factorial-normalized monomial bases.

   theorem toMatrix_normalized_path_action
       (b : Basis I ℝ V) (c : Basis J ℝ W) (F : V →ₗ[ℝ] W)
       (shift : I → P → J) (weight : I → P → ℝ)
       (haction : ∀ i, F (b i) = ∑ p, weight i p • c (shift i p))
       (sourceScale : I → ℝˣ) (targetScale : J → ℝˣ) :
       LinearMap.toMatrix (b.unitsSMul sourceScale) (c.unitsSMul targetScale) F =
         pathShiftMatrix shift (fun i p =>
           (targetScale (shift i p) : ℝ)⁻¹ * (sourceScale i : ℝ) * weight i p) := by
   …

   Mentions: OAI.Problem335.pathShiftMatrix