TracialSmallColumn.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The small vectors in propagation are actual left compressions of the completed base space. Scalar freeness gives their exact norm, first on algebra vectors and then throughout the completion by density.

theorem OAI.KadisonSimilarity.ScalarFree.trace_product line 20
Source documentation
Centered freeness gives the product trace formula for arbitrary letters from the two algebras.
```
theorem trace_product (hf : ScalarFree τ D A) (hτ : τ 1 = 1)
    {x y : P} (hx : x ∈ D) (hy : y ∈ A) : τ (x * y) = τ x * τ y := by
…
```
Mentions: OAI.KadisonSimilarity.ScalarFree
def OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn line 38
Source documentation
The actual small-column map is left multiplication by the projection, restricted to the completed base Hilbert space.
```
def tracialSmallColumn (q : P) : G.baseSpace A →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_apply line 41
theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_vector line 44

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_inner_base line 50

Source documentation

The exact inner-product scaling on bounded base-algebra vectors follows from the projection identity, traciality, and scalar freeness.

theorem tracialSmallColumn_inner_base (D : StarSubalgebra ℂ P)
    (hf : ScalarFree G.trace D A) (hτ : G.trace 1 = 1)
    (q : P) (hq : IsStarProjection q) (hqD : q ∈ D) (b c : A) :
    inner ℂ (G.tracialSmallColumn A q (G.baseVector A b))
      (G.tracialSmallColumn A q (G.baseVector A c)) =
        G.trace q * inner ℂ (G.baseVector A b) (G.baseVector A c) := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_inner line 68

Source documentation

The inner-product formula extends from bounded algebra vectors to the entire completed base space.

theorem tracialSmallColumn_inner (D : StarSubalgebra ℂ P)
    (hf : ScalarFree G.trace D A) (hτ : G.trace 1 = 1)
    (q : P) (hq : IsStarProjection q) (hqD : q ∈ D) (v w : G.baseSpace A) :
    inner ℂ (G.tracialSmallColumn A q v) (G.tracialSmallColumn A q w) =
      G.trace q * inner ℂ v w := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_tracialSmallColumn line 82

Source documentation

The small vectors have the exact square-root trace scaling. This is a consequence of freeness and density, not an additional word-model field.

theorem norm_tracialSmallColumn (D : StarSubalgebra ℂ P)
    (hf : ScalarFree G.trace D A) (hτ : G.trace 1 = 1)
    (q : P) (hq : IsStarProjection q) (hqD : q ∈ D)
    {a : ℝ} (ha : 0 ≤ a) (htrace : G.trace q = (a : ℂ)) (v : G.baseSpace A) :
    ‖G.tracialSmallColumn A q v‖ = Real.sqrt a * ‖v‖ := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_support line 102
Source documentation
The small column is supported by its defining projection.
```
theorem tracialSmallColumn_support (q : P) (hq : IsStarProjection q) :
    (G.left q).comp (G.tracialSmallColumn A q) = G.tracialSmallColumn A q := by
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_intertwines line 110

Source documentation

Commutation with the projection transfers the base action to the small column, giving the level-zero identity required by propagation.

theorem tracialSmallColumn_intertwines (q : P) (Y : H →L[ℂ] H)
    (B₀ : G.baseSpace A →L[ℂ] G.baseSpace A)
    (hbase : Y.comp (G.baseInclusion A).toContinuousLinearMap =
      (G.baseInclusion A).toContinuousLinearMap.comp B₀)
    (hcomm : Y.comp (G.left q) = (G.left q).comp Y) :
    Y.comp (G.tracialSmallColumn A q) = (G.tracialSmallColumn A q).comp B₀ := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialSmallColumn_level_zero line 123

Source documentation

Invariance of the actual base subspace identifies the level-zero operator with the actual compression of the ambient operator.

theorem tracialSmallColumn_level_zero (q : P) (Y : H →L[ℂ] H)
    (hbase : ∀ v ∈ G.baseSpace A, Y v ∈ G.baseSpace A)
    (hcomm : Y.comp (G.left q) = (G.left q).comp Y) (v : G.baseSpace A) :
    Y (G.tracialSmallColumn A q v) =
      G.tracialSmallColumn A q (G.baseOperator A Y v) := by
…