Open Research Index

Formalization of a sharp cone square-function estimate via superorthogonality

Joris Roos

Palomar Registrypalomar/PALOMAR-2026-10-16-000005Oct 17, 2026math.CAscore 0

This is a Lean 4 formalization of Theorems 1.1 and 1.4 from the paper "Diameter-free reverse inequalities and superorthogonality" by A. Cushman, C. Demeter and S. Wu. Theorem 1.1 is a reverse square-function estimate in L^4 under a superorthogonality hypothesis that is weaker than the Type IV superorthogonality of Gressman-Pierce-Roos-Yung. Theorem 1.4 applies a similar estimate to the three-dimensional light cone, yielding a refinement of the reverse cone square-function estimate of Guth-Wang-Zhang.

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-10-16-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000005/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-10-16-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'