Spaces where indicators of closed sets have decreasing approximations by continuous functions

In this file we define a typeclass HasOuterApproxClosed for topological spaces in which indicator functions of closed sets have sequences of bounded continuous functions approximating them from above. All pseudo-emetrizable spaces have this property, see instHasOuterApproxClosed.

In spaces with the HasOuterApproxClosed property, finite Borel measures are uniquely characterized by the integrals of bounded continuous functions. Also weak convergence of finite measures and convergence in distribution for random variables behave somewhat well in spaces with this property.

Main definitions

• HasOuterApproxClosed: the typeclass for topological spaces in which indicator functions of closed sets have sequences of bounded continuous functions approximating them.
• IsClosed.apprSeq: a (non-constructive) choice of an approximating sequence to the indicator function of a closed set.

Main results

• instHasOuterApproxClosed: Any pseudo-emetrizable space has the property HasOuterApproxClosed.
• tendsto_lintegral_apprSeq: The integrals of the approximating functions to the indicator of a closed set tend to the measure of the set.
• ext_of_forall_lintegral_eq_of_IsFiniteMeasure: Two finite measures are equal if the integrals of all bounded continuous functions with respect to both agree.

theorem MeasureTheory.tendsto_lintegral_nn_filter_of_le_const {Ω : Type u_1} [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [Filter.IsCountablyGenerated L] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) {f : Ω → NNReal} (fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (i : ι) => (fs i) ω) L (nhds (f ω))) : Filter.Tendsto (fun (i : ι) => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (nhds (∫⁻ (ω : Ω), ↑(f ω) ∂μ))

A bounded convergence theorem for a finite measure: If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a limit, then their integrals against the finite measure tend to the integral of the limit. This formulation assumes:

• the functions tend to a limit along a countably generated filter;
• the limit is in the almost everywhere sense;
• boundedness holds almost everywhere;
• integration is MeasureTheory.lintegral, i.e., the functions and their integrals are ℝ≥0∞-valued.

theorem MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [Filter.IsCountablyGenerated L] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {c : NNReal} {E : Set Ω} (E_mble : MeasurableSet E) (fs : ι → BoundedContinuousFunction Ω NNReal) (fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) (fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (i : ι) => (fs i) ω) L (nhds (Set.indicator E (fun (x : Ω) => 1) ω))) : Filter.Tendsto (fun (n : ι) => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) L (nhds (↑↑μ E))

If bounded continuous functions tend to the indicator of a measurable set and are uniformly bounded, then their integrals against a finite measure tend to the measure of the set. This formulation assumes:

• the functions tend to a limit along a countably generated filter;
• the limit is in the almost everywhere sense;
• boundedness holds almost everywhere.

theorem MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator {Ω : Type u_1} [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {c : NNReal} {E : Set Ω} (E_mble : MeasurableSet E) (fs : ℕ → BoundedContinuousFunction Ω NNReal) (fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) (fs_lim : Filter.Tendsto (fun (n : ℕ) (ω : Ω) => (fs n) ω) Filter.atTop (nhds (Set.indicator E fun (x : Ω) => 1))) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) Filter.atTop (nhds (↑↑μ E))

If a sequence of bounded continuous functions tends to the indicator of a measurable set and the functions are uniformly bounded, then their integrals against a finite measure tend to the measure of the set.

A similar result with more general assumptions is MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator.

theorem MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed {Ω : Type u_2} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {F : Set Ω} (F_closed : IsClosed F) {δs : ℕ → ℝ} (δs_pos : ∀ (n : ℕ), 0 < δs n) (δs_lim : Filter.Tendsto δs Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) Filter.atTop (nhds (↑↑μ F))

The integrals of thickened indicators of a closed set against a finite measure tend to the measure of the closed set if the thickening radii tend to zero.

class HasOuterApproxClosed (X : Type u_1) [TopologicalSpace X] : Prop

A type class for topological spaces in which the indicator functions of closed sets can be approximated pointwise from above by a sequence of bounded continuous functions.

• exAppr : ∀ (F : Set X), IsClosed F → ∃ (fseq : ℕ → BoundedContinuousFunction X NNReal), (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧ (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧ Filter.Tendsto (fun (n : ℕ) (x : X) => (fseq n) x) Filter.atTop (nhds (Set.indicator F fun (x : X) => 1))

noncomputable def IsClosed.apprSeq {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) : ℕ → BoundedContinuousFunction X NNReal

A sequence of continuous functions X → [0,1] tending to the indicator of a closed set.

Equations

• IsClosed.apprSeq hF = Exists.choose ⋯

theorem HasOuterApproxClosed.apprSeq_apply_le_one {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ℕ) (x : X) : (IsClosed.apprSeq hF n) x ≤ 1

theorem HasOuterApproxClosed.apprSeq_apply_eq_one {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ℕ) {x : X} (hxF : x ∈ F) : (IsClosed.apprSeq hF n) x = 1

theorem HasOuterApproxClosed.tendsto_apprSeq {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) : Filter.Tendsto (fun (n : ℕ) (x : X) => (IsClosed.apprSeq hF n) x) Filter.atTop (nhds (Set.indicator F fun (x : X) => 1))

theorem HasOuterApproxClosed.indicator_le_apprSeq {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ℕ) : (Set.indicator F fun (x : X) => 1) ≤ ⇑(IsClosed.apprSeq hF n)

theorem HasOuterApproxClosed.measure_le_lintegral {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) (n : ℕ) : ↑↑μ F ≤ ∫⁻ (x : X), ↑((IsClosed.apprSeq hF n) x) ∂μ

The measure of a closed set is at most the integral of any function in a decreasing approximating sequence to the indicator of the set.

theorem HasOuterApproxClosed.tendsto_lintegral_apprSeq {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : X), ↑((IsClosed.apprSeq hF n) x) ∂μ) Filter.atTop (nhds (↑↑μ F))

The integrals along a decreasing approximating sequence to the indicator of a closed set tend to the measure of the closed set.

noncomputable instance instHasOuterApproxClosed (X : Type u_1) [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] : HasOuterApproxClosed X

Equations

• ⋯ = ⋯

theorem MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) {F : Set Ω} (F_closed : IsClosed F) : ↑↑μ F = ↑↑ν F

Two finite measures give equal values to all closed sets if the integrals of all bounded continuous functions with respect to the two measures agree.

theorem MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) : μ = ν

Two finite Borel measures are equal if the integrals of all bounded continuous functions with respect to both agree.