Favard-length decay exponent ()
Favard-length decay exponent: determine or improve its bounds; the repository records (lower) and 1 (upper).
Editorial MSC2020 classification. Original article codes and source evidence are recorded in the literature directory.
Problem statement
Let be a planar set. The Favard length of is defined by
where is orthogonal projection to the horizontal axis and is rotation by angle . [NPV2011-def-fav]
The Favard length has the following probabilistic interpretation: up to a constant factor, is the probability that a “Buffon’s needle” (a long line segment dropped at random) hits . [NPV2011-buffon-interpretation]
Let be the -th stage in the construction of the middle-half Cantor set, and let
Then is a union of axis-parallel squares of side length . [NPV2011-Kn-4n-squares]
A classical theorem of Besicovitch implies that as , and it remains open to determine the exact rate of decay. [NPV2011-besicovitch-open-decay]
We define the Favard-length decay exponent by
The best established range currently is
Lean 4
No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.
Background
-
Prior explicit upper bound. Before the power-law bound, the only explicit upper bound recorded in this literature was of iterated-log type, , attributed to Peres–Solomyak. [NPV2011-exp-logstar]
-
Non-optimality and a method barrier. Nazarov–Peres–Volberg remark that the exponent is not optimal, but that decay faster than would require new ideas (relative to their methods). [NPV2011-remark-n-1-4]
References (from the repository page)
-
[BV2010] Bateman, Michael; Volberg, Alexander. An estimate from below for the Buffon needle probability of the four-corner Cantor set. Mathematical Research Letters 17 (2010), no. 5, 959–967. DOI: https://doi.org/10.4310/MRL.2010.v17.n5.a12. arXiv PDF: https://arxiv.org/pdf/0807.2953. Google Scholar
-
[BV2010-thm1-lb-logn-over-n] loc: arXiv v1 PDF p.3, Theorem 1 (display (1.2)) quote: “There exists such that for all .”
-
[NPV2011] Nazarov, Fedor; Peres, Yuval; Volberg, Alexander. The power law for the Buffon needle probability of the four-corner Cantor set. St. Petersburg Mathematical Journal 22 (2011), no. 1, 61–72. DOI: https://doi.org/10.1090/S1061-0022-2010-01133-6. arXiv PDF: https://arxiv.org/pdf/0801.2942. Google Scholar
-
[NPV2011-besicovitch-open-decay] loc: arXiv v1 PDF p.1, Abstract (sentences on Besicovitch and open problem) quote: “A classical theorem of Besicovitch implies that the Favard length of tends to zero. It is still an open problem to determine its exact rate of decay.”
-
[NPV2011-exp-logstar] loc: arXiv v1 PDF p.1, Abstract (sentence on iterated-log upper bound) quote: “Until recently, the only explicit upper bound was , due to Peres and Solomyak.”
-
[NPV2011-def-fav] loc: arXiv v1 PDF p.2, equation (1.1) quote: “.”
-
[NPV2011-buffon-interpretation] loc: arXiv v1 PDF p.2, paragraph after (1.1) quote: “it is the probability that the “Buffon’s needle,” a long line segment dropped at random, hits ”
-
[NPV2011-Kn-4n-squares] loc: arXiv v1 PDF p.2, paragraph after the Buffon-needle interpretation quote: “The set is a union of squares with side length .”
-
[NPV2011-thm1-powerlaw] loc: arXiv v1 PDF p.3, Theorem 1 quote: “For every , there exists such that for all .”
-
[NPV2011-remark-n-1-4] loc: arXiv v1 PDF p.3, Remarks (bullet after Theorem 1) quote: “a bound decaying faster than would require new ideas.”
Progress & source assessment
Repository table (commit 2c1968c, 26 September 2026): best known lower bound ; best known upper bound 1. Values marked with an asterisk have minimal verification.
Known upper bounds
| Bound | Reference | Comments |
|---|---|---|
| [BV2010] | Bateman–Volberg prove , which rules out any estimate with . [BV2010-thm1-lb-logn-over-n] |
Known lower bounds
| Bound | Reference | Comments |
|---|---|---|
| Trivial (since is uniformly bounded). | ||
| [NPV2011] | Nazarov–Peres–Volberg prove (equivalently, ) for every . [NPV2011-thm1-powerlaw] |
- [1]Davis, Damek; Ivanisvili, Paata; Tao, Terence (maintainers). Optimization Constants in Mathematics, github.com/teorth/optimizationproblems (commit 2c1968c, 26 September 2026). — Favard-length decay exponent ($C_{60}$) linkApache-2.0 (repository license); constant pages reproduced with attribution; repository references retained.
Recorded progress
Add yours →Nothing recorded yet. A pointer to a paper the entry is missing counts.
Machine attempts
0 recordedAttempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.
No machine attempts recorded.
Sign in to run an attempt. New accounts start with enough credits for ten.
Discussion
0 notesNotes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.
No notes yet.
Sign in to add a note.