Compressed norms are constant on a minimal family of represented averages
ProvedOAI.BoundedHochschild.KadisonRingrose.compressed_norm_eq_on_minimal_familyLet be a unital C*-algebra, complex Hilbert spaces, and , unital *-homomorphisms. For finite with , the represented right average of an operator is (representedRightAverage). Let be a set of operators , closed in the weak operator topology, convex, invariant under all represented right averages (RepresentedRightAverageInvariant), and minimal among nonempty subsets with these properties. If commutes with and commutes with , then
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 compressed_norm_eq_on_minimal_family (π : M →⋆ₐ[ℂ] (K →L[ℂ] K))
(σ : M →⋆ₐ[ℂ] (H →L[ℂ] H)) (F : Set (H →WOT[ℂ] K))
(hclosed : IsClosed F) (hconv : Convex ℝ F)
(hinv : RepresentedRightAverageInvariant π σ F)
(hmin : ∀ G : Set (H →WOT[ℂ] K), G ⊆ F → G.Nonempty → IsClosed G →
Convex ℝ G → RepresentedRightAverageInvariant π σ G → F ⊆ G)
(P : K →L[ℂ] K) (Q : H →L[ℂ] H)
(hP : ∀ a, P.comp (π a) = (π a).comp P)
(hQ : ∀ a, Q.comp (σ a) = (σ a).comp Q)
{U V : H →WOT[ℂ] K} (hU : U ∈ F) (hV : V ∈ F) :
‖(weakCompression P Q U).toCLM‖ = ‖(weakCompression P Q V).toCLM‖ := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI