NormalOrbitHull.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The norm-closed convex orbit of a normal positive functional

This family remains normal and positive, preserves values on the center, and satisfies the uniform orthogonal-projection decay in Ringrose Lemma 5.2.

def OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM line 28
Source documentation
The bounded functional underlying a positive functional.
```
def positiveFunctionalCLM (ψ : M →ₚ[ℂ] ℂ) : StrongDual ℂ M :=
…
```
def OAI.BoundedHochschild.KadisonRingrose.unitaryPullback line 32
Source documentation
Pull a functional back along conjugation by a unitary.
```
def unitaryPullback (F : StrongDual ℂ M) (u : unitary M) : StrongDual ℂ M :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPullback_apply line 37
def OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull line 41
Source documentation
The closed convex orbit used in the fixed-point construction of a trace.
```
def unitaryOrbitHull (F : StrongDual ℂ M) : Set (StrongDual ℂ M) :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull_normal line 44
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull_eval_bound line 54
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull_eval_eq line 69
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull_positive line 82
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull_central line 97

theorem OAI.BoundedHochschild.KadisonRingrose.normal_positive_uniform_orbit_hull line 106

Source documentation

Uniform decay survives both convex averaging and norm closure.

theorem normal_positive_uniform_orbit_hull (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ)
    (q : ℕ → M) (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n in atTop, ∀ G ∈ unitaryOrbitHull (positiveFunctionalCLM ψ), ‖G (q n)‖ < ε := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull, OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM