von Neumann double commutant theorem

vonNeumann_doubleCommutant_tfae — a formalization challenge from the lean-eval benchmark.

Notes

The classical double commutant theorem: for a unital *-subalgebra of bounded operators on a complex Hilbert space, equality with the double commutant is equivalent to closedness in the weak operator topology and to closedness in the strong operator topology. WOT and SOT live on Mathlib's irreducible type copies of H →L[ℂ] H (ContinuousLinearMapWOT and PointwiseConvergenceCLM), so each closure condition is phrased on the image of the carrier under the canonical inclusion.

Formal statement

theorem vonNeumann_doubleCommutant_tfae
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    List.TFAE
      [ Set.centralizer (Set.centralizer (S : Set (H →L[ℂ] H))) = S
      , IsClosed
          (ContinuousLinearMapWOT.ofCLM '' (S : Set (H →L[ℂ] H)))
      , IsClosed
          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
            (S : Set (H →L[ℂ] H))) ] := by
  sorry

Informal solution sketch

One direction: centralizers are WOT-closed, so any set equal to its double commutant is WOT-closed; norm topology refines WOT refines SOT for continuity of evaluation, and closedness under a finer convex topology is implied by closedness under a coarser one (via Hahn-Banach for convex sets). Hard direction: given a unital *-subalgebra S that is SOT-closed, for any T in S'' and any finite family of vectors use the amplification S ⊗ 1_n acting diagonally on H^n together with the projection onto the closure of (S ⊗ 1_n) applied to the vector to produce a net in S converging SOT to T.

Source

J. von Neumann, Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren, Math. Ann. 102 (1930), 370-427.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: vonNeumann_doubleCommutant_tfae
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.