feat: add von Neumann double commutant theorem eval problem

LeanEval/Analysis/VonNeumannDoubleCommutant.lean

@@ -0,0 +1,39 @@
+import Mathlib.Analysis.VonNeumannAlgebra.Basic
+import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
+import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Analysis
+
+/-!
+Von Neumann's double commutant theorem.
+
+For a unital *-subalgebra `S` of bounded operators on a complex Hilbert space `H`, the
+following are equivalent:
+
+1. `S` equals its double commutant `S''`.
+2. `S` is closed in the weak operator topology.
+3. `S` is closed in the strong operator topology (in Mathlib, the topology of pointwise
+   convergence on continuous linear maps).
+
+The WOT and SOT live on irreducible type copies of `H →L[ℂ] H`, so each closed-ness
+condition is stated as the closedness of the image of `S` under the canonical inclusion
+into the corresponding type copy.
+-/
+
+@[eval_problem]
+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
+          (ContinuousLinearMap.toWOT (RingHom.id ℂ) H H '' (S : Set (H →L[ℂ] H)))
+      , IsClosed
+          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
+            (S : Set (H →L[ℂ] H))) ] := by
+  sorry
+
+end Analysis
+end LeanEval

generated/index.json

@@ -250,5 +250,14 @@
     "module": "LeanEval.Topology.SmaleConjecture",
     "theorem": "smale_conjecture",
     "generated_path": "generated/smale_conjecture"
+  },
+  {
+    "id": "vonNeumann_doubleCommutant_tfae",
+    "title": "von Neumann double commutant theorem",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Analysis.VonNeumannDoubleCommutant",
+    "theorem": "vonNeumann_doubleCommutant_tfae",
+    "generated_path": "generated/vonNeumann_doubleCommutant_tfae"
   }
 ]

generated/vonNeumann_doubleCommutant_tfae/Challenge.lean

@@ -0,0 +1,12 @@
+import Mathlib
+
+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
+          (ContinuousLinearMap.toWOT (RingHom.id ℂ) H H '' (S : Set (H →L[ℂ] H)))
+      , IsClosed
+          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
+            (S : Set (H →L[ℂ] H))) ] := by
+  sorry

generated/vonNeumann_doubleCommutant_tfae/README.md

@@ -0,0 +1,25 @@
+# `vonNeumann_doubleCommutant_tfae`
+
+von Neumann double commutant theorem
+
+- Problem ID: `vonNeumann_doubleCommutant_tfae`
+- Test Problem: no
+- Submitter: Kim Morrison
+- 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.
+- Source: J. von Neumann, Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren, Math. Ann. 102 (1930), 370-427.
+- Informal solution: 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.
+
+Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the
+trusted benchmark and fixed by the repository.
+
+Write your solution in `Submission.lean` and any additional local modules under
+`Submission/`.
+
+Participants may use Mathlib freely. Any helper code not already available in
+Mathlib must be inlined into the submission workspace.
+
+Multi-file submissions are allowed through `Submission.lean` and additional local
+modules under `Submission/`.
+
+`lake test` runs comparator for this problem. The command expects a comparator
+binary in `PATH`, or in the `COMPARATOR_BIN` environment variable.

generated/vonNeumann_doubleCommutant_tfae/Solution.lean

@@ -0,0 +1,13 @@
+import Mathlib
+import Submission
+
+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
+          (ContinuousLinearMap.toWOT (RingHom.id ℂ) H H '' (S : Set (H →L[ℂ] H)))
+      , IsClosed
+          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
+            (S : Set (H →L[ℂ] H))) ] := by
+  exact Submission.vonNeumann_doubleCommutant_tfae S

generated/vonNeumann_doubleCommutant_tfae/Submission.lean

@@ -0,0 +1,17 @@
+import Mathlib
+import Submission.Helpers
+
+namespace Submission
+
+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
+          (ContinuousLinearMap.toWOT (RingHom.id ℂ) H H '' (S : Set (H →L[ℂ] H)))
+      , IsClosed
+          (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H ''
+            (S : Set (H →L[ℂ] H))) ] := by
+  sorry
+
+end Submission

generated/vonNeumann_doubleCommutant_tfae/Submission/Helpers.lean

@@ -0,0 +1,3 @@
+namespace Submission.Helpers
+
+end Submission.Helpers

generated/vonNeumann_doubleCommutant_tfae/WorkspaceTest.lean

@@ -0,0 +1,38 @@
+import Lean
+
+open Lean
+
+def comparatorExists (comparatorBin : String) : IO Bool := do
+  if comparatorBin.contains '/' then
+    return (← System.FilePath.pathExists comparatorBin)
+  try
+    let child ← IO.Process.spawn {
+      cmd := "sh"
+      args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
+    }
+    let exitCode ← child.wait
+    return exitCode == 0
+  catch _ =>
+    return false
+
+def main : IO UInt32 := do
+  let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
+  if !(← comparatorExists comparatorBin) then
+    IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
+    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
+    pure 1
+  else
+    try
+      let child ← IO.Process.spawn {
+        cmd := "lake"
+        args := #["env", comparatorBin, "config.json"]
+      }
+      let exitCode ← child.wait
+      pure exitCode
+    catch err =>
+      IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
+      IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+      IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
+      IO.eprintln s!"Original error: {err}"
+      pure 1

generated/vonNeumann_doubleCommutant_tfae/config.json

@@ -0,0 +1,13 @@
+{
+  "challenge_module": "Challenge",
+  "solution_module": "Solution",
+  "theorem_names": [
+    "vonNeumann_doubleCommutant_tfae"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ],
+  "enable_nanoda": false
+}

generated/vonNeumann_doubleCommutant_tfae/lakefile.toml

@@ -0,0 +1,24 @@
+name = "vonNeumann_doubleCommutant_tfae"
+testDriver = "workspace_test"
+defaultTargets = ["Challenge", "Solution", "Submission"]
+
+[leanOptions]
+autoImplicit = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "50d5513e83c"
+
+[[lean_lib]]
+name = "Challenge"
+
+[[lean_lib]]
+name = "Solution"
+
+[[lean_lib]]
+name = "Submission"
+
+[[lean_exe]]
+name = "workspace_test"
+root = "WorkspaceTest"

generated/vonNeumann_doubleCommutant_tfae/lean-toolchain

@@ -0,0 +1,2 @@
+leanprover/lean4:v4.30.0-rc1
+

manifests/problems.toml

@@ -307,3 +307,14 @@ submitter = "Kim Morrison"
 notes = "Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform rel boundary to a family fully factoring through O(4)). Mathlib does not yet carry the C-infinity topology on Diffeomorph, which would be needed for the direct homotopy-equivalence formulation."
 source = "A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983)."
 informal_solution = "Hatcher proves Diff(S3) is homotopy equivalent to O(4) by analyzing configurations of 2-spheres in S3 (the bigon criterion) and deducing by induction that every self-diffeomorphism is isotopic to a linear one, with all higher parameterized versions handled by the same incompressible-surface machinery."
+
+[[problem]]
+id = "vonNeumann_doubleCommutant_tfae"
+title = "von Neumann double commutant theorem"
+test = false
+module = "LeanEval.Analysis.VonNeumannDoubleCommutant"
+theorem = "vonNeumann_doubleCommutant_tfae"
+submitter = "Kim Morrison"
+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."
+source = "J. von Neumann, Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren, Math. Ann. 102 (1930), 370-427."
+informal_solution = "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."