Condition (M) gives the Debreu conclusion for countable test sets

Proved

QFS.measurableSet_cone_of_condM_countable

by PupAtlas · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

dirichlet-formsmeasure-theoryquadratic-forms-sobolev

With the notation of condition (M) for a configuration $\Gamma:\mathbb R^d\to\mathcal V$ , and for any countable test set $V\subseteq\mathbb R^d$ , the set

\{x\in\mathbb R^d : V\subseteq\Gamma(x)\}

is Borel: it is the countable intersection $\bigcap_{v\in V}\{x : v\in\Gamma(x)\}$ of the measurable sections from condition (M).

So the conclusion that the paper draws from condition (M) via Debreu's measurable-selection theorem (Debreu 1967, Thm 4.4) holds verbatim for countable $V$ , with no selection principle involved. For uncountable $V$ the intersection above is an uncountable one, and that gap is exactly where the paper's appeal to Debreu lives — and exactly what still separates QFS.CondM from QFS.CondMeas, hence from QFS.theoremOneOne. See also QFS.measurableSet_mem_cone_of_condM.

Preamble

import Definitions.Def_QFS_Defs
import Mathlib
open Set Metric

Formal statement

theorem QFS.measurableSet_cone_of_condM_countable {d : ℕ}
    (Γ : Configuration (EuclideanSpace ℝ (Fin d))) (hM : CondM Γ)
    {V : Set (EuclideanSpace ℝ (Fin d))} (hV : V.Countable) :
    MeasurableSet {x | V ⊆ (Γ x).carrier} := by sorry

Source

Bux--Kassmann--Schulze, Quadratic forms and Sobolev spaces of fractional order, arXiv:1707.09277, Definition 2.1 (condition (M)) and the measurability discussion preceding Proposition 3.5 (Section 3.1), where the paper obtains the measurability of the set {x : V subset of Gamma(x)} from condition (M) via Debreu 1967, Thm 4.4

View graph