def rectangleVertex {d : ℕ} (a b : Fin d → ℝ) (S : Finset (Fin d)) : Fin d → ℝ

The vertex of the rectangle [a, b] ⊆ ℝᵈ obtained by selecting the lower coordinate a i for indices i ∈ S and the upper coordinate b i otherwise. Used to compute inclusion–exclusion sums over all 2^d vertices.

def rectangleValue {d : ℕ} (F : (Fin d → ℝ) → ℝ) (a b : Fin d → ℝ) : ℝ

The alternating sum of F over the 2^d vertices of the rectangle (a, b]. For a distribution function F on ℝᵈ, this equals the mass μ((a, b]) of the associated measure (signed inclusion–exclusion).

def IsCoordNonDecreasing {d : ℕ} (F : (Fin d → ℝ) → ℝ) : Prop

F : ℝᵈ → ℝ is coordinate-wise non-decreasing: for every coordinate i, fixing the remaining coordinates and increasing the i-th argument does not decrease the value of F.

def IsCoordRightContinuous {d : ℕ} (F : (Fin d → ℝ) → ℝ) : Prop

F : ℝᵈ → ℝ is coordinate-wise right continuous: in every coordinate i, with the remaining coordinates fixed, F is right-continuous in the i-th argument.

def IsRectangleNonneg {d : ℕ} (F : (Fin d → ℝ) → ℝ) : Prop

F assigns a non-negative inclusion–exclusion value to every rectangle (a, b] with a ≤ b coordinate-wise. This is the multivariate analogue of monotonicity of a CDF and is needed for F to come from a measure.

theorem MeasureTheory.Real.isCountablySpanning_range_Iic : IsCountablySpanning (Set.range Set.Iic)

The family of left-infinite intervals {Iic n : n ∈ ℕ} is a countable spanning collection of ℝ: their union covers all of ℝ.

theorem MeasureTheory.Real.generateFrom_range_Iic : MeasurableSpace.generateFrom (Set.range Set.Iic) = inferInstance

The Borel σ-algebra on ℝ is generated by the left-infinite intervals Iic x for x ∈ ℝ.

theorem MeasureTheory.isPiSystem_piIic (d : ℕ) : IsPiSystem (Set.univ.pi '' Set.univ.pi fun (x : Fin d) => Set.range Set.Iic)

The collection of d-dimensional boxes of the form ∏ᵢ Iic (aᵢ) is a π-system in ℝᵈ: finite intersections of such boxes are again of this form.

theorem MeasureTheory.generateFrom_piIic (d : ℕ) : MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi fun (x : Fin d) => Set.range Set.Iic) = inferInstance

The Borel σ-algebra on ℝᵈ is generated by d-dimensional boxes of the form ∏ᵢ Iic (aᵢ).

theorem MeasureTheory.ProbabilityMeasure.ext_of_Iic (d : ℕ) (μ ν : Measure (Fin d → ℝ)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (h : ∀ (a : Fin d → ℝ), μ (Set.Iic a) = ν (Set.Iic a)) : μ = ν

Two probability measures on ℝᵈ are equal whenever they agree on all left-closed quadrants Iic a = {x | x ≤ a} for a ∈ ℝᵈ. This is the multivariate analogue of CDF determining a probability measure.

theorem caratheodory_extension_rectangleFunction {d : ℕ} (F : (Fin d → ℝ) → ℝ) (hF_mono : IsCoordNonDecreasing F) (hF_rcont : IsCoordRightContinuous F) (hF_rect : IsRectangleNonneg F) : ∃ (μ : MeasureTheory.Measure (Fin d → ℝ)), ∀ (a b : Fin d → ℝ), (∀ (i : Fin d), a i ≤ b i) → μ (Set.univ.pi fun (i : Fin d) => Set.Ioc (a i) (b i)) = ENNReal.ofReal (rectangleValue F a b)

Existence (Carathéodory extension). Given F : ℝᵈ → ℝ that is coordinate-wise non-decreasing, coordinate-wise right-continuous, and assigns non-negative rectangle values, there exists a Borel measure μ on ℝᵈ whose mass on each rectangle (a, b] equals rectangleValue F a b.

def C_Ioc_pi : Set (Set ℝ)

The collection of nonempty bounded half-open intervals (l, u] in ℝ. Used as a generating π-system for the Borel σ-algebra.

theorem isPiSystem_C_Ioc_pi : IsPiSystem C_Ioc_pi

The family of nonempty bounded half-open intervals (l, u] is a π-system.

theorem generateFrom_C_Ioc_pi : MeasurableSpace.generateFrom C_Ioc_pi = inferInstance

The Borel σ-algebra on ℝ is generated by the family of nonempty bounded half-open intervals (l, u].

theorem isCountablySpanning_C_Ioc_pi : IsCountablySpanning C_Ioc_pi

The family of nonempty bounded half-open intervals (l, u] is countably spanning: e.g. the intervals (-n-1, n+1] for n ∈ ℕ cover ℝ.

theorem exists_unique_borelMeasure_of_rectangleFunction {d : ℕ} (F : (Fin d → ℝ) → ℝ) (hF_mono : IsCoordNonDecreasing F) (hF_rcont : IsCoordRightContinuous F) (hF_rect : IsRectangleNonneg F) : ∃! μ : MeasureTheory.Measure (Fin d → ℝ), ∀ (a b : Fin d → ℝ), (∀ (i : Fin d), a i ≤ b i) → μ (Set.univ.pi fun (i : Fin d) => Set.Ioc (a i) (b i)) = ENNReal.ofReal (rectangleValue F a b)

Characterization of probability measures on ℝᵈ. Given F : ℝᵈ → ℝ that is coordinate-wise non-decreasing, coordinate-wise right-continuous, and rectangle-nonnegative, there exists a unique Borel measure μ on ℝᵈ whose value on each finite rectangle (a, b] is determined by the inclusion–exclusion rectangleValue F a b.