Column.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The triangular representation for the column estimate

The triangular representation is constructed and bounded directly. Haagerup's cyclic similarity theorem is isolated as the precise published input at the cyclic restriction step.

theorem OAI.KadisonKastler.innerDerivation_mul line 31
def OAI.KadisonKastler.representedInnerDerivation line 37
Source documentation
The represented commutator, with its boundedness proved from multiplication.
```
def representedInnerDerivation (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (h : H →L[ℂ] H) :
    A →L[ℂ] (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.representedInnerDerivation_apply line 49
def OAI.KadisonKastler.triangularMatrix line 53
def OAI.KadisonKastler.triangularRepresentation line 57
theorem OAI.KadisonKastler.triangularMatrix_decomposition line 90
theorem OAI.KadisonKastler.norm_triangularRepresentation_le_two line 98

def OAI.KadisonKastler.triangularHilbertRepresentation line 121

Source documentation

The same triangular homomorphism on the actual Hilbert direct sum.

def triangularHilbertRepresentation (ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (h : H →L[ℂ] H) (δ : ℝ) :
    A →ₐ[ℂ] (Generator.FiniteHilbert (Fin 2) H →L[ℂ] Generator.FiniteHilbert (Fin 2) H) :=
…

Mentions: OAI.Generator.FiniteHilbert

theorem OAI.KadisonKastler.norm_triangularHilbertRepresentation_le_two line 126
theorem OAI.KadisonKastler.triangularHilbertRepresentation_apply_upper line 134

def OAI.KadisonKastler.RepresentationCompletelyBoundedBy line 145

Source documentation

Complete bound for a Hilbert-space algebra representation.

def RepresentationCompletelyBoundedBy {K : Type v} [NormedAddCommGroup K]
    [InnerProductSpace ℂ K] [CompleteSpace K]
    (Φ : A →ₐ[ℂ] (K →L[ℂ] K)) (C : ℝ) : Prop :=
…

theorem OAI.KadisonKastler.RepresentationCompletelyBoundedBy.column_vector line 153

Source documentation

A complete bound controls the action of each column on a vector.

theorem RepresentationCompletelyBoundedBy.column_vector
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    {Φ : A →ₐ[ℂ] (K →L[ℂ] K)} {C : ℝ} (hcb : RepresentationCompletelyBoundedBy Φ C)
    (p : ℕ) (X : CStarMatrix (Fin p) (Fin 1) A) (ξ : K) :
    ‖WithLp.toLp 2 (fun i => Φ (X i 0) ξ)‖ ≤ C * ‖X‖ * ‖ξ‖ := by
…

Mentions: OAI.KadisonKastler.RepresentationCompletelyBoundedBy

theorem OAI.KadisonKastler.cyclic_column_coordinate_bound line 176

Source documentation

Restricting to a cyclic orbit and then keeping one coordinate does not increase a column bound.

theorem cyclic_column_coordinate_bound
    (Φ : A →ₐ[ℂ] (Generator.FiniteHilbert (Fin 2) H →L[ℂ]
      Generator.FiniteHilbert (Fin 2) H))
    (η : Generator.FiniteHilbert (Fin 2) H) {C : ℝ}
    (hcb : RepresentationCompletelyBoundedBy (restrictCyclicRepresentation Φ η) C)
    (p : ℕ) (X : CStarMatrix (Fin p) (Fin 1) A) :
    ‖WithLp.toLp 2 (fun i => Φ (X i 0) η 0)‖ ≤ C * ‖X‖ * ‖η‖ := by
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.RepresentationCompletelyBoundedBy, OAI.KadisonKastler.restrictCyclicRepresentation

def OAI.KadisonKastler.PublishedCyclicSimilarity line 196
Source documentation
Haagerup, Solution of the similarity problem for cyclic representations of C-algebras*, Ann. of Math. 118 (1983), Theorem 1.1 and its proof, pp. 217 and 225: a cyclic representation bounded by C is completely bounded by C³. This consequence is also stated explicitly in Pitts, Proc. Amer. Math. Soc. 136 (2008), 1757–1768, Remark 2.12 (arXiv:math/0609604, p. 6). Only this consequence is assumed.
```
def PublishedCyclicSimilarity : Prop :=
…
```
theorem OAI.KadisonKastler.triangular_cyclic_completelyBoundedBy line 203
theorem OAI.KadisonKastler.commutator_column_vector_bound line 223
Source documentation
Haagerup's cyclic bound controls the commutator column on every vector.
```
theorem commutator_column_vector_bound
    (hPublished : PublishedCyclicSimilarity.{u, v} (A := A))
…
```
theorem OAI.KadisonKastler.commutator_column_bound line 250
Source documentation
The manuscript's column-commutator estimate, conditional only on Haagerup's cyclic similarity theorem.
```
theorem commutator_column_bound
    (hPublished : PublishedCyclicSimilarity.{u, v} (A := A))
…
```
theorem OAI.KadisonKastler.commutator_column_norm_bound line 278
Source documentation
The intrinsic scalar norm of the commutator controls every finite column.
```
theorem commutator_column_norm_bound
    (hPublished : PublishedCyclicSimilarity.{u, v} (A := A))
…
```