MatrixFreeCornerApplication.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The free-corner estimate for an actual matrix GNS operator

The matrix subfactor is the entrywise image of the original inclusion. Projection comparison transports the scalar bound to all sufficiently small matrix corners. Popa's local conjugacy input chooses the free copy, while all native GNS geometry is the canonical generated geometry. The remaining local input consists exactly of the published structural data for that geometry; it contains no commutator bound.

abbrev OAI.KadisonSimilarity.MatrixFreeCornerLocalInput line 52
Source documentation
The exact local published bundle on the canonical matrix free-product model. This abbreviation only fixes the generated geometry and transported frame; it does not assert the existence of any of its fields.
```
abbrev MatrixFreeCornerLocalInput
    (u : unitary (Ultrapower τRn hRn ω trRn))
    (x : CStarMatrix (Fin n) (Fin n) B) (hxsq : x * x = 1) : Prop :=
…
```

theorem OAI.KadisonSimilarity.matrixFreeCornerLocalInput_of_normal_source line 63

Source documentation

Construct the actual matrix free-product comparison from the normal source and its matrix tower.

theorem matrixFreeCornerLocalInput_of_normal_source
    (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
    (hsource : τR.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τR.gnsStarAlgHom).toStarSubalgebra)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (u : unitary (Ultrapower τRn hRn ω trRn))
    (hf : ScalarFree (quotientTrace τBn hBn ω trBn).toLinearMap
      (constant τBn hBn ω trBn).range (ψ u).range)
    (x : CStarMatrix (Fin n) (Fin n) B) (hxsq : x * x = 1) :
    MatrixFreeCornerLocalInput τR τB hR hB ω trR trB ρ hρτ hfR n M Q u x hxsq :=
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.MatrixFreeCornerLocalInput

theorem OAI.KadisonSimilarity.matrix_symmetry_bound_of_local_free_corner line 80

Source documentation

The matrix GNS centered-symmetry estimate, derived from projection comparison, the free-position input and the structural local bundles.

theorem matrix_symmetry_bound_of_local_free_corner
    (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
    (popa : Popa1995ConjugateFreenessInput τRn τBn hRn hBn ω trRn trBn
      ρn hρn hω (matrixDiagonalHom n))
    (S : RealTracialSequence τR.toLinearMap)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (comparison : FiniteFactorProjectionComparison
      (fun X : CStarMatrix (Fin n) (Fin n) R => (τRn X).re))
    (rounding : SpectralProjectionRoundingInput τRn)
    (source_normal : τB.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τB.gnsStarAlgHom).toStarSubalgebra)
    (published : ∀ (u : unitary (Ultrapower τRn hRn ω trRn)),
…

Mentions: OAI.KadisonSimilarity.Popa1995ConjugateFreenessInput, OAI.KadisonSimilarity.matrixDiagonalHom, OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.SpectralProjectionRoundingInput, OAI.KadisonSimilarity.representationVonNeumannAlgebra