Existence of a minimal invariant family of represented averages
ProvedOAI.BoundedHochschild.KadisonRingrose.exists_minimal_represented_averagesLet be a unital C*-algebra, complex Hilbert spaces, , unital *-homomorphisms and a bounded operator. Let be the weak-operator closure of the set of represented right averages with (closedRepresentedAveragingOrbit). Then contains a nonempty set that is weak-operator closed, convex, invariant under all represented right averages, and contained in every nonempty closed convex invariant subset of itself.
Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.
import Mathlib
import Definitions.Def_KadisonRingroseSupport2
namespace OAI
noncomputable section
open Topology
namespace BoundedHochschild.KadisonRingrose
variable {M H K : Type*} [CStarAlgebra M]
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
[NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
theorem exists_minimal_represented_averages (π : M →⋆ₐ[ℂ] (K →L[ℂ] K))
(σ : M →⋆ₐ[ℂ] (H →L[ℂ] H)) (W : H →WOT[ℂ] K) :
∃ F : Set (H →WOT[ℂ] K), F ⊆ closedRepresentedAveragingOrbit π σ W ∧
F.Nonempty ∧ IsClosed F ∧ Convex ℝ F ∧ RepresentedRightAverageInvariant π σ F ∧
∀ G : Set (H →WOT[ℂ] K), G ⊆ F → G.Nonempty → IsClosed G →
Convex ℝ G → RepresentedRightAverageInvariant π σ G → F ⊆ G := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI