Condition (M) gives measurable cone sections

Proved

QFS.measurableSet_mem_cone_of_condM

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

dirichlet-formsmeasure-theoryquadratic-forms-sobolev

Let $d\in\mathbb N$ , let $E=\mathbb R^d$ and let $\Gamma:E\to\mathcal V$ be a configuration in the sense of Definition 2.1: $\Gamma(x)$ is a double cone $V(a_x,\vartheta_x)$ with unit axis $a_x$ and apex angle $\vartheta_x\in(0,\pi/2]$ . Recall condition (M): the set

\{(x,y)\in E\times E : y-x\in\Gamma(x)\}

is a Borel subset of $E\times E$ .

Then for every fixed direction $v\in E$ the section

\{x\in E : v\in\Gamma(x)\}

is again Borel. No measurable-selection theorem is needed for this one-directional consequence: the section is the preimage of the set in (M) under the measurable map $x\mapsto(x,x+v)$ , since $(x+v)-x=v$ .

This isolates exactly what condition (M) yields on its own. The paper's full statement — measurability of $\{x : V\subseteq\Gamma(x)\}$ for every set $V$ — is obtained there by quoting Debreu's measurable-selection theorem, and it is that step which is not formalised here: QFS.CondMeas carries it as a hypothesis, and QFS.theoremOneOneCondMeas_two (Theorem 1.1 with CondMeas made explicit) is proved from it.

Preamble

import Definitions.Def_QFS_Defs
import Mathlib
open Set Metric

Formal statement

theorem QFS.measurableSet_mem_cone_of_condM {d : ℕ}
    (Γ : Configuration (EuclideanSpace ℝ (Fin d))) (hM : CondM Γ)
    (v : EuclideanSpace ℝ (Fin d)) :
    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