OAI/Analysis/KadisonSimilarity/Tracial/FiniteFactorTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.vectorPositiveFunctional line 19
2. theorem OAI.KadisonSimilarity.vectorPositiveFunctional_apply line 25
3. theorem OAI.KadisonSimilarity.vectorPositiveFunctional_normal line 28
4. theorem OAI.KadisonSimilarity.vectorPositiveFunctional_one line 39
5. theorem OAI.KadisonSimilarity.exists_faithful_normal_trace line 48

   Source documentation

   Finiteness gives a normalized normal trace; a scalar center makes it faithful. This constructs the finite-factor trace rather than assuming it.

   theorem exists_faithful_normal_trace [Nontrivial H]
       (hfinite : FiniteAlgebra M.toStarSubalgebra)
       (hfactor : ∀ a : M.toStarSubalgebra, (∀ b, a * b = b * a) →
         ∃ c : ℂ, a = algebraMap ℂ M.toStarSubalgebra c) :
       ∃ τ : M.toStarSubalgebra →ₚ[ℂ] ℂ,
         TraceInPredual (concretePredualEquiv M) τ ∧ τ 1 = 1 ∧
         (∀ a b, τ (a * b) = τ (b * a)) ∧
         (∀ a, τ (star a * a) = 0 → a = 0) ∧ HasNormalGNS τ := by
   …

   Mentions: OAI.KadisonSimilarity.concretePredualEquiv, OAI.KadisonSimilarity.HasNormalGNS

6. def OAI.KadisonSimilarity.finiteFactorTrace line 75

   Source documentation

   A fixed choice of the normalized normal trace, for the subsequent hyperfinite-subfactor construction.

   def finiteFactorTrace [Nontrivial H]
       (hfinite : FiniteAlgebra M.toStarSubalgebra)
       (hfactor : ∀ a : M.toStarSubalgebra, (∀ b, a * b = b * a) →
         ∃ c : ℂ, a = algebraMap ℂ M.toStarSubalgebra c) :
       M.toStarSubalgebra →ₚ[ℂ] ℂ :=
   …

7. theorem OAI.KadisonSimilarity.finiteFactorTrace_spec line 82