Ordered packet law (packetLaw, slotMarginal, retainedMass)

Definition

packetLaw

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

harmonic-analysiskakeyaprobability

An ordered $r$ -packet $U$ over $n$ tubes with weights $w$ has law $\prod_j w(U_j)/W^r$ where $W = \sum_i w_i$ . The slot- $s$ marginal $\mu_s(x)$ and the retained mass $\alpha = \sum_{U \in A} \prod_j w(U_j)/W^r$ of a packet event $A$ are defined from it.

Definition code

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Pi
import Mathlib.Data.Real.Basic

/-!
# Filtered descent — finite packet model (paper (9), (17)–(18), (25))

Finite model of the descent's "packet" picture.  The paper works with
ordered packets of tubes `U = (U_1, …, U_r)` weighted by the product of the
tube weights; R5 ((9)/(25)) says that after retaining an event of mass `α`,
each slot's marginal is dominated by `α⁻¹` times the base law.
-/

namespace FilteredDescent

/-- Finite symmetric packet law (paper (17)): on ordered `r`-tuples of tubes,
the product weight normalized by the total mass `W^r`. -/
noncomputable def packetLaw {n r : ℕ} (w : Fin n → ℝ) : (Fin r → Fin n) → ℝ :=
  fun U => (∏ j, w (U j)) / (∑ i, w i) ^ r

/-- One-slot marginal mass: total packet mass of tuples with `U j = t`.
Paper (18): before conditioning this equals the coarse shaded-incidence
marginal `w t / W`. -/
noncomputable def slotMarginal {n r : ℕ} (w : Fin n → ℝ) (j : Fin r)
    (t : Fin n) : ℝ :=
  ∑ U : Fin r → Fin n, if U j = t then packetLaw w U else 0

/-- Retained packet mass of an event `A` under the packet law.  This is the
finite form of the retained mass `α` in R5 (paper (9)/(25)). -/
noncomputable def retainedMass {n r : ℕ} (w : Fin n → ℝ)
    (A : Finset (Fin r → Fin n)) : ℝ :=
  ∑ U ∈ A, packetLaw w U

end FilteredDescent

Source

Cai, Filtered Descent for the Physical Kakeya Incidence, 2026, https://cchx0000.github.io/papers/filtered-descent-physical-kakeya/filtered-descent-physical-kakeya.pdf, §2 (R5 setup, (9), (25))

Read-back

What the Lean code literally says, in plain math · muse-spark

I have read the auditor instructions and the Lean code. I am writing blind read-backs based solely on what the code literally says, without importing any outside context. Here are my read-backs:

FilteredDescent.packetLaw

For any two implicit natural numbers $n$ and $r$ (each of which may be $0$ ) and any explicit function $w$ from the $n$ -element index set $\mathrm{Fin}\,n$ to the real numbers, $\mathrm{packetLaw}$ is defined to be the function from the set of all $r$ -tuples of $n$ -indices (i.e., all functions $U : \mathrm{Fin}\,r \to \mathrm{Fin}\,n$ ) to $\mathbb{R}$ given by

\mathrm{packetLaw}(w)(U) \;=\; \frac{\displaystyle\prod_{j \in \mathrm{Fin}\,r} w(U_j)}{\left(\displaystyle\sum_{i \in \mathrm{Fin}\,n} w_i\right)^r}.

In words, the numerator multiplies the values of $w$ at each coordinate of the tuple $U$ , and the denominator raises the total $W = \sum_i w_i$ to the $r$ -th power. The declaration is marked noncomputable. The code imposes no hypotheses on $w$ : weights may be negative, zero, or arbitrary. Degenerate cases: if the total weight $W$ equals $0$ and $r > 0$ , the denominator is $0$ and real division by zero returns $0$ , so $\mathrm{packetLaw}(w)(U) = 0$ for every tuple $U$ . If $r = 0$ , the numerator is the empty product (equal to $1$ ) and the denominator is $W^0 = 1$ (with $0^0 = 1$ ), so the value is $1$ on the unique empty tuple — even when $W = 0$ . If $n = 0$ , then $w$ is the empty function and $W = 0$ .

FilteredDescent.slotMarginal

For implicit natural numbers $n$ and $r$ , and explicit arguments $w : \mathrm{Fin}\,n \to \mathbb{R}$ , a slot index $j \in \mathrm{Fin}\,r$ , and a tube index $t \in \mathrm{Fin}\,n$ , $\mathrm{slotMarginal}$ is defined to be the real number

\mathrm{slotMarginal}(w, j, t) \;=\; \sum_{U : \mathrm{Fin}\,r \to \mathrm{Fin}\,n} \begin{cases} \mathrm{packetLaw}(w)(U) & \text{if } U_j = t, \\ 0 & \text{otherwise}, \end{cases}

i.e., the sum of $\mathrm{packetLaw}(w)(U)$ over all $r$ -tuples $U$ whose $j$ -th coordinate equals $t$ (expanding the definition, each contributing summand is $\left(\prod_k w(U_k)\right)/W^r$ ). The sum ranges over the entire finite type of functions $\mathrm{Fin}\,r \to \mathrm{Fin}\,n$ , and the test $U_j = t$ uses decidable equality on $\mathrm{Fin}\,n$ . The declaration is marked noncomputable. Degenerate cases: if $r = 0$ there exists no slot index $j$ that can be supplied, and if $n = 0$ there exists no tube index $t$ ; the definition remains well-formed but cannot be applied in those cases. If $W = 0$ and $r > 0$ , every summand is $0$ (by the division-by-zero behavior described above), so the result is $0$ .

FilteredDescent.retainedMass

For implicit natural numbers $n$ and $r$ , an explicit weight function $w : \mathrm{Fin}\,n \to \mathbb{R}$ , and an explicit finite set $A$ of $r$ -tuples (a $\mathrm{Finset}$ over $\mathrm{Fin}\,r \to \mathrm{Fin}\,n$ ), $\mathrm{retainedMass}$ is defined to be the real number

\mathrm{retainedMass}(w, A) \;=\; \sum_{U \in A} \mathrm{packetLaw}(w)(U),

i.e., the sum of $\left(\prod_j w(U_j)\right)/W^r$ over exactly those tuples $U$ that belong to $A$ . Unlike $\mathrm{slotMarginal}$ , the sum is restricted to the members of the given finite set $A$ directly, with no indicator function involved. The declaration is marked noncomputable. Degenerate cases: no hypotheses are placed on $A$ or on $w$ ; in particular, if $A$ is the empty finite set, the sum is $0$ .

These read-backs report only what the Lean code literally defines: the binders (implicit $n, r$ ; explicit $w, j, t, A$ ), the exact formulas including the placement of division and powers, the noncomputable marking, and the behavior at degenerate inputs ( $n = 0$ , $r = 0$ , zero total weight, empty $A$ ).

View graph