OAI/Analysis/KadisonSimilarity/Representation/CompactAlgebraEstimate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.commutator_matrix_bound_of_close_commutant line 17
2. theorem OAI.KadisonSimilarity.compact_group_commutator_estimate line 46

   Source documentation

   The Haar integral gives the required approximation uniformly in matrix size, as soon as commutation with the group implies commutation with P.

   theorem compact_group_commutator_estimate
       (P : VonNeumannAlgebra H) (ν : Measure Γ)
       [IsProbabilityMeasure ν] [ν.IsMulLeftInvariant]
       (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
       (hmem : ∀ g, U g ∈ P)
       (hgenerate : ∀ Z : H →L[ℂ] H,
         (∀ g, commutator Z (U g) = 0) →
         ∀ a : H →L[ℂ] H, a ∈ P → commutator Z a = 0)
       (hintegrable : ∀ Y : H →L[ℂ] H,
         WeaklyIntegrable ν (unitaryConjugate U Y)) :
       CommutatorEstimate P 2 := by
   …

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

3. theorem OAI.KadisonSimilarity.compact_generated_algebra_estimate line 73

   Source documentation

   Double-commutant generation supplies the generation condition used by Haar averaging, without a separate operator-invariance hypothesis.

   theorem compact_generated_algebra_estimate
       (P : VonNeumannAlgebra H) (ν : Measure Γ)
       [IsProbabilityMeasure ν] [ν.IsMulLeftInvariant]
       (U : Γ →* (H →L[ℂ] H)) (hU : ∀ g, ‖U g‖ ≤ 1)
       (hmem : ∀ g, U g ∈ P)
       (hgenerate : (P : Set (H →L[ℂ] H)) =
         Set.centralizer (Set.centralizer (Set.range U)))
       (hintegrable : ∀ Y : H →L[ℂ] H,
         WeaklyIntegrable ν (unitaryConjugate U Y)) :
       CommutatorEstimate P 2 := by
   …

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