FiniteFactorApplication.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-factor application of the free-corner argument

The local hypotheses below specify the actual increasing-matrix inclusion, its normal represented closure, and the published projection and free-product inputs. The commutator estimates combine Haar averaging, the free-corner theorem, and the exact finite and countable amplification transfers.

structure OAI.KadisonSimilarity.FiniteFactorFreeCornerInputs line 44
Source documentation
Exact remaining structural inputs for the fixed finite-factor application. Only the free position remains explicit. Stage commutation, source and generated-factor comparison, rounding and diffuse corners are constructed from the faithful normal traces and the dense matrix tower.
```
structure FiniteFactorFreeCornerInputs : Prop where
…
```

theorem OAI.KadisonSimilarity.finite_standard_bound_of_local_free_corner line 57

Source documentation

The paper's finite-standard-multiplicity estimate. The centered test is proved from the local free-corner theorem after extending stage commutation by the actual trace-vector density.

theorem finite_standard_bound_of_local_free_corner
    (inputs : FiniteFactorFreeCornerInputs τR τB hR hB ω trR trB ρ hρτ hω)
    (source_normalR : τR.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τR.gnsStarAlgHom).toStarSubalgebra)
    (source_normal : τB.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τB.gnsStarAlgHom).toStarSubalgebra)
    (S : RealTracialSequence τR.toLinearMap)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    {r : ℕ} (Y : HilbertCopies τB.GNS r →L[ℂ] HilbertCopies τB.GNS r)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : ∀ a, ‖commutator Y (amplify (τB.gnsStarAlgHom a) r)‖ ≤ δ * ‖a‖)
    (h : ℕ) (X : CStarMatrix (Fin h) (Fin h) B) :
…

Mentions: OAI.KadisonSimilarity.FiniteFactorFreeCornerInputs, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.normal_bound_of_local_free_corner line 101

Source documentation

The same finite-factor bound in an arbitrary supplied normal representation, with no increase of the finite-standard constant.

theorem normal_bound_of_local_free_corner
    (inputs : FiniteFactorFreeCornerInputs τR τB hR hB ω trR trB ρ hρτ hω)
    (source_normalR : τR.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τR.gnsStarAlgHom).toStarSubalgebra)
    (source_normal : τB.gnsStarAlgHom.range =
      (representationVonNeumannAlgebra τB.gnsStarAlgHom).toStarSubalgebra)
    (S : RealTracialSequence τR.toLinearMap)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop)
    (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (embedding : HiaiNormalStandardEmbeddingInput τB σ)
    (Y : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : ∀ a, ‖commutator Y (σ a)‖ ≤ δ * ‖a‖)
…

Mentions: OAI.KadisonSimilarity.FiniteFactorFreeCornerInputs, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.RealTracialSequence, OAI.KadisonSimilarity.HiaiNormalStandardEmbeddingInput, OAI.KadisonSimilarity.commutator