OAI/Analysis/KadisonSimilarity/Derivation/DerivationEndgame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.derivation_inner_of_finite_columns line 20

   Source documentation

   Finite cyclic column implementers, uniform commutator control and Paulsen similarity give an implementer for the whole derivation.

   theorem derivation_inner_of_finite_columns {l : Filter I} [l.NeBot]
       (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (δ : A →L[ℂ] (H →L[ℂ] H))
       (hδ : ∀ a b, δ (a * b) = (σ a).comp (δ b) + (δ a).comp (σ b))
       (P : VonNeumannAlgebra H) (hP : ∀ a, σ a ∈ P)
       (kaplansky : TwoVectorKaplanskyInput σ P)
       (columns : FiniteColumnImplementers σ δ l)
       {C : ℝ} (hC : 0 ≤ C) (estimate : CommutatorEstimate P C)
       (paulsen : PaulsenSimilarityInput (normalizedRectangularRepresentation σ σ δ hδ)) :
       ∃ V : H →L[ℂ] H, ∀ a, δ a = V.comp (σ a) - (σ a).comp V := by
   …

   Mentions: OAI.KadisonSimilarity.TwoVectorKaplanskyInput, OAI.KadisonSimilarity.FiniteColumnImplementers, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.PaulsenSimilarityInput, OAI.KadisonSimilarity.normalizedRectangularRepresentation

2. theorem OAI.KadisonSimilarity.universalHyperreflexivity_of_uniformCommutator line 40

   Source documentation

   The uniform commutator theorem implies quantitative hyperreflexivity using spectral step approximation and Arveson's distance formula.

   theorem universalHyperreflexivity_of_uniformCommutator
       {C : ℝ} (hC : 0 ≤ C) (estimate : UniformCommutatorEstimate.{u} C)
       (spectral : ∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
         [CompleteSpace K] (M : VonNeumannAlgebra K), SpectralStepApproximation M.commutant)
       (arveson : ∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
         [CompleteSpace K] (M : VonNeumannAlgebra K) (T : K →L[ℂ] K), ArvesonDistanceFormula M T) :
       UniversalHyperreflexivity.{u} C := by
   …

   Mentions: OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.ArvesonDistanceFormula