Open Research Index

Exponential separation of analytic self-conformal sets on the real line: Lean formalisation

Balázs Bárány, István Kolossváry, Sascha Troscheit

Palomar Registrypalomar/PALOMAR-2026-10-11-000004Oct 14, 2026math.DSscore 0

Lean 4 formalisation of exponential separation for analytic iterated function systems on the real line. Strong exponential separation holds on an open and dense subset in the C2 topology and follows from an explicit criterion involving dual projections. The development characterises conjugacy to self-similar systems and proves dimension consequences conditional on cited results of Rapaport and Bowen, including a drop in the L^q dimensions of the natural measure of a concrete three-map example.

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