ProperlyInfiniteEstimate.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The properly infinite commutator estimate. Internal orthogonal isometries supply the row, and Dickson supplies its actual commutator error bounds.

theorem OAI.KadisonSimilarity.norm_cstarMatrix_conjTranspose_le line 20
theorem OAI.KadisonSimilarity.norm_cstarMatrix_conjTranspose line 34
Source documentation
Rectangular conjugate transpose preserves the native C-star matrix norm.
```
theorem norm_cstarMatrix_conjTranspose {m n : Type*} [Fintype m] [Fintype n]
    (M : CStarMatrix m n A) : ‖M.conjTranspose‖ = ‖M‖ := by
…
```

theorem OAI.KadisonSimilarity.norm_cstar_isometry_adjoint_column_le_one line 44

Source documentation

The adjoint column of orthogonal internal isometries is contractive in the native C-star matrix norm.

theorem norm_cstar_isometry_adjoint_column_le_one {n : ℕ} (v : Fin n → A)
    (hv : ∀ i j, star (v i) * v j = if i = j then 1 else 0) :
    ‖CStarMatrix.ofMatrix (fun i (_ : Fin 1) => star (v i))‖ ≤ 1 := by
…

theorem OAI.KadisonSimilarity.norm_cstar_isometry_row_le_one line 75

Source documentation

The row of internal orthogonal isometries has native matrix norm at most one.

theorem norm_cstar_isometry_row_le_one {n : ℕ} (v : Fin n → A)
    (hv : ∀ i j, star (v i) * v j = if i = j then 1 else 0) :
    ‖CStarMatrix.ofMatrix (fun (_ : Fin 1) i => v i)‖ ≤ 1 := by
…

instance OAI.KadisonSimilarity.vonNeumannAlgebra_isClosed line 86
Source documentation
A von Neumann algebra is closed in the operator norm.
```
instance vonNeumannAlgebra_isClosed (P : VonNeumannAlgebra H) :
    IsClosed (P : Set (H →L[ℂ] H)) := by
…
```
instance OAI.KadisonSimilarity.vonNeumannAlgebra_smulMemClass line 92
def OAI.KadisonSimilarity.internalIsometryRow line 97
Source documentation
The actual row of a finite family of internal isometries.
```
def internalIsometryRow (P : VonNeumannAlgebra H) {n : ℕ} (v : Fin n → P) :
    HilbertCopies H n →L[ℂ] H := sumColumns (fun i => (v i : H →L[ℂ] H))
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.sumColumns
theorem OAI.KadisonSimilarity.internal_isometry_relation line 100
theorem OAI.KadisonSimilarity.internalIsometryRow_adjoint_self line 107
def OAI.KadisonSimilarity.vonNeumannRepresentation line 124
def OAI.KadisonSimilarity.vonNeumannInnerDerivation line 127
theorem OAI.KadisonSimilarity.vonNeumannInnerDerivation_apply line 131
theorem OAI.KadisonSimilarity.norm_vonNeumannInnerDerivation line 134
theorem OAI.KadisonSimilarity.internalIsometryRow_error line 140
Source documentation
Dickson's row estimate gives the actual error of the internal isometry row.
```
theorem internalIsometryRow_error (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H)
    (dickson : DicksonTwoBound (A := P) (RectangularSum H H))
…
```
Mentions: OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum
theorem OAI.KadisonSimilarity.internalIsometryRow_adjoint_error line 176
Source documentation
Dickson's column estimate gives the adjoint-row error independently of whether the operator being commuted is selfadjoint.
```
theorem internalIsometryRow_adjoint_error (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H)
    (dickson : DicksonTwoBound (A := P) (RectangularSum H H))
…
```
Mentions: OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum
theorem OAI.KadisonSimilarity.internalIsometryRow_compression_mem line 219
def OAI.KadisonSimilarity.HasInternalIsometryRows line 239
Source documentation
Existence of finite families of orthogonal isometries. For a properly infinite algebra this is supplied by its projection classification.
```
def HasInternalIsometryRows (P : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonSimilarity.properlyInfinite_commutatorEstimate line 244
Source documentation
The properly infinite estimate is derived from internal isometries and the published row/column estimate, with no row-error hypotheses.
```
theorem properlyInfinite_commutatorEstimate (P : VonNeumannAlgebra H)
    (isometries : HasInternalIsometryRows P)
    (dickson : DicksonTwoBound (A := P) (RectangularSum H H)) :
…
```
Mentions: OAI.KadisonSimilarity.HasInternalIsometryRows, OAI.KadisonSimilarity.DicksonTwoBound, OAI.KadisonSimilarity.RectangularSum