ConcreteHalfProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A small projection in an actual diffuse tracial von Neumann algebra can be completed to trace one half. The only projection-existence step is the proved exact-trace subprojection theorem.

def OAI.KadisonSimilarity.concreteTraceLinear line 23
Source documentation
The vector trace bundled only as the linear map needed by the half-projection construction.
```
def concreteTraceLinear (τ : TracialRepresentation M) : M.toStarSubalgebra →ₗ[ℂ] ℂ where
…
```
theorem OAI.KadisonSimilarity.concreteTraceLinear_apply line 31
theorem OAI.KadisonSimilarity.concreteTraceLinear_one line 34

theorem OAI.KadisonSimilarity.exists_concreteHalfTraceProjectionData line 39

Source documentation

Exact trace cutting in the orthogonal complement supplies the missing part of a half-trace projection.

theorem exists_concreteHalfTraceProjectionData (τ : TracialRepresentation M)
    (hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (e : M.toStarSubalgebra) (he : IsStarProjection e)
    {t : ℝ} (hetrace : τ.trace e = (t : ℂ)) (ht : t ≤ 1 / 2) :
    Nonempty (HalfTraceProjectionData (concreteTraceLinear τ) e) := by
…

Mentions: OAI.KadisonSimilarity.HalfTraceProjectionData, OAI.KadisonSimilarity.concreteTraceLinear

def OAI.KadisonSimilarity.concreteHalfTraceProjectionData line 67

Source documentation

A concrete choice of the half projection used to make the centered reflection in the finite-factor argument.

def concreteHalfTraceProjectionData (τ : TracialRepresentation M)
    (hdiff : ∀ p : M.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : M.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (e : M.toStarSubalgebra) (he : IsStarProjection e)
    {t : ℝ} (hetrace : τ.trace e = (t : ℂ)) (ht : t ≤ 1 / 2) :
    HalfTraceProjectionData (concreteTraceLinear τ) e :=
…

Mentions: OAI.KadisonSimilarity.HalfTraceProjectionData, OAI.KadisonSimilarity.concreteTraceLinear