FiniteCenter.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Scalar orbit averages and central projections of a nearby algebra

Least vectors in the trace Hilbert space give scalar orbit averages in a finite factor. Operator-norm balls centred at ambient operators are retained under this averaging, even when their centre is outside the factor.

theorem OAI.KadisonKastler.traceHull_mem_external_ball line 27

Source documentation

Trace convex hulls of uniformly bounded operators retain norm bounds relative to an arbitrary ambient operator.

theorem traceHull_mem_external_ball (J : Algebra M →ₗ[ℂ] E)
    (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) (hτ : FiniteVectorTrace τ)
    {s : Set (Algebra M)} {C r : ℝ} (hC : 0 ≤ C) (hr : 0 ≤ r)
    (a : H →L[ℂ] H) (hsC : ∀ x ∈ s, ‖x‖ ≤ C)
    (hsr : ∀ x ∈ s, ‖(x : H →L[ℂ] H) - a‖ ≤ r)
    {z : E} (hz : z ∈ diagonalTraceHull J s) :
    ∃ b : Algebra M, J b = z ∧ ‖(b : H →L[ℂ] H) - a‖ ≤ r := by
…

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

def OAI.KadisonKastler.unitaryConjugacyOrbit line 74
Source documentation
Unitary conjugates of an element, as an actual subset of the algebra.
```
def unitaryConjugacyOrbit (a : Algebra M) : Set (Algebra M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_scalar_in_traceOrbit line 79

Source documentation

A bounded unitary orbit in a finite factor has a scalar in its trace closed convex hull.

theorem exists_scalar_in_traceOrbit [CompleteSpace E]
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ)
    (hfactor : ∀ b : Algebra M, (∀ x : Algebra M, x * b = b * x) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (a : Algebra M) (ha : ‖a‖ ≤ 1) :
    ∃ c : ℂ, J (c • (1 : Algebra M)) ∈ diagonalTraceHull J (unitaryConjugacyOrbit a) := by
…

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

theorem OAI.KadisonKastler.exists_scalar_near_of_unitary_orbit line 120

Source documentation

A contraction all of whose conjugates stay near an ambient operator has a scalar near that same operator.

theorem exists_scalar_near_of_unitary_orbit [CompleteSpace E]
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ)
    (hfactor : ∀ b : Algebra M, (∀ x : Algebra M, x * b = b * x) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    (a : Algebra M) (ha : ‖a‖ ≤ 1) (q : H →L[ℂ] H) {r : ℝ} (hr : 0 ≤ r)
    (hclose : ∀ u : unitary (Algebra M),
      ‖((u : Algebra M) * a * star (u : Algebra M) : Algebra M).val - q‖ ≤ r) :
    ∃ c : ℂ, ‖c • (1 : H →L[ℂ] H) - q‖ ≤ r := by
…

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

theorem OAI.KadisonKastler.projection_eq_zero_or_one_of_near_scalar line 142

Source documentation

A projection within one half of a scalar is trivial.

theorem projection_eq_zero_or_one_of_near_scalar {A : Type*} [CStarAlgebra A]
    (q : A) (hq : IsStarProjection q) (c : ℂ)
    (hclose : ‖c • (1 : A) - q‖ < 1 / 2) : q = 0 ∨ q = 1 := by
…

theorem OAI.KadisonKastler.central_projection_trivial_of_near line 175

Source documentation

A central projection in an algebra within one tenth of a finite factor is zero or one. The trace data are supplied separately.

theorem central_projection_trivial_of_near [CompleteSpace E]
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ)
    (hfactor : ∀ b : Algebra M, (∀ x : Algebra M, x * b = b * x) →
      ∃ c : ℂ, b = c • (1 : Algebra M))
    {N : VonNeumannAlgebra H} (hgap : kkDistance M N < 1 / 10)
    (q : Algebra N) (hq : IsStarProjection q)
    (hcentral : ∀ b : Algebra N, b * q = q * b) : q = 0 ∨ q = 1 := by
…

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