Open Research Index

Vulkin-prog/paper-c-lean

Brice Pouly

Palomar Registrypalomar/PALOMAR-2026-08-26-000010Aug 27, 2026math.NTscore 0

Lean 4 formalization of three Poisson-limit statements for the starting points of long constant stretches of an extended Rademacher random completely multiplicative function in a dyadic block, corresponding to the three clauses of Theorem 1.2 in the cited source article. The first proves a total-variation Poisson approximation uniformly over every deterministic mask of the dyadic block. The second gives the Laplace-functional characterization of the limiting spatial Poisson point process. The third gives the corresponding marked characterization together with uniform tightness of the…

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