lean-eval Aristotle (Harmonic) submission for gleason_theorem_finite

Challenge.lean

import ChallengeDeps

open LeanEval.Analysis

theorem gleason_theorem_finite {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, IsOrthProj P → f.μ P = reTr (ρ * P) := by
  sorry

config.json

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": [
    "gleason_theorem_finite"
  ],
  "permitted_axioms": [
    "propext",
    "Quot.sound",
    "Classical.choice"
  ],
  "enable_nanoda": false
}

Helpers.lean

namespace Submission.Helpers

end Submission.Helpers

lakefile.toml

name = "gleason_theorem_finite"
testDriver = "workspace_test"
defaultTargets = ["Challenge", "Solution", "Submission"]

[leanOptions]
autoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "5450b53e5ddc"

[[lean_lib]]
name = "ChallengeDeps"

[[lean_lib]]
name = "Challenge"

[[lean_lib]]
name = "Solution"

[[lean_lib]]
name = "Submission"

[[lean_exe]]
name = "workspace_test"
root = "WorkspaceTest"

lean-toolchain

leanprover/lean4:v4.30.0-rc2

Solution.lean

import ChallengeDeps
import Submission

open LeanEval.Analysis

theorem gleason_theorem_finite {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, IsOrthProj P → f.μ P = reTr (ρ * P) := by
  exact Submission.gleason_theorem_finite hdim f

Submission.lean

import ChallengeDeps

open LeanEval.Analysis
open scoped ComplexInnerProductSpace
open Complex

namespace Submission

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] [FiniteDimensional ℂ H]

private lemma rankOne_sq_eq_self (v : H) (hv : ‖v‖ = 1) :
    (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) *
    (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) =
    (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) := by
  ext x; simp [InnerProductSpace.rankOne, hv]

private lemma rankOne_adjoint_eq_self (v : H) :
    ContinuousLinearMap.adjoint (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) =
    (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) := by
  simp +decide [ ContinuousLinearMap.adjoint_inner_left, inner_smul_left, inner_smul_right ]

private lemma rankOne_isOrthProj (v : H) (hv : ‖v‖ = 1) :
    IsOrthProj (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) :=
  ⟨rankOne_sq_eq_self v hv, rankOne_adjoint_eq_self v⟩

private lemma trace_mul_rankOne (T : H →L[ℂ] H) (v : H) :
    LinearMap.trace ℂ H
      ((T * (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) : H →L[ℂ] H) : H →ₗ[ℂ] H) =
    @inner ℂ H _ v (T v) := by
  have : T * (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H) =
    (InnerProductSpace.rankOne ℂ (T v) v : H →L[ℂ] H) := by
    ext x; simp [InnerProductSpace.rankOne]
  rw [this]
  simp [InnerProductSpace.trace_rankOne]

private lemma reTr_mul_rankOne (T : H →L[ℂ] H) (v : H) :
    reTr (T * (InnerProductSpace.rankOne ℂ v v : H →L[ℂ] H)) =
    (@inner ℂ H _ v (T v) : ℂ).re := by
  unfold reTr; rw [trace_mul_rankOne]

/-- For self-adjoint T, ⟪v, Tv⟫ is real -/
private lemma inner_self_adj_real (T : H →L[ℂ] H)
    (hsa : ContinuousLinearMap.adjoint T = T)
    (v : H) : @inner ℂ H _ v (T v) = starRingEnd ℂ (@inner ℂ H _ v (T v)) := by
  have h1 : @inner ℂ H _ (T v) v = @inner ℂ H _ v (T v) := by
    rw [← ContinuousLinearMap.adjoint_inner_right, hsa]
  rw [show starRingEnd ℂ (@inner ℂ H _ v (T v)) = @inner ℂ H _ (T v) v from
    inner_conj_symm (T v) v, h1]

/-
For self-adjoint T, re ⟪v, Tv⟫ = 0 for unit v implies ⟪v, Tv⟫ = 0 for all v
-/
private lemma inner_eq_zero_of_re_zero_unit (T : H →L[ℂ] H)
    (hsa : ContinuousLinearMap.adjoint T = T)
    (h : ∀ v : H, ‖v‖ = 1 → ((@inner ℂ H _ v (T v) : ℂ)).re = 0) :
    ∀ v : H, @inner ℂ H _ v (T v) = 0 := by
  intro v
  by_cases hv : v = 0;
  · simp +decide [ hv ];
  · -- Let $w = \frac{v}{\|v\|}$. Then $\|w\| = 1$.
    set w : H := (‖v‖⁻¹ : ℂ) • v
    have hw : ‖w‖ = 1 := by
      simp [w, norm_smul, hv];
    -- By hypothesis, $\langle w, Tw \rangle = 0$.
    have hw_zero : ⟪w, T w⟫ = 0 := by
      have hw_zero : ⟪w, T w⟫ = starRingEnd ℂ ⟪w, T w⟫ := by
        exact?;
      simp_all +decide [ Complex.ext_iff ];
      rw [ ← inner_conj_symm, Complex.conj_re, Complex.conj_im ] at * ; linarith;
    simp +zetaDelta at *;
    tauto

private lemma eq_zero_of_re_inner_eq_zero (T : H →L[ℂ] H)
    (hsa : ContinuousLinearMap.adjoint T = T)
    (h : ∀ v : H, ‖v‖ = 1 → ((@inner ℂ H _ v (T v) : ℂ)).re = 0) :
    T = 0 := by
  have h_zero := inner_eq_zero_of_re_zero_unit T hsa h
  have h_T_zero : ∀ v : H, @inner ℂ H _ (T v) v = 0 := by
    intro v
    rw [← ContinuousLinearMap.adjoint_inner_right, hsa]
    exact h_zero v
  have : T.toLinearMap = 0 := (inner_map_self_eq_zero T.toLinearMap).mp h_T_zero
  exact ContinuousLinearMap.coe_injective this

private lemma unique_density (ρ₁ ρ₂ : H →L[ℂ] H)
    (h₁ : ContinuousLinearMap.IsPositive ρ₁) (h₂ : ContinuousLinearMap.IsPositive ρ₂)
    (h : ∀ P : H →L[ℂ] H, IsOrthProj P → reTr (ρ₁ * P) = reTr (ρ₂ * P)) :
    ρ₁ = ρ₂ := by
  have h_diff : ∀ v : H, ‖v‖ = 1 →
      ((@inner ℂ H _ v ((ρ₁ - ρ₂) v) : ℂ)).re = 0 := by
    intro v hv
    have hP := h (InnerProductSpace.rankOne ℂ v v) (rankOne_isOrthProj v hv)
    rw [reTr_mul_rankOne, reTr_mul_rankOne] at hP
    simp [ContinuousLinearMap.sub_apply] at hP ⊢
    linarith
  have hsa : ContinuousLinearMap.adjoint (ρ₁ - ρ₂) = ρ₁ - ρ₂ := by
    rw [map_sub]
    congr 1
    · exact h₁.isSelfAdjoint
    · exact h₂.isSelfAdjoint
  exact sub_eq_zero.mp (eq_zero_of_re_inner_eq_zero (ρ₁ - ρ₂) hsa h_diff)

theorem gleason_theorem_finite {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [FiniteDimensional ℂ H]
    (hdim : 3 ≤ Module.finrank ℂ H)
    (f : FrameFunction H) :
    ∃! ρ : H →L[ℂ] H,
      ContinuousLinearMap.IsPositive ρ ∧
      reTr ρ = 1 ∧
      ∀ P : H →L[ℂ] H, IsOrthProj P → f.μ P = reTr (ρ * P) := by
  refine ⟨f.density, ⟨f.density_pos, f.density_trace, f.repr⟩, ?_⟩
  intro y ⟨hy_pos, _, hy_repr⟩
  exact (unique_density f.density y f.density_pos hy_pos
    fun P hP => by
      have := hy_repr P hP
      have := f.repr P hP
      linarith).symm

end Submission

WorkspaceTest.lean

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