SeparableRepresentationTests.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Common contraction tests for representations

A norm-dense sequence in the unit ball of a separable C-star algebra works in every representation. The proved finite-vector Kaplansky theorem extends its weak-operator closure to the unit ball of the represented bicommutant. This does not require normality of a representation or of a pointwise fiber map.

theorem OAI.KadisonSimilarity.mem_weak_closure_of_finite_strong_approximation line 25

Source documentation

Finite-vector strong approximation implies membership in the weak operator closure.

theorem mem_weak_closure_of_finite_strong_approximation
    (S : Set (H →L[ℂ] H)) (T : H →L[ℂ] H)
    (happrox : ∀ (s : Finset H) (ε : ℝ), 0 < ε →
      ∃ R ∈ S, ∀ x ∈ s, ‖R x - T x‖ < ε) :
    ofCLM T ∈ closure (ofCLM '' S) := by
…

theorem OAI.KadisonSimilarity.exists_norm_dense_contraction_tests line 55

Source documentation

Choose one sequence in the source unit ball, dense for its norm topology.

theorem exists_norm_dense_contraction_tests :
    ∃ test : ℕ → A, (∀ n, ‖test n‖ ≤ 1) ∧
      ∀ a : A, ‖a‖ ≤ 1 → a ∈ closure (Set.range test) := by
…

theorem OAI.KadisonSimilarity.represented_contraction_mem_test_closure line 74

Source documentation

The image of a norm-dense source unit-ball sequence is weakly dense in every represented bicommutant's unit ball.

theorem represented_contraction_mem_test_closure
    (test : ℕ → A)
    (hdense : ∀ a : A, ‖a‖ ≤ 1 → a ∈ closure (Set.range test))
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (T : H →L[ℂ] H) (hT : T ∈ representationVonNeumannAlgebra σ) (hn : ‖T‖ ≤ 1) :
    ofCLM T ∈ closure (Set.range fun n => ofCLM (σ (test n))) := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.exists_common_representation_contraction_tests line 95

Source documentation

One source sequence works simultaneously for all representations on a fixed Hilbert space. Its construction is independent of that space.

theorem exists_common_representation_contraction_tests :
    ∃ test : ℕ → A, (∀ n, ‖test n‖ ≤ 1) ∧
      ∀ (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H),
        T ∈ representationVonNeumannAlgebra σ → ‖T‖ ≤ 1 →
        ofCLM T ∈ closure (Set.range fun n => ofCLM (σ (test n))) := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.exists_common_fiber_contraction_tests line 106

Source documentation

In particular the same source tests work on every Hilbert space of a family, as required for a field of representations.

theorem exists_common_fiber_contraction_tests
    {Ω : Type*} (K : Ω → Type*) [∀ a, NormedAddCommGroup (K a)]
    [∀ a, InnerProductSpace ℂ (K a)] [∀ a, CompleteSpace (K a)]
    (σ : ∀ a, A →⋆ₐ[ℂ] (K a →L[ℂ] K a)) :
    ∃ test : ℕ → A, (∀ n, ‖test n‖ ≤ 1) ∧
      ∀ a (T : K a →L[ℂ] K a), T ∈ representationVonNeumannAlgebra (σ a) → ‖T‖ ≤ 1 →
        ofCLM T ∈ closure (Set.range fun n => ofCLM (σ a (test n))) := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.exists_common_fiber_scalar_tests line 119

Source documentation

Countably many almost-everywhere tests in the common source algebra control the full scalar commutator seminorm almost everywhere.

theorem exists_common_fiber_scalar_tests
    {Ω : Type*} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
    (K : Ω → Type*) [∀ a, NormedAddCommGroup (K a)]
    [∀ a, InnerProductSpace ℂ (K a)] [∀ a, CompleteSpace (K a)]
    (σ : ∀ a, A →⋆ₐ[ℂ] (K a →L[ℂ] K a)) :
    ∃ test : ℕ → A, (∀ n, ‖test n‖ ≤ 1) ∧
      ∀ (Y : ∀ a, K a →L[ℂ] K a) (c : ℝ), 0 ≤ c →
        (∀ n, ∀ᵐ a ∂μ, ‖commutator (Y a) (σ a (test n))‖ ≤ c) →
        ∀ᵐ a ∂μ, scalarCommutatorNorm (representationVonNeumannAlgebra (σ a)) (Y a) ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.representationVonNeumannAlgebra