Squares.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Square approximation, square swap, and orthogonal additivity.

theorem OAI.Kaplansky.squareSwap_scalar_error line 19

Source documentation

The scalar error estimate underlying approximate comparison of xx* and x*x.

theorem squareSwap_scalar_error {t δ : ℝ} (ht : 0 ≤ t) (hδ : 0 < δ) :
    |t - (Real.sqrt (t+δ))⁻¹ * t * t * (Real.sqrt (t+δ))⁻¹| ≤ δ := by
…

theorem OAI.Kaplansky.exists_squareSwap_approx line 33
Source documentation
A concrete functional-calculus approximation. No polar decomposition or square-swap property of dimension functions is assumed.
```
theorem exists_squareSwap_approx (x : A) (ε : ℝ) (hε : 0 < ε) :
    ∃ v : A, ‖x * star x - v * (star x * x) * star v‖ < ε := by
…
```

theorem OAI.Kaplansky.cuntzLE_mul_star_self line 75

Source documentation

Cuntz square swapping is proved by norm approximants.

theorem cuntzLE_mul_star_self [DecidableEq ι] (x : CStarMatrix ι ι A) :
    CuntzLE (CStarMatrix.ofMatrix.symm (x * star x))
      (CStarMatrix.ofMatrix.symm (star x * x)) := by
…

Mentions: OAI.Kaplansky.CuntzLE

theorem OAI.Kaplansky.cuntzEquivalent_square_swap line 83
theorem OAI.Kaplansky.cuntzEquivalent_rectangular_gram line 90
Source documentation
Rectangular Gram matrices of different sizes have the same Cuntz class.
```
theorem cuntzEquivalent_rectangular_gram (v : Matrix ι κ A) :
    CuntzEquivalent (v * v.conjTranspose) (v.conjTranspose * v) := by
…
```
Mentions: OAI.Kaplansky.CuntzEquivalent

theorem OAI.Kaplansky.CuntzDimensionState.value_square_swap line 109

Source documentation

Positives formed as either square have equal values under every constructed dimension state; this is not an assumed quasitrace axiom.

theorem CuntzDimensionState.value_square_swap (d : CuntzDimensionState A) (n : ℕ)
    (x : CStarMatrix (Fin n) (Fin n) A) :
    d.value ⟨n, CStarMatrix.ofMatrix.symm (x * star x), mul_star_self_nonneg x⟩ =
      d.value ⟨n, CStarMatrix.ofMatrix.symm (star x * x), star_mul_self_nonneg x⟩ :=
…

Mentions: OAI.Kaplansky.CuntzDimensionState

theorem OAI.Kaplansky.sqrt_mul_sqrt_eq_zero_of_mul_eq_zero line 126

Source documentation

Orthogonality passes to actual positive square roots.

theorem sqrt_mul_sqrt_eq_zero_of_mul_eq_zero {a b : A} (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hab : a*b = 0) : CFC.sqrt a * CFC.sqrt b = 0 := by
…

theorem OAI.Kaplansky.cuntzEquivalent_orthogonal_add line 146

Source documentation

Orthogonal positive addition agrees with block addition in the Cuntz monoid.

theorem cuntzEquivalent_orthogonal_add {n : ℕ}
    (a b : CStarMatrix (Fin n) (Fin n) A) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a*b = 0) :
    CuntzEquivalent (CStarMatrix.ofMatrix.symm (a+b))
      (cuntzBlock (CStarMatrix.ofMatrix.symm a) (CStarMatrix.ofMatrix.symm b)) := by
…

Mentions: OAI.Kaplansky.CuntzEquivalent, OAI.Kaplansky.cuntzBlock

theorem OAI.Kaplansky.CuntzDimensionState.value_orthogonal_add line 177