Volume of a closed cube in ℝ^d

Proved

DbarRegularity.volume_closedCube

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

harmonic-analysislebesgue-measuremeasure-theory

For $a\in\mathbb{R}^d$ and $s\in\mathbb{R}$ let $Q(a,s)=\{x\in\mathbb{R}^d:\ a_i\le x_i\le a_i+s\ \text{for all } i\}$ be the closed cube with corner $a$ and side length $s$ . Then its Lebesgue measure is

|Q(a,s)| = (s^+)^d,

where $s^+=\max(s,0)$ . In particular $|Q(a,s)|=s^d$ for $s\ge 0$ .

This is the basic volume formula for coordinate cubes in $\mathbb{R}^d$ .

Formalization Note. closedCube a s comes from Definitions.Def_DbarRegularity_Setting; $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with volume its Lebesgue measure, valued in ℝ≥0∞. The value $(s^+)^d$ is written ENNReal.ofReal s ^ d. No restriction on $d$ or $s$ : for $d=0$ both sides equal $1$ .

Preamble

import Definitions.Def_DbarRegularity_Setting

Formal statement

namespace DbarRegularity

open MeasureTheory
open scoped ENNReal

/-- The Lebesgue measure of the closed cube `∏ᵢ [aᵢ, aᵢ + s]` in `ℝ^d` is `s^d` (and `0` when
`s < 0` and `d ≥ 1`). -/
theorem volume_closedCube {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (s : ℝ) :
    volume (closedCube a s) = ENNReal.ofReal s ^ d := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter I, § 3.2, p. 16

View graph