feat: add von Neumann double commutant theorem eval problem - #11
Merged
Conversation
States the classical DCT for a unital *-subalgebra of B(H): equality with the double commutant is equivalent to WOT-closedness and to SOT-closedness (the latter appearing in Mathlib as the topology of pointwise convergence on continuous linear maps). WOT and SOT live on irreducible type copies of `H →L[ℂ] H`, so each closure condition is stated on the image of the carrier under the canonical inclusion into the corresponding type copy. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
kim-em
force-pushed
the
eval/vonneumann-double-commutant
branch
from
April 17, 2026 11:01
8526d29 to
2588e03
Compare
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds an eval problem for von Neumann's double commutant theorem.
For a unital *-subalgebra
SofH →L[ℂ] Hon a complex Hilbert spaceH, the statement asserts the TFAE of:Sequals its double commutant (Set.centralizer (Set.centralizer S) = S)Sis closed in the weak operator topologySis closed in the strong operator topology (in Mathlib: the topology of pointwise convergence on continuous linear maps)Mathlib already has
VonNeumannAlgebra,StarSubalgebra,Set.centralizer, the WOT type copy (ContinuousLinearMapWOT/H →WOT[ℂ] H), and the SOT type copy (PointwiseConvergenceCLM/H →Lₚₜ[ℂ] H, documented as "sometimes also called the strong operator topology"). The statement pushes the carrier through each canonical inclusion and asserts closedness in the type copy — the ergonomic cost of WOT/SOT being irreducible type copies rather than topologies onH →L[ℂ] Hitself.Test plan
lake build FormalMathEval.Analysis.VonNeumannDoubleCommutantlake exe lean-eval validate-manifestlake exe lean-eval check-problem-buildlake exe lean-eval generate --problem vonNeumann_doubleCommutant_tfaelake exe lean-eval check-generated-builds --problem vonNeumann_doubleCommutant_tfae🤖 Generated with Claude Code