Marked lines, packing dimension, and finite-scale source interfaces in R4

Definition

sticky_kakeya4_core

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

contact-geometrygeometric-measure-theorykakeyapacking-dimension

This module fixes the complete interface used by the mission. It defines valid marked oriented lines in $\mathbb R^4$ , direction selectors, their unit fronts, covering numbers, upper Minkowski dimension, packing dimension, and compact full-direction Sticky data.

It also defines shaded and weighted finite-scale sources. Each source retains its affine fibre mark and an arbitrary finite nested carrier tree. Fractional source restrictions may lower weights and replace shadings by measurable subsets while keeping the lines, marks, and tree; retained descendant restrictions are recorded separately. The module states three proof interfaces: a coherent normalized discretization of one front probability measure at every small scale, a uniform $L^2$ /union estimate for every fractional restriction, and Frostman probability measures on the selector front.

The collision residual and the matrix-pencil/Lagrangian-incidence model supply the contact--symplectic local geometry used by the finite-scale estimate.

Definition code

import Mathlib

open Filter MeasureTheory Set
open scoped ENNReal RealInnerProductSpace Topology

noncomputable section

namespace StickyKakeya4

abbrev E3 := EuclideanSpace ℝ (Fin 3)
abbrev E4 := EuclideanSpace ℝ (Fin 4)
abbrev MarkedLine := (E4 × E4) × ℝ

def direction (line : MarkedLine) : E4 := line.1.1
def offset (line : MarkedLine) : E4 := line.1.2
def mark (line : MarkedLine) : ℝ := line.2

def IsValidLine (line : MarkedLine) : Prop :=
  ‖direction line‖ = 1 ∧ inner ℝ (offset line) (direction line) = 0

def lineCarrier (lines : Set MarkedLine) : Set (E4 × E4) :=
  (fun line => (direction line, offset line)) '' lines

def FullDirection (lines : Set MarkedLine) : Prop :=
  ∀ θ : E4, ‖θ‖ = 1 → ∃ line ∈ lines, direction line = θ

def IsDirectionSelector (lines : Set MarkedLine) : Prop :=
  ∀ θ : E4, ‖θ‖ = 1 → ∃! line, line ∈ lines ∧ direction line = θ

def unitFront (lines : Set MarkedLine) : Set E4 :=
  {x | ∃ line ∈ lines, ∃ t ∈ Set.Icc (-(1 / 2 : ℝ)) (1 / 2 : ℝ),
    x = offset line + (mark line + t) • direction line}

def coversAtRadius {X : Type*} [PseudoMetricSpace X]
    (s : Set X) (r : ℝ) (centers : Finset X) : Prop := by
  classical
  exact s ⊆ ⋃ x ∈ (centers : Set X), Metric.ball x r

def coveringNumber {X : Type*} [PseudoMetricSpace X]
    (s : Set X) (r : ℝ) : ℝ≥0∞ := by
  classical
  exact sInf {n : ℝ≥0∞ | ∃ centers : Finset X,
    coversAtRadius s r centers ∧ n = centers.card}

def upperMinkowskiDim {X : Type*} [PseudoMetricSpace X]
    (s : Set X) : ℝ≥0∞ :=
  sInf {d : ℝ≥0∞ | d ≠ ⊤ ∧ ∃ C : ℝ≥0∞, C ≠ ⊤ ∧
    ∀ᶠ r in 𝓝[>] (0 : ℝ),
      coveringNumber s r ≤ C * (ENNReal.ofReal r).rpow (-d.toReal)}

def packingDim {X : Type*} [PseudoMetricSpace X]
    (s : Set X) : ℝ≥0∞ :=
  sInf {d : ℝ≥0∞ | ∃ pieces : ℕ → Set X,
    s ⊆ ⋃ n, pieces n ∧ ∀ n, upperMinkowskiDim (pieces n) ≤ d}

def IsStickyDatum (lines : Set MarkedLine) : Prop :=
  IsCompact lines ∧
  (∀ line ∈ lines, IsValidLine line) ∧
  FullDirection lines ∧
  packingDim (lineCarrier lines) = 3

def collisionTime (α β : E3) : ℝ :=
  -inner ℝ α β / ‖α‖ ^ 2

def collisionResidual (α β : E3) : E3 :=
  β + collisionTime α β • α

abbrev Mat3 := Matrix (Fin 3) (Fin 3) ℝ

def pencil (A B : Mat3) (s : ℝ) : Mat3 := B + s • A

