MinimalRightAverages.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A minimal compact convex invariant family of right averages. The proof uses the finite intersection property and does not presume a fixed point.

def OAI.BoundedHochschild.KadisonRingrose.RightAverageInvariant line 20
Source documentation
Invariance under every finite normalized right average.
```
def RightAverageInvariant (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (K : Set (M → WeakDual ℂ X)) : Prop :=
…
```

theorem OAI.BoundedHochschild.KadisonRingrose.exists_minimal_right_averages line 27

Source documentation

The averaging orbit contains a minimal nonempty closed convex invariant subset. The separate module-map step must still show that it is a singleton.

theorem exists_minimal_right_averages (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) (T : M →L[ℂ] M) {C : ℝ}
    (hT : CompletelyBoundedEstimate T C) :
    ∃ K : Set (M → WeakDual ℂ X), K ⊆ weakRightAverageOrbit e T ∧
      K.Nonempty ∧ IsClosed K ∧ Convex ℝ K ∧ RightAverageInvariant e K ∧
      ∀ L : Set (M → WeakDual ℂ X), L ⊆ K → L.Nonempty → IsClosed L →
        Convex ℝ L → RightAverageInvariant e L → K ⊆ L := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedEstimate, OAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit, OAI.BoundedHochschild.KadisonRingrose.RightAverageInvariant