Open Research Index

lukasliehr/GrothendieckBessel

Lukas Liehr, Mitchell A. Taylor, Peiyang Yu

Palomar Registrypalomar/PALOMAR-2026-08-26-000002Aug 26, 2026math.FAscore 0

A Lean 4 formalization of the existence assertion in Theorem 1.1 of arXiv:2608.12280v1 with the sharp constant K = 1: for every countable Bessel sequence with bound 1 in a complex Hilbert space, there exist measurable functions on the unit interval, pointwise bounded by 1, whose correlations reproduce the sequence's Gram matrix. This solves an open problem posed by Olevskii.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-26-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-26-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-26-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'