ControlledFreeHaar.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Free Haar unitaries with finite-matrix representatives

The two independence applications are combined with the actual quotient embedding and diagonal unitary lifts. The output keeps the finite matrix units in each coordinate, so the scalar derivation controls every lift.

def OAI.KadisonKastler.controlledScalarBase line 37
instance OAI.KadisonKastler.controlledScalarBaseFinite line 40
def OAI.KadisonKastler.finiteModelQuotientUnitary line 49
Source documentation
The represented unitary associated with a finite-model lift.
```
def finiteModelQuotientUnitary
    (E : ∀ j, Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
    (v : unitary (VaryingBoundedSequence (FiniteMatrixModel n))) : unitary C :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel
theorem OAI.KadisonKastler.finiteModelQuotientUnitary_conjugate line 59
Source documentation
Diagonal conjugation of the matrix units gives the exact conjugation of the represented model unitary.
```
theorem finiteModelQuotientUnitary_conjugate
    (E : ∀ j, Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
    (v : unitary (VaryingBoundedSequence (FiniteMatrixModel n)))
    (z : unitary (BoundedSequence (Algebra M))) (w : unitary C)
    (hz : R.quotient (concreteDiagonalSequence (n := n) (z : BoundedSequence _)) = (w : C)) :
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.concreteDiagonalSequence

theorem OAI.KadisonKastler.exists_freeHaar_conjugated_model line 80

Source documentation

The second independence application and the scalar commutant lift, with a fixed first model.

theorem exists_freeHaar_conjugated_model
    (hM : Generator.IsII1Factor M.toStarSubalgebra) (hτ : FiniteVectorTrace τ)
    (Qbase : TraceQuotientMap τ σB ω) (hindR : FiniteBaseIndependence σ)
    (E₀ : ∀ j, Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
    (v : unitary (VaryingBoundedSequence (FiniteMatrixModel n)))
    (hv : FreeHaarMoments σ (controlledScalarBase τ R) (finiteModelQuotientUnitary τ R E₀ v)) :
    ∃ E : ∀ j, Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M),
      FreeHaarMoments σ R.constant.range (finiteModelQuotientUnitary τ R E v) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.FiniteBaseIndependence, OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.controlledScalarBase, OAI.KadisonKastler.finiteModelQuotientUnitary

theorem OAI.KadisonKastler.swap_exists_models line 107
Source documentation
Eliminate the first lift in an abstract existential proposition, so no concrete finite-matrix representation is expanded by the eliminator.
```
private theorem swap_exists_models {V : Type*} {E : Type*} {P : V → Prop}
    {F : E → V → Prop} (hv : ∃ v, P v)
    (hf : ∀ v, P v → ∃ e, F e v) : ∃ e, ∃ v, F e v := by
…
```
theorem OAI.KadisonKastler.exists_controlled_freeHaar_from_model line 116
Source documentation
The two-stage construction, with the independence inputs specialized to the two quotient algebras actually used.
```
theorem exists_controlled_freeHaar_from_model
    (hM : Generator.IsII1Factor M.toStarSubalgebra) (hτ : FiniteVectorTrace τ)
    (Qbase : TraceQuotientMap τ σB ω) (Q : FiniteMatrixUltraproduct n ω)
    (hindQ : FiniteBaseIndependence (concreteFactorTrace Q.factor))
    (hindR : FiniteBaseIndependence σ) :
    ∃ E : ∀ j, Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M),
      ∃ v : unitary (VaryingBoundedSequence (FiniteMatrixModel n)),
        FreeHaarMoments σ R.constant.range
          (finiteModelQuotientUnitary τ R E v) := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.FiniteMatrixUltraproduct, OAI.KadisonKastler.FiniteBaseIndependence, OAI.KadisonKastler.concreteFactorTrace, OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.finiteModelQuotientUnitary
theorem OAI.KadisonKastler.exists_controlled_freeHaar line 133
Source documentation
The complete finite-matrix free lift, conditional only on the three specified published ultraproduct/independence inputs. All matrix units, embeddings, separability, scalar freeness, and unitary lifts are constructed.
```
theorem exists_controlled_freeHaar
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ Filter.atTop) :
    ∃ P : TracialUltrapower (matrixVonNeumannTrace (ι := Fin n) M (concreteFactorTrace hM)) ω,
…
```
Mentions: OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct, OAI.Generator.IsII1Factor, OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.matrixVonNeumannTrace, OAI.KadisonKastler.concreteFactorTrace