OAI/Analysis/KadisonSimilarity/Representation/CountableProjectionJoin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.finiteProjectionJoin line 21
2. theorem OAI.KadisonSimilarity.finiteProjectionJoin_isStarProjection line 26
3. theorem OAI.KadisonSimilarity.finiteProjectionJoin_step line 33
4. theorem OAI.KadisonSimilarity.finiteProjectionJoin_contains line 39
5. theorem OAI.KadisonSimilarity.finiteProjectionJoin_mono line 57
6. theorem OAI.KadisonSimilarity.finiteProjectionJoin_least line 71
7. theorem OAI.KadisonSimilarity.trace_finiteProjectionJoin_le line 80
8. theorem OAI.KadisonSimilarity.exists_countable_projection_join line 93

   Source documentation

   The join has trace bounded by every common bound on finite trace sums.

   theorem exists_countable_projection_join (M : VonNeumannAlgebra H)
       (υ : TracialRepresentation M) (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
       (hτ : ∀ a, τ a = υ.trace a)
       (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
       (C : ℝ) (hC : ∀ n, ∑ i ∈ Finset.range n, (τ (p i)).re ≤ C) :
       ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ (τ q).re ≤ C ∧
         (∀ n, q * p n = p n) ∧
         ∀ r : M.toStarSubalgebra, IsStarProjection r → (∀ n, r * p n = p n) → r * q = q := by
   …

9. theorem OAI.KadisonSimilarity.exists_countable_projection_join_of_equiv line 123

   Source documentation

   The countable trace bound transports through a star isomorphism. Only the target trace needs to be presented by a concrete vector.

   theorem exists_countable_projection_join_of_equiv
       {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
       (M : VonNeumannAlgebra H) (N : VonNeumannAlgebra K)
       [IsClosed (N.toStarSubalgebra : Set (K →L[ℂ] K))]
       (e : M.toStarSubalgebra ≃⋆ₐ[ℂ] N.toStarSubalgebra)
       (υ : TracialRepresentation N)
       (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ) (σ : N.toStarSubalgebra →ₚ[ℂ] ℂ)
       (hσ : ∀ b, σ b = υ.trace b) (he : ∀ a, σ (e a) = τ a)
       (p : ℕ → M.toStarSubalgebra) (hp : ∀ n, IsStarProjection (p n))
       (C : ℝ) (hC : ∀ n, ∑ i ∈ Finset.range n, (τ (p i)).re ≤ C) :
       ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ (τ q).re ≤ C ∧
         (∀ n, q * p n = p n) ∧
   …