NormalOrderIntervals.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Compact order intervals of normal positive functionals.

def OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval line 23
Source documentation
The positive order interval below a fixed positive functional, represented in the weak dual of the algebra.
```
def weakPositiveOrderInterval (ψ : M →ₚ[ℂ] ℂ) : Set (WeakDual ℂ M) :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval_norm_bound line 26
lemma OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval_closed line 48
theorem OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval_compact line 60
Source documentation
Positive order intervals are weak-star compact by Banach--Alaoglu.
```
theorem weakPositiveOrderInterval_compact (ψ : M →ₚ[ℂ] ℂ) :
    IsCompact (weakPositiveOrderInterval ψ) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval
theorem OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval_normal line 70
Source documentation
If the upper endpoint is normal, every functional in the compact order interval is normal as well.
```
theorem weakPositiveOrderInterval_normal (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ) {F : WeakDual ℂ M}
    (hF : F ∈ weakPositiveOrderInterval ψ) : WeakDual.toStrongDual F ∈ normalDual e := by
…
```
Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.KadisonRingrose.weakPositiveOrderInterval