Uniform marked source-hereditary finite-scale estimate

Open

StickyKakeya4.uniform_marked_source_hereditary_finite_scale

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

contact-geometrygeometric-measure-theorykakeya

Let $S$ be a measurable valid direction selector with carrier packing dimension $3$ . For every $\varepsilon>0$ , uniformly over every sufficiently fine admissible shaded, weighted source $D$ from $S$ and every fractional restriction $R$ of that source,

\int F_R(x)^2\,dx\le C_\varepsilon\delta^{-\varepsilon}S_R, \qquad S_R\le C_\varepsilon\delta^{-\varepsilon}|U_R|.

Here $S_R=\int F_R$ , $U_R=\{F_R>0\}$ , and $\delta$ is the source thickness. Because all fractional restrictions are allowed, the assertion includes arbitrary retained descendant/source restrictions. Its constant is independent of the finite carrier tree, and the affine fibre mark remains part of the admissibility data.

Preamble

import Definitions.Def_sticky_kakeya4_core

open MeasureTheory Set

Formal statement

namespace StickyKakeya4

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

end StickyKakeya4

Source

Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, uniform finite-scale marked-source conclusion in Section 9 and Appendix B.

Read-back

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

For every measurable set $S$ of marked lines $\ell=((u,v),m)$ in $\mathbb R^4$ , assume that every member has $\|u\|=1$ and $\langle v,u\rangle=0$ , every unit direction occurs in exactly one member of $S$ , and the custom packing dimension of the unmarked carrier is exactly $3$ , where packing dimension is the countable-cover infimum of upper Minkowski dimensions defined through finite open-ball covering numbers. Then, for every real $\varepsilon>0$ and every $C_{\mathrm{pack}}\in[0,\infty]$ with $C_{\mathrm{pack}}\ne0,\infty$ , there exist $A\in[0,\infty]$ with $A\ne0,\infty$ and $\delta_0>0$ such that the following holds for every natural number $n$ , including $0$ , and every two finite-scale sources $D,R$ indexed by $\operatorname{Fin}(n)$ . Assume $D$ has thickness at most $\delta_0$ , all of its marked lines belong to $S$ , and $D$ is admissible: its thickness $\delta_D$ satisfies $0<\delta_D<1$ ; its weights are at most $1$ ; its stored fibre marks equal the line marks; its lines have unit direction orthogonal to offset; its shadings are measurable and lie within distance $\delta_D$ of their corresponding marked unit segments; and, for every $\delta_D\le r\le1$ , the covering number of its direction-offset pairs is at most $C_{\mathrm{pack}}(\operatorname{ofReal}r)^{-(3+\varepsilon)}$ . Assume also that $R$ has the same thickness, indexed marked lines, fibre marks, and entire nested carrier tree as $D$ , while each shading of $R$ is a measurable subset of the corresponding shading of $D$ and each weight of $R$ is at most the corresponding weight of $D$ . Define

f_R(x)=\sum_{i\in\operatorname{Fin}(n)}w_i^R\mathbf1_{Y_i^R}(x),\quad M_R=\int_{\mathbb R^4}f_R(x)\,d\operatorname{vol}(x),\quad U_R=\{x:0<f_R(x)\}.

Then

\int_{\mathbb R^4}f_R(x)^2\,d\operatorname{vol}(x) \le A(\operatorname{ofReal}\delta_D)^{-\varepsilon}M_R

and

M_R\le A(\operatorname{ofReal}\delta_D)^{-\varepsilon}\operatorname{vol}(U_R).

No positivity of $M_R$ or of any individual retained weight is assumed.

View graph