Documentation

Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

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 #

Main results #

theorem MeasureTheory.tendsto_lintegral_nn_filter_of_le_const {Ω : Type u_1} [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] (μ : 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} [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] (μ : 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 (E.indicator (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 (E.indicator 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.

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.

Instances
    theorem HasOuterApproxClosed.exAppr {X : Type u_1} [TopologicalSpace X] [self : HasOuterApproxClosed X] (F : Set X) :
    IsClosed F∃ (fseq : BoundedContinuousFunction X NNReal), (∀ (n : ) (x : X), (fseq n) x 1) (∀ (n : ), xF, 1 (fseq n) x) Filter.Tendsto (fun (n : ) (x : X) => (fseq n) x) Filter.atTop (nhds (F.indicator fun (x : X) => 1))
    noncomputable def IsClosed.apprSeq {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) :

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

    Equations
    • hF.apprSeq = .choose
    Instances For
      theorem HasOuterApproxClosed.apprSeq_apply_le_one {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ) (x : X) :
      (hF.apprSeq 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) :
      (hF.apprSeq 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) => (hF.apprSeq n) x) Filter.atTop (nhds (F.indicator fun (x : X) => 1))
      theorem HasOuterApproxClosed.indicator_le_apprSeq {X : Type u_1} [TopologicalSpace X] [HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F) (n : ) :
      (F.indicator fun (x : X) => 1) (hF.apprSeq 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), ((hF.apprSeq 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), ((hF.apprSeq 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.

      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.