MatrixStateAveraging.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Matrix averages in the centralizer of a vector state

Finite signed-permutation averages preserve a vector state centralizing the matrix stages. Their bounded weak cluster points are scalar by relative irreducibility. State preservation identifies each scalar, and the ultrafilter criterion then gives actual weak convergence of the whole sequence. No traciality of the ambient algebra is required.

def OAI.KadisonKastler.ambientVectorFunctional line 25

theorem OAI.KadisonKastler.matrixUnitAverage_preserves_vectorFunctional line 32

Source documentation

Each finite average preserves the vector state when its unitary matrix group lies in the state's centralizer.

theorem matrixUnitAverage_preserves_vectorFunctional
    (M : VonNeumannAlgebra H) (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hcentral : ∀ a ∈ E.algebra, ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) :
    inner ℂ Ω (matrixUnitAverage E x Ω) = inner ℂ Ω (x Ω) := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixUnitAverage

theorem OAI.KadisonKastler.stateAverage_norm_le line 58
theorem OAI.KadisonKastler.matrixUnitAverage_mem_algebra line 65

theorem OAI.KadisonKastler.matrixUnitAverage_tendsto_vectorState line 81

Source documentation

The entire sequence of concrete matrix averages converges weakly to the scalar determined by the normalized vector state.

theorem matrixUnitAverage_tendsto_vectorState
    (M : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
    (hirr : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hcentral : ∀ n a, a ∈ (E n).algebra → ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) (ξ η : H) :
    Tendsto (fun n => inner ℂ η (matrixUnitAverage (E n) x ξ)) atTop
      (𝓝 (inner ℂ η (((inner ℂ Ω (x Ω)) • (1 : H →L[ℂ] H)) ξ))) := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixUnitAverage

theorem OAI.KadisonKastler.vectorState_sandwich_tendsto line 116

Source documentation

Weak coefficient convergence gives the corresponding sandwiched vector-state limit, the form used for mixed fourth moments.

theorem vectorState_sandwich_tendsto
    {I : Type*} {l : Filter I} (F : I → H →L[ℂ] H) (T : H →L[ℂ] H)
    (hlim : ∀ ξ η, Tendsto (fun i => inner ℂ η (F i ξ)) l (𝓝 (inner ℂ η (T ξ))))
    (Ω : H) (a b : H →L[ℂ] H) :
    Tendsto (fun i => inner ℂ Ω ((a * F i * b) Ω)) l
      (𝓝 (inner ℂ Ω ((a * T * b) Ω))) := by
…