Matrix.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Corner-compatible two-quasitraces on the usual CStarMatrix algebra and the fixed-pair counterexample proposition.

def OAI.Kaplansky.upperLeft line 16
Also declared: ComparatorChallenges/KaplanskyQuasitrace.lean:31 (same declaration text), ComparatorChallenges/KaplanskyStableFiniteness.lean:131 (same declaration text).
def OAI.Kaplansky.OneQuasitrace.IsTwo line 20
Source documentation
The extension is a 1-quasitrace, not a normalized 1-quasitrace.
Also declared: ComparatorChallenges/KaplanskyQuasitrace.lean:34 (same declaration text), ComparatorChallenges/KaplanskyStableFiniteness.lean:134 (same declaration text).
```
def OneQuasitrace.IsTwo (τ : OneQuasitrace A) : Prop :=
…
```
Mentions: OAI.Kaplansky.OneQuasitrace
def OAI.Kaplansky.PositiveContraction line 25
Source documentation
Positivity via an adjoint square is equivalent to C*-positivity; the norm bound is the actual contraction condition.
Also declared: ComparatorChallenges/KaplanskyQuasitrace.lean:37 (same declaration text).
```
def PositiveContraction (a : A) : Prop := (∃ x, a = star x * x) ∧ ‖a‖ ≤ 1
```
def OAI.Kaplansky.MainTarget line 27
Also declared: ComparatorChallenges/KaplanskyQuasitrace.lean:39 (same declaration text).
def OAI.Kaplansky.entry line 50
Source documentation
A single matrix entry with the C*-matrix norm.
```
def entry (i j : n) (a : A) : CStarMatrix n n A := CStarMatrix.ofMatrix (Matrix.single i j a)
```
def OAI.Kaplansky.corner line 51
def OAI.Kaplansky.diagonal line 52
theorem OAI.Kaplansky.entry_star line 55
theorem OAI.Kaplansky.entry_mul line 60
theorem OAI.Kaplansky.corner_star line 66
theorem OAI.Kaplansky.corner_mul line 67
theorem OAI.Kaplansky.corner_selfAdjoint line 70
theorem OAI.Kaplansky.corner_commute line 75
theorem OAI.Kaplansky.diagonal_eq_sum line 81
theorem OAI.Kaplansky.corner_square_swap line 85
theorem OAI.Kaplansky.corner_square_equal line 89
theorem OAI.Kaplansky.map_diagonal line 95