OAI.KadisonSimilarity.universalCommutatorTheorem
OpenThe theorem states that there is a single real constant C ≥ 0, independent of everything else, such that the following commutator estimate holds for every complex Hilbert space K in the universe Type u, with its complete inner product structure, and every von Neumann algebra P of bounded operators on K. For every bounded operator Y on K, every natural number n, and every n×n matrix X whose entries X_ij are all elements of P, regard X as a bounded operator on the n-fold Hilbert direct sum K^n (with the ℓ² norm) acting by matrix multiplication, and let Y⊗1ₙ be the operator on K^n applying Y in each coordinate. Then the operator norm of the commutator [Y⊗1ₙ, X] = (Y⊗1ₙ)X − X(Y⊗1ₙ) is at most C times δ times the operator norm of X, where δ is the norm of the inner derivation Z ↦ YZ − ZY restricted to P, that is, the scalar-level commutator norm of Y against P. Thus one constant C works uniformly for all n, all matrices over P, all Y, and all such K and P. This is the statement that the defined proposition UniversalCommutatorTheorem holds; the source leaves its proof as sorry.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/KadisonSimilarity.lean; bytes 3944..4095
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
import Definitions.Def_KadisonSimilarity
namespace OAI
noncomputable section
namespace KadisonSimilarity
universe u v
variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
/-- One absolute constant controls every finite matrix commutator. -/
theorem universalCommutatorTheorem : UniversalCommutatorTheorem.{u} := by
sorry
end KadisonSimilarity
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.