OAI/Analysis/Cuntz/State.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Dimension states of the Cuntz monoid and positivity.

  1. theorem OAI.Kaplansky.normalizedCuntzState_exists line 14
  2. structure OAI.Kaplansky.CuntzDimensionState line 24

    Source documentation

    A normalized dimension state on actual positive finite matrices. This is a semigroup state, not yet a quasitrace or its regularization.

    structure CuntzDimensionState (A : Type*) [CStarAlgebra A] where
…
  3. theorem OAI.Kaplansky.cuntzDimensionState_nonempty line 29
  4. def OAI.Kaplansky.CuntzDimensionState.value line 37
  5. theorem OAI.Kaplansky.CuntzDimensionState.value_mono line 39
  6. theorem OAI.Kaplansky.CuntzDimensionState.value_eq line 43
  7. theorem OAI.Kaplansky.CuntzDimensionState.value_add line 47
  8. theorem OAI.Kaplansky.CuntzDimensionState.value_unit line 51
  9. theorem OAI.Kaplansky.CuntzDimensionState.value_zero line 57
  10. theorem OAI.Kaplansky.CuntzDimensionState.value_nonneg line 59
  11. theorem OAI.Kaplansky.CuntzDimensionState.value_le_size line 62
  12. theorem OAI.Kaplansky.exists_positiveOrder_approx line 76

    Source documentation

    Positive order gives actual approximate conjugation. An inverse square-root of b+δ1 supplies a contraction and an error bounded by δ.

    theorem exists_positiveOrder_approx {a b : A} (ha : 0 ≤ a) (hab : a ≤ b)
    (ε : ℝ) (hε : 0 < ε) : ∃ v : A, ‖a - v*b*star v‖ < ε := by
…
  13. theorem OAI.Kaplansky.cuntzLE_of_nonneg_le line 110
  14. theorem OAI.Kaplansky.CuntzDimensionState.value_mono_positive line 118