structure MeasuresAndSigmaAlgebras.IsOuterMeasure {X : Type u_1} (μstar : Set X → ENNReal) : Prop

Predicate axiomatising an outer measure μ* on X: empty set has measure zero, monotone with respect to inclusion, and countably subadditive.

• empty : μstar ∅ = 0
• mono {A B : Set X} : A ⊆ B → μstar A ≤ μstar B
• iUnion_le (A : ℕ → Set X) : μstar (⋃ (j : ℕ), A j) ≤ ∑' (j : ℕ), μstar (A j)

theorem MeasuresAndSigmaAlgebras.outerMeasure_isOuterMeasure {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) : IsOuterMeasure ⇑μ

Every Mathlib OuterMeasure satisfies the predicate IsOuterMeasure.

noncomputable def MeasuresAndSigmaAlgebras.IsOuterMeasure.toOuterMeasure {X : Type u_1} {μstar : Set X → ENNReal} (h : IsOuterMeasure μstar) : MeasureTheory.OuterMeasure X

Conversion from an IsOuterMeasure proof to a Mathlib OuterMeasure bundle.

noncomputable def MeasuresAndSigmaAlgebras.rectangleVolume {n : ℕ} (a b : Fin n → ℝ) : ENNReal

Volume of the axis-aligned rectangle [a, b] in ℝⁿ, defined as the product of side lengths b i - a i.

theorem MeasuresAndSigmaAlgebras.lebesgue_outer_measure_eq_volume_rectangle {n : ℕ} (a b : Fin n → ℝ) : MeasureTheory.volume (Set.Icc a b) = rectangleVolume a b

The Lebesgue measure of a closed rectangle [a, b] in ℝⁿ equals the product of its side lengths.

@[reducible, inline]

abbrev MeasuresAndSigmaAlgebras.SigmaAlgebra (X : Type u_1) : Type u_1

A σ-algebra on X (Melrose Def 2.1) is identified with MeasurableSpace X.

class MeasuresAndSigmaAlgebras.IsRadonMeasure {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) extends μ.Regular : Prop

A Radon measure on a topological measurable space is a Borel measure that is regular (inner regular on opens, outer regular, locally finite).

• lt_top_of_isCompact ⦃K : Set X⦄ : IsCompact K → μ K < ⊤
• outerRegular ⦃A : Set X⦄ : MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r
• innerRegular : μ.InnerRegularWRT IsCompact IsOpen

instance MeasuresAndSigmaAlgebras.Regular.toIsRadonMeasure {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.Regular] : IsRadonMeasure μ

Any regular measure is automatically a Radon measure in our sense.

theorem MeasuresAndSigmaAlgebras.lebesgue_borel_le_caratheodory (n : ℕ) : borel (Fin n → ℝ) ≤ MeasureTheory.volume.caratheodory

Every Borel set in ℝⁿ is Carathéodory-measurable with respect to Lebesgue outer measure.

def MeasuresAndSigmaAlgebras.IsOuterMeasureMeasurable {X : Type u_1} (μstar : Set X → ENNReal) (E : Set X) : Prop

Carathéodory measurability condition: E splits every test set A additively with respect to the outer measure μ*.

theorem MeasuresAndSigmaAlgebras.isOuterMeasureMeasurable_iff_isCaratheodory {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) (E : Set X) : IsOuterMeasureMeasurable (⇑μ) E ↔ μ.IsCaratheodory E

Our IsOuterMeasureMeasurable predicate agrees with Mathlib's IsCaratheodory.

@[reducible]

def MeasuresAndSigmaAlgebras.caratheodorySigmaAlgebra {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) : SigmaAlgebra X

The σ-algebra of Carathéodory-measurable sets for an outer measure μ.

noncomputable def MeasuresAndSigmaAlgebras.caratheodoryMeasure {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) : MeasureTheory.Measure X

The measure on the Carathéodory σ-algebra induced by an outer measure μ by restriction.

theorem MeasuresAndSigmaAlgebras.isOuterMeasureMeasurable_of_measure_zero {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) {E : Set X} (hE : μ E = 0) : μ.IsCaratheodory E

Any null set is Carathéodory-measurable.

theorem MeasuresAndSigmaAlgebras.caratheodoryMeasure_isComplete {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) : (caratheodoryMeasure μ).IsComplete

The Carathéodory measure on μ.caratheodory is complete: every null set is measurable.

theorem MeasuresAndSigmaAlgebras.caratheodory_theorem {X : Type u_1} (μ : MeasureTheory.OuterMeasure X) : ∃ (m : MeasureTheory.Measure X), m.IsComplete ∧ ∀ (s : Set X), MeasurableSet s → m s = μ s

Carathéodory's extension theorem (Melrose Thm 2.4): every outer measure restricts to a complete measure on its σ-algebra of measurable sets, with the values matching the outer measure.

theorem MeasuresAndSigmaAlgebras.isOpen_outerMeasureMeasurable_and_measure_eq_innerContent {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [MeasurableSpace X] [BorelSpace X] (U : Set X) (hU : IsOpen U) : IsOuterMeasureMeasurable (⇑(rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ)).outerMeasure) U ∧ (rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ)).measure U = (rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ)).innerContent { carrier := U, is_open' := hU }

For the Riesz content associated to a positive linear functional, open sets are Carathéodory-measurable and their measure equals the inner content.

instance MeasuresAndSigmaAlgebras.rieszMeasure_isRadonMeasure {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [LocallyCompactSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) : IsRadonMeasure (RealRMK.rieszMeasure Λ)

The Riesz-Markov-Kakutani measure associated with a positive linear functional on C_c(X, ℝ) is a Radon measure.

noncomputable def MeasuresAndSigmaAlgebras.inclusionCcC0 {X : Type u_1} [TopologicalSpace X] : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ZeroAtInftyContinuousMap X ℝ

Linear inclusion of compactly supported continuous functions into the space of continuous functions vanishing at infinity.

noncomputable def MeasuresAndSigmaAlgebras.restrictC0ToCc {X : Type u_1} [TopologicalSpace X] (Φ : ZeroAtInftyContinuousMap X ℝ →ₗ[ℝ] ℝ) (hΦ : ∀ (f : ZeroAtInftyContinuousMap X ℝ), (∀ (x : X), 0 ≤ f x) → 0 ≤ Φ f) : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

Restriction of a positive linear functional on C₀(X, ℝ) to C_c(X, ℝ), viewed as a positive linear map.

noncomputable def MeasuresAndSigmaAlgebras.rieszMeasureOfC0Functional {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [LocallyCompactSpace X] (Φ : ZeroAtInftyContinuousMap X ℝ →ₗ[ℝ] ℝ) (hΦ : ∀ (f : ZeroAtInftyContinuousMap X ℝ), (∀ (x : X), 0 ≤ f x) → 0 ≤ Φ f) : MeasureTheory.Measure X

The Riesz measure on X produced from a positive linear functional defined on C₀(X, ℝ), by restricting it to C_c(X, ℝ) and applying the RMK theorem.

theorem MeasuresAndSigmaAlgebras.prop_2_8_radon_measure_from_C0_functional {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [LocallyCompactSpace X] (Φ : ZeroAtInftyContinuousMap X ℝ →ₗ[ℝ] ℝ) (hΦ : ∀ (f : ZeroAtInftyContinuousMap X ℝ), (∀ (x : X), 0 ≤ f x) → 0 ≤ Φ f) : IsRadonMeasure (rieszMeasureOfC0Functional Φ hΦ)

Melrose Proposition 2.8: a positive linear functional on C₀(X, ℝ) produces a Radon measure on X.

theorem MeasuresAndSigmaAlgebras.borel_le_caratheodory_of_openSets_measurable {X : Type u_1} [TopologicalSpace X] (μ : MeasureTheory.OuterMeasure X) (h : ∀ (U : Set X), IsOpen U → IsOuterMeasureMeasurable (⇑μ) U) : borel X ≤ μ.caratheodory

Sufficient condition for the Borel σ-algebra to be contained in the Carathéodory σ-algebra of μ: every open set must be μ*-measurable.