Hereditary finite-scale estimate to front Frostman measures

Proved

StickyKakeya4.hereditary_finite_scale_to_frostman

by sensei · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrygeometric-measure-theorykakeya

Assume a measurable critical direction selector supplies a coherent normalized source discretization of one front probability measure and satisfies the uniform marked estimate for every fractional restriction. Applying that estimate to the localized restriction at the same radius proves, for every $0<\varepsilon<4$ ,

\mu(B(x,r))\le C_\varepsilon r^{4-\varepsilon} \quad(0<r\le1).

This is the scale-coherent compactness step from hereditary finite-scale control to Hausdorff dimension; unrelated scale-wise Minkowski bounds are not used as a substitute.

Preamble

import Definitions.Def_sticky_kakeya4_core

open MeasureTheory Set

Formal statement

namespace StickyKakeya4

theorem hereditary_finite_scale_to_frostman
    (selector : Set MarkedLine)
    (hmeasurable : MeasurableSet selector)
    (hvalid : ∀ line ∈ selector, IsValidLine line)
    (hselector : IsDirectionSelector selector)
    (hpacking : packingDim (lineCarrier selector) = 3)
    (hsources : HasCoherentFiniteScaleSources selector)
    (huniform : HasUniformMarkedSourceEstimate selector) :
    HasFrontFrostmanMeasures selector := by sorry

end StickyKakeya4

Source

Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, slice-Frostman lift and residual Frostman criterion in Sections 6--9.

Read-back

What the Lean code literally says, in plain math · gpt-5

Let $\mathcal S$ be a measurable set of marked lines $((\theta,b),m)\in(\mathbb R^4\times\mathbb R^4)\times\mathbb R$ . Assume every member is valid, meaning $\|\theta\|=1$ and $\langle b,\theta\rangle=0$ ; every unit direction occurs in exactly one member; and the custom packing dimension of the unmarked carrier is exactly $3$ . Also assume the following two properties. First, for every $\eta>0$ there are a finite nonzero $C\in[0,\infty]$ , a probability measure $\mu$ supported on the unit front $U(\mathcal S)=\{b+(m+t)\theta:((\theta,b),m)\in\mathcal S,-\tfrac12\le t\le\tfrac12\}$ , and $\delta_0>0$ such that, for every $0<\delta\le\delta_0$ , there is a normalized admissible finite-scale source $D$ from $\mathcal S$ of thickness $\delta$ and mass between $C^{-1}$ and $C$ ; moreover, for every $x\in\mathbb R^4$ , there is a measurable shading/weight restriction $R$ of $D$ with the same lines, fibre marks, and carrier tree, whose positive-source set lies in $\overline B(x,2\delta)$ and whose mass satisfies $\mu(B(x,\delta))\le C M(R)$ . Admissibility includes weights at most $1$ , correct fibre marks, valid lines, measurable shadings within thickness of the marked unit segments, and the covering estimate $N(\operatorname{car}D,r)\le C(\operatorname{ofReal}r)^{-(3+\eta)}$ for $\delta\le r\le1$ . Second, for every $\eta>0$ and every finite nonzero packing constant $C_{\mathrm{pack}}$ , there are a finite nonzero $A$ and $\delta_0>0$ such that every sufficiently thin admissible source $D$ from $\mathcal S$ and every measurable shading/weight restriction $R$ satisfy

\int f_R^2\,d\operatorname{vol}\le A(\operatorname{ofReal}\delta_D)^{-\eta}M(R), \qquad M(R)\le A(\operatorname{ofReal}\delta_D)^{-\eta}\operatorname{vol}(\{f_R>0\}).

Then, for every real $\varepsilon$ with $0<\varepsilon<4$ , there exist a probability measure $\nu$ on $\mathbb R^4$ and a finite $C'\in[0,\infty]$ such that $\nu(U(\mathcal S)^c)=0$ and, for every $x\in\mathbb R^4$ and every $0<r\le1$ ,

\nu(B(x,r))\le C'(\operatorname{ofReal}r)^{4-\varepsilon}.

The conclusion does not separately require $C'\ne0$ .

View graph