WeakOperatorCompactness.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Pointwise weak-star compactness for bounded linear maps

This realization keeps the algebra's given predual. Norm bounded closed families of maps can therefore be used in the right-averaging construction without a separability hypothesis.

def OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage line 25
Source documentation
A linear map viewed as a pointwise weak-star continuous-dual valued function. No continuity of the original map for the weak-star topology is required.
```
def weakOperatorImage (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (T : M →L[ℂ] M) :
    M → WeakDual ℂ X := fun a => StrongDual.toWeakDual (e.symm (T a))
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage_injective line 28
lemma OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage_add line 35
lemma OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage_real_smul line 42

def OAI.BoundedHochschild.KadisonRingrose.weakOperatorImageLinear line 57

Source documentation

The weak-star realization is real linear.

def weakOperatorImageLinear (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    (M →L[ℂ] M) →ₗ[ℝ] (M → WeakDual ℂ X) where
…

def OAI.BoundedHochschild.KadisonRingrose.weakOperatorBall line 66
Source documentation
The norm ball of linear maps, expressed by closed pointwise conditions. The conjugate scalar appears because the chosen predual identification is conjugate linear.
```
def weakOperatorBall (C : ℝ) : Set (M → WeakDual ℂ X) :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage_mem line 71
lemma OAI.BoundedHochschild.KadisonRingrose.weakOperatorBall_realize line 89
lemma OAI.BoundedHochschild.KadisonRingrose.weakOperatorBall_isClosed line 113
theorem OAI.BoundedHochschild.KadisonRingrose.weakOperatorBall_isCompact line 136
theorem OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage_ball_isCompact line 145
Source documentation
The pointwise weak-star image of an operator norm ball is compact.
```
theorem weakOperatorImage_ball_isCompact (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {C : ℝ} (hC : 0 ≤ C) :
    IsCompact (weakOperatorImage e '' {T : M →L[ℂ] M | ‖T‖ ≤ C}) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.weakOperatorImage