ProjectionSchroederBernstein.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Schroeder--Bernstein for concrete projection equivalence

The proof constructs the unilateral shift on the iterated defect of a partial isometry, then adds the identity on its orthogonal complement. The construction uses the existing strong sums of partial isometries; no finiteness or trace assumption occurs.

theorem OAI.Generator.Tracial.PartialIsometry.power_initial line 24
theorem OAI.Generator.Tracial.PartialIsometry.defect_mul line 40
theorem OAI.Generator.Tracial.PartialIsometry.defect_mul_pow line 47
def OAI.Generator.Tracial.PartialIsometry.defectOrbit line 53
theorem OAI.Generator.Tracial.PartialIsometry.defectOrbit_target_le line 73
theorem OAI.Generator.Tracial.PartialIsometry.defectOrbit_zero line 90
theorem OAI.Generator.Tracial.PartialIsometry.defectOrbit_cross line 99
theorem OAI.Generator.Tracial.PartialIsometry.defectOrbit_orthogonal line 119
theorem OAI.Generator.Tracial.PartialIsometry.defect_copies line 140
Source documentation
A partial isometry whose range lies in its source has orthogonal copies of its defect, all lying under the original source projection.
```
theorem defect_copies (v : PartialIsometry M) (h : v.target ≤ v.support) :
    ∃ a : ℕ → PartialIsometry M,
      (∀ n, (a n).support = AlgebraProjection.remainder v.target v.support h) ∧
      (∀ n, (a n).target ≤ v.support) ∧
      Pairwise (fun i j => (a i).target.val * (a j).target.val = 0) :=
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection.remainder, OAI.Generator.Tracial.PartialIsometry.target
theorem OAI.Generator.Tracial.PartialIsometry.equivalent_intermediate line 151
Source documentation
A projection between the initial and final projections of a partial isometry is equivalent to the initial projection. This is the shift form of projection Schroeder--Bernstein.
```
theorem equivalent_intermediate (v : PartialIsometry M) (p : AlgebraProjection M)
    (ht : v.target ≤ p) (hp : p ≤ v.support) : v.support.Equivalent p := by
…
```
Mentions: OAI.Generator.Tracial.PartialIsometry, OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.AlgebraProjection.equivalent_of_le_of_subequivalent line 227
Source documentation
Comparable projections satisfy Schroeder--Bernstein without any finite trace or finite-isometry assumption.
```
theorem equivalent_of_le_of_subequivalent {p q : AlgebraProjection M}
    (hpq : p ≤ q) (hqp : q.Subequivalent p) : p.Equivalent q := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection
theorem OAI.Generator.Tracial.AlgebraProjection.schroederBernstein line 235
Source documentation
Murray--von Neumann Schroeder--Bernstein in the concrete algebra.
```
theorem schroederBernstein {p q : AlgebraProjection M}
    (hpq : p.Subequivalent q) (hqp : q.Subequivalent p) : p.Equivalent q := by
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection