Lemma A.1 — from an enlarged ball down to the same ball

Proved

QFS.formHs_le_form_of_ballComparability

by dbenbenn · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismeasure-theoryquadratic-forms-sobolev

Superseded (2026-09-27). This takes Whitney data as a hypothesis. The QFS mission uses QFS.lemmaAOne_ball, the ball case of Lemma A.1 with no such hypothesis and with the $\alpha_0$ clause.

Assume a Whitney ball family $W$ for the parameters $(d,\alpha,\kappa)$ : a countable index set, an overlap bound $N \ge 1$ , a constant $\gamma > 0$ , centres $c_i$ and radii $r_i$ such that each $\kappa$ -enlarged ball lies inside $B(x_0,R)$ , no point lies in more than $N$ of them, and

\gamma\,|g|^2_{H^{\alpha/2}(B(x_0,R))} \;\le\; \sum_i |g|^2_{H^{\alpha/2}(B(c_i,r_i))} \qquad\text{for \emph{every} } g.

Assume also, for the one fixed $f$ and with one constant $c_0 \ge 1$ , the comparability on every enlarged ball: for all $y_0$ and all $S > 0$ , if $f \in L^2(B(y_0,\kappa S))$ then $|f|^2_{H^{\alpha/2}(B(y_0,S))} \le c_0\,\mathcal{E}_{B(y_0,\kappa S)}[k,f]$ .

Then, for $f \in L^2(B(x_0,R))$ with measurable energy integrand,

\frac{\gamma}{c_0 N}\;|f|^2_{H^{\alpha/2}(B(x_0,R))} \;\le\; \mathcal{E}_{B(x_0,R)}[k,f].

The enlargement is gone. The hypothesis compares a ball against its $\kappa$ -dilate; the conclusion compares a ball against itself. Removing that dilation is the entire content, and the price is the explicit factor $\gamma/(c_0N)$ .

This is the step the paper takes by quoting a Whitney decomposition and Dyda's inequality; both are carried here as the explicit hypothesis $W$ rather than proved.

Two things worth knowing. The kernel $k$ is arbitrary — not assumed symmetric, not assumed to satisfy the bounds (2), not attached to any configuration; no cone hypothesis appears anywhere, and $\alpha$ is an arbitrary real with no restriction to $(0,2)$ . And $\kappa$ is not assumed positive: if $\kappa \le 0$ the enlarged balls are empty and the comparability hypothesis forces $|f|^2_{H^{\alpha/2}}$ to vanish on every ball, so that branch is degenerate rather than vacuous. Likewise an empty index set would force the same through the Dyda field.

Preamble

-- Generated by skeleton subtraction from QuadraticFormsSobolev/AppendixA.lean
-- source: quadratic-forms-sobolev@7a1a680db212
import Definitions.Def_QFS_Translate
import Definitions.Def_QFS_Defs
import Definitions.Def_QFS_ConeGap
import Definitions.Def_QFS_RefCones
import Definitions.Def_QFS_Section4
import Definitions.Def_QFS_Cubes
import Definitions.Def_QFS_Section3
import Definitions.Def_QFS_Section5
import Definitions.Def_QFS_Section1
import Definitions.Def_QFS_ThinCones
import Definitions.Def_QFS_Section3Kernel
import Definitions.Def_QFS_LebesgueDiff
import Definitions.Def_QFS_LebesgueDiff2
import Definitions.Def_QFS_Renormalization
import Definitions.Def_QFS_FirstJump
import Definitions.Def_QFS_Assembly
import Definitions.Def_QFS_PathAssembly
import Definitions.Def_QFS_BlockPaths
import Definitions.Def_QFS_Section6
import Definitions.Def_QFS_Rescaling
import Definitions.Def_QFS_Section32
import Definitions.Def_QFS_AppendixA
import Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

/-!
# Appendix A: the auxiliary lemmas

The paper's `\appendix` prints as Appendix A, with Lemmas A.1 and A.2.

**The chain (18) inside Lemma A.1.** Lemma A.1 passes from balls to a bounded
Lipschitz domain using a Whitney family and Dyda's inequality (13), both quoted
rather than proved. The one step the paper carries out itself is the
finite-overlap estimate, and it is proved here
(`tsum_setLIntegral_le_of_overlap`); `lemma_ball_to_domain` then assembles the
whole chain with the two quoted inputs as explicit hypotheses.
-/

open MeasureTheory Filter Set Metric
open scoped ENNReal NNReal Topology

open QFS

variable {d : ℕ}

/-! ## The finite-overlap step of Lemma A.1

Lemma A.1's proof runs the chain (18). Its first inequality is the only step
carried out in the paper rather than quoted: if the enlarged Whitney balls `B*`
lie in `Ω` and no point lies in more than `M` of them, the sum of the forms over
the `B*` is controlled by the form over `Ω`. -/

/-! ## The last link: from the enlarged ball to Theorem 1.1

Section 3.2 ends by applying Lemma A.1 with `Ω = B` a ball, turning the
enlarged-ball comparability `|f|_{H^{α/2}(B)} ≲ |f|_{H_k(B*)}` into the
same-ball one. That step is proved here, so the only unproved links in the
chain from the discrete theory to Theorem 1.1 are the ones the paper does not
prove either — plus §3.2's remaining inclusion. -/

Formal statement

theorem QFS.formHs_le_form_of_ballComparability {α κ c₀ : ℝ} (hc₀ : 1 ≤ c₀)
    (W : WhitneyBallData d α κ)
    {k : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ≥0∞}
    {f : EuclideanSpace ℝ (Fin d) → ℝ}
    (H : ∀ (y₀ : EuclideanSpace ℝ (Fin d)) (S : ℝ), 0 < S →
      MemLp f 2 (volume.restrict (ball y₀ (κ * S))) →
      formHs (ball y₀ S) α f ≤ ENNReal.ofReal c₀ * form (ball y₀ (κ * S)) k f)
    (x₀ : EuclideanSpace ℝ (Fin d)) (R : ℝ) (hR : 0 < R)
    (hf : MemLp f 2 (volume.restrict (ball x₀ R)))
    (hFmeas : Measurable fun p : EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) =>
      ENNReal.ofReal ((f p.2 - f p.1) ^ 2) * k p.1 p.2) :
    ENNReal.ofReal (c₀⁻¹ * W.dydaConst / (W.overlapBound : ℝ)) * formHs (ball x₀ R) α f
      ≤ form (ball x₀ R) k f := by sorry

Source

https://github.com/dbenbenn/quadratic-forms-sobolev/blob/7a1a680db2124d46ce370c91fd450aa454edf491/QuadraticFormsSobolev/AppendixA.lean#L161-L222

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by dbenbenn · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph