def MeasuresAndSigmaAlgebras.IsPositiveLinearFunctional {X : Type u_1} [MetricSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) : Prop

A continuous linear functional u : C₀(X, ℝ) →L[ℝ] ℝ is positive if u f ≥ 0 whenever f ≥ 0 pointwise.

noncomputable def MeasuresAndSigmaAlgebras.functionalMeasureOpen {X : Type u_1} [MetricSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (U : Set X) : IsOpen U → ENNReal

The premeasure of an open set U associated to a positive linear functional u: the supremum of u f over all f : C₀(X, ℝ) with 0 ≤ f ≤ 1 and tsupport f ⊆ U compact. This is the open-set value used to induce an outer measure (Section 1.11 of Melrose).

theorem MeasuresAndSigmaAlgebras.zeroAtInfty_eq_zero_of_tsupport_subset_empty {X : Type u_2} [MetricSpace X] {f : ZeroAtInftyContinuousMap X ℝ} (h : tsupport ⇑f ⊆ ∅) : f = 0

A continuous function vanishing at infinity whose topological support is contained in ∅ must be identically zero.

theorem MeasuresAndSigmaAlgebras.functionalMeasureOpen_empty {X : Type u_2} [MetricSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) : functionalMeasureOpen u ∅ ⋯ = 0

The functional premeasure of the empty open set is zero: the only test function with support in ∅ is the zero function.

theorem MeasuresAndSigmaAlgebras.functionalMeasureOpen_mono {X : Type u_2} [MetricSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) ⦃U V : Set X⦄ (hU : IsOpen U) (hV : IsOpen V) (h : U ⊆ V) : functionalMeasureOpen u U hU ≤ functionalMeasureOpen u V hV

Monotonicity of the functional premeasure on open sets: if U ⊆ V then functionalMeasureOpen u U ≤ functionalMeasureOpen u V.

theorem MeasuresAndSigmaAlgebras.functionalMeasureOpen_partition_of_unity_bound {X : Type u_2} [MetricSpace X] [LocallyCompactSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (hu : IsPositiveLinearFunctional u) (f : ZeroAtInftyContinuousMap X ℝ) (hf_range : ∀ (x : X), f x ∈ Set.Icc 0 1) (hf_compact : IsCompact (tsupport ⇑f)) (U : ℕ → Set X) (hU : ∀ (i : ℕ), IsOpen (U i)) (s : Finset ℕ) (hs : tsupport ⇑f ⊆ ⋃ i ∈ s, U i) : ENNReal.ofReal (u f) ≤ ∑ i ∈ s, functionalMeasureOpen u (U i) ⋯

Partition-of-unity inequality for the functional premeasure: if f is a compactly supported test function with 0 ≤ f ≤ 1 whose support is covered by finitely many open sets U i, then u f ≤ ∑ i ∈ s, functionalMeasureOpen u (U i).

theorem MeasuresAndSigmaAlgebras.functionalMeasureOpen_countable_subadditive {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (hu : IsPositiveLinearFunctional u) ⦃U : ℕ → Set X⦄ (hU : ∀ (i : ℕ), IsOpen (U i)) : functionalMeasureOpen u (⋃ (i : ℕ), U i) ⋯ ≤ ∑' (i : ℕ), functionalMeasureOpen u (U i) ⋯

Countable subadditivity of the functional premeasure on open sets: for any sequence of open sets U i, functionalMeasureOpen u (⋃ U i) ≤ ∑' i, functionalMeasureOpen u (U i).

noncomputable def MeasuresAndSigmaAlgebras.functionalOuterMeasure {X : Type u_1} [MetricSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) : IsPositiveLinearFunctional u → MeasureTheory.OuterMeasure X

The outer measure on X induced by a positive linear functional u via its values on open sets (Section 1.11/1.12 of Melrose). Used as the starting point for constructing the associated Radon measure via Caratheodory's theorem.

theorem MeasuresAndSigmaAlgebras.functionalOuterMeasure_isOuterMeasure {X : Type u_1} [MetricSpace X] [LocallyCompactSpace X] (u : ZeroAtInftyContinuousMap X ℝ →L[ℝ] ℝ) (hu : IsPositiveLinearFunctional u) : IsOuterMeasure ⇑(functionalOuterMeasure u hu)

functionalOuterMeasure u hu satisfies the abstract axioms of an outer measure (monotonicity, σ-subadditivity, and vanishing on the empty set).