OAI/Analysis/Quasitrace/Basic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kaplansky.OneQuasitrace line 17

   Also declared: ComparatorChallenges/KaplanskyQuasitrace.lean:15 (same declaration text), ComparatorChallenges/KaplanskyStableFiniteness.lean:101 (same declaration text).

2. instance OAI.Kaplansky.(instance at line 27) line 27
3. def OAI.Kaplansky.OneQuasitrace.Normalized line 29

   Distinct definitions of this name: ComparatorChallenges/KaplanskyQuasitrace.lean:27 (same statement text; different proof or body), ComparatorChallenges/KaplanskyStableFiniteness.lean:113 (same declaration text). Qualify references as OAI.Kaplansky.OneQuasitrace.Normalized@path.

4. theorem OAI.Kaplansky.OneQuasitrace.linearOn line 32

   Source documentation

   The closed unital abelian case follows from the actual nonunital axiom.

   theorem OneQuasitrace.linearOn (τ : OneQuasitrace A)
       (S : StarSubalgebra ℂ A) (hS : IsClosed (S : Set A))
       (hcomm : ∀ x y : S, x * y = y * x) :
       ∃ f : S →ₗ[ℂ] ℂ, ∀ x : S, f x = τ x := by
   …

   Mentions: OAI.Kaplansky.OneQuasitrace

5. theorem OAI.Kaplansky.OneQuasitrace.map_add_of_mem line 42
6. theorem OAI.Kaplansky.OneQuasitrace.map_sub_of_mem line 49
7. theorem OAI.Kaplansky.OneQuasitrace.map_smul_of_mem line 56
8. theorem OAI.Kaplansky.OneQuasitrace.map_zero line 63
9. theorem OAI.Kaplansky.OneQuasitrace.map_smul_selfAdjoint line 69
10. theorem OAI.Kaplansky.OneQuasitrace.map_scalar_sub line 76
11. theorem OAI.Kaplansky.OneQuasitrace.linearOn_hull line 87

    Source documentation

    Abelian linearity applied to the closed star algebra generated by a commuting family of self-adjoint elements.

    theorem linearOn_hull (s : Set A) (hsa : ∀ a ∈ s, IsSelfAdjoint a)
        (hc : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
        ∃ f : (StarAlgebra.adjoin ℂ s).topologicalClosure →ₗ[ℂ] ℂ,
          ∀ x, f x = τ x := by
    …

12. theorem OAI.Kaplansky.OneQuasitrace.map_add line 103

    Source documentation

    Only commuting self-adjoint pairs are added here.

    theorem map_add {a b : A} (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b)
        (hc : Commute a b) : τ (a + b) = τ a + τ b := by
    …

13. theorem OAI.Kaplansky.OneQuasitrace.map_neg line 122
14. theorem OAI.Kaplansky.OneQuasitrace.map_sub line 125
15. theorem OAI.Kaplansky.OneQuasitrace.map_sum line 130

    Source documentation

    Finite additivity is derived only for pairwise commuting self-adjoints.

    theorem map_sum {ι : Type*} (s : Finset ι) (f : ι → A)
        (hsa : ∀ i ∈ s, IsSelfAdjoint (f i))
        (hc : ∀ i ∈ s, ∀ j ∈ s, Commute (f i) (f j)) :
        τ (∑ i ∈ s, f i) = ∑ i ∈ s, τ (f i) := by
    …