FiniteDerivationColumns.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The finite-column passage from the uniform commutator estimate to complete boundedness of a derivation. The finite implementers need no uniform norm bound; only their scalar commutator bounds are used.

def OAI.KadisonSimilarity.ScalarKaplanskyClosure line 21
Source documentation
The scalar specialization of matrix Kaplansky density and the C*-quotient norm used in the final derivation argument (Blackadar, I.9.1.3).
```
def ScalarKaplanskyClosure (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (P : VonNeumannAlgebra H) : Prop :=
…
```
structure OAI.KadisonSimilarity.FiniteColumnImplementers line 27
Source documentation
Data obtained by implementing a derivation on finitely many cyclic summands, with strong convergence of the corresponding projections.
```
structure FiniteColumnImplementers (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (δ : A →L[ℂ] (H →L[ℂ] H)) (l : Filter I) where
…
```

theorem OAI.KadisonSimilarity.amplify_tendsto_apply line 37

Source documentation

Strong convergence is preserved by a fixed finite Hilbert amplification.

theorem amplify_tendsto_apply {l : Filter I} (Q : I → H →L[ℂ] H)
    (hQ : ∀ x, Tendsto (fun i => Q i x) l (𝓝 x)) (n : ℕ) (ξ : HilbertCopies H n) :
    Tendsto (fun i => amplify (Q i) n ξ) l (𝓝 ξ) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.matrix_finite_column_identity line 53

Source documentation

The finite-column commutator identity at every matrix level.

theorem matrix_finite_column_identity (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (δ : A →L[ℂ] (H →L[ℂ] H)) (V Q : H →L[ℂ] H)
    (hV : ∀ a, commutator V (σ a) = (δ a).comp Q)
    (n : ℕ) (X : Matrix (Fin n) (Fin n) A) :
    commutator (amplify V n) (matrixOperator (X.map σ)) =
      (matrixOperator (X.map δ)).comp (amplify Q n) := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixOperator

theorem OAI.KadisonSimilarity.derivation_completeBound_of_finite_columns line 65

Source documentation

A uniform matrix commutator estimate controls an arbitrary derivation once cyclic implementation has supplied its finite columns.

theorem derivation_completeBound_of_finite_columns {l : Filter I} [l.NeBot]
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (δ : A →L[ℂ] (H →L[ℂ] H))
    (P : VonNeumannAlgebra H) (hσ : ∀ a, σ a ∈ P)
    (kaplansky : ScalarKaplanskyClosure σ P)
    (columns : FiniteColumnImplementers σ δ l)
    {C : ℝ} (hC : 0 ≤ C) (estimate : CommutatorEstimate P C) :
    CompleteBound δ (C * ‖δ‖) := by
…

Mentions: OAI.KadisonSimilarity.ScalarKaplanskyClosure, OAI.KadisonSimilarity.FiniteColumnImplementers, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.CompleteBound