ProjectionDimensionStrata.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Measurable trivializations of projection ranges on dimension strata

def OAI.KadisonKastler.projectionDimensionIndex line 15
Source documentation
A fixed countable index type for each dimension stratum.
```
def projectionDimensionIndex : ℕ → Type
  | 0 => ℕ
  | n + 1 => Fin n
```
instance OAI.KadisonKastler.projectionDimensionIndex_countable line 19
def OAI.KadisonKastler.projectionDimensionIndexNat line 22
def OAI.KadisonKastler.projectionRankStratum line 30
def OAI.KadisonKastler.projectionStratumBasis line 34
Source documentation
A basis with a fixed index set on the whole dimension stratum.
```
def projectionStratumBasis (n : ℕ) (x : projectionRankStratum P b n) :
    HilbertBasis (projectionDimensionIndex n) ℂ (P x.val).range := by
…
```
Mentions: OAI.KadisonKastler.projectionRankStratum, OAI.KadisonKastler.projectionDimensionIndex
theorem OAI.KadisonKastler.projectionStratumBasis_coe line 40
def OAI.KadisonKastler.projectionStratumCoordinates line 49
Source documentation
The coordinate unitary uses the same target Hilbert space throughout a stratum.
```
def projectionStratumCoordinates (n : ℕ) (x : projectionRankStratum P b n) :
    (P x.val).range ≃ₗᵢ[ℂ] ℓ²(projectionDimensionIndex n, ℂ) :=
…
```
Mentions: OAI.KadisonKastler.projectionRankStratum, OAI.KadisonKastler.projectionDimensionIndex
theorem OAI.KadisonKastler.measurableSet_projectionRankStratum line 56
theorem OAI.KadisonKastler.projectionStratumBasis_measurable line 62
theorem OAI.KadisonKastler.projectionStratumCoordinates_measurable line 70
theorem OAI.KadisonKastler.projectionStratumCoordinates_symm_measurable line 80