All workflows

Workflow runs

• Prove modularUnitaryGroup_conj_image and tomita_theorem (stage 5c com…

  failed:
  Lean Action CI#712:Commitf01f55cpushedbyKellyJDavis
  tomita-takesaki

  Nov 15, 20261m 35s
  More actions for workflow run 712

• Prove the Fourier step and that Δ^{it} Ja'J Δ^{-it} commutes with M'

  failed:
  Lean Action CI#711:Commitd813417pushedbyKellyJDavis
  tomita-takesaki

  Nov 15, 20261m 35s
  More actions for workflow run 711

• Prove Jones's Proposition 13.2.2 for all vectors

  failed:
  Lean Action CI#710:Commit6df44ddpushedbyKellyJDavis
  tomita-takesaki

  Nov 15, 20261m 57s
  More actions for workflow run 710

• Prove Jones's Proposition 13.2.2 on H₀ via the strip formula

  failed:
  Lean Action CI#709:Commitb34d3dcpushedbyKellyJDavis
  tomita-takesaki

  Nov 15, 20261m 38s
  More actions for workflow run 709

• Prove integrability of the van Daele integrand

  failed:
  Lean Action CI#708:Commit6d6d58dpushedbyKellyJDavis
  tomita-takesaki

  Nov 15, 20262m 4s
  More actions for workflow run 708

• Prove the rearranged identities (Tomita–Takesaki stage 5b complete)

  failed:
  Lean Action CI#707:Commitb788692pushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20261m 51s
  More actions for workflow run 707

• Prove the approximation in the graphs of S and S*

  failed:
  Lean Action CI#706:Commit84d6fdfpushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20262m 3s
  More actions for workflow run 706

• Prove Jones's Lemma 13.1.5 (exists_isVanDaeleTriple)

  failed:
  Lean Action CI#705:Commitce512e8pushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20261m 47s
  More actions for workflow run 705

• Prove the domains of g_λ(Δ)ψ for ψ ∈ Dom Δ^{-1/2}

  failed:
  Lean Action CI#704:Commitaaf5a90pushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20261m 55s
  More actions for workflow run 704

• Prove Δ^{±1/2} = p_{±1/2,n}(Δ) on Range E_n and H₀ ⊆ Dom S ∩ Dom S*

  failed:
  Lean Action CI#703:Commit3574a0dpushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20262m 0s
  More actions for workflow run 703

• State Jones Prop 13.2.2 and Tomita's theorem (Tomita–Takesaki stage 5c)

  failed:
  Lean Action CI#702:Commitfd0a90bpushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20261m 44s
  More actions for workflow run 702

• Add the approved definitions JTJ and van Daele triple

  failed:
  Lean Action CI#701:Commit7d677aepushedbyKellyJDavis
  tomita-takesaki

  Nov 14, 20261m 57s
  More actions for workflow run 701

• Record the van Daele batch 5b review (PASS)

  failed:
  Lean Action CI#700:Commitee61f3cpushedbyKellyJDavis
  tomita-takesaki

  Nov 13, 20261m 33s
  More actions for workflow run 700

• Prove the strip formula (Tomita–Takesaki stage 4 complete)

  failed:
  Lean Action CI#699:Commit9489cbepushedbyKellyJDavis
  tomita-takesaki

  Nov 13, 20262m 0s
  More actions for workflow run 699

• Prove regularity of the strip quotient and its horizontal bound

  failed:
  Lean Action CI#698:Commit40d5d83pushedbyKellyJDavis
  tomita-takesaki

  Nov 13, 20261m 40s
  More actions for workflow run 698

• State the strip formula and Fourier uniqueness (Tomita–Takesaki stage 4)

  failed:
  Lean Action CI#697:Commit6ff5c4apushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20262m 1s
  More actions for workflow run 697

• Drop unused hypotheses in the stage 3 Tomita–Takesaki lemmas

  completed successfully:
  Lean Action CI#696:Commitcf6399cpushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 202617m 2s
  More actions for workflow run 696

• Prove the commutant's modular conjugation is J (Tomita–Takesaki stage…

  failed:
  Lean Action CI#695:Commitd3df0c0pushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20263m 47s
  More actions for workflow run 695

• Prove S* = Δ^{1/2} J and S* = J Δ^{-1/2}

  failed:
  Lean Action CI#694:Commit1f256dapushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20264m 12s
  More actions for workflow run 694

• Prove that the approximants of a0 lie in M' and converge to (ξ, η)

  failed:
  Lean Action CI#693:Commit24d5204pushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20264m 3s
  More actions for workflow run 693

• Prove the closure properties of a0 and that unitaries of M commute wi…

  failed:
  Lean Action CI#692:Commit2fbd67dpushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20264m 12s
  More actions for workflow run 692

• Prove the core form of S* and that the closure of F0's graph lies in S*

  failed:
  Lean Action CI#691:Commit5d3e6f7pushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20264m 16s
  More actions for workflow run 691

• Prove the square root of A⁻¹ and the commutant-of-unitaries lemma

  failed:
  Lean Action CI#690:Commit26dba86pushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20264m 42s
  More actions for workflow run 690

• Prove the unitary a + i√(1 − a²) lies in a von Neumann set

  failed:
  Lean Action CI#689:Commit25a0b26pushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20263m 46s
  More actions for workflow run 689

• Prove the commuting-unitary and approximant lemmas (Tomita–Takesaki s…

  failed:
  Lean Action CI#688:Commit62b0adbpushedbyKellyJDavis
  tomita-takesaki

  Nov 12, 20265m 7s
  More actions for workflow run 688