OAI/Analysis/BoundedHochschild/ProjectionJoinComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedHochschild.KadisonRingrose.orthogonal_projection_sum_range line 21
2. theorem OAI.BoundedHochschild.KadisonRingrose.projection_join_subequivalence line 37

   Source documentation

   If two projections embed into orthogonal target projections, their join embeds into the sum of those targets.

   theorem projection_join_subequivalence (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
       {p₁ p₂ q₁ q₂ : M} (hp₁ : IsStarProjection p₁) (hp₂ : IsStarProjection p₂)
       (hq₁ : IsStarProjection q₁) (hq₂ : IsStarProjection q₂) (hqorth : q₁ * q₂ = 0)
       (a b : PartialIso M) (hai : a.initial = p₁) (haf : a.final ≤ q₁)
       (hbi : b.initial = p₂) (hbf : b.final ≤ q₂) :
       ∃ t : PartialIso M, t.final ≤ q₁ + q₂ ∧ p₁ ≤ t.initial ∧ p₂ ≤ t.initial ∧
         ∀ r : M, IsStarProjection r → p₁ ≤ r → p₂ ≤ r → t.initial ≤ r := by
   …

3. theorem OAI.BoundedHochschild.KadisonRingrose.finite_join_subequivalence line 66

   Source documentation

   Finite joins of projections equivalent to orthogonal projections embed into the corresponding finite orthogonal sum.

   theorem finite_join_subequivalence (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
       (p q : ℕ → M) (hp : ∀ n, IsStarProjection (p n))
       (hq : ∀ n, IsStarProjection (q n))
       (horth : ∀ i j, i ≠ j → q i * q j = 0)
       (hembed : ∀ n, ∃ v : PartialIso M, v.initial = p n ∧ v.final ≤ q n)
       (n : ℕ) :
       ∃ v : PartialIso M, v.final ≤ ∑ i ∈ Finset.range n, q i ∧
         (∀ i < n, p i ≤ v.initial) ∧
         ∀ r : M, IsStarProjection r → (∀ i < n, p i ≤ r) → v.initial ≤ r := by
   …