ProjectionCorner.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Unital C⋆ structure and unitary paths in a projection corner

The corner has unit q; its inclusion in the ambient algebra is nonunital. A corner unitary becomes an ambient unitary by adding 1-q, preserving norm differences and therefore the quantitative path estimates.

def OAI.WeakPureInfiniteness.projectionCornerAlgebra line 19
lemma OAI.WeakPureInfiniteness.projectionCornerAlgebra_closed line 30
abbrev OAI.WeakPureInfiniteness.ProjectionCorner line 36
Source documentation
The closed supported corner, equipped below with unit q.
```
abbrev ProjectionCorner (q : E) (hq : star q = q) (_hqq : q * q = q) : Type _ :=
…
```
instance OAI.WeakPureInfiniteness.projectionCornerClosed line 39
instance OAI.WeakPureInfiniteness.projectionCornerSemiring line 42
instance OAI.WeakPureInfiniteness.projectionCornerRing line 50
instance OAI.WeakPureInfiniteness.projectionCornerNormedRing line 56
instance OAI.WeakPureInfiniteness.projectionCornerAlgebraStructure line 62
instance OAI.WeakPureInfiniteness.projectionCornerNormedAlgebra line 67
instance OAI.WeakPureInfiniteness.projectionCornerCStarAlgebra line 72
instance OAI.WeakPureInfiniteness.projectionCornerNontrivial line 84
def OAI.WeakPureInfiniteness.projectionCornerInclusion line 92
Source documentation
The algebra inclusion sends the corner unit to q.
```
def projectionCornerInclusion (q : E) (hq : star q = q) (hqq : q * q = q) :
    ProjectionCorner q hq hqq →⋆ₙₐ[ℂ] E where
…
```
Mentions: OAI.WeakPureInfiniteness.ProjectionCorner
lemma OAI.WeakPureInfiniteness.projectionCornerInclusion_one line 101
def OAI.WeakPureInfiniteness.projectionCornerUnitary line 105
Source documentation
Extending by the complementary identity gives an ambient unitary.
```
def projectionCornerUnitary (q : E) (hq : star q = q) (hqq : q * q = q)
    (u : unitary (ProjectionCorner q hq hqq)) : unitary E := by
…
```
Mentions: OAI.WeakPureInfiniteness.ProjectionCorner
lemma OAI.WeakPureInfiniteness.projectionCornerUnitary_one line 128
lemma OAI.WeakPureInfiniteness.projectionCornerUnitary_continuous line 134
lemma OAI.WeakPureInfiniteness.projectionCornerUnitary_sub_norm line 141

lemma OAI.WeakPureInfiniteness.projectionCornerPath_controlled line 152

Source documentation

Quantitative paths lift to the ambient algebra with no loss.

lemma projectionCornerPath_controlled (q : E) (hq : star q = q) (hqq : q * q = q)
    {u v : unitary (ProjectionCorner q hq hqq)}
    (p : Path u v) (L : ℝ)
    (hp : ∀ a b, ‖(p a : ProjectionCorner q hq hqq) - p b‖ ≤ L * |(a : ℝ) - b|) :
    ∃ r : Path (projectionCornerUnitary q hq hqq u) (projectionCornerUnitary q hq hqq v),
      ∀ a b, ‖(r a : E) - r b‖ ≤ L * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.ProjectionCorner, OAI.WeakPureInfiniteness.projectionCornerUnitary