ConcreteFullColumn.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The full-column estimate in the concrete tracial Hilbert space.

theorem OAI.KadisonSimilarity.mapCopies_single line 18

theorem OAI.KadisonSimilarity.extend_column line 25

Source documentation

Diagonal extension agrees with the given corner map on every column.

theorem extend_column
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (Lr : P →⋆ₐ[ℂ] (D →L[ℂ] D))
    (ρ : C →⋆ₐ[ℂ] (F →L[ℂ] F)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K))
    {n : ℕ} (U : FiniteOrthogonalColumns F H n) (V : FiniteOrthogonalColumns K D n)
    (entry : P → Matrix (Fin n) (Fin n) C)
    (hU : ∀ a i j, ρ (entry a i j) =
      (U.inclusion i).adjoint.comp ((L a).comp (U.inclusion j)))
    (hV : ∀ a i j, σ (entry a i j) =
      (V.inclusion i).adjoint.comp ((Lr a).comp (V.inclusion j)))
    (T : K →L[ℂ] F) (i : Fin n) (x : K) :
    (fullColumnCoordinatesOfColumns L Lr ρ σ U V entry hU hV).extend T
      (V.inclusion i x) = U.inclusion i (T x) := by
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns, OAI.KadisonSimilarity.fullColumnCoordinatesOfColumns

theorem OAI.KadisonSimilarity.FiniteOrthogonalColumns.ext_on_columns line 43
Source documentation
Equality on a complete finite family of columns determines an operator.
```
theorem FiniteOrthogonalColumns.ext_on_columns {n : ℕ}
    (V : FiniteOrthogonalColumns K D n) (S T : D →L[ℂ] H)
    (h : ∀ i x, S (V.inclusion i x) = T (V.inclusion i x)) : S = T := by
…
```
Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns

theorem OAI.KadisonSimilarity.TracialCornerGeometry.inclusion_cornerRestriction line 61

Source documentation

Commutation with the left corner projection makes output compression exact.

theorem inclusion_cornerRestriction (Y : H →L[ℂ] H)
    (hYe : Y.comp (G.left e) = (G.left e).comp Y) (x : G.corner e r) :
    ((G.cornerRestriction e r Y x : G.corner e 1) : H) = Y (x : H) := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.extend_cornerRestriction line 73

Source documentation

Matrix commutation extends the actual compressed operator to the full column.

theorem extend_cornerRestriction (hr : IsStarProjection r) {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1)
    (Y : H →L[ℂ] H) (hYe : Y.comp (G.left e) = (G.left e).comp Y)
    (hYv : ∀ i, Y.comp (G.left (v i)) = (G.left (v i)).comp Y) :
    (G.fullColumnCoordinates e he r hr v hv hsum).extend
      (G.cornerRestriction e r Y) = Y.comp (G.corner 1 r).toSubmodule.subtypeL := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.full_column line 99

Source documentation

The paper's full-column conclusion, with all corner representations and matrix coordinates constructed from the tracial geometry. Its only analytic inputs are the explicitly cited cyclic results and tracial commutation.

theorem full_column
    (hfaithful : Function.Injective G.vector)
    (τ : P → ℝ) (comparison : FiniteFactorProjectionComparison τ)
    (hr : IsStarProjection r) (hτ : τ r ≤ τ e)
    {n : ℕ} (hn : 0 < n) (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1)
    (Y : H →L[ℂ] H) (hYe : Y.comp (G.left e) = (G.left e).comp Y)
    (hYv : ∀ i, Y.comp (G.left (v i)) = (G.left (v i)).comp Y)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hY : ∀ a : CStarCorner e he, ‖commutator Y (G.left (a : P))‖ ≤ ε * ‖a‖)
    (published : PublishedDerivationInputs.{u,v} (CStarCorner e he))
…

Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.commutator