WeakPredual.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The normal dual, with its weak-star topology, is the weak predual.

def OAI.BoundedHochschild.KadisonRingrose.weakPredualMap line 24
Source documentation
The normal-functional embedding with both weak topologies.
```
def weakPredualMap (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (x : WeakSpace ℂ X) : WeakDual ℂ M :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakPredualMap_apply line 28
lemma OAI.BoundedHochschild.KadisonRingrose.weakPredualMap_continuous line 32
theorem OAI.BoundedHochschild.KadisonRingrose.weakPredualMap_isEmbedding line 40
Source documentation
Evaluating against every algebra element recovers the weak topology on its predual; hence the normal embedding is a topological embedding.
```
theorem weakPredualMap_isEmbedding (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    Topology.IsEmbedding (weakPredualMap e) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.weakPredualMap
lemma OAI.BoundedHochschild.KadisonRingrose.range_weakPredualMap line 56
theorem OAI.BoundedHochschild.KadisonRingrose.normal_positive_predual_orbit_compact line 71
Source documentation
The positive unitary orbit has a compact realization in the weak predual.
```
theorem normal_positive_predual_orbit_compact (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ) :
    IsCompact ((weakPredualMap e) ⁻¹'
      weakFunctionalClosure (unitaryOrbitHull (positiveFunctionalCLM ψ))) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual, OAI.BoundedHochschild.KadisonRingrose.weakPredualMap, OAI.BoundedHochschild.KadisonRingrose.weakFunctionalClosure, OAI.BoundedHochschild.KadisonRingrose.unitaryOrbitHull, OAI.BoundedHochschild.KadisonRingrose.positiveFunctionalCLM