WeakRightAveraging.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The elementary right-averaging actions are continuous for pointwise weak-star convergence. Multiplication normality is used only in the output variable; the maps being averaged need not themselves be normal.

def OAI.BoundedHochschild.KadisonRingrose.weakDualOperator line 20
Source documentation
Transport a bounded linear operator to the weak dual.
```
def weakDualOperator (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (L : M →L[ℂ] M)
    (F : WeakDual ℂ X) : WeakDual ℂ X :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakDualOperator_image line 24
lemma OAI.BoundedHochschild.KadisonRingrose.weakDualOperator_continuous line 31
def OAI.BoundedHochschild.KadisonRingrose.weakRightAverage line 45
Source documentation
Right averaging acts on the ambient space of all weak-dual-valued functions, so its continuity also applies to closures of operator families.
```
def weakRightAverage {I : Type*} [Fintype I] (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (m : I → M) (F : M → WeakDual ℂ X) : M → WeakDual ℂ X := fun a =>
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.weakRightAverage_image line 49
lemma OAI.BoundedHochschild.KadisonRingrose.weakRightAverage_continuous line 60