Theorem 1.4 on $\mathbb{R}^d$ , granted Theorem 1.1

Proved

QFS.theoremOneFourUniv_of_theoremOneOne

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

analysismeasure-theoryquadratic-forms-sobolev

Superseded (2026-09-27). This is only the reduction from Theorem 1.1. The QFS mission uses QFS.theoremOneFour_univ, which states the $\mathbb{R}^d$ half of Theorem 1.4 outright.

A bare implication: if TheoremOneOne d holds, then the same comparability holds with the ball replaced by all of $\mathbb{R}^d$ —

|f|^2_{H^{\alpha/2}(\mathbb{R}^d)} \;\le\; c\,\mathcal{E}_{\mathbb{R}^d}[k,f],

for every $\vartheta$ -admissible $\Gamma$ , every $k$ with the bounds (2), and every $f$ that lies in $L^2$ of every ball of every positive radius, with $c \ge 1$ depending only on $d$ , $\vartheta$ , $\Lambda$ , $\alpha$ .

The trade is exact and is the whole content: the hypothesis quantifies over balls and asks $f \in L^2$ of that ball; the conclusion drops the ball quantifiers, integrates over all of space, and correspondingly strengthens the requirement on $f$ to $L^2$ of every ball. Nothing else changes — in particular the right-hand domain is not enlarged, so this is not the …Ball… form.

Both statements use IsAdmissible, i.e. boundedness together with the paper's condition (M) — not the stronger CondMeas of milestones 9, 12–15.

Note $f$ is not required to lie in $L^2(\mathbb{R}^d)$ — only in $L^2$ of each ball, which is precisely what is needed to apply the hypothesis on every ball.

Preamble

-- Generated by skeleton subtraction from QuadraticFormsSobolev/Section1.lean
-- source: quadratic-forms-sobolev@7a1a680db212
/-
Section 1 of Bux–Kassmann–Schulze: the quadratic forms, the function spaces
`H_k(Ω)` and `H^{α/2}(Ω)`, assumption (2) on the kernel, the reverse
inequality of Theorem 1.1 (which "trivially holds"), and the inclusion (5).

The two main theorems are also *stated* here, as `Prop`s, so that the targets
are precise and type-checked. `QFS.TheoremOneThree` is proved in `Section6`;
`QFS.TheoremOneOne` is not, and the README records what it still needs.

Theorem 1.4 on `ℝ^d` closes the file. The paper obtains it from Lemma 3.7 "in
the limit `R → ∞` using monotone convergence", the point being that the
comparability constant does not depend on the ball. That deduction needs nothing
from Section 3.2 beyond Theorem 1.1 itself, so it is proved here, conditionally
(`QFS.theoremOneFourUniv_of_theoremOneOne`).
-/
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 Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

open Real Set Metric MeasureTheory ENNReal

open QFS

variable {d : ℕ}

/-! ## The kernels and the quadratic forms -/

/-! ## Assumption (2) -/

/-! ## The reverse inequality, and the inclusion (5) -/

/-! ## The statements of Theorems 1.1 and 1.3

These are recorded as `Prop`s so that the targets are precise and type-checked.
`QFS.TheoremOneThree` is proved as `QFS.theoremOneThree` in `Section6`, on top
of Theorem 5.15. `QFS.TheoremOneOne` is not proved: it needs Section 3's
discrete kernel and limiting argument, and a final step the paper quotes from a
Whitney decomposition. See the README. -/

/-! ## Theorem 1.4 on `ℝ^d` -/

Formal statement

theorem QFS.theoremOneFourUniv_of_theoremOneOne (h : TheoremOneOne d) : TheoremOneFourUniv d := by sorry

Source

https://github.com/dbenbenn/quadratic-forms-sobolev/blob/7a1a680db2124d46ce370c91fd450aa454edf491/QuadraticFormsSobolev/Section1.lean#L265-L275

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

Theorem 1.4 on Rd\mathbb{R}^dRd, granted Theorem 1.1

Theorem 1.4 on $\mathbb{R}^d$ , granted Theorem 1.1