SeparableReducingTest.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Separable reducing subspaces for finitely many tests

Take the closed complex span of the orbit of finitely many vectors under words in finitely many operators and their adjoints. The orbit is countable, so the resulting Hilbert subspace is separable. No representation estimate or separability assumption on the ambient space is used.

def OAI.KadisonSimilarity.testLetter line 21
def OAI.KadisonSimilarity.testWord line 24
def OAI.KadisonSimilarity.testOrbit line 28
def OAI.KadisonSimilarity.separableReducingTestSpace line 32
Source documentation
The canonical separable reducing space of a finite test family.
```
def separableReducingTestSpace (T : Fin m → H →L[ℂ] H) (ξ : Fin r → H) :
    ClosedSubmodule ℂ H :=
…
```
instance OAI.KadisonSimilarity.separableReducingTestSpace_separable line 36
theorem OAI.KadisonSimilarity.mem_separableReducingTestSpace line 45
theorem OAI.KadisonSimilarity.testLetter_invariant line 51
theorem OAI.KadisonSimilarity.separableReducingTestSpace_invariant line 66
theorem OAI.KadisonSimilarity.separableReducingTestSpace_adjoint_invariant line 72
theorem OAI.KadisonSimilarity.separableReducingTestSpace_projection_commutes line 79
Source documentation
Reduction is an actual projection identity, not merely invariance.
```
theorem separableReducingTestSpace_projection_commutes
    (T : Fin m → H →L[ℂ] H) (ξ : Fin r → H) (i : Fin m) :
    Commute (separableReducingTestSpace T ξ).toSubmodule.starProjection (T i) := by
…
```
Mentions: OAI.KadisonSimilarity.separableReducingTestSpace

theorem OAI.KadisonSimilarity.exists_separable_reducing_test_space line 98

Source documentation

Every finite collection of bounded operators and test vectors admits a common separable closed reducing Hilbert subspace.

theorem exists_separable_reducing_test_space
    (T : Fin m → H →L[ℂ] H) (ξ : Fin r → H) :
    ∃ M : ClosedSubmodule ℂ H, TopologicalSpace.SeparableSpace M ∧
      (∀ i, ξ i ∈ M) ∧
      (∀ i x, x ∈ M → T i x ∈ M) ∧
      (∀ i x, x ∈ M → (T i).adjoint x ∈ M) ∧
      (∀ i, Commute M.toSubmodule.starProjection (T i)) :=
…