def graphPlane (A B : Mat3) : Set (E3 × E3) :=
  {(x, y) | ∃ c : E3, x = A.mulVec c ∧ y = B.mulVec c}

def lagrangianPencil (s : ℝ) : Set (E3 × E3) :=
  {(x, y) | y = (-s) • x}

/-!
Finite-scale marked sources.  The tree is part of the data rather than a
cardinality parameter: its cells are nested along parent edges, and the
affine fibre mark is retained separately from the unmarked carrier.
-/

structure NestedCarrierTree (n : ℕ) where
  parent : Fin n → Option (Fin n)
  level : Fin n → ℕ
  parent_level : ∀ {i p}, parent i = some p → level p < level i
  carrierCell : Fin n → Set (E4 × E4)
  nested : ∀ {i p}, parent i = some p → carrierCell i ⊆ carrierCell p

structure FiniteScaleSource (n : ℕ) where
  thickness : ℝ
  line : Fin n → MarkedLine
  shading : Fin n → Set E4
  weight : Fin n → ℝ≥0∞
  fibreMark : Fin n → ℝ
  tree : NestedCarrierTree n
  line_in_carrier : ∀ i, (direction (line i), offset (line i)) ∈ tree.carrierCell i

def sourceFunction {n : ℕ} (D : FiniteScaleSource n) (x : E4) : ℝ≥0∞ := by
  classical
  exact ∑ i, if x ∈ D.shading i then D.weight i else 0

def sourceMass {n : ℕ} (D : FiniteScaleSource n) : ℝ≥0∞ :=
  ∫⁻ x, sourceFunction D x ∂volume

def sourceUnion {n : ℕ} (D : FiniteScaleSource n) : Set E4 :=
  {x | 0 < sourceFunction D x}

def ComesFromSelector {n : ℕ} (D : FiniteScaleSource n)
    (selector : Set MarkedLine) : Prop :=
  ∀ i, D.line i ∈ selector

def IsAdmissibleStickySource {n : ℕ} (D : FiniteScaleSource n)
    (ε : ℝ) (C : ℝ≥0∞) : Prop :=
  0 < D.thickness ∧ D.thickness < 1 ∧
  (∀ i, D.weight i ≤ 1) ∧
  (∀ i, D.fibreMark i = mark (D.line i)) ∧
  (∀ i, IsValidLine (D.line i)) ∧
  (∀ i, MeasurableSet (D.shading i)) ∧
  (∀ i x, x ∈ D.shading i →
    Metric.infDist x (unitFront {D.line i}) ≤ D.thickness) ∧
  (∀ r : ℝ, D.thickness ≤ r → r ≤ 1 →
    coveringNumber (lineCarrier (Set.range D.line)) r ≤
      C * (ENNReal.ofReal r).rpow (-(3 + ε)))

def IsFractionalSourceRestriction {n : ℕ}
    (R D : FiniteScaleSource n) : Prop :=
  R.thickness = D.thickness ∧
  R.line = D.line ∧
  R.fibreMark = D.fibreMark ∧
  R.tree = D.tree ∧
  (∀ i, MeasurableSet (R.shading i)) ∧
  (∀ i, R.shading i ⊆ D.shading i) ∧
  ∀ i, R.weight i ≤ D.weight i

def IsCarrierDescendant {n : ℕ} (T : NestedCarrierTree n)
    (child root : Fin n) : Prop :=
  Relation.ReflTransGen (fun i p => T.parent i = some p) child root

def IsRetainedDescendant {n : ℕ} (R D : FiniteScaleSource n)
    (root : Fin n) : Prop :=
  IsFractionalSourceRestriction R D ∧
  ∀ i, 0 < R.weight i → IsCarrierDescendant D.tree i root

/-!
The coherent form is the Hausdorff-scale interface.  A single probability
measure on the physical front is discretized at every small radius.  For each
ball at that radius there is a measurable shading/weight restriction whose
mass dominates the measure of the ball and whose physical union stays in the
doubled ball.  Thus the source-hereditary union estimate can be applied at the
same radius as the desired Frostman bound.
-/

def HasCoherentFiniteScaleSources (selector : Set MarkedLine) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∃ C : ℝ≥0∞, C ≠ 0 ∧ C ≠ ⊤ ∧
    ∃ μ : Measure E4,
      IsProbabilityMeasure μ ∧
      μ (unitFront selector)ᶜ = 0 ∧
      ∃ δ₀ : ℝ, 0 < δ₀ ∧
      ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
        ∃ n : ℕ, ∃ D : FiniteScaleSource n,
          D.thickness = δ ∧
          ComesFromSelector D selector ∧
          IsAdmissibleStickySource D ε C ∧
          C⁻¹ ≤ sourceMass D ∧ sourceMass D ≤ C ∧
          ∀ x : E4, ∃ R : FiniteScaleSource n,
            IsFractionalSourceRestriction R D ∧
            sourceUnion R ⊆ Metric.closedBall x (2 * δ) ∧
            μ (Metric.ball x δ) ≤ C * sourceMass R

def HasUniformMarkedSourceEstimate (selector : Set MarkedLine) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∀ Cpack : ℝ≥0∞, Cpack ≠ 0 → Cpack ≠ ⊤ →
    ∃ A : ℝ≥0∞, A ≠ 0 ∧ A ≠ ⊤ ∧
    ∃ δ₀ : ℝ, 0 < δ₀ ∧
    ∀ (n : ℕ) (D R : FiniteScaleSource n),
      D.thickness ≤ δ₀ →
      ComesFromSelector D selector →
      IsAdmissibleStickySource D ε Cpack →
      IsFractionalSourceRestriction R D →
      (∫⁻ x, (sourceFunction R x) ^ 2 ∂volume) ≤
          A * (ENNReal.ofReal D.thickness).rpow (-ε) * sourceMass R ∧
      sourceMass R ≤
          A * (ENNReal.ofReal D.thickness).rpow (-ε) * volume (sourceUnion R)

def HasFrontFrostmanMeasures (selector : Set MarkedLine) : Prop :=
  ∀ ε : ℝ, 0 < ε → ε < 4 →
    ∃ μ : Measure E4,
      IsProbabilityMeasure μ ∧
      μ (unitFront selector)ᶜ = 0 ∧
      ∃ C : ℝ≥0∞, C ≠ ⊤ ∧
        ∀ (x : E4) (r : ℝ), 0 < r → r ≤ 1 →
          μ (Metric.ball x r) ≤
            C * (ENNReal.ofReal r).rpow (4 - ε)

end StickyKakeya4

Source

Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, Sections 2--9 and the finite-scale/Frostman interfaces in Section 9 and Appendix B.

Read-back

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

E3. $E3$ abbreviates the real Euclidean space $\mathbb R^{\operatorname{Fin}3}$ . E4. $E4$ abbreviates $\mathbb R^{\operatorname{Fin}4}$ . MarkedLine. A marked line is an unconstrained element $\ell=((\theta,o),m)\in(E4\times E4)\times\mathbb R$ ; direction, offset, and mark return $\theta,o,m$ , respectively. IsValidLine. Such a line is valid iff $\|\theta\|=1$ and $\langle o,\theta\rangle=0$ ; $m$ is unrestricted. lineCarrier. For a set $L$ of marked lines, $\operatorname{lineCarrier}(L)=\{(\theta,o):\exists m,((\theta,o),m)\in L\}$ , so marks are discarded. FullDirection. Every unit $\theta\in E4$ occurs as the direction of at least one member of $L$ , without uniqueness or validity. IsDirectionSelector. Every unit direction occurs in exactly one entire marked line in $L$ , without a validity condition. unitFront. $\operatorname{unitFront}(L)=\{o+(m+t)\theta:((\theta,o),m)\in L,-\tfrac12\le t\le\tfrac12\}$ ; invalid lines are not excluded and the empty front is empty. coversAtRadius. In any pseudometric space, this means containment in a finite union of open radius- $r$ balls; $r$ is any real, and for $r\le0$ only the empty set can be covered. coveringNumber. $N(S,r)$ is the extended-nonnegative-real infimum of cardinalities of finite sets of ambient centers whose open radius- $r$ balls cover $S$ ; it is $\top$ if no finite cover exists and $0$ for the empty set. upperMinkowskiDim. This is the infimum of finite $d\in[0,\infty]$ for which some finite $C\in[0,\infty]$ satisfies $N(S,r)\le C(\operatorname{ofReal}r)^{-d_{\mathbb R}}$ for all sufficiently small positive $r$ ; $C$ may be $0$ , and the value is $\top$ if no such $d$ exists. packingDim. This is the infimum of all $d\in[0,\infty]$ such that $S$ is contained in a countable union of arbitrary sets of upper Minkowski dimension at most $d$ ; pieces need not be measurable, disjoint, or nonempty, and $d=\top$ is allowed. IsStickyDatum. $L$ is compact, all its lines are valid, every unit direction occurs, and the preceding packing dimension of its unmarked carrier is exactly $3$ ; uniqueness and mark restrictions are absent. collisionTime. $\tau(\alpha,\beta)=-\langle\alpha,\beta\rangle/\|\alpha\|^2$ for $\alpha,\beta\in E3$ ; total real division makes $\tau(0,\beta)=0$ . collisionResidual. This is $\beta+\tau(\alpha,\beta)\alpha$ , hence $\beta$ when $\alpha=0$ . Mat3. Real $3\times3$ matrices indexed by $\operatorname{Fin}3$ . pencil. $B+sA$ . graphPlane. $\{(Ac,Bc):c\in E3\}$ , with no rank or symmetry hypotheses. lagrangianPencil. $\{(x,y):y=-sx\}$ . NestedCarrierTree. For any natural $n$ , including $0$ , each $i\in\operatorname{Fin}n$ has an optional parent, natural level, and cell in $E4\times E4$ ; a parent has smaller level and contains its child's cell. No root, covering, nonemptiness, or branching condition is imposed. FiniteScaleSource. For such $n$ , this consists of a real thickness, marked lines $\ell_i$ , arbitrary shadings $S_i\subseteq E4$ , weights $w_i\in[0,\infty]$ , real fibre marks $f_i$ , and a nested carrier tree, requiring only that the direction-offset pair of $\ell_i$ lies in its cell. Positivity, measurability, validity, and equality of fibre and line marks are not structural requirements. sourceFunction. $f_D(x)=\sum_i\mathbf1_{S_i}(x)w_i$ , equal to $0$ everywhere when $n=0$ . sourceMass. $\int^-f_D\,d\mathrm{volume}$ , without a measurability assumption in this definition. sourceUnion. $\{x:0<f_D(x)\}$ , not merely $\bigcup_iS_i$ . ComesFromSelector. Every indexed line lies in the given set, vacuously for $n=0$ . IsAdmissibleStickySource. For real $\varepsilon$ and $C\in[0,\infty]$ , it requires $0<\delta<1$ , weights at most $1$ , fibre marks equal to line marks, valid lines, measurable shadings within distance $\delta$ of their marked unit segments, and $N(\{(\theta_i,o_i)\},r)\le C(\operatorname{ofReal}r)^{-(3+\varepsilon)}$ whenever $\delta\le r\le1$ . It does not itself require $C\ne0,\top$ or positive weights. IsFractionalSourceRestriction. $R$ and $D$ have equal thickness, line function, fibre-mark function, and entire tree; each $R$ -shading is a measurable subset of its $D$ -shading and each $R$ -weight is no larger. Shading and weight reductions need not be proportional. IsCarrierDescendant. Zero or more parent steps lead from the child to the root, so every index is its own descendant. IsRetainedDescendant. $R$ is a fractional restriction and every positive-weight retained index is a descendant of the given root; zero-weight indices are unrestricted. HasCoherentFiniteScaleSources. For every $\varepsilon>0$ there are $0<C<\top$ , a probability measure $\mu$ supported on $\operatorname{unitFront}(L)$ , and $\delta_0>0$ such that each $0<\delta\le\delta_0$ has an admissible source $D$ from $L$ of thickness $\delta$ and mass between $C^{-1}$ and $C$ ; for every $x\in E4$ there is a fractional restriction $R$ with $\{f_R>0\}\subseteq\overline B(x,2\delta)$ and $\mu(B(x,\delta))\le C\int^-f_R$ . The same $C,\mu,\delta_0$ serve all $\delta$ , while $n,D,R$ may vary. HasUniformMarkedSourceEstimate. For every $\varepsilon>0$ and $0<C_{\rm pack}<\top$ , there are $0<A<\top$ and $\delta_0>0$ such that every admissible sufficiently thin source $D$ from $L$ and every fractional restriction $R$ satisfy $\int^-f_R^2\le A(\operatorname{ofReal}\delta_D)^{-\varepsilon}\int^-f_R$ and $\int^-f_R\le A(\operatorname{ofReal}\delta_D)^{-\varepsilon}\operatorname{volume}\{f_R>0\}$ . Admissibility supplies positive thickness; positive mass and weights are not assumed. HasFrontFrostmanMeasures. For every $0<\varepsilon<4$ , there are a probability measure $\mu$ supported on $\operatorname{unitFront}(L)$ and $C<\top$ such that $\mu(B(x,r))\le C(\operatorname{ofReal}r)^{4-\varepsilon}$ for all $x\in E4$ and $0<r\le1$ ; balls are open and $C$ is not explicitly required nonzero.

View graph