Comparison.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix comparison, block sums, and reindexing of positive matrices.

def OAI.Kaplansky.CuntzLE line 21
Source documentation
Rectangular Cuntz comparison: norm closure of actual conjugations. The finite product topology here is the topology of the C*-matrix norm.
```
def CuntzLE (a : Matrix ι ι A) (b : Matrix κ κ A) : Prop :=
…
```
theorem OAI.Kaplansky.CuntzLE.exact line 26
theorem OAI.Kaplansky.CuntzLE.refl line 29
theorem OAI.Kaplansky.CuntzLE.zero line 33
theorem OAI.Kaplansky.CuntzLE.isClosed line 36
theorem OAI.Kaplansky.CuntzLE.of_mem_closure line 39
theorem OAI.Kaplansky.CuntzLE.conjugate line 43
theorem OAI.Kaplansky.CuntzLE.trans line 51
theorem OAI.Kaplansky.CuntzLE.of_eq line 57
theorem OAI.Kaplansky.CuntzLE.le_zero_iff line 60

theorem OAI.Kaplansky.CuntzLE.iff_approx line 64

Source documentation

Explicit norm-approximation contract, using the actual C*-matrix norm.

theorem iff_approx [Fintype ι] (a : Matrix ι ι A) (b : Matrix κ κ A) :
    CuntzLE a b ↔ ∀ ε : ℝ, 0 < ε → ∃ v : Matrix ι κ A,
      ‖CStarMatrix.ofMatrix (a - v * b * v.conjTranspose)‖ < ε := by
…

Mentions: OAI.Kaplansky.CuntzLE

def OAI.Kaplansky.CuntzEquivalent line 78
Source documentation
Mutual actual rectangular comparison; no order or state is assumed.
```
def CuntzEquivalent (a : Matrix ι ι A) (b : Matrix κ κ A) : Prop :=
…
```
theorem OAI.Kaplansky.CuntzEquivalent.refl line 83
theorem OAI.Kaplansky.CuntzEquivalent.symm line 84
theorem OAI.Kaplansky.CuntzEquivalent.trans line 87

def OAI.Kaplansky.cuntzBlock line 103

Source documentation

Block addition before passing to Cuntz classes.

def cuntzBlock (a : Matrix ι ι A) (b : Matrix κ κ A) :
    Matrix (ι ⊕ κ) (ι ⊕ κ) A := Matrix.fromBlocks a 0 0 b

theorem OAI.Kaplansky.continuous_cuntzBlock line 106
theorem OAI.Kaplansky.cuntzBlock_conjugate line 114

theorem OAI.Kaplansky.CuntzLE.block line 122

Source documentation

Actual rectangular comparison is compatible with block addition.

theorem CuntzLE.block {a : Matrix ι ι A} {b : Matrix κ κ A}
    {c : Matrix ν ν A} {d : Matrix μ μ A} (hab : CuntzLE a b) (hcd : CuntzLE c d) :
    CuntzLE (cuntzBlock a c) (cuntzBlock b d) := by
…

Mentions: OAI.Kaplansky.CuntzLE, OAI.Kaplansky.cuntzBlock

theorem OAI.Kaplansky.CuntzEquivalent.block line 136
theorem OAI.Kaplansky.CuntzLE.submatrix line 152
Source documentation
Taking the same row and column submatrix is an actual rectangular conjugation.
```
theorem CuntzLE.submatrix (a : Matrix ι ι A) (f : κ → ι) :
    CuntzLE (a.submatrix f f) a := by
…
```
Mentions: OAI.Kaplansky.CuntzLE
theorem OAI.Kaplansky.cuntzEquivalent_submatrix_equiv line 169
Source documentation
Relabeling the finite coordinates preserves the actual Cuntz class.
```
theorem cuntzEquivalent_submatrix_equiv (a : Matrix ι ι A) (e : κ ≃ ι) :
    CuntzEquivalent (a.submatrix e e) a := by
…
```
Mentions: OAI.Kaplansky.CuntzEquivalent
theorem OAI.Kaplansky.cuntzLE_submatrix_equiv_iff line 174
theorem OAI.Kaplansky.cuntzEquivalent_block_zero line 180
Source documentation
Enlarging by an arbitrary zero corner does not change a Cuntz class.
```
theorem cuntzEquivalent_block_zero (a : Matrix ι ι A) :
    CuntzEquivalent (cuntzBlock a (0 : Matrix κ κ A)) a := by
…
```
Mentions: OAI.Kaplansky.CuntzEquivalent, OAI.Kaplansky.cuntzBlock
theorem OAI.Kaplansky.cuntzEquivalent_block_comm line 193
Source documentation
The permutation exchanging the blocks witnesses commutativity.
```
theorem cuntzEquivalent_block_comm (a : Matrix ι ι A) (b : Matrix κ κ A) :
    CuntzEquivalent (cuntzBlock a b) (cuntzBlock b a) := by
…
```
Mentions: OAI.Kaplansky.CuntzEquivalent, OAI.Kaplansky.cuntzBlock

theorem OAI.Kaplansky.cuntzEquivalent_block_assoc line 201

Source documentation

Rebracketing three blocks witnesses associativity.

theorem cuntzEquivalent_block_assoc (a : Matrix ι ι A) (b : Matrix κ κ A)
    (c : Matrix ν ν A) :
    CuntzEquivalent (cuntzBlock (cuntzBlock a b) c) (cuntzBlock a (cuntzBlock b c)) := by
…

Mentions: OAI.Kaplansky.CuntzEquivalent, OAI.Kaplansky.cuntzBlock

theorem OAI.Kaplansky.cuntzBlock_nonneg line 222
theorem OAI.Kaplansky.cuntzSubmatrix_nonneg line 248
theorem OAI.Kaplansky.cuntzLE_one_of_nonneg line 269
Source documentation
Every positive finite matrix is Cuntz below its own identity matrix. The witness is its actual positive square root.
```
theorem cuntzLE_one_of_nonneg [DecidableEq ι] (a : Matrix ι ι A) (ha : 0 ≤ CStarMatrix.ofMatrix a) :
    CuntzLE a (1 : Matrix ι ι A) := by
…
```
Mentions: OAI.Kaplansky.CuntzLE
structure OAI.Kaplansky.CuntzPositiveMatrix line 284
Source documentation
An actual positive matrix with a finite, explicitly stored size.
```
structure CuntzPositiveMatrix (A : Type*) [CStarAlgebra A] where
…
```
def OAI.Kaplansky.CuntzPositiveMatrix.zero line 291
def OAI.Kaplansky.CuntzPositiveMatrix.unit line 293
def OAI.Kaplansky.CuntzPositiveMatrix.add line 296
Source documentation
Actual block addition, relabeled by the standard finite-sum equivalence.
```
def add (a b : CuntzPositiveMatrix A) : CuntzPositiveMatrix A where
…
```
Mentions: OAI.Kaplansky.CuntzPositiveMatrix
instance OAI.Kaplansky.CuntzPositiveMatrix.(instance at line 301) line 301
theorem OAI.Kaplansky.CuntzPositiveMatrix.add_equiv line 306
theorem OAI.Kaplansky.CuntzPositiveMatrix.add_le_add line 310
theorem OAI.Kaplansky.CuntzPositiveMatrix.zero_le line 314
theorem OAI.Kaplansky.CuntzPositiveMatrix.le_unit line 316