ProjectionFrameCoordinates.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fixed Hilbert coordinates on each measurable rank stratum

def OAI.KadisonKastler.finiteFrameIndexEquiv line 14
Source documentation
Increasing enumeration identifies a finite rank stratum with Fin n.
```
def finiteFrameIndexEquiv (p : ℕ → Prop) (n : ℕ)
    (h : ∀ k, frameIndexAvailable p k ↔ k < n) : Fin n ≃ {m // p m} :=
…
```
Mentions: OAI.KadisonKastler.frameIndexAvailable
def OAI.KadisonKastler.infiniteFrameIndexEquiv line 23
Source documentation
Increasing enumeration identifies an infinite rank stratum with ℕ.
```
def infiniteFrameIndexEquiv (p : ℕ → Prop) (h : ∀ k, frameIndexAvailable p k) :
    ℕ ≃ {m // p m} :=
…
```
Mentions: OAI.KadisonKastler.frameIndexAvailable
theorem OAI.KadisonKastler.finiteFrameIndexEquiv_val line 31
theorem OAI.KadisonKastler.infiniteFrameIndexEquiv_val line 35
def OAI.KadisonKastler.reindexedHilbertBasis line 43
Source documentation
Reindex a Hilbert basis while retaining its concrete vectors.
```
def reindexedHilbertBasis (b : HilbertBasis I ℂ H) (e : J ≃ I) : HilbertBasis J ℂ H :=
…
```
theorem OAI.KadisonKastler.reindexedHilbertBasis_apply line 47
def OAI.KadisonKastler.finiteProjectionBasis line 55
Source documentation
The finite-dimensional coordinate basis on the rank n stratum.
```
def finiteProjectionBasis (n : ℕ) (x : X)
    (hx : x ∈ frameDimensionStratum (fun x i => measurableProjectionFrame P b x i ≠ 0) (n + 1)) :
    HilbertBasis (Fin n) ℂ (P x).range := by
…
```
Mentions: OAI.KadisonKastler.frameDimensionStratum, OAI.KadisonKastler.measurableProjectionFrame
def OAI.KadisonKastler.infiniteProjectionBasis line 64
Source documentation
The infinite-dimensional coordinate basis on the infinite rank stratum.
```
def infiniteProjectionBasis (x : X)
    (hx : x ∈ frameDimensionStratum (fun x i => measurableProjectionFrame P b x i ≠ 0) 0) :
    HilbertBasis ℕ ℂ (P x).range := by
…
```
Mentions: OAI.KadisonKastler.frameDimensionStratum, OAI.KadisonKastler.measurableProjectionFrame
theorem OAI.KadisonKastler.finiteProjectionBasis_coe line 72
theorem OAI.KadisonKastler.infiniteProjectionBasis_coe line 81