RelativeTraceAveraging.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Relative scalar averaging in the trace Hilbert space

The least-vector argument applies to the unitary group of an irreducible subalgebra. This supplies the relative averaging needed for bounded-ball tests without an amenability hypothesis on the ambient factor.

def OAI.KadisonKastler.relativeUnitaryOrbit line 25
Source documentation
The orbit under the unitary group of the given subalgebra map.
```
def relativeUnitaryOrbit (φ : R →⋆ₐ[ℂ] Algebra M) (a : Algebra M) : Set (Algebra M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_relative_scalar_in_traceOrbit line 30

Source documentation

Irreducibility makes the unique least vector of a relative unitary orbit scalar. The closure is taken in the actual trace Hilbert space.

theorem exists_relative_scalar_in_traceOrbit
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (a : Algebra M) :
    ∃ c : ℂ, J (c • (1 : Algebra M)) ∈ diagonalTraceHull J (relativeUnitaryOrbit φ a) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.diagonalTraceHull, OAI.KadisonKastler.relativeUnitaryOrbit

theorem OAI.KadisonKastler.trace_relativeUnitaryOrbit line 86
Source documentation
Relative unitary conjugation preserves the given trace.
```
theorem trace_relativeUnitaryOrbit (φ : R →⋆ₐ[ℂ] Algebra M) (a : Algebra M)
    {x : Algebra M} (hx : x ∈ relativeUnitaryOrbit φ a) :
    τ.toLinearMap x = τ.toLinearMap a := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.relativeUnitaryOrbit

theorem OAI.KadisonKastler.trace_scalar_mem_relativeOrbit_hull line 99

Source documentation

The scalar in the relative orbit hull is precisely the trace.

theorem trace_scalar_mem_relativeOrbit_hull
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ b : Algebra M, (∀ r : R, φ r * b = b * φ r) →
      ∃ c : ℂ, b = c • (1 : Algebra M)) (a : Algebra M) :
    J (τ.toLinearMap a • (1 : Algebra M)) ∈ diagonalTraceHull J (relativeUnitaryOrbit φ a) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.diagonalTraceHull, OAI.KadisonKastler.relativeUnitaryOrbit