OAI/Analysis/Nuclearity/SpatialStateUltralimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Ultralimits of unit-vector states. This supplies the compactness step after the finite spatial approximations, without claiming normality of the limiting state or continuity of a nonnormal expectation.

  1. def OAI.WeakPureInfiniteness.spatialStateUltraValue line 20
  2. lemma OAI.WeakPureInfiniteness.spatialStateUltraValue_tendsto line 23
  3. def OAI.WeakPureInfiniteness.spatialStateUltra line 32
  4. lemma OAI.WeakPureInfiniteness.spatialStateUltra_one line 54
  5. lemma OAI.WeakPureInfiniteness.spatialStateUltra_norm_apply_le line 61
  6. lemma OAI.WeakPureInfiniteness.spatialStateUltra_eq_of_tendsto line 70
  7. theorem OAI.WeakPureInfiniteness.exists_spatial_state_of_finite_approximation line 79

    Source documentation

    Compactness for finite unit-vector approximations. The limit is a state, but need not be normal. In particular, this construction makes no continuity claim about an expectation in the weak operator topology.

    theorem exists_spatial_state_of_finite_approximation {κ : Type*}
    (T : κ → (H →L[ℂ] H)) (c : κ → ℂ)
    (h : ∀ (s : Finset κ) (ε : ℝ), 0 < ε →
      ∃ ξ : H, ‖ξ‖ = 1 ∧ ∀ k ∈ s, ‖inner ℂ ξ (T k ξ) - c k‖ < ε) :
    ∃ φ : (H →L[ℂ] H) →ₚ[ℂ] ℂ, φ 1 = 1 ∧ ∀ k, φ (T k) = c k := by
…