PositiveOrbitCompactness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Weak compactness of positive normal orbits

The positive-functional specialization of Ringrose, Theorem 4.7 and Lemma 5.3. The gliding-block estimate and complete-additivity criterion ensure that no singular functional enters the weak-star closure.

def OAI.BoundedHochschild.KadisonRingrose.weakFunctionalClosure line 30
Source documentation
Weak-star closure of a family of bounded functionals.
```
def weakFunctionalClosure (K : Set (StrongDual ℂ M)) : Set (WeakDual ℂ M) :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakFunctionalClosure_positive line 34

theorem OAI.BoundedHochschild.KadisonRingrose.weakFunctionalClosure_normal line 46

Source documentation

A uniform orthogonal-sequence estimate makes every positive weak-star cluster functional normal.

theorem weakFunctionalClosure_normal (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (K : Set (StrongDual ℂ M))
    (hpos : ∀ F ∈ K, ∀ a : M, 0 ≤ a → 0 ≤ F a)
    (hnormal : ∀ F ∈ K, F ∈ normalDual e)
    (hdecay : ∀ q : ℕ → M, (∀ n, IsStarProjection (q n)) →
      (∀ m n, m ≠ n → q m * q n = 0) → ∀ ε : ℝ, 0 < ε →
        ∀ᶠ n in atTop, ∀ F ∈ K, ‖F (q n)‖ < ε)
    {F : WeakDual ℂ M} (hF : F ∈ weakFunctionalClosure K) :
    WeakDual.toStrongDual F ∈ normalDual e := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.weakFunctionalClosure

lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPullback_norm_le line 102
lemma OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull_norm_le line 112
theorem OAI.BoundedHochschild.KadisonRingrose.normal_positive_orbit_compact line 122
Source documentation
The weak-star closure of the positive normal orbit is compact.
```
theorem normal_positive_orbit_compact (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ) :
    IsCompact (weakFunctionalClosure (unitaryOrbitHull (positiveFunctionalCLM ψ))) ∧
      ∀ F ∈ weakFunctionalClosure (unitaryOrbitHull (positiveFunctionalCLM ψ)),
        WeakDual.toStrongDual F ∈ normalDual e := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.KadisonRingrose.weakFunctionalClosure, OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull, OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM