FinalDerivations.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The passage from the uniform commutator bound to similarity through cyclic summands and their finite-column implementers.

structure OAI.KadisonSimilarity.PublishedDerivationInputs line 20
Source documentation
Approximate cyclic column factorization for every cyclic representation.
```
structure PublishedDerivationInputs (A : Type u) [CStarAlgebra A]
    [PartialOrder A] [StarOrderedRing A] : Prop where
…
```
theorem OAI.KadisonSimilarity.publishedDerivationInputs line 27
Source documentation
The direct regularized-column construction supplies every cyclic case.
```
theorem publishedDerivationInputs : PublishedDerivationInputs.{u,v} A := by
…
```
def OAI.KadisonSimilarity.derivationColumn line 38
Source documentation
Restrict the source of an operator-valued derivation to a closed summand.
```
def derivationColumn (δ : A →L[ℂ] (H →L[ℂ] H)) (U : K →L[ℂ] H) :
    A →L[ℂ] (K →L[ℂ] H) :=
…
```
theorem OAI.KadisonSimilarity.derivationColumn_apply line 43

theorem OAI.KadisonSimilarity.derivationColumn_leibniz line 50

Source documentation

The Leibniz identity on a reducing summand follows from its intertwining inclusion, without requiring the summand to be faithful.

theorem derivationColumn_leibniz
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (τ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (δ : A →L[ℂ] (H →L[ℂ] H))
    (hδ : ∀ a b, δ (a * b) = (σ a).comp (δ b) + (δ a).comp (σ b))
    (U : K →L[ℂ] H) (hU : ∀ a, (σ a).comp U = U.comp (τ a)) (a b : A) :
    derivationColumn δ U (a * b) =
      (σ a).comp (derivationColumn δ U b) + (derivationColumn δ U a).comp (τ b) := by
…

Mentions: OAI.KadisonSimilarity.derivationColumn

theorem OAI.KadisonSimilarity.derivation_inner_of_uniformCommutator line 62

Source documentation

Uniform commutator control, Paulsen similarity and Kaplansky approximation imply that every bounded derivation is inner.

theorem derivation_inner_of_uniformCommutator
    (published : PublishedDerivationInputs.{u,v} A)
    {C : ℝ} (hC : 0 ≤ C) (estimate : UniformCommutatorEstimate.{v} C)
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (δ : A →L[ℂ] (H →L[ℂ] H))
    (hδ : ∀ a b, δ (a * b) = (σ a).comp (δ b) + (δ a).comp (σ b)) :
    ∃ V : H →L[ℂ] H, ∀ a, δ a = V.comp (σ a) - (σ a).comp V := by
…

theorem OAI.KadisonSimilarity.algebraSimilarityProperty_of_uniformCommutator line 95

Source documentation

Kirchberg's derivation criterion yields similarity for every bounded representation of the algebra.

theorem algebraSimilarityProperty_of_uniformCommutator
    (published : PublishedDerivationInputs.{u,v} A)
    (kirchberg : KirchbergDerivationCriterion.{u,v} A)
    {C : ℝ} (hC : 0 ≤ C) (estimate : UniformCommutatorEstimate.{v} C) :
    AlgebraSimilarityProperty.{u,v} A := by
…