SmallFreeCornerData.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The small projection, its full matrix frame, the containing half projection, and the Haar unitary all belong to the same corner. The matrix frame is constructed from the tower. Only trace cutting and the local Haar existence statement are required for the two remaining choices.

structure OAI.KadisonSimilarity.SmallFreeCornerData line 21
Source documentation
The exact geometric data used in one application of the free-corner estimate. None of the fields mentions the operator being estimated.
```
structure SmallFreeCornerData (τ : P →ₗ[ℂ] ℂ) (s : ℝ) where
…
```
theorem OAI.KadisonSimilarity.exists_smallFreeCornerData line 39
Source documentation
The frame and its trace are chosen from an actual matrix stage. The half-projection and Haar hypotheses are the two local diffuse-corner facts, not any estimate for a commutator.
```
theorem exists_smallFreeCornerData (τ : P →ₗ[ℂ] ℂ) (V : P →ₗ[ℂ] H)
    (M : NestedTracialMatrices (A := I) τ V)
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices
def OAI.KadisonSimilarity.ThielDiffuseCornerHaarInput line 72
Source documentation
The local specialization of H. Thiel, Diffuse traces and Haar unitaries, arXiv:2009.06940v3, Proposition 7.2 and the following paragraph (printed p.20). A nonzero corner of a diffuse von Neumann algebra is diffuse; its normalized normal trace has a Haar unitary. The ambient trace is used here, since multiplying its vanishing moments by the normalization gives exactly HaarCornerMoments. This is an explicit conditional input.
```
def ThielDiffuseCornerHaarInput (τ : TracialRepresentation N) : Prop :=
…
```
theorem OAI.KadisonSimilarity.exists_concreteHaarCorner line 80
Source documentation
Package the cited Haar statement in precisely the normalization used by the propagation theorem.
```
theorem exists_concreteHaarCorner (τ : TracialRepresentation N)
    (published : ThielDiffuseCornerHaarInput τ)
    (q : N.toStarSubalgebra) (hq : IsStarProjection q)
    {t : ℝ} (ht : 0 < t) (htrace : τ.trace q = (t : ℂ)) :
    ∃ z : unitary (CStarCorner q hq),
      HaarCornerMoments (concreteTraceLinear τ) z t := by
…
```
Mentions: OAI.KadisonSimilarity.ThielDiffuseCornerHaarInput, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.concreteTraceLinear

theorem OAI.KadisonSimilarity.exists_concreteSmallFreeCornerData line 94

Source documentation

Trace cutting supplies the half projection in the concrete diffuse algebra, and the Haar input supplies the corner unitary.

theorem exists_concreteSmallFreeCornerData (τ : TracialRepresentation N)
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (published : ThielDiffuseCornerHaarInput τ)
    (V : N.toStarSubalgebra →ₗ[ℂ] H)
    (M : NestedTracialMatrices (A := I) (concreteTraceLinear τ) V)
…

Mentions: OAI.KadisonSimilarity.ThielDiffuseCornerHaarInput, OAI.KadisonSimilarity.NestedTracialMatrices, OAI.KadisonSimilarity.concreteTraceLinear