TracialMatrixSymmetrization.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The compact groups in free-product symmetrization are the actual matrix unitary groups. Their compatibility follows from the nested matrix embeddings and uniqueness of the trace-preserving extension on the two factors.

theorem OAI.KadisonSimilarity.commutator_unitaryConjugate_of_covariance line 24

Source documentation

Conjugation transports a commutator through its actual covariance.

theorem commutator_unitaryConjugate_of_covariance
    (U : Γ →* (H →L[ℂ] H)) (T B C : H →L[ℂ] H) (g : Γ)
    (hcov : U g⁻¹ * B = C * U g⁻¹) :
    commutator (unitaryConjugate U T g) B =
      unitaryConjugate U (commutator T C) g := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.unitaryConjugate

def OAI.KadisonSimilarity.TracialCornerGeometry.matrixStageUnitaryInclusion line 68
Source documentation
A nested matrix star embedding maps the compact unitary groups.
```
def matrixStageUnitaryInclusion (i j : ℕ) (h : i ≤ j) :
    Matrix.unitaryGroup (I i) ℂ →* Matrix.unitaryGroup (I j) ℂ :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.matrixStageUnitaryInclusion_embedding line 73

theorem OAI.KadisonSimilarity.TracialCornerGeometry.chosenMatrixExtension_compatible line 83

Source documentation

The ambient extension does not depend on the matrix stage used to represent the same unitary in the factor.

theorem chosenMatrixExtension_compatible (i j : ℕ) (h : i ≤ j)
    (u : Matrix.unitaryGroup (I i) ℂ) :
    G.chosenMatrixExtension A D (M.embedding j) (hext j)
        (G.matrixStageUnitaryInclusion D M i j h u) =
      G.chosenMatrixExtension A D (M.embedding i) (hext i) u := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryRepresentation_compatible line 102

Source documentation

Compatibility of the actual Hilbert-space representations is proved on dense algebra vectors.

theorem tracialMatrixUnitaryRepresentation_compatible (i j : ℕ) (h : i ≤ j)
    (u : Matrix.unitaryGroup (I i) ℂ) :
    G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext j
        (G.matrixStageUnitaryInclusion D M i j h u) =
      G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext i u := by
…

def OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryOperator line 117
Source documentation
Forgetting the unitary subtype gives the group homomorphism consumed by the weak Haar integral.
```
def tracialMatrixUnitaryOperator (j : ℕ) :
    Matrix.unitaryGroup (I j) ℂ →* (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryOperator_star line 123
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_tracialMatrixUnitaryOperator_le line 136
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryOperator_compatible line 148
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryOperator_fixes_base line 157
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryOperator_stronglyContinuous line 165
theorem OAI.KadisonSimilarity.TracialCornerGeometry.weaklyIntegrable_tracialMatrixUnitaryConjugate line 189
Source documentation
The weak integrability needed for the actual Haar average is a consequence of the proved strong continuity.
```
theorem weaklyIntegrable_tracialMatrixUnitaryConjugate (j : ℕ)
    (μ : Measure (Matrix.unitaryGroup (I j) ℂ)) [IsFiniteMeasure μ] (T : H →L[ℂ] H) :
    WeaklyIntegrable μ
      (unitaryConjugate (G.tracialMatrixUnitaryOperator A D M hgen hfaithful hext j) T) :=
…
```
Mentions: OAI.KadisonSimilarity.WeaklyIntegrable, OAI.KadisonSimilarity.unitaryConjugate
def OAI.KadisonSimilarity.TracialCornerGeometry.TraceCornerBound line 199
Source documentation
The original manuscript hypothesis is uniform over all projections of the selected trace in the other free factor.
```
def TraceCornerBound (T : H →L[ℂ] H) (t ε : ℝ) : Prop :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryConjugate_commutator line 204
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryConjugate_commutes_factor line 217
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryConjugate_cornerBound line 233
def OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixHaarProbability line 264
Source documentation
Actual normalized Haar measure of the finite matrix unitary group.
```
def tracialMatrixHaarProbability (j : ℕ) : Measure (Matrix.unitaryGroup (I j) ℂ) :=
…
```
instance OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixHaarProbability_probability line 267
instance OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixHaarProbability_leftInvariant line 272
def OAI.KadisonSimilarity.TracialCornerGeometry.traceCornerElements line 277
Source documentation
The test elements supported by a projection of the selected trace.
```
def traceCornerElements (t : ℝ) : Set P :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.exists_tracially_symmetrized line 285

Source documentation

Simultaneous compact averaging produces the exact additional symmetries used by word classification. It preserves the original base compression and the uniform corner bound. No invariant limiting operator is an input.

theorem exists_tracially_symmetrized (T : H →L[ℂ] H)
    (hTD : ∀ d : D, T.comp (G.left (d : P)) = (G.left (d : P)).comp T)
    {t ε : ℝ} (hε : 0 ≤ ε) (hcorner : G.TraceCornerBound D T t ε) :
    ∃ Y : H →L[ℂ] H,
      ‖Y‖ ≤ ‖T‖ ∧
      (∀ d : D, Y.comp (G.left (d : P)) = (G.left (d : P)).comp Y) ∧
      (∀ j w, Y.comp
          (G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext j w : H →L[ℂ] H) =
        (G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext j w : H →L[ℂ] H).comp Y) ∧
      G.TraceCornerBound D Y t ε ∧ G.baseOperator A Y = G.baseOperator A T := by
…