Translation.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Order of spectral cutoffs, translations, and continuity.

theorem OAI.Kaplansky.cuntzLE_cutoff_of_le_add line 18

Source documentation

One-sided order perturbation suffices for strict cutoff comparison.

theorem cuntzLE_cutoff_of_le_add {n : ℕ}
    {a b : CStarMatrix (Fin n) (Fin n) A} (ha : 0 ≤ a)
    {δ ε : ℝ} (hδε : δ < ε) (hab : a ≤ b + δ • 1) :
    CuntzLE (CStarMatrix.ofMatrix.symm (cuntzCutoff a ε))
      (CStarMatrix.ofMatrix.symm b) := by
…

Mentions: OAI.Kaplansky.CuntzLE, OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.le_cuntzCutoff_add line 38
Source documentation
The positive part plus the threshold dominates the original element.
```
theorem le_cuntzCutoff_add {a : A} (ha : 0 ≤ a) (t : ℝ) :
    a ≤ cuntzCutoff a t + t • 1 := by
…
```
Mentions: OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.cuntzLE_cutoff_of_le line 48

Source documentation

Positive order preserves matching cutoff Cuntz classes. This is Cuntz comparison, not operator monotonicity of positive parts.

theorem cuntzLE_cutoff_of_le {n : ℕ} {a b : CStarMatrix (Fin n) (Fin n) A}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a ≤ b) (t : ℝ) :
    CuntzLE (CStarMatrix.ofMatrix.symm (cuntzCutoff a t))
      (CStarMatrix.ofMatrix.symm (cuntzCutoff b t)) := by
…

Mentions: OAI.Kaplansky.CuntzLE, OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.CuntzDimensionState.distribution_mono_positive line 60

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_mono_positive line 68

Source documentation

The actual layer-cake integral is monotone on each positive matrix cone.

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

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.cuntzCutoff_add_scalar line 83
theorem OAI.Kaplansky.neg_smul_one_le_cuntzCutoff line 97
Source documentation
A negative spectral threshold contributes at least its opposite scalar.
```
theorem neg_smul_one_le_cuntzCutoff {a : A} (ha : 0 ≤ a) (t : ℝ) :
    (-t) • (1 : A) ≤ cuntzCutoff a t := by
…
```
Mentions: OAI.Kaplansky.cuntzCutoff
def OAI.Kaplansky.CuntzPositiveMatrix.shift line 108
Source documentation
Adding a nonnegative scalar identity to an actual positive finite matrix.
```
def CuntzPositiveMatrix.shift (a : CuntzPositiveMatrix A) (r : ℝ) (hr : 0 ≤ r) :
    CuntzPositiveMatrix A :=
…
```
Mentions: OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.distribution_shift line 115
theorem OAI.Kaplansky.CuntzDimensionState.distribution_of_neg line 131
Source documentation
Below zero, every positive matrix has full normalized spectral dimension.
```
theorem distribution_of_neg (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A)
    {t : ℝ} (ht : t < 0) : d.distribution a t = (a.size : ℝ) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_shift line 145
Source documentation
Translation by a nonnegative scalar identity adds exactly size times scalar.
```
theorem spectralValue_shift (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A)
    (r : ℝ) (hr : 0 ≤ r) :
    d.spectralValue (a.shift r hr) = d.spectralValue a + r * a.size := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_le_add_norm line 182

Source documentation

One-sided norm control for the actual spectral integral.

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

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.CuntzDimensionState.abs_spectralValue_sub_le line 196

Source documentation

On n-by-n positives the integral is n-Lipschitz in the actual C*-norm.

theorem abs_spectralValue_sub_le (d : CuntzDimensionState A) {n : ℕ}
    {a b : CStarMatrix (Fin n) (Fin n) A} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    |d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm a, ha⟩ -
      d.spectralValue ⟨n, CStarMatrix.ofMatrix.symm b, hb⟩| ≤ ‖a-b‖ * n := by
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_lipschitz line 205

theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_continuous line 214

Source documentation

Continuity on the full positive cone, without a finite-spectrum assumption.

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

Mentions: OAI.Kaplansky.CuntzDimensionState