The weak right-averaging orbit stays in the ball of the complete bound
ProvedOAI.BoundedHochschild.KadisonRingrose.weakRightAverageOrbit_subset_ballLet be a unital C*-algebra with star-ordered partial order and predual via an isometric conjugate-linear isomorphism , with no finite central summand: a central projection whose corner is finite vanishes (NoFiniteCentralSummand). Let be a bounded linear map with complete bound . Then the closure of the right averages , , viewed as maps into with the weak-* topology (weakRightAverageOrbit), lies in the ball of radius :
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 : Type*} [CStarAlgebra M]
universe u
variable {N X : Type u} [CStarAlgebra N] [PartialOrder N] [StarOrderedRing N]
[NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
theorem weakRightAverageOrbit_subset_ball (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] N)
(hno : NoFiniteCentralSummand N) (T : N →L[ℂ] N) {C : ℝ}
(hT : CompletelyBoundedEstimate T C) : weakRightAverageOrbit e T ⊆ weakOperatorBall C := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI