Subpower bound $\lesssim_\delta$

Definition

SubpowerLE

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

asymptoticsharmonic-analysiskakeya

A scale-dependent quantity $x(\delta)$ is subpower-bounded by $y(\delta)$ , written $x \lesssim y$ , if for every $\varepsilon > 0$ there exists $C \geq 0$ (independent of $\delta$ ) with $x(\delta) \leq C\, \delta^{-\varepsilon}\, y(\delta)$ for all $\delta \in (0,1)$ . Includes the reflexivity and right-transitivity lemmas.

Definition code

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Real.Basic

namespace FilteredDescent

/-- Subpower-loss domination `x ≲ y` uniformly for `δ ∈ (0,1)` (paper's `≲ δ^{-o(1)}`).

  For every `ε > 0` there is a constant `C ≥ 0` — allowed to depend on `ε`
  and on the dimension, but *not* on `δ` — such that
  `x δ ≤ C * δ ^ (-ε) * y δ` for *all* `δ ∈ (0,1)`.
  The paper uses this pervasively to bookkeep subpower losses as `δ → 0`.
  Quantities compared here are functions of the scale `δ`; constant
  quantities are embedded via `fun _ => c`. -/
def SubpowerLE (x y : ℝ → ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 ≤ C ∧ ∀ δ : ℝ, 0 < δ → δ < 1 → x δ ≤ C * δ ^ (-ε) * y δ

/-- Subpower domination is reflexive on quantities nonnegative on `(0,1)`. -/
theorem SubpowerLE.refl {x : ℝ → ℝ} (hx : ∀ δ : ℝ, 0 < δ → δ < 1 → 0 ≤ x δ) :
    SubpowerLE x x := by
  unfold SubpowerLE
  intro ε hε
  refine ⟨1, zero_le_one, fun δ hδ0 hδ1 => ?_⟩
  have h : (1 : ℝ) ≤ δ ^ (-ε) := by
    rw [Real.rpow_neg (le_of_lt hδ0)]
    exact (one_le_inv_iff₀).mpr ⟨Real.rpow_pos_of_pos hδ0 ε,
      le_of_lt (Real.rpow_lt_one (le_of_lt hδ0) hδ1 hε)⟩
  calc x δ = 1 * x δ := by ring
    _ ≤ δ ^ (-ε) * x δ := mul_le_mul_of_nonneg_right h (hx δ hδ0 hδ1)
    _ = 1 * δ ^ (-ε) * x δ := by ring

/-- Chaining a subpower bound through a middle factor. -/
theorem SubpowerLE.trans_right {x y z : ℝ → ℝ}
    (hxy : SubpowerLE x y) (hyz : SubpowerLE y z) :
    SubpowerLE x z := by
  unfold SubpowerLE at *
  intro ε hε
  obtain ⟨C₁, hC₁, h₁⟩ := hxy (ε / 2) (by linarith)
  obtain ⟨C₂, hC₂, h₂⟩ := hyz (ε / 2) (by linarith)
  refine ⟨C₁ * C₂, mul_nonneg hC₁ hC₂, fun δ hδ0 hδ1 => ?_⟩
  have hpow : δ ^ (-ε) = δ ^ (-(ε / 2)) * δ ^ (-(ε / 2)) := by
    rw [← Real.rpow_add hδ0]
    ring_nf
  have hnn : 0 ≤ δ ^ (-(ε / 2)) := Real.rpow_nonneg (le_of_lt hδ0) _
  calc x δ ≤ C₁ * δ ^ (-(ε / 2)) * y δ := h₁ δ hδ0 hδ1
    _ ≤ C₁ * δ ^ (-(ε / 2)) * (C₂ * δ ^ (-(ε / 2)) * z δ) :=
        mul_le_mul_of_nonneg_left (h₂ δ hδ0 hδ1) (mul_nonneg hC₁ hnn)
    _ = (C₁ * C₂) * δ ^ (-ε) * z δ := by rw [hpow]; ring

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, §1 (the

\delta^{-o(1)}

convention)

Read-back

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

Blind read-back: `FilteredDescent_SubpowerLE`

File: Definitions/Def_FilteredDescent_Subpower.lean Namespace: FilteredDescent. Imports: Mathlib.Analysis.SpecialFunctions.Pow.Real, Mathlib.Data.Real.Basic. No sorry / axiom in the file; both theorems carry complete tactic proofs.

Definitions

def SubpowerLE (x y : ℝ → ℝ) : Prop

Compares functions of a scale parameter δ, not scalar reals at a fixed δ:

SubpowerLE x y := ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 ≤ C ∧
  ∀ δ : ℝ, 0 < δ → δ < 1 → x δ ≤ C * δ ^ (-ε) * y δ

Quantifier order is ∀ ε, ∃ C, ∀ δ ∈ (0,1): the constant C is chosen before δ is quantified, so as written C may depend on ε (and on x, y) but cannot depend on δ. This is a uniform-in-δ family-level bound, matching the doc comment's claim ("allowed to depend on ε … but not on δ").

No nonnegativity of x or y is built into the definition. Since δ ^ (-ε) > 0 for δ > 0, if y δ < 0 somewhere then C * δ ^ (-ε) * y δ ≤ 0, forcing x δ ≤ 0 there. The zero function is subpower-bounded by everything (take C = 0).

Theorems (both fully proved)

theorem SubpowerLE.refl {x : ℝ → ℝ} (hx : ∀ δ : ℝ, 0 < δ → δ < 1 → 0 ≤ x δ) : SubpowerLE x x

Reflexivity, but only under the explicit hypothesis that x is nonnegative on (0,1). Proof uses C = 1 and δ ^ (-ε) ≥ 1 for δ ∈ (0,1), ε > 0.

theorem SubpowerLE.trans_right {x y z : ℝ → ℝ} (hxy : SubpowerLE x y) (hyz : SubpowerLE y z) : SubpowerLE x z

Right-transitivity. Proof splits ε as ε/2 + ε/2, multiplies the constants (C₁ * C₂, nonnegative), and uses δ ^ (-ε) = δ ^ (-ε/2) * δ ^ (-ε/2) via Real.rpow_add. No sign hypotheses needed because the multiplier C₁ * δ ^ (-ε/2) is shown nonnegative before chaining.

Notes

The definition is genuinely uniform in δ by quantifier order; it is not the weaker per-δ formulation ∀ δ, ∀ ε, ∃ C, ....
refl is not unconditional: it needs 0 ≤ x on (0,1). This is a real hypothesis, not a formality.
trans_right is right-composition only (x ≲ y ≲ z ⇒ x ≲ z); there is no left-transitivity or monotonicity lemma in this file.

View graph

Subpower bound ≲δ\lesssim_\delta≲δ​

Blind read-back: FilteredDescent_SubpowerLE

Definitions

Theorems (both fully proved)

Notes

Subpower bound $\lesssim_\delta$

Blind read-back: `FilteredDescent_SubpowerLE`