CanonicalFreeCornerCore.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The canonical free-corner estimate for a positive tracial algebra. The estimate is expressed through the generated algebra and its compressed tracial representation.

theorem OAI.KadisonSimilarity.canonicalFirstRange_closed line 29
theorem OAI.KadisonSimilarity.canonicalSecondRange_closed line 34
def OAI.KadisonSimilarity.canonicalSmallFrameCore line 46
Source documentation
Transport all small-frame data into the actual second range.
```
def canonicalSmallFrameCore {b : ℝ} (Q : SmallFreeCornerData τR.toLinearMap b) :
    SmallFreeCornerData ((G).baseGeometry D₀).trace b :=
…
```
Mentions: OAI.KadisonSimilarity.SmallFreeCornerData
abbrev OAI.KadisonSimilarity.CanonicalFreeCornerCoreInput line 60
Source documentation
The exact local structural input, with the native trace and faithfulness proofs supplied by the canonical generated model.
```
abbrev CanonicalFreeCornerCoreInput {b : ℝ}
    (_Q : SmallFreeCornerData ((G).baseGeometry D₀).trace b)
    (_x : A) (_hxsq : _x * _x = 1) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.SmallFreeCornerData

theorem OAI.KadisonSimilarity.canonical_free_corner_bound line 70

Source documentation

Apply the local theorem after the actual compression to the canonical algebra. The statement estimates the same compression used in recovery.

theorem canonical_free_corner_bound
    (hf : ScalarFree τ.toLinearMap φ.range ψ.range)
    (S : RealTracialSequence τR.toLinearMap)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    {b : ℝ} (Q : SmallFreeCornerData ((G).baseGeometry D₀).trace b)
    (x : A) (hxstar : star x = x) (hxsq : x * x = 1) (hx0 : τ (φ x) = 0)
    (published : CanonicalFreeCornerCoreInput τ htr φ ψ τR hψτ M hfτ Q x hxsq)
    (baseExpectation : Nonempty (TracialExpectation (G).trace A₀))
    (hnormal : ∃ N : VonNeumannAlgebra (canonicalGeneratedTrace τ htr φ ψ).GNS,
      (G).left.range = N.toStarSubalgebra)
    (T : τ.GNS →L[ℂ] τ.GNS)
    (hcomm : ∀ r, T.comp (τ.gnsStarAlgHom (ψ r)) =
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.SmallFreeCornerData, OAI.KadisonSimilarity.CanonicalFreeCornerCoreInput, OAI.KadisonSimilarity.TracialExpectation, OAI.KadisonSimilarity.canonicalGeneratedTrace