SquareCutoff.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Intertwining functional calculus and cutoffs of adjoint squares.

theorem OAI.Kaplansky.cfc_cuntzBlock line 22

Source documentation

Real functional calculus commutes with genuine diagonal blocks.

theorem cfc_cuntzBlock (a : CStarMatrix ι ι A) (b : CStarMatrix κ κ A)
    (ha : 0 ≤ a) (hb : 0 ≤ b) (f : ℝ → ℝ) (hf : Continuous f) :
    cfc f (CStarMatrix.ofMatrix (cuntzBlock a b)) =
      CStarMatrix.ofMatrix (cuntzBlock (CStarMatrix.ofMatrix.symm (cfc f a))
        (CStarMatrix.ofMatrix.symm (cfc f b))) := by
…

Mentions: OAI.Kaplansky.cuntzBlock

theorem OAI.Kaplansky.cfc_matrix_intertwine line 38

Source documentation

Intertwining positives also intertwines their continuous real functions. The proof uses block commutation, so no polar decomposition is assumed.

theorem cfc_matrix_intertwine (a : CStarMatrix ι ι A) (b : CStarMatrix κ κ A)
    (x : Matrix ι κ A) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hx : CStarMatrix.ofMatrix.symm a * x = x * CStarMatrix.ofMatrix.symm b)
    (f : ℝ → ℝ) (hf : Continuous f) :
    CStarMatrix.ofMatrix.symm (cfc f a) * x = x * CStarMatrix.ofMatrix.symm (cfc f b) := by
…

def OAI.Kaplansky.cutoffSquareFactor line 67
Source documentation
A continuous cutoff factor, regular at zero for a strictly positive threshold.
```
def cutoffSquareFactor (ε t : ℝ) : ℝ := Real.sqrt (max (t-ε) 0 / max t ε)
```
theorem OAI.Kaplansky.cutoffSquareFactor_continuous line 69
theorem OAI.Kaplansky.cutoffSquareFactor_identity line 76

theorem OAI.Kaplansky.cutoffSquareFactor_cfc line 87

Source documentation

The actual cutoff factors as g(a) a g(a).

theorem cutoffSquareFactor_cfc {a : A} (ha : 0 ≤ a) {ε : ℝ} (hε : 0 < ε) :
    cfc (cutoffSquareFactor ε) a * a * cfc (cutoffSquareFactor ε) a =
      cuntzCutoff a ε := by
…

Mentions: OAI.Kaplansky.cutoffSquareFactor, OAI.Kaplansky.cuntzCutoff

theorem OAI.Kaplansky.cuntzEquivalent_cutoff_rectangular_gram line 103

Source documentation

Matching positive cutoffs of unequal rectangular Gram matrices are Cuntz equivalent, proved by an exact rectangular factorization.

theorem cuntzEquivalent_cutoff_rectangular_gram {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (x : Matrix ι κ A) (ha : 0 ≤ CStarMatrix.ofMatrix (x*x.conjTranspose))
    (hb : 0 ≤ CStarMatrix.ofMatrix (x.conjTranspose*x)) {ε : ℝ} (hε : 0 < ε) :
    CuntzEquivalent
      (CStarMatrix.ofMatrix.symm (cuntzCutoff (CStarMatrix.ofMatrix (x*x.conjTranspose)) ε))
      (CStarMatrix.ofMatrix.symm (cuntzCutoff (CStarMatrix.ofMatrix (x.conjTranspose*x)) ε)) := by
…

Mentions: OAI.Kaplansky.CuntzEquivalent, OAI.Kaplansky.cuntzCutoff