OAI/Analysis/KadisonKastler/PreparedPairIrreducibility.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.matrixUnitAverage_norm_le line 27
2. theorem OAI.KadisonKastler.matrixUnitAverage_mem line 34
3. theorem OAI.KadisonKastler.matrixUnitAverage_sub_fixed_norm_le line 48
4. theorem OAI.KadisonKastler.matrixUnitAverage_weak_limit_commutes line 72

   Source documentation

   A bounded weak cluster point of the concrete stage averages commutes with every fixed stage.

   theorem matrixUnitAverage_weak_limit_commutes
       (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
       (hmono : Monotone (fun n => (E n).algebra))
       (x T : H →L[ℂ] H) {l : Filter ℕ} [l.NeBot] (hl : l ≤ atTop)
       (hlim : ∀ ξ η, Tendsto (fun n => inner ℂ η (matrixUnitAverage (E n) x ξ)) l
         (𝓝 (inner ℂ η (T ξ)))) :
       ∀ n a, a ∈ (E n).algebra → a * T = T * a := by
   …

   Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixUnitAverage

5. theorem OAI.KadisonKastler.exists_scalar_near_of_increasing_matrix_averages line 99

   Source documentation

   Concrete matrix-stage averages provide a scalar near every ambient operator which commutes with those stages.

   theorem exists_scalar_near_of_increasing_matrix_averages
       (M : VonNeumannAlgebra H)
       (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
       (hmono : Monotone (fun n => (E n).algebra))
       (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
       (hirr : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
         ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
       (x p : H →L[ℂ] H) (hx : x ∈ M)
       (hp : ∀ n a, a ∈ (E n).algebra → a * p = p * a) :
       ∃ z : ℂ, ‖z • (1 : H →L[ℂ] H) - p‖ ≤ ‖x - p‖ := by
   …

   Mentions: OAI.Generator.MatrixUnitSystem

6. theorem OAI.KadisonKastler.relative_projection_trivial_of_increasing_matrix_averages line 129

   Source documentation

   The neighbor has no nontrivial projections in the relative commutant when the ordinary gap is below one half.

   theorem relative_projection_trivial_of_increasing_matrix_averages
       (M N : VonNeumannAlgebra H)
       (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
       (hmono : Monotone (fun n => (E n).algebra))
       (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
       (hirr : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
         ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
       (hgap : kkDistance M N < 1 / 2)
       (p : Algebra N) (hp : IsStarProjection p)
       (hcomm : ∀ n a, a ∈ (E n).algebra → a * p.val = p.val * a) :
       p = 0 ∨ p = 1 := by
   …

   Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Algebra

7. theorem OAI.KadisonKastler.commute_generated_of_commute_matrix_stages line 151

   Source documentation

   Commutation with all matrix stages extends to their generated von Neumann algebra.

   theorem commute_generated_of_commute_matrix_stages
       (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
       (T : H →L[ℂ] H)
       (hT : ∀ n a, a ∈ (E n).algebra → a * T = T * a) :
       ∀ a ∈ generatedVonNeumannAlgebra (⨆ n, (E n).algebra), a * T = T * a := by
   …

   Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.generatedVonNeumannAlgebra

8. theorem OAI.KadisonKastler.relative_irreducibility_of_near_increasing_matrices line 182

   Source documentation

   Relative irreducibility in the first algebra passes to the neighbor for the actual weakly generated common increasing matrix algebra.

   theorem relative_irreducibility_of_near_increasing_matrices
       (M N : VonNeumannAlgebra H)
       (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
       (hmono : Monotone (fun n => (E n).algebra))
       (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
       (hirr : ∀ T ∈ M,
         (∀ a ∈ generatedVonNeumannAlgebra (⨆ n, (E n).algebra), a * T = T * a) →
         ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
       (hgap : kkDistance M N < 1 / 2) :
       ∀ T ∈ N,
         (∀ a ∈ generatedVonNeumannAlgebra (⨆ n, (E n).algebra), a * T = T * a) →
         ∃ z : ℂ, T = z • (1 : H →L[ℂ] H) := by
   …

   Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.kkDistance