Spectral.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Spectral candidates on squares, orthogonal elements, and complex elements.

theorem OAI.Kaplansky.CuntzDimensionState.distribution_rectangular_gram line 30

Source documentation

The spectral distributions of rectangular Gram matrices agree at all strictly positive thresholds, not just on the uncut matrices.

theorem distribution_rectangular_gram (d : CuntzDimensionState A) {n m : ℕ}
    (x : Matrix (Fin n) (Fin m) A) (ha : 0 ≤ CStarMatrix.ofMatrix (x*x.conjTranspose))
    (hb : 0 ≤ CStarMatrix.ofMatrix (x.conjTranspose*x)) {t : ℝ} (ht : 0 < t) :
    d.distribution ⟨n, x*x.conjTranspose, ha⟩ t =
      d.distribution ⟨m, x.conjTranspose*x, hb⟩ t :=
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_rectangular_gram line 38

Source documentation

The spectral integral satisfies square swapping in unequal sizes.

theorem spectralValue_rectangular_gram (d : CuntzDimensionState A) {n m : ℕ}
    (x : Matrix (Fin n) (Fin m) A) (ha : 0 ≤ CStarMatrix.ofMatrix (x*x.conjTranspose))
    (hb : 0 ≤ CStarMatrix.ofMatrix (x.conjTranspose*x)) :
    d.spectralValue ⟨n, x*x.conjTranspose, ha⟩ =
      d.spectralValue ⟨m, x.conjTranspose*x, hb⟩ := by
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_square_swap line 54

Source documentation

In particular, the original square-swap axiom holds on the positive squares.

theorem spectralValue_square_swap (d : CuntzDimensionState A) {n : ℕ}
    (x : CStarMatrix (Fin n) (Fin n) A) :
    d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (x*star x), mul_star_self_nonneg x⟩ =
      d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (star x*x), star_mul_self_nonneg x⟩ :=
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.exists_orthogonal_sum_gram line 64

Source documentation

An orthogonal positive sum and its diagonal block form are exactly the two Gram matrices of a rectangular matrix of square roots.

theorem exists_orthogonal_sum_gram {n : ℕ}
    (a b : CStarMatrix (Fin n) (Fin n) A) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a*b = 0) :
    ∃ v : Matrix (Fin n) (Fin (n+n)) A,
      v*v.conjTranspose = CStarMatrix.ofMatrix.symm (a+b) ∧
      v.conjTranspose*v =
        (CuntzPositiveMatrix.add ⟨n, CStarMatrix.ofMatrix.symm a, ha⟩
          ⟨n, CStarMatrix.ofMatrix.symm b, hb⟩).matrix := by
…

Mentions: OAI.Kaplansky.CuntzPositiveMatrix.add

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_orthogonal_add line 107

Source documentation

Orthogonal additivity for the spectral integral follows from its proved rectangular square swap and block additivity.

theorem CuntzDimensionState.spectralValue_orthogonal_add (d : CuntzDimensionState A) {n : ℕ}
    (a b : CStarMatrix (Fin n) (Fin n) A) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a*b = 0) :
    d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm (a+b), add_nonneg ha hb⟩ =
      d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm a, ha⟩ +
      d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm b, hb⟩ := by
…

Mentions: OAI.Kaplansky.CuntzDimensionState

def OAI.Kaplansky.CuntzDimensionState.positiveValue line 124
Source documentation
The spectral value in a fixed matrix size, on the genuine positive cone.
```
def positiveValue (d : CuntzDimensionState A) {n : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) (ha : 0 ≤ a) : ℝ :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.positiveValue_zero line 128
def OAI.Kaplansky.CuntzDimensionState.signedValue line 134
Source documentation
The same positive construction gives a canonical signed value by positive and negative parts. Additivity on general commuting elements is not assumed.
```
def signedValue (d : CuntzDimensionState A) {n : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) : ℝ :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.signedValue_of_nonneg line 138
theorem OAI.Kaplansky.CuntzDimensionState.signedValue_zero line 145
theorem OAI.Kaplansky.CuntzDimensionState.signedValue_neg line 149
theorem OAI.Kaplansky.CuntzDimensionState.signedValue_smul line 154
Source documentation
Real scalar homogeneity holds for the signed construction.
```
theorem signedValue_smul (d : CuntzDimensionState A) {n : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) (r : ℝ) : d.signedValue (r • a) = r*d.signedValue a := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.abs_signedValue_le line 170
Source documentation
A sharp size times norm bound, since both positive-part values lie in [0, size times norm].
```
theorem abs_signedValue_le (d : CuntzDimensionState A) {n : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) : |d.signedValue a| ≤ ‖a‖ * n := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
def OAI.Kaplansky.CuntzDimensionState.complexValue line 191
Source documentation
A single complex-valued extension of the spectral construction in every finite matrix size. Abelian linearity is not asserted by this definition.
```
def complexValue (d : CuntzDimensionState A) {n : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) : ℂ :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.complexValue_selfAdjoint line 196
theorem OAI.Kaplansky.CuntzDimensionState.complexValue_of_nonneg line 201
theorem OAI.Kaplansky.CuntzDimensionState.complexValue_zero line 206

theorem OAI.Kaplansky.CuntzDimensionState.complexValue_real_imag line 211

Source documentation

The original real/imaginary axiom, without assuming that h and k commute.

theorem complexValue_real_imag (d : CuntzDimensionState A) {n : ℕ}
    (h k : CStarMatrix (Fin n) (Fin n) A) (hh : IsSelfAdjoint h) (hk : IsSelfAdjoint k) :
    d.complexValue (h + Complex.I • k) = d.complexValue h + Complex.I * d.complexValue k := by
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.CuntzDimensionState.complexValue_square_nonneg line 218
Source documentation
Nonnegativity of squares for the single whole-matrix construction.
```
theorem complexValue_square_nonneg (d : CuntzDimensionState A) {n : ℕ}
    (x : CStarMatrix (Fin n) (Fin n) A) : 0 ≤ d.complexValue (star x*x) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.complexValue_square_swap line 224
Source documentation
Square swapping for the same whole-matrix construction.
```
theorem complexValue_square_swap (d : CuntzDimensionState A) {n : ℕ}
    (x : CStarMatrix (Fin n) (Fin n) A) :
    d.complexValue (star x*x) = d.complexValue (x*star x) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.complexValue_one line 230
theorem OAI.Kaplansky.CuntzDimensionState.norm_complexValue_le line 238
Source documentation
The uniform bound needed for compact finite-constraint candidates.
```
theorem norm_complexValue_le (d : CuntzDimensionState A) {n : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) : ‖d.complexValue a‖ ≤ 2*‖a‖*n := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState