Uniqueness of measures on Euclidean space

DefinitionVertex of a rectangle#✓fully proved

Let \(d\) be a natural number, let \(a, b \in \mathbb{R}^d\), and let \(S\) be a finite set of coordinate indices in \(\{0, \dots, d-1\}\). The vertex of the rectangle \((a, b]\) selected by \(S\) is the point \(v \in \mathbb{R}^d\) with \(v_i = a_i\) for \(i \in S\) and \(v_i = b_i\) for \(i \notin S\).

As \(S\) ranges over all \(2^d\) subsets of indices, these points are the vertices used in inclusion-exclusion sums over the rectangle.

def rectangleVertex {d : ℕ} (a b : Fin d → ℝ) (S : Finset (Fin d)) : Fin d → ℝ :=
  fun i => if i ∈ S then a i else b i

Used by 1

Used byRectangle value of a function

DefinitionRectangle value of a function#✓fully proved

For \(F : \mathbb{R}^d \to \mathbb{R}\) and arbitrary \(a, b \in \mathbb{R}^d\), the rectangle value of \(F\) at \(a, b\) is

\[\Delta_{a,b} F = \sum_{S \subseteq \{1, \dots, d\}} (-1)^{|S|} F(v_S),\]

where \(v_S \in \mathbb{R}^d\) is the vertex with \((v_S)_i = a_i\) for \(i \in S\) and \((v_S)_i = b_i\) for \(i \notin S\).

Write \((a, b] = \prod_{i=1}^d (a_i, b_i]\). When \(a_i \le b_i\) for every \(i\) and \(F\) is a distribution function on \(\mathbb{R}^d\), this signed inclusion–exclusion sum equals the mass \(\mu((a, b])\) of the associated measure \(\mu\).

def rectangleValue {d : ℕ} (F : (Fin d → ℝ) → ℝ) (a b : Fin d → ℝ) : ℝ :=
  ∑ S ∈ Finset.univ.powerset, (-1 : ℝ) ^ S.card * F (rectangleVertex a b S)

Uses 1 · Used by 1

Statement usesVertex of a rectangle

Used byUniqueness from rectangle values

LemmaLower orthants form a π-system#✓fully proved

For \(a \in \mathbb{R}^d\) let \(L_a = \prod_{i=1}^d (-\infty, a_i]\). If two such boxes \(L_a\) and \(L_b\) intersect, then their intersection is \(L_c\) for some \(c \in \mathbb{R}^d\).

lemma isPiSystem_piIic (d : ℕ) :
    IsPiSystem (univ.pi '' univ.pi (fun _ : Fin d => range (Iic : ℝ → Set ℝ)))

Used by 1

Used byQuadrant uniqueness for measures on \(\mathbb{R}^d\)

LemmaLower orthants generate the product σ-algebra on \(\mathbb{R}^d\)#✓fully proved

The product σ-algebra on \(\mathbb{R}^d\), built from the Borel σ-algebra on each coordinate, is generated by the boxes \(\prod_{i=1}^d (-\infty, a_i]\) for \(a \in \mathbb{R}^d\).

lemma generateFrom_piIic (d : ℕ) :
    generateFrom (univ.pi '' univ.pi (fun _ : Fin d => range (Iic : ℝ → Set ℝ))) =
      MeasurableSpace.pi

Used by 1

Used byQuadrant uniqueness for measures on \(\mathbb{R}^d\)

TheoremQuadrant uniqueness for measures on \(\mathbb{R}^d\)#✓fully proved

Let \(\mu\) and \(\nu\) be finite measures on \(\mathbb{R}^d\). If \(\mu(\{x : x \le a\}) = \nu(\{x : x \le a\})\) for every \(a \in \mathbb{R}^d\), where \(x \le a\) means \(x_i \le a_i\) for every \(i\), then \(\mu = \nu\).

This is the multivariate analogue of a CDF determining a probability measure.

theorem Measure.ext_of_Iic_pi (d : ℕ)
    (μ ν : Measure (Fin d → ℝ))
    [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (h : ∀ a : Fin d → ℝ, μ (Iic a) = ν (Iic a)) :
    μ = ν

Uses 2

Proof usesLower orthants generate the product σ-algebra on \(\mathbb{R}^d\) · Lower orthants form a π-system

DefinitionNonempty bounded half-open intervals#✓fully proved

The family of all intervals \((l, u] \subseteq \mathbb{R}\) with real endpoints \(l < u\). It is used as a generating π-system for the Borel σ-algebra on \(\mathbb{R}\).

def C_Ioc_pi : Set (Set ℝ) := { S | ∃ l u, l < u ∧ Ioc l u = S }

Used by 5

Used byRectangle uniqueness for measures on \(\mathbb{R}^d\) · Uniqueness from rectangle values · Half-open intervals generate the Borel σ-algebra on \(\mathbb{R}\) · Half-open intervals countably span \(\mathbb{R}\) · Nonempty bounded half-open intervals form a π-system

LemmaNonempty bounded half-open intervals form a π-system#✓fully proved

If two intervals \((l, u]\) and \((l', u']\) in \(\mathbb{R}\) with \(l < u\) and \(l' < u'\) intersect, then their intersection is again an interval \((l'', u'']\) with \(l'' < u''\).

lemma isPiSystem_C_Ioc_pi : IsPiSystem C_Ioc_pi

Uses 1 · Used by 2

Statement usesNonempty bounded half-open intervals

Used byRectangle uniqueness for measures on \(\mathbb{R}^d\) · Uniqueness from rectangle values

LemmaHalf-open intervals generate the Borel σ-algebra on \(\mathbb{R}\)#✓fully proved

The Borel σ-algebra on \(\mathbb{R}\) is the σ-algebra generated by the nonempty bounded half-open intervals \((l, u]\) with \(l < u\).

lemma generateFrom_C_Ioc_pi :
    generateFrom C_Ioc_pi = (inferInstance : MeasurableSpace ℝ)

Uses 1 · Used by 2

Statement usesNonempty bounded half-open intervals

Used byRectangle uniqueness for measures on \(\mathbb{R}^d\) · Uniqueness from rectangle values

LemmaHalf-open intervals countably span \(\mathbb{R}\)#✓fully proved

There is a sequence of nonempty bounded half-open intervals \((l, u]\) with \(l < u\) whose union is \(\mathbb{R}\); for example, the intervals \((-n - 1, n + 1]\) for \(n \in \mathbb{N}\).

lemma isCountablySpanning_C_Ioc_pi : IsCountablySpanning C_Ioc_pi

Uses 1 · Used by 2

Statement usesNonempty bounded half-open intervals

Used byRectangle uniqueness for measures on \(\mathbb{R}^d\) · Uniqueness from rectangle values

TheoremRectangle uniqueness for measures on \(\mathbb{R}^d\)#✓fully proved

Let \(\mu_1\) and \(\mu_2\) be finite measures on \(\mathbb{R}^d\). If \(\mu_1((a, b]) = \mu_2((a, b])\) for all \(a, b \in \mathbb{R}^d\) with \(a_i \le b_i\) for every \(i\), where \((a, b] = \prod_{i=1}^d (a_i, b_i]\), then \(\mu_1 = \mu_2\).

The finiteness hypothesis is essential: for \(d \ge 1\), counting measure and twice counting measure agree on every rectangle (both give \(\infty\) on every nonempty rectangle and \(0\) on every empty one) but are distinct.

theorem Measure.eq_of_forall_Ioc_eq (d : ℕ)
    (μ₁ μ₂ : Measure (Fin d → ℝ))
    [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂]
    (h : ∀ (a b : Fin d → ℝ), (∀ i, a i ≤ b i) →
      μ₁ (univ.pi fun i => Ioc (a i) (b i)) = μ₂ (univ.pi fun i => Ioc (a i) (b i))) :
    μ₁ = μ₂

Uses 4

Proof usesNonempty bounded half-open intervals · Half-open intervals generate the Borel σ-algebra on \(\mathbb{R}\) · Half-open intervals countably span \(\mathbb{R}\) · Nonempty bounded half-open intervals form a π-system

TheoremUniqueness from rectangle values#✓fully proved

Let \(F : \mathbb{R}^d \to \mathbb{R}\), and let \(\mu_1\) and \(\mu_2\) be measures on \(\mathbb{R}^d\). Suppose that for all \(a, b \in \mathbb{R}^d\) with \(a_i \le b_i\) for every \(i\), both \(\mu_1\) and \(\mu_2\) assign the rectangle \((a, b] = \prod_{i=1}^d (a_i, b_i]\) the mass \(\max(\Delta_{a,b} F, 0)\), where \(\Delta_{a,b} F\) is the rectangle value of \(F\) at \(a, b\). Then \(\mu_1 = \mu_2\).

This is the uniqueness half of the characterization of measures on \(\mathbb{R}^d\) by a distribution function. No finiteness hypothesis is needed: the rectangle formula itself forces the measures to be finite on every rectangle \((a, b]\).

theorem Measure.eq_of_forall_rectangleValue_eq {d : ℕ}
    (F : (Fin d → ℝ) → ℝ)
    {μ₁ μ₂ : Measure (Fin d → ℝ)}
    (h₁ : ∀ (a b : Fin d → ℝ), (∀ i, a i ≤ b i) →
      μ₁ (univ.pi fun i => Ioc (a i) (b i)) = ENNReal.ofReal (rectangleValue F a b))
    (h₂ : ∀ (a b : Fin d → ℝ), (∀ i, a i ≤ b i) →
      μ₂ (univ.pi fun i => Ioc (a i) (b i)) = ENNReal.ofReal (rectangleValue F a b)) :
    μ₁ = μ₂

Uses 5

Statement usesRectangle value of a function

Proof usesNonempty bounded half-open intervals · Half-open intervals generate the Borel σ-algebra on \(\mathbb{R}\) · Half-open intervals countably span \(\mathbb{R}\) · Nonempty bounded half-open intervals form a π-system

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.