OAI/Analysis/KadisonKastler/FiniteBaseExpectation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The trace projection onto a finite dimensional base

Nondegeneracy of the trace pairing on a finite dimensional star algebra constructs the projection onto that algebra. Only its range and pairing properties are needed for the finite word argument.

  1. def OAI.KadisonKastler.baseTracePairing line 19
  2. theorem OAI.KadisonKastler.baseTracePairing_injective line 36
  3. def OAI.KadisonKastler.baseTracePairingEquiv line 49
  4. def OAI.KadisonKastler.finiteBaseExpectation line 56

    Source documentation

    The actual trace projection, defined by solving the finite trace-pairing system. No conditional expectation existence theorem is assumed.

    def finiteBaseExpectation (τ : FaithfulTracialState B)
    (D : StarSubalgebra ℂ B) [FiniteDimensional ℂ D] : B →ₗ[ℂ] B :=
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState

  5. theorem OAI.KadisonKastler.finiteBaseExpectation_mem line 61
  6. theorem OAI.KadisonKastler.finiteBaseExpectation_pairing line 66
  7. theorem OAI.KadisonKastler.finiteBaseExpectation_trace line 72
  8. theorem OAI.KadisonKastler.finiteBaseExpectation_fixed line 77
  9. theorem OAI.KadisonKastler.finiteBaseExpectation_zero_iff line 83
  10. theorem OAI.KadisonKastler.traceOrthogonal_sub_finiteBaseExpectation line 94