RegularizedState.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Regularized dimension states and subadditivity.

theorem OAI.Kaplansky.CuntzDimensionState.cutoff_value_add_le_regularized line 19
Source documentation
A common smaller cutoff controls two independent cutoff thresholds.
```
theorem cutoff_value_add_le_regularized (d : CuntzDimensionState A)
    (a b : CuntzPositiveMatrix A) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    d.value (a.cutoff ε) + d.value (b.cutoff δ) ≤ d.regularized (a.add b) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.regularized_add line 30
def OAI.Kaplansky.CuntzDimensionState.regularize line 49
Source documentation
The regularization descends to an additive, normalized monotone state on the actual Cuntz monoid.
```
def regularize (d : CuntzDimensionState A) : CuntzDimensionState A where
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.regularize_value line 67
theorem OAI.Kaplansky.CuntzDimensionState.regularize_lowerSemicontinuous line 70
theorem OAI.Kaplansky.CuntzDimensionState.regularize_idempotent_value line 75

theorem OAI.Kaplansky.CuntzDimensionState.regularized_rectangular_gram line 81

Source documentation

Square swapping for the regularization follows from the proved Cuntz equivalence, even for unequal matrix sizes.

theorem regularized_rectangular_gram (d : CuntzDimensionState A) {n m : ℕ}
    (v : Matrix (Fin n) (Fin m) A)
    (hv : 0 ≤ CStarMatrix.ofMatrix (v*v.conjTranspose))
    (hw : 0 ≤ CStarMatrix.ofMatrix (v.conjTranspose*v)) :
    d.regularized ⟨n, v*v.conjTranspose, hv⟩ =
      d.regularized ⟨m, v.conjTranspose*v, hw⟩ :=
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.cuntzLE_sum_block line 101
Source documentation
The row of two identities compresses the diagonal block to the ordinary sum.
```
theorem cuntzLE_sum_block {n : ℕ} (a b : Matrix (Fin n) (Fin n) A) :
    CuntzLE (a+b) (cuntzBlock a b) := by
…
```
Mentions: OAI.Kaplansky.CuntzLE, OAI.Kaplansky.cuntzBlock

theorem OAI.Kaplansky.CuntzDimensionState.value_sum_le line 113

Source documentation

Dimension is subadditive for positive sums, without a commutation hypothesis.

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

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.CuntzDimensionState.regularized_sum_le line 124
theorem OAI.Kaplansky.CuntzDimensionState.regularized_orthogonal_add line 131