NormalGNSWeakTopology.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

On bounded sets the faithful normal representation preserves the weak-star compactness needed to realize limits of the elementary averaging operators.

def OAI.BoundedHochschild.KadisonRingrose.normalGNSWeak line 22
lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSWeak_continuous line 26
lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSWeak_injective line 40
lemma OAI.BoundedHochschild.KadisonRingrose.normalGNSWeak_image_ball line 48
theorem OAI.BoundedHochschild.KadisonRingrose.normalGNSWeak_ball_isCompact line 66
Source documentation
Norm balls of the represented algebra are weak-operator compact.
```
theorem normalGNSWeak_ball_isCompact (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (C : ℝ) :
    IsCompact {A : NormalGNS e →WOT[ℂ] NormalGNS e | ∃ a : M, ‖a‖ ≤ C ∧
      ContinuousLinearMapWOT.ofCLM (normalGNSRepresentation e a) = A} := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NormalGNS, OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation
theorem OAI.BoundedHochschild.KadisonRingrose.normalGNSWeak_ball_isClosed line 79
Source documentation
A bounded weak-operator limit in this representation still belongs to the original algebra with the same bound.
```
theorem normalGNSWeak_ball_isClosed (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (C : ℝ) :
    IsClosed {A : NormalGNS e →WOT[ℂ] NormalGNS e | ∃ a : M, ‖a‖ ≤ C ∧
      ContinuousLinearMapWOT.ofCLM (normalGNSRepresentation e a) = A} :=
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NormalGNS, OAI.BoundedHochschild.KadisonRingrose.normalGNSRepresentation