Projection.lean`

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Projection frames and faithful normalized vector projections.

def OAI.Kaplansky.projectionLine line 20
Source documentation
The actual one-dimensional subspace selected by a rank-one projection.
```
def projectionLine (p : projectionSpace d 1) : Submodule ℂ (EuclideanSpace ℂ (Fin d)) :=
…
```
Mentions: OAI.Kaplansky.projectionSpace
theorem OAI.Kaplansky.projectionLine_finrank line 23
def OAI.Kaplansky.projectionColumn line 29
Source documentation
The projected coordinate vector supplies a local frame wherever nonzero.
```
def projectionColumn (p : projectionSpace d 1) (i : Fin d) : EuclideanSpace ℂ (Fin d) :=
…
```
Mentions: OAI.Kaplansky.projectionSpace
theorem OAI.Kaplansky.projectionColumn_mem line 32
theorem OAI.Kaplansky.continuous_projectionColumn line 38
theorem OAI.Kaplansky.exists_projectionColumn_ne_zero line 44
def OAI.Kaplansky.projectionChartSet line 54
theorem OAI.Kaplansky.isOpen_projectionChartSet line 56
def OAI.Kaplansky.unitProjectionColumn line 59
theorem OAI.Kaplansky.unitProjectionColumn_norm line 62
theorem OAI.Kaplansky.unitProjectionColumn_mem line 66
theorem OAI.Kaplansky.continuousOn_unitProjectionColumn line 71
theorem OAI.Kaplansky.projectionLine_eq_span line 77
theorem OAI.Kaplansky.unitProjectionColumn_reconstruct line 84
Source documentation
The local frame gives the actual orthogonal coordinate formula on each line.
```
theorem unitProjectionColumn_reconstruct (p : projectionSpace d 1) (i : Fin d)
    (hi : p ∈ projectionChartSet i) (v : EuclideanSpace ℂ (Fin d)) (hv : v ∈ projectionLine p) :
    inner ℂ (unitProjectionColumn p i) v • unitProjectionColumn p i = v := by
…
```
Mentions: OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionChartSet, OAI.Kaplansky.projectionLine, OAI.Kaplansky.unitProjectionColumn
def OAI.Kaplansky.vectorOuter line 102
theorem OAI.Kaplansky.vectorOuter_hermitian line 105
theorem OAI.Kaplansky.unitVector_dot line 109
theorem OAI.Kaplansky.vectorOuter_idempotent line 116
theorem OAI.Kaplansky.vectorOuter_trace line 121
def OAI.Kaplansky.unitVectorProjection line 127
Source documentation
The ordinary rank-one orthogonal projector of a unit vector.
```
def unitVectorProjection (v : EuclideanSpace ℂ (Fin d)) (hv : ‖v‖=1) : projectionSpace d 1 :=
…
```
Mentions: OAI.Kaplansky.projectionSpace
theorem OAI.Kaplansky.continuous_vectorOuter line 131
theorem OAI.Kaplansky.projection_toEuclideanLin_symmetricProjection line 136
theorem OAI.Kaplansky.projectionLine_injective line 142
theorem OAI.Kaplansky.vectorOuter_toEuclideanLin line 157
theorem OAI.Kaplansky.unitVectorProjection_line line 162
def OAI.Kaplansky.nonzeroVectorProjection line 184
theorem OAI.Kaplansky.nonzeroVectorProjection_line line 187
theorem OAI.Kaplansky.continuousOn_normalizedOuter line 195
theorem OAI.Kaplansky.continuous_nonzeroVectorProjection line 202
Source documentation
The canonical rank-one projection is continuous in a nonzero vector.
```
theorem continuous_nonzeroVectorProjection :
    Continuous (fun v : {v : EuclideanSpace ℂ (Fin d) // v≠0} => nonzeroVectorProjection v.val v.property) :=
…
```
Mentions: OAI.Kaplansky.nonzeroVectorProjection