SimultaneousSymmetrization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous symmetry for an increasing family of compact groups, using actual Haar averages and a weak-operator cluster point.

theorem OAI.KadisonSimilarity.compression_eq_of_weakOperator_cluster line 21

Source documentation

A fixed rectangular compression is weak-operator continuous, so an exact compression identity survives a weak-operator cluster point.

theorem compression_eq_of_weakOperator_cluster (T : ℕ → H →L[ℂ] H)
    (S : H →L[ℂ] H) (A : K →L[ℂ] H) (B : H →L[ℂ] K) (C : K →L[ℂ] K)
    (hcluster : MapClusterPt (ofCLM S) atTop (fun n => ofCLM (T n)))
    (heq : ∀ᶠ n in atTop, B.comp ((T n).comp A) = C) : B.comp (S.comp A) = C := by
…

theorem OAI.KadisonSimilarity.exists_simultaneously_symmetrized line 47

Source documentation

A single cluster point has every finite-stage symmetry, all common commutator bounds, and the original compression to the fixed subspace. The stage maps are ordinary group-element inclusions; no limiting invariant operator is assumed among the data.

theorem exists_simultaneously_symmetrized
    (U : ∀ n, Γ n →* (H →L[ℂ] H)) (hU : ∀ n g, ‖U n g‖ ≤ 1)
    (hstar : ∀ n g, (U n g).adjoint = U n g⁻¹)
    (embedding : ∀ n m, n ≤ m → Γ n → Γ m)
    (hcompat : ∀ n m h g, U m (embedding n m h g) = U n g)
    (T : H →L[ℂ] H)
    (hI : ∀ n, WeaklyIntegrable (μ n) (unitaryConjugate (U n) T))
    (J : K →L[ℂ] H) (hfix : ∀ n g, (U n g).comp J = J)
    {ι : Type*} (test : ι → H →L[ℂ] H) (bound : ι → ℝ) (hbound : ∀ i, 0 ≤ bound i)
    (htest : ∀ n g i, ‖commutator (unitaryConjugate (U n) T g) (test i)‖ ≤ bound i) :
    ∃ S : H →L[ℂ] H,
      ‖S‖ ≤ ‖T‖ ∧
…

Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate, OAI.KadisonSimilarity.commutator