CountableTraceGroup.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A countable group dense in the trace topology

The boundary argument only needs a countable discrete group whose unitary image approximates every unitary in trace two-norm. A free group on a countable dense set supplies an actual subgroup with this property.

theorem OAI.KadisonKastler.exists_countable_traceDense_unitary_subgroup line 22

Source documentation

There is a countable subgroup of the unitary group that is dense for the faithful trace two-norm.

theorem exists_countable_traceDense_unitary_subgroup
    [TopologicalSpace.SeparableSpace H]
    (τ : FaithfulTracialState (Algebra M)) (hτ : FiniteVectorTrace τ) :
    ∃ G : Subgroup (unitary (Algebra M)), (G : Set (unitary (Algebra M))).Countable ∧
      ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
        ∃ g : G, traceTwoNorm τ ((u : Algebra M) - (g.val : Algebra M)) < ε := by
…

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

theorem OAI.KadisonKastler.traceTwoNorm_unitary_conj_sub_le line 48

Source documentation

Unitary conjugation of a fixed bounded element is Lipschitz in the trace two-norm, with constant twice its operator norm.

theorem traceTwoNorm_unitary_conj_sub_le
    (τ : FaithfulTracialState (Algebra M)) (u v : unitary (Algebra M))
    (a : Algebra M) :
    traceTwoNorm τ ((u : Algebra M) * a * star (u : Algebra M) -
      (v : Algebra M) * a * star (v : Algebra M)) ≤
        2 * ‖a‖ * traceTwoNorm τ ((u : Algebra M) - v) := by
…

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

theorem OAI.KadisonKastler.inner_conjugation_invariant_of_traceDense line 78

Source documentation

Invariance of coefficients extends from a trace-dense family of unitaries to all unitaries.

theorem inner_conjugation_invariant_of_traceDense
    (τ : FaithfulTracialState (Algebra M)) (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ a, ‖J a‖ = traceTwoNorm τ a)
    (ρ : I → unitary (Algebra M))
    (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
      ∃ i, traceTwoNorm τ ((u : Algebra M) - ρ i) < ε)
    (v : E) (hinv : ∀ i a, inner ℂ v
      (J ((ρ i : Algebra M) * a * star (ρ i : Algebra M))) = inner ℂ v (J a))
    (u : unitary (Algebra M)) (a : Algebra M) :
    inner ℂ v (J ((u : Algebra M) * a * star (u : Algebra M))) = inner ℂ v (J a) := by
…

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

theorem OAI.KadisonKastler.concreteTrace_scalar_of_traceDense_invariant line 114
Source documentation
Invariance under the chosen trace-dense group already forces a scalar trace vector. No strong-density assumption is added.
```
theorem concreteTrace_scalar_of_traceDense_invariant
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (ρ : I → unitary (Algebra M))
    (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
      ∃ i, traceTwoNorm (concreteFactorTrace hM) ((u : Algebra M) - ρ i) < ε)
    (v : ConcreteTraceHilbert hM)
    (hinv : ∀ i, concreteTraceLeftAction hM (ρ i)
      (concreteTraceRightAction hM (star (ρ i : Algebra M)) v) = v) :
    ∃ z : ℂ, v = z • concreteTraceEmbedding hM 1 := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.concreteFactorTrace, OAI.KadisonKastler.ConcreteTraceHilbert, OAI.KadisonKastler.concreteTraceLeftAction, OAI.KadisonKastler.concreteTraceRightAction, OAI.KadisonKastler.concreteTraceEmbedding