Proposition 3.5 — the discretised kernel dominates a cone kernel

Proved

QFS.prop_test_fct

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

analysismeasure-theoryquadratic-forms-sobolev

For $d \ge 2$ , $0 < \vartheta \le \pi/2$ and $0 < \alpha \le 2$ there are a constant $C > 0$ and an angle $\theta' \in (0,\pi/2]$ — uniform in everything that follows — such that for every $\vartheta$ -bounded configuration $\Gamma$ satisfying CondMeas, and every $\Lambda$ and kernel $k$ with the bounds (2), there is a new configuration $\Gamma'$ , bounded by $\theta'$ , with: for all lattice points $x,y$ separated by more than $\sqrt d$ ,

\frac{C}{\Lambda}\Bigl(\mathbf 1[y \in V^{\Gamma'}\![x]] + \mathbf 1[x \in V^{\Gamma'}\![y]]\Bigr)\, \|x-y\|^{-d-\alpha} \;\le\; \int_{Q(x)\times Q(y)} k ,

the right side being the mass of $k$ over the open unit cubes at $x$ and $y$ .

$C$ and $\theta'$ depend only on $d$ , $\vartheta$ , $\alpha$ ; $\Gamma'$ is chosen after $\Gamma$ , $\Lambda$ and $k$ but before $x$ and $y$ , so one $\Gamma'$ serves all admissible lattice pairs.

Note $\alpha \le 2$ is non-strict here — $\alpha = 2$ is permitted, unlike in Theorem 1.1. Nothing is asserted for pairs at distance $\le \sqrt d$ , or for non-lattice points, and the bound is one-sided: no upper bound on the discretised kernel is claimed.

What is not said about $\Gamma'$ : it is related to $\Gamma$ only through the displayed inequality. It is not required to be measurable, nor to have cones contained in or containing those of $\Gamma$ ; and $\theta'$ is not required to be below or above $\vartheta$ — only to lie in $(0,\pi/2]$ .

Preamble

-- Generated by skeleton subtraction from QuadraticFormsSobolev/Section3Kernel.lean
-- source: quadratic-forms-sobolev@7a1a680db212
/-
Section 3.1 of Bux–Kassmann–Schulze: the discrete version of the kernel.

For a kernel `k` on `ℝ^d × ℝ^d` and `h > 0` the paper sets

  `ω^k_h(x, y) = h^{-2d} ∫∫_{A_h(x) × A_h(y)} k(s, t) d(s,t)`,

a kernel on `hℤ^d`, and Proposition 3.5 checks that it satisfies assumption
(4). The upper bound is "just a consequence of Lemma 3.4": on the product of
the two cubes `|s − t|` is bounded below by `|x − y|/(2√d)`, so the kernel is
bounded above by `(2√d)^{d+α}` times its value at `(x, y)`.
-/
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 Mathlib

set_option autoImplicit true
set_option relaxedAutoImplicit false
set_option maxSynthPendingDepth 3

open Real Set Metric MeasureTheory ENNReal

open QFS

variable {d : ℕ}

/-! ## Towards the lower bound of Proposition 3.5 -/

/-! ## Integrating the estimate

The integration needs the sets `A_h^m(u)` to be measurable, i.e. the sets
`{x | V ⊆ Γ(x)}` to be measurable. The paper obtains this from condition (M) by
quoting Debreu's measurable-selection theorem; that implication is not
formalised here, so it is carried as an explicit hypothesis. -/

/-! ## Proposition 3.5 -/

Formal statement

theorem QFS.prop_test_fct {ϑ : ℝ} (hϑ : 0 < ϑ) (hϑ' : ϑ ≤ π / 2) (hd : 2 ≤ d) {α : ℝ}
    (hα : 0 < α) (hα2 : α ≤ 2) :
    ∃ C θ' : ℝ, 0 < C ∧ 0 < θ' ∧ θ' ≤ π / 2 ∧
      ∀ Γ : Configuration (EuclideanSpace ℝ (Fin d)), IsBounded Γ ϑ → CondMeas Γ →
      ∀ (Λ : ℝ) (k : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ≥0∞),
        KernelBounds Γ α Λ k →
      ∃ Γ' : Configuration (EuclideanSpace ℝ (Fin d)), IsBounded Γ' θ' ∧
        ∀ x ∈ lattice d, ∀ y ∈ lattice d, Real.sqrt d < ‖x - y‖ →
          ENNReal.ofReal (C * Λ⁻¹) *
              ((indE (coneAt Γ' x) y + indE (coneAt Γ' y) x) * jumpKernel d α x y)
            ≤ discreteKernel d k 1 x y := by sorry

Source

https://github.com/dbenbenn/quadratic-forms-sobolev/blob/7a1a680db2124d46ce370c91fd450aa454edf491/QuadraticFormsSobolev/Section3Kernel.lean#L320-L437

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