OAI/Analysis/Cuntz/Quasitrace.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.spectralCornerHom line 18
2. theorem OAI.Kaplansky.spectralCorner_posPart line 26
3. theorem OAI.Kaplansky.spectralCorner_negPart line 31
4. theorem OAI.Kaplansky.spectralCorner_realPart line 36
5. theorem OAI.Kaplansky.spectralCorner_imaginaryPart line 40
6. theorem OAI.Kaplansky.CuntzDimensionState.positiveValue_corner line 46

   Source documentation

   A single rectangular entry implements equality of spectral values between any positive corner and its one-by-one matrix.

   theorem CuntzDimensionState.positiveValue_corner (d : CuntzDimensionState A) {n : ℕ}
       (i : Fin n) {a : A} (ha : 0 ≤ a) :
       d.positiveValue (corner i a) (corner_nonneg i ha) =
         d.positiveValue (corner (0 : Fin 1) a) (corner_nonneg _ ha) := by
   …

   Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.corner, OAI.Kaplansky.corner_nonneg

7. theorem OAI.Kaplansky.CuntzDimensionState.signedValue_corner line 67
8. theorem OAI.Kaplansky.CuntzDimensionState.complexValue_corner line 75

   Source documentation

   Whole-algebra corner compatibility for the same stabilized construction.

   theorem CuntzDimensionState.complexValue_corner (d : CuntzDimensionState A) {n : ℕ}
       (i : Fin n) (a : A) :
       d.complexValue (corner i a) = d.complexValue (corner (0 : Fin 1) a) := by
   …

   Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.corner

9. theorem OAI.Kaplansky.spectralCorner_finOne line 81
10. def OAI.Kaplansky.CuntzDimensionState.baseValue line 94

    Source documentation

    The same spectral construction on the original coefficient algebra.

    def baseValue (d : CuntzDimensionState A) (a : A) : ℂ :=
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState

11. theorem OAI.Kaplansky.CuntzDimensionState.baseValue_square_nonneg line 97
12. theorem OAI.Kaplansky.CuntzDimensionState.baseValue_square_swap line 102
13. theorem OAI.Kaplansky.CuntzDimensionState.baseValue_real_imag line 107
14. theorem OAI.Kaplansky.CuntzDimensionState.baseValue_one line 114
15. theorem OAI.Kaplansky.CuntzDimensionState.norm_baseValue_le line 124
16. def OAI.Kaplansky.CuntzDimensionState.spectralCandidate line 135

    Source documentation

    A single compatible base/M2 candidate, built from one dimension state. Only the abelian linearity constraints are still missing.

    def spectralCandidate (d : CuntzDimensionState A) : QuasitraceCandidate A :=
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.QuasitraceCandidate

17. theorem OAI.Kaplansky.CuntzDimensionState.spectralCandidate_corner line 138
18. theorem OAI.Kaplansky.CuntzDimensionState.spectralCandidate_matrix_unit line 144
19. def OAI.Kaplansky.CuntzDimensionState.oneQuasitraceOfSpectralCandidate line 148
20. theorem OAI.Kaplansky.CuntzDimensionState.normalizedTwoQuasitrace_of_spectral_linearity line 158
21. def OAI.Kaplansky.CuntzDimensionState.commutativeValueLinearMap line 176

    Source documentation

    Gelfand duality transfers the proved integral linearity to any unital commutative C*-algebra represented in a finite matrix algebra over A.

    def commutativeValueLinearMap (d : CuntzDimensionState A)
        {B : Type*} [CommCStarAlgebra B] {n : ℕ}
        (φ : B →⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) A) : B →ₗ[ℂ] ℂ := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState

22. theorem OAI.Kaplansky.CuntzDimensionState.commutativeValueLinearMap_apply line 184
23. def OAI.Kaplansky.CuntzDimensionState.nonunitalCommutativeValueLinearMap line 191
24. theorem OAI.Kaplansky.CuntzDimensionState.nonunitalCommutativeValueLinearMap_apply line 197
25. theorem OAI.Kaplansky.CuntzDimensionState.complexValue_abelian_linear line 209

    Source documentation

    The exact abelian-linearity axiom for the fixed matrix spectral candidate.

    theorem complexValue_abelian_linear (d : CuntzDimensionState A) (n : ℕ)
        (S : NonUnitalStarSubalgebra ℂ (CStarMatrix (Fin n) (Fin n) A))
        (hS : IsClosed (S : Set (CStarMatrix (Fin n) (Fin n) A)))
        (hcomm : ∀ x y : S, x*y=y*x) :
        ∃ f : S →ₗ[ℂ] ℂ, ∀ x : S, f x = d.complexValue (x : CStarMatrix (Fin n) (Fin n) A) := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState

26. theorem OAI.Kaplansky.CuntzDimensionState.baseValue_abelian_linear line 220

    Source documentation

    The same axiom at size one, expressed on the original coefficient algebra.

    theorem baseValue_abelian_linear (d : CuntzDimensionState A)
        (S : NonUnitalStarSubalgebra ℂ A) (hS : IsClosed (S : Set A))
        (hcomm : ∀ x y : S, x*y=y*x) :
        ∃ f : S →ₗ[ℂ] ℂ, ∀ x : S, f x = d.baseValue x := by
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState

27. theorem OAI.Kaplansky.CuntzDimensionState.normalizedTwoQuasitrace_exists line 232

    Source documentation

    A normalized two-quasitrace from a dimension state, with both original abelian-linearity premises now discharged for the SAME spectral construction.

    theorem normalizedTwoQuasitrace_exists (d : CuntzDimensionState A) :
        ∃ τ : OneQuasitrace A, τ.Normalized ∧ τ.IsTwo :=
    …

    Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.OneQuasitrace