CentralDecompositionTests.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The countable tests in a central decomposition

Starting with representations of one norm-separable C-star subalgebra, their bicommutant-generation property, and almost-everywhere agreement with the ambient fiber representatives, the contraction tests are constructed. Only countably many agreements are used; pointwise fiber evaluation is not assumed to be a normal map on the von Neumann algebra.

theorem OAI.KadisonSimilarity.exists_central_decomposition_tests line 29

Source documentation

Construct exactly the test, test_norm, and test_dense fields used by CentralDecompositionData, from a separable source and its fiber representations.

theorem exists_central_decomposition_tests
    (P : VonNeumannAlgebra H)
    (B : StarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (B : Set (H →L[ℂ] H))]
    [TopologicalSpace.SeparableSpace B] (hB : B ≤ P.toStarSubalgebra)
    (algebra : ∀ a, VonNeumannAlgebra (K a))
    (fiber : (vonNeumannCenter P).commutant.toStarSubalgebra → ∀ a, K a →L[ℂ] K a)
    (σ : ∀ a, B →⋆ₐ[ℂ] (K a →L[ℂ] K a))
    (hagrees : ∀ b : B, ∀ᵐ a ∂μ,
      fiber (centerCommutantInclusion P ⟨b.val, hB b.property⟩) a = σ a b)
    (hgenerates : ∀ᵐ a ∂μ, algebra a = representationVonNeumannAlgebra (σ a)) :
    ∃ test : ℕ → P.toStarSubalgebra,
      (∀ n, ‖(test n : H →L[ℂ] H)‖ ≤ 1) ∧
…

Mentions: OAI.KadisonSimilarity.vonNeumannCenter, OAI.KadisonSimilarity.centerCommutantInclusion, OAI.KadisonSimilarity.representationVonNeumannAlgebra