Cutoff.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Functional calculus cutoffs and perturbation comparison.

def OAI.Kaplansky.cuntzCutoff line 17
Source documentation
The genuine continuous spectral cutoff (a-ε)₊.
```
def cuntzCutoff (a : A) (ε : ℝ) : A := cfc (fun t : ℝ => max (t-ε) 0) a
```
theorem OAI.Kaplansky.cuntzCutoff_nonneg line 19
theorem OAI.Kaplansky.cuntzCutoff_le line 22
theorem OAI.Kaplansky.cuntzCutoff_antitone line 28
theorem OAI.Kaplansky.norm_sub_cuntzCutoff_le line 33
Source documentation
Uniform norm control, with the actual C*-norm.
```
theorem norm_sub_cuntzCutoff_le {a : A} (ha : 0 ≤ a) {ε : ℝ} (hε : 0 ≤ ε) :
    ‖a - cuntzCutoff a ε‖ ≤ ε := by
…
```
Mentions: OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.cuntzLE_iff_all_cutoffs line 50

Source documentation

Norm comparison of positives is detected by all strictly positive spectral cutoffs. This does not assume continuity of a dimension state.

theorem cuntzLE_iff_all_cutoffs {n m : ℕ}
    (a : CStarMatrix (Fin n) (Fin n) A) (ha : 0 ≤ a)
    (b : CStarMatrix (Fin m) (Fin m) A) :
    CuntzLE (CStarMatrix.ofMatrix.symm a) (CStarMatrix.ofMatrix.symm b) ↔
      ∀ ε : ℝ, 0 < ε → CuntzLE (CStarMatrix.ofMatrix.symm (cuntzCutoff a ε))
        (CStarMatrix.ofMatrix.symm b) := by
…

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

def OAI.Kaplansky.CuntzPositiveMatrix.cutoff line 77
Source documentation
The cutoff remains an actual positive matrix of the same finite size.
```
def CuntzPositiveMatrix.cutoff (a : CuntzPositiveMatrix A) (ε : ℝ) : CuntzPositiveMatrix A :=
…
```
Mentions: OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.cutoff_value_antitone line 81
theorem OAI.Kaplansky.CuntzDimensionState.cutoff_value_le line 86

theorem OAI.Kaplansky.cuntzLE_smul line 92

Source documentation

Positive scalar multiplication is implemented by scalar conjugation.

theorem cuntzLE_smul {n : ℕ} (a : CStarMatrix (Fin n) (Fin n) A)
    {r : ℝ} (hr : 0 ≤ r) :
    CuntzLE (CStarMatrix.ofMatrix.symm (r • a)) (CStarMatrix.ofMatrix.symm a) := by
…

Mentions: OAI.Kaplansky.CuntzLE

theorem OAI.Kaplansky.cuntzEquivalent_pos_smul line 103
theorem OAI.Kaplansky.exists_cutoff_localizer line 113
Source documentation
A cutoff square root localized above ε. The inequality is scalar functional calculus in a single self-adjoint element.
```
theorem exists_cutoff_localizer {a : A} (ha : 0 ≤ a) (ε : ℝ) :
    ∃ x : A, star x = x ∧ x*x = cuntzCutoff a ε ∧
      ε • cuntzCutoff a ε ≤ x*a*x := by
…
```
Mentions: OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.cuntzLE_cutoff_of_norm_sub_lt line 142

Source documentation

A strict norm perturbation gives cutoff Cuntz comparison. No operator monotonicity of the positive-part function is used.

theorem cuntzLE_cutoff_of_norm_sub_lt {n : ℕ}
    {a b : CStarMatrix (Fin n) (Fin n) A} (ha : 0 ≤ a) (hb : IsSelfAdjoint b)
    {ε : ℝ} (h : ‖a-b‖ < ε) :
    CuntzLE (CStarMatrix.ofMatrix.symm (cuntzCutoff a ε))
      (CStarMatrix.ofMatrix.symm b) := by
…

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

theorem OAI.Kaplansky.CuntzLE.exists_cutoff line 170

Source documentation

Every positive cutoff of a Cuntz-smaller matrix is already below a strictly positive cutoff of the larger matrix, including unequal sizes.

theorem CuntzLE.exists_cutoff {n m : ℕ}
    {a : CStarMatrix (Fin n) (Fin n) A} {b : CStarMatrix (Fin m) (Fin m) A}
    (ha : 0 ≤ a) (hb : 0 ≤ b)
    (h : CuntzLE (CStarMatrix.ofMatrix.symm a) (CStarMatrix.ofMatrix.symm b))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ CuntzLE (CStarMatrix.ofMatrix.symm (cuntzCutoff a ε))
      (CStarMatrix.ofMatrix.symm (cuntzCutoff b δ)) := by
…

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

theorem OAI.Kaplansky.cuntzLE_iff_cutoff_comparison line 207

Source documentation

The cutoff quantifiers characterize the original norm-closure relation.

theorem cuntzLE_iff_cutoff_comparison (a b : CuntzPositiveMatrix A) :
    CuntzLE a.matrix b.matrix ↔ ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
      CuntzLE (a.cutoff ε).matrix (b.cutoff δ).matrix := by
…

Mentions: OAI.Kaplansky.CuntzPositiveMatrix, OAI.Kaplansky.CuntzLE