ProperlyInfiniteColumns.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Properly infinite projections from orthogonal columns

Countably many equivalent orthogonal projections split into even and odd columns. The resulting operators are actual partial isometries in the algebra.

def OAI.BoundedHochschild.KadisonRingrose.ProperlyInfiniteProjection line 24
Source documentation
A projection admits two orthogonal copies of itself inside itself.
```
def ProperlyInfiniteProjection (p : M) : Prop :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.column_transition_initial line 29
def OAI.BoundedHochschild.KadisonRingrose.columnTransition line 36
lemma OAI.BoundedHochschild.KadisonRingrose.columnTransition_initial line 45
lemma OAI.BoundedHochschild.KadisonRingrose.columnTransition_final line 49
lemma OAI.BoundedHochschild.KadisonRingrose.projection_le_complement_of_mul_zero line 57

theorem OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_of_columns line 66

Source documentation

The supremum of countably many equivalent orthogonal projections is properly infinite. Only the particular even/odd shift operators are needed.

theorem properlyInfinite_of_columns (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {p : M} (c : ℕ → PartialIso M) (hi : ∀ i, (c i).initial = p)
    (ho : ∀ i j, i ≠ j → (c i).final * (c j).final = 0) :
    ∃ q : M, IsStarProjection q ∧ ProperlyInfiniteProjection q ∧
      (∀ i, (c i).final ≤ q) ∧
      (∀ r : M, IsStarProjection r → (∀ i, (c i).final ≤ r) → q ≤ r) := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.ProperlyInfiniteProjection

theorem OAI.BoundedHochschild.KadisonRingrose.nonunitary_isometry_has_properlyInfinite_projection line 111
Source documentation
A nonunitary isometry produces a nonzero properly infinite projection.
```
theorem nonunitary_isometry_has_properlyInfinite_projection
    (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) {v : M} (hv : star v * v = 1)
    (hnot : v * star v ≠ 1) :
    ∃ q : M, IsStarProjection q ∧ q ≠ 0 ∧ ProperlyInfiniteProjection q := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.ProperlyInfiniteProjection