StandardTraceInvariants.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar invariant vectors in common standard position

def OAI.KadisonKastler.StandardTracialPosition.diagonalRepresentation line 20
Source documentation
Restrict the actual product representation to the diagonal group.
```
def diagonalRepresentation : G →* unitary (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.StandardTracialPosition.diagonalRepresentation_vector line 27

theorem OAI.KadisonKastler.StandardTracialPosition.scalar_of_diagonal_invariant line 41

Source documentation

Trace density suffices to identify every invariant vector of the diagonal representation; no extra invariant-vector input is needed.

theorem scalar_of_diagonal_invariant
    (hfactor : ∀ a : Algebra M,
      (∀ b : Algebra M, b * a = a * b) → ∃ c : ℂ, a = c • (1 : Algebra M))
    (hU : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
      ∃ g, traceTwoNorm p.trace ((u : Algebra M) - U g) < ε)
    (v : H) (hv : ∀ g, (p.diagonalRepresentation U g : H →L[ℂ] H) v = v) :
    ∃ z : ℂ, v = z • p.vector := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm