RepresentedFiniteSymmetrization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix averaging in a fixed represented algebra

The scalar bound is supplied on the source C-star algebra. Actual normalized Haar measures on the finite matrix-unitary groups produce a single operator commuting with every stage. No von Neumann closure or independently chosen invariant operator is needed in this step.

theorem OAI.KadisonSimilarity.represented_scalar_bound_of_close line 25

Source documentation

A norm perturbation by δ changes a source-algebra scalar commutator bound δ into at most 3δ.

theorem represented_scalar_bound_of_close
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Y₀ Y : H →L[ℂ] H)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : ∀ a, ‖commutator Y (σ a)‖ ≤ δ * ‖a‖)
    (hclose : ‖Y₀ - Y‖ ≤ δ) :
    ∀ a, ‖commutator Y₀ (σ a)‖ ≤ (3 * δ) * ‖a‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_matrixUnitary_image_le_one line 40

theorem OAI.KadisonSimilarity.exists_represented_finite_matrix_symmetrization line 59

Source documentation

Actual Haar averages and a weak-operator cluster point give the finite factor's initial perturbation. The scalar norm is measured on the original source algebra; the bound and the distance do not depend on matrix sizes.

theorem exists_represented_finite_matrix_symmetrization
    [∀ n, Nonempty (I n)]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (ι : ∀ n, Matrix (I n) (I n) ℂ →⋆ₐ[ℂ] A)
    (transition : ∀ n m, n ≤ m →
      Matrix (I n) (I n) ℂ →⋆ₐ[ℂ] Matrix (I m) (I m) ℂ)
    (hcompat : ∀ n m h a, ι m (transition n m h a) = ι n a)
    (Y : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : ∀ a, ‖commutator Y (σ a)‖ ≤ δ * ‖a‖) :
    ∃ Y₀ : H →L[ℂ] H, ‖Y₀‖ ≤ ‖Y‖ ∧ ‖Y₀ - Y‖ ≤ δ ∧
      (∀ a, ‖commutator Y₀ (σ a)‖ ≤ (3 * δ) * ‖a‖) ∧
      ∀ n a, commutator Y₀ (σ (ι n a)) = 0 := by
…

Mentions: OAI.KadisonSimilarity.commutator