Null sets

TheoremSets with locally null image have null image#✓fully proved

Let \(X\) be a second-countable topological space, \(Y\) a measurable space with a measure \(\mu\), \(f : X \to Y\) a function and \(s \subseteq X\). If every point \(x \in s\) has a neighbourhood \(V\) with \(\mu(f(V \cap s)) = 0\), then \(\mu(f(s)) = 0\).

Here \(\mu\) is evaluated as an outer measure, so the images need not be measurable.

theorem measure_image_null_of_locally_null
    (h : ∀ x ∈ s, ∃ V ∈ nhds x, μ (f '' (V ∩ s)) = 0) :
    μ (f '' s) = 0

Used by 3

Used byParametric Sard theorem for real analytic families · Sard's theorem on open subsets of finite-dimensional spaces · Sard's theorem for maps into Euclidean space

TheoremNonzero polynomials over nondiscrete fields have Haar-null zero sets#✓fully proved

A nonzero multivariate polynomial over a nondiscrete locally compact second-countable Hausdorff topological field has an additive Haar-null zero set. This includes the empty variable type.

public theorem measure_setOf_eval_eq_zero_of_ne_zero
    (F : Type*) [Field F] [TopologicalSpace F] [IsTopologicalRing F]
    [LocallyCompactSpace F] [T2Space F] [SecondCountableTopology F]
    [MeasurableSpace F] [BorelSpace F] (hF : ¬ DiscreteTopology F)
    (ι : Type*) [Fintype ι] (p : MvPolynomial ι F) (hp : p ≠ 0)
    (μ : Measure (ι → F)) [μ.IsAddHaarMeasure] :
    μ {x : ι → F | eval x p = 0} = 0

TheoremThe graph of a measurable function is a null set#●ready to prove

Let \(d \ge 0\) be an integer and let \(f : \mathbb{R}^d \to \mathbb{R}\) be Borel measurable. Identify \(\mathbb{R}^d \times \mathbb{R}\) with \(\mathbb{R}^{d+1}\) by taking the last coordinate as \(y\). Then the graph \(\Gamma = \{(x, y) \in \mathbb{R}^d \times \mathbb{R} : y = f(x)\}\) is a Borel measurable subset of \(\mathbb{R}^{d+1}\) and has Lebesgue measure \(0\).

public theorem_wanted measurableSet_and_volume_eq_zero_graph
    {d : ℕ} (f : (Fin d → ℝ) → ℝ) (Γ : Set (Fin (d + 1) → ℝ))
    (hΓ : Γ = {z : Fin (d + 1) → ℝ | z (Fin.last d) = f (fun i : Fin d => z (Fin.castSucc i))})
    (hf : Measurable f) : MeasurableSet Γ ∧ volume Γ = 0

Sources

MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Measure and integration; Classical measure theory), problem ma_proofbench_l1_38.

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.