Regularization.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Regularized dimensions, cutoff calculus, and topological regularization.

def OAI.Kaplansky.CuntzDimensionState.regularized line 19
Source documentation
Cutoff regularization of the constructed dimension state, as a finite real supremum.
```
def regularized (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A) : ℝ :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.cutoff_values_nonempty line 22
theorem OAI.Kaplansky.CuntzDimensionState.cutoff_values_bddAbove line 26
theorem OAI.Kaplansky.CuntzDimensionState.cutoff_value_le_regularized line 32
theorem OAI.Kaplansky.CuntzDimensionState.regularized_le line 36
theorem OAI.Kaplansky.CuntzDimensionState.regularized_le_value line 42
theorem OAI.Kaplansky.CuntzDimensionState.regularized_nonneg line 45
theorem OAI.Kaplansky.CuntzDimensionState.regularized_le_size line 49
theorem OAI.Kaplansky.CuntzDimensionState.regularized_mono line 53
Source documentation
Cuntz monotonicity is proved using the two-cutoff comparison theorem.
```
theorem regularized_mono (d : CuntzDimensionState A) {a b : CuntzPositiveMatrix A}
    (h : CuntzLE a.matrix b.matrix) : d.regularized a ≤ d.regularized b := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix, OAI.Kaplansky.CuntzLE
theorem OAI.Kaplansky.CuntzDimensionState.regularized_eq line 61
theorem OAI.Kaplansky.CuntzDimensionState.regularized_zero line 65
theorem OAI.Kaplansky.CuntzDimensionState.exists_lt_cutoff_value line 69
Source documentation
Every number strictly below the supremum is exceeded by one actual cutoff value.
```
theorem exists_lt_cutoff_value (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A)
    {r : ℝ} (h : r < d.regularized a) : ∃ ε : ℝ, 0 < ε ∧ r < d.value (a.cutoff ε) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix

theorem OAI.Kaplansky.cuntzCutoff_cutoff line 77

Source documentation

Iterated cutoffs add their thresholds.

theorem cuntzCutoff_cutoff {a : A} (ha : 0 ≤ a) (ε : ℝ) {δ : ℝ} (hδ : 0 ≤ δ) :
    cuntzCutoff (cuntzCutoff a ε) δ = cuntzCutoff a (ε+δ) := by
…

Mentions: OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.CuntzPositiveMatrix.cutoff_cutoff line 91
theorem OAI.Kaplansky.cuntzCutoff_one_half line 101
theorem OAI.Kaplansky.CuntzDimensionState.regularized_unit line 107
Source documentation
Regularization preserves the value of every finite identity matrix.
```
theorem CuntzDimensionState.regularized_unit (d : CuntzDimensionState A) (n : ℕ) :
    d.regularized (.unit n) = (n : ℝ) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.regularized_idempotent line 120
Source documentation
Applying the cutoff supremum a second time does not change its value.
```
theorem CuntzDimensionState.regularized_idempotent (d : CuntzDimensionState A)
    (a : CuntzPositiveMatrix A) :
    sSup ((fun ε : ℝ => d.regularized (a.cutoff ε)) '' Set.Ioi 0) = d.regularized a := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix

theorem OAI.Kaplansky.CuntzDimensionState.cutoff_value_le_regularized_of_norm line 143

Source documentation

A norm neighborhood controls one fixed cutoff by the regularized value.

theorem CuntzDimensionState.cutoff_value_le_regularized_of_norm {n : ℕ}
    (d : CuntzDimensionState A) {a b : CStarMatrix (Fin n) (Fin n) A}
    (ha : 0 ≤ a) (hb : 0 ≤ b) {ε : ℝ} (hε : 0 < ε) (hab : ‖a-b‖ < ε/2) :
    d.value ((⟨n, CStarMatrix.ofMatrix.symm a, ha⟩ : CuntzPositiveMatrix A).cutoff ε) ≤
      d.regularized ⟨n, CStarMatrix.ofMatrix.symm b, hb⟩ := by
…

Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix

theorem OAI.Kaplansky.CuntzDimensionState.regularized_lowerSemicontinuous line 159

Source documentation

Lower semicontinuity on the full positive cone in each actual matrix norm.

theorem CuntzDimensionState.regularized_lowerSemicontinuous (d : CuntzDimensionState A)
    (n : ℕ) : LowerSemicontinuous (fun a : {a : CStarMatrix (Fin n) (Fin n) A // 0 ≤ a} =>
      d.regularized ⟨n, CStarMatrix.ofMatrix.symm a.val, a.property⟩) := by
…

Mentions: OAI.Kaplansky.CuntzDimensionState

def OAI.Kaplansky.cuntzBlockHom line 182

Source documentation

The genuine block-diagonal unital star homomorphism.

def cuntzBlockHom : (CStarMatrix ι ι A × CStarMatrix κ κ A) →⋆ₐ[ℂ]
    CStarMatrix (ι ⊕ κ) (ι ⊕ κ) A where
…

theorem OAI.Kaplansky.cuntzCutoff_block line 207
theorem OAI.Kaplansky.cuntzCutoff_reindex line 220
theorem OAI.Kaplansky.CuntzPositiveMatrix.cutoff_add line 227