NonseparableReduction.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Removing separability from the uniform commutator estimate

Each operator-norm test involves finitely many matrix entries and finitely many vectors. Their common reducing subspace is separable. We restrict the actual C-star algebra generated by those entries, use the two-vector Kaplansky specialization to reach its bicommutant, and recover the original vector test by the isometric inclusion.

def OAI.KadisonSimilarity.finiteMatrixTestAlgebra line 25
Source documentation
The norm-closed C-star algebra generated by the entries of one test.
```
def finiteMatrixTestAlgebra {n : ℕ} (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    StarSubalgebra ℂ (H →L[ℂ] H) :=
…
```
instance OAI.KadisonSimilarity.finiteMatrixTestAlgebra_closed line 29
theorem OAI.KadisonSimilarity.matrix_entry_mem_test_algebra line 34
theorem OAI.KadisonSimilarity.finiteMatrixTestAlgebra_le line 40

theorem OAI.KadisonSimilarity.finiteMatrixTestAlgebra_invariant line 52

Source documentation

A common reducing space for the entries reduces their generated algebra.

theorem finiteMatrixTestAlgebra_invariant {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) (M : ClosedSubmodule ℂ H)
    (hX : ∀ i j, Commute M.toSubmodule.starProjection (X i j)) :
    ∀ a : finiteMatrixTestAlgebra X, ∀ x : H, x ∈ M → (a : H →L[ℂ] H) x ∈ M := by
…

Mentions: OAI.KadisonSimilarity.finiteMatrixTestAlgebra

def OAI.KadisonSimilarity.invariantStarRepresentation line 77

Source documentation

Restriction of an invariant star subalgebra to the closed subspace.

def invariantStarRepresentation (B : StarSubalgebra ℂ (H →L[ℂ] H))
    (M : ClosedSubmodule ℂ H)
    (hM : ∀ a : B, ∀ x : H, x ∈ M → (a : H →L[ℂ] H) x ∈ M) :
    B →⋆ₐ[ℂ] (M →L[ℂ] M) where
…

theorem OAI.KadisonSimilarity.invariantStarRepresentation_apply line 98

theorem OAI.KadisonSimilarity.exists_matrix_test_reducing_space line 104

Source documentation

A fixed finite test fits in a separable reducing subspace.

theorem exists_matrix_test_reducing_space {n : ℕ}
    (Y : H →L[ℂ] H) (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H))
    (ξ : HilbertCopies H n) :
    ∃ M : ClosedSubmodule ℂ H, TopologicalSpace.SeparableSpace M ∧
      (∀ i, ξ i ∈ M) ∧ (∀ x, x ∈ M → Y x ∈ M) ∧
      (∀ i j, Commute M.toSubmodule.starProjection (X i j)) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies

def OAI.KadisonSimilarity.SeparableUniformCommutatorEstimate line 123
Source documentation
The separable version of the actual universal von Neumann estimate.
```
def SeparableUniformCommutatorEstimate (C : ℝ) : Prop :=
…
```
def OAI.KadisonSimilarity.SeparableTwoVectorKaplanskyInput line 130
Source documentation
Blackadar I.9.1.3 and C-star quotient norm lifting, only on two test vectors in a separable represented Hilbert space. This is the exact published closure input used in the reduction below.
```
def SeparableTwoVectorKaplanskyInput : Prop :=
…
```
theorem OAI.KadisonSimilarity.norm_mapCopies_subtype line 137
theorem OAI.KadisonSimilarity.intertwines_commutator line 145

theorem OAI.KadisonSimilarity.uniformCommutatorEstimate_of_separable line 158

Source documentation

The uniform estimate on separable Hilbert spaces implies the same estimate, with the identical constant, on arbitrary Hilbert spaces.

theorem uniformCommutatorEstimate_of_separable {C : ℝ} (hC : 0 ≤ C)
    (estimate : SeparableUniformCommutatorEstimate.{u} C)
    (kaplansky : SeparableTwoVectorKaplanskyInput.{u}) : UniformCommutatorEstimate.{u} C := by
…