OAI/Analysis/KadisonKastler/SeparableReducingSpace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A separable reducing subspace containing finitely many vectors

The closed complex span of the algebra orbits of a finite vector family is separable when the algebra is norm separable. It is invariant under the algebra and its adjoints, so its orthogonal projection commutes with every element of the algebra.

  1. def OAI.KadisonKastler.finiteAlgebraOrbit line 20
  2. def OAI.KadisonKastler.finiteReducingSpace line 23
  3. theorem OAI.KadisonKastler.finiteAlgebraOrbit_subset line 27
  4. theorem OAI.KadisonKastler.mem_finiteReducingSpace line 31
  5. theorem OAI.KadisonKastler.isClosed_finiteReducingSpace line 36
  6. theorem OAI.KadisonKastler.isSeparable_finiteAlgebraOrbit line 40
  7. instance OAI.KadisonKastler.finiteReducingSpaceSeparable line 47
  8. theorem OAI.KadisonKastler.finiteReducingSpace_invariant line 55
  9. instance OAI.KadisonKastler.finiteReducingSpaceComplete line 69
  10. theorem OAI.KadisonKastler.finiteReducingSpace_projection_commutes line 73
  11. theorem OAI.KadisonKastler.exists_separable_reducingSpace line 83

    Source documentation

    The actual closed separable reducing subspace needed for finitely many vector tests, with its projection commutation stated explicitly.

    theorem exists_separable_reducingSpace (A : StarSubalgebra ℂ (H →L[ℂ] H))
    [TopologicalSpace.SeparableSpace A] (V : Finset H) :
    ∃ K : Submodule ℂ H, IsClosed (K : Set H) ∧
      TopologicalSpace.SeparableSpace K ∧
      (∀ v ∈ V, v ∈ K) ∧
      (∀ a : A, ∀ x ∈ K, (a : H →L[ℂ] H) x ∈ K) :=
…