The boundary of a closed cube in $\mathbb R^d$ is Lebesgue-null

Proved

DbarRegularity.volume_closedCube_diff_interior

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexitylebesgue-measuremeasure-theory

Let $d\ge0$ , $a\in\mathbb R^d$ and $s\in\mathbb R$ , and let $Q=\prod_{i}[a_i,a_i+s]$ be the closed cube with corner $a$ and side $s$ . Then the set $Q\setminus\operatorname{int}Q$ has Lebesgue measure zero.

So a closed cube and its interior agree up to a null set. Integrals and measures over closed cubes, for example those from a Calderón–Zygmund decomposition, can therefore be computed on the open cubes, which are pairwise disjoint whenever the closed cubes have disjoint interiors.

Formalization Note. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. The cube is closedCube a s = {x | ∀ i, a i ≤ x i ∧ x i ≤ a i + s} from the mission's Setting definitions, and its interior is the topological interior.

Preamble

import Definitions.Def_DbarRegularity_Setting
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Formal statement

namespace DbarRegularity

open MeasureTheory Set

/-- The boundary `Q \ interior Q` of a closed cube `Q = ∏ᵢ [aᵢ, aᵢ + s]` in `ℝ^d` is a Lebesgue
null set. -/
theorem volume_closedCube_diff_interior {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (s : ℝ) :
    volume (closedCube a s \ interior (closedCube a s)) = 0 := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton University Press (1970), Chapter I, § 3.1

View graph

The boundary of a closed cube in Rd\mathbb R^dRd is Lebesgue-null

The boundary of a closed cube in $\mathbb R^d$ is Lebesgue-null