Documentation

Mathlib.MeasureTheory.Measure.FiniteMeasure

Finite measures #

This file defines the type of finite measures on a given measurable space. When the underlying space has a topology and the measurable space structure (sigma algebra) is finer than the Borel sigma algebra, then the type of finite measures is equipped with the topology of weak convergence of measures. The topology of weak convergence is the coarsest topology w.r.t. which for every bounded continuous ℝ≥0-valued function f, the integration of f against the measure is continuous.

Main definitions #

The main definitions are

Main results #

Implementation notes #

The topology of weak convergence of finite Borel measures is defined using a mapping from MeasureTheory.FiniteMeasure Ω to WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0), inheriting the topology from the latter.

The implementation of MeasureTheory.FiniteMeasure Ω and is directly as a subtype of MeasureTheory.Measure Ω, and the coercion to a function is the composition ENNReal.toNNReal and the coercion to function of MeasureTheory.Measure Ω. Another alternative would have been to use a bijection with MeasureTheory.VectorMeasure Ω ℝ≥0 as an intermediate step. Some considerations:

References #

Tags #

weak convergence of measures, finite measure

Finite measures #

In this section we define the Type of MeasureTheory.FiniteMeasure Ω, when Ω is a measurable space. Finite measures on Ω are a module over ℝ≥0.

If Ω is moreover a topological space and the sigma algebra on Ω is finer than the Borel sigma algebra (i.e. [OpensMeasurableSpace Ω]), then MeasureTheory.FiniteMeasure Ω is equipped with the topology of weak convergence of measures. This is implemented by defining a pairing of finite measures μ on Ω with continuous bounded nonnegative functions f : Ω →ᵇ ℝ≥0 via integration, and using the associated weak topology (essentially the weak-star topology on the dual of Ω →ᵇ ℝ≥0).

Finite measures are defined as the subtype of measures that have the property of being finite measures (i.e., their total mass is finite).

Equations
Instances For

    Coercion from MeasureTheory.FiniteMeasure Ω to MeasureTheory.Measure Ω.

    Equations
    • MeasureTheory.FiniteMeasure.toMeasure = Subtype.val
    Instances For

      A finite measure can be interpreted as a measure.

      Equations
      • MeasureTheory.FiniteMeasure.instCoe = { coe := MeasureTheory.FiniteMeasure.toMeasure }
      Equations
      @[simp]
      theorem MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) :
      ((fun (s : Set Ω) => (ν s).toNNReal) s) = ν s
      theorem MeasureTheory.FiniteMeasure.toMeasure_injective {Ω : Type u_1} [MeasurableSpace Ω] :
      Function.Injective MeasureTheory.FiniteMeasure.toMeasure
      theorem MeasureTheory.FiniteMeasure.apply_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {s₁ : Set Ω} {s₂ : Set Ω} (h : s₁ s₂) :
      (fun (s : Set Ω) => (μ s).toNNReal) s₁ (fun (s : Set Ω) => (μ s).toNNReal) s₂

      The (total) mass of a finite measure μ is μ univ, i.e., the cast to NNReal of (μ : measure Ω) univ.

      Equations
      • μ.mass = (fun (s : Set Ω) => (μ s).toNNReal) Set.univ
      Instances For
        @[simp]
        theorem MeasureTheory.FiniteMeasure.apply_le_mass {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) :
        (fun (s : Set Ω) => (μ s).toNNReal) s μ.mass
        @[simp]
        theorem MeasureTheory.FiniteMeasure.ennreal_mass {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} :
        μ.mass = μ Set.univ
        Equations
        • MeasureTheory.FiniteMeasure.instZero = { zero := 0, }
        theorem MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) (h : ∀ (s : Set Ω), MeasurableSet s(fun (s : Set Ω) => (μ s).toNNReal) s = (fun (s : Set Ω) => (ν s).toNNReal) s) :
        μ = ν
        Equations
        • MeasureTheory.FiniteMeasure.instInhabited = { default := 0 }
        Equations
        Equations
        theorem MeasureTheory.FiniteMeasure.coeFn_zero {Ω : Type u_1} [MeasurableSpace Ω] :
        (fun (s : Set Ω) => (0 s).toNNReal) = 0
        @[simp]
        theorem MeasureTheory.FiniteMeasure.coeFn_add {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) :
        (fun (s : Set Ω) => ((μ + ν) s).toNNReal) = (fun (s : Set Ω) => (μ s).toNNReal) + fun (s : Set Ω) => (ν s).toNNReal
        @[simp]
        theorem MeasureTheory.FiniteMeasure.coeFn_smul {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal] (c : R) (μ : MeasureTheory.FiniteMeasure Ω) :
        (fun (s : Set Ω) => ((c μ) s).toNNReal) = c fun (s : Set Ω) => (μ s).toNNReal
        Equations
        @[simp]
        theorem MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom_apply {Ω : Type u_1} [MeasurableSpace Ω] :
        ∀ (a : MeasureTheory.FiniteMeasure Ω), MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom a = a

        Coercion is an AddMonoidHom.

        Equations
        • MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom = { toFun := MeasureTheory.FiniteMeasure.toMeasure, map_zero' := , map_add' := }
        Instances For
          Equations
          theorem MeasureTheory.FiniteMeasure.coeFn_smul_apply {Ω : Type u_1} [MeasurableSpace Ω] {R : Type u_2} [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal ENNReal] [IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal] (c : R) (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) :
          (fun (s : Set Ω) => ((c μ) s).toNNReal) s = c (fun (s : Set Ω) => (μ s).toNNReal) s

          Restrict a finite measure μ to a set A.

          Equations
          • μ.restrict A = (μ).restrict A,
          Instances For
            theorem MeasureTheory.FiniteMeasure.restrict_measure_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) :
            (μ.restrict A) = (μ).restrict A
            theorem MeasureTheory.FiniteMeasure.restrict_apply_measure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) :
            (μ.restrict A) s = μ (s A)
            theorem MeasureTheory.FiniteMeasure.restrict_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) :
            (fun (s : Set Ω) => ((μ.restrict A) s).toNNReal) s = (fun (s : Set Ω) => (μ s).toNNReal) (s A)
            theorem MeasureTheory.FiniteMeasure.restrict_mass {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) :
            (μ.restrict A).mass = (fun (s : Set Ω) => (μ s).toNNReal) A
            theorem MeasureTheory.FiniteMeasure.restrict_eq_zero_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) :
            μ.restrict A = 0 (fun (s : Set Ω) => (μ s).toNNReal) A = 0
            theorem MeasureTheory.FiniteMeasure.restrict_nonzero_iff {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) :
            μ.restrict A 0 (fun (s : Set Ω) => (μ s).toNNReal) A 0
            theorem MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {ν : MeasureTheory.FiniteMeasure Ω} (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.

            The pairing of a finite (Borel) measure μ with a nonnegative bounded continuous function is obtained by (Lebesgue) integrating the (test) function against the measure. This is MeasureTheory.FiniteMeasure.testAgainstNN.

            Equations
            • μ.testAgainstNN f = (∫⁻ (ω : Ω), (f ω)μ).toNNReal
            Instances For
              @[simp]
              theorem MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {f : BoundedContinuousFunction Ω NNReal} :
              (μ.testAgainstNN f) = ∫⁻ (ω : Ω), (f ω)μ
              theorem MeasureTheory.FiniteMeasure.testAgainstNN_mono {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {f : BoundedContinuousFunction Ω NNReal} {g : BoundedContinuousFunction Ω NNReal} (f_le_g : f g) :
              μ.testAgainstNN f μ.testAgainstNN g
              @[simp]
              theorem MeasureTheory.FiniteMeasure.testAgainstNN_one {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) :
              μ.testAgainstNN 1 = μ.mass
              @[simp]
              theorem MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] (c : NNReal) (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) :
              (c μ).testAgainstNN f = c μ.testAgainstNN f
              theorem MeasureTheory.FiniteMeasure.testAgainstNN_add {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (f₁ : BoundedContinuousFunction Ω NNReal) (f₂ : BoundedContinuousFunction Ω NNReal) :
              μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂

              Finite measures yield elements of the WeakDual of bounded continuous nonnegative functions via MeasureTheory.FiniteMeasure.testAgainstNN, i.e., integration.

              Equations
              Instances For
                @[simp]
                theorem MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) :
                μ.toWeakDualBCNN = μ.testAgainstNN
                @[simp]
                theorem MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) :
                μ.toWeakDualBCNN f = (∫⁻ (x : Ω), (f x)μ).toNNReal

                The topology of weak convergence on MeasureTheory.FiniteMeasure Ω is inherited (induced) from the weak-* topology on WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) via the function MeasureTheory.FiniteMeasure.toWeakDualBCNN.

                Equations
                • MeasureTheory.FiniteMeasure.instTopologicalSpace = TopologicalSpace.induced MeasureTheory.FiniteMeasure.toWeakDualBCNN inferInstance
                theorem MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] :
                Continuous MeasureTheory.FiniteMeasure.toWeakDualBCNN

                Integration of (nonnegative bounded continuous) test functions against finite Borel measures depends continuously on the measure.

                The total mass of a finite measure depends continuously on the measure.

                theorem Filter.Tendsto.mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (h : Filter.Tendsto μs F (nhds μ)) :
                Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass)

                Convergence of finite measures implies the convergence of their total masses.

                theorem MeasureTheory.FiniteMeasure.tendsto_iff_weak_star_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} :
                Filter.Tendsto μs F (nhds μ) Filter.Tendsto (fun (i : γ) => (μs i).toWeakDualBCNN) F (nhds μ.toWeakDualBCNN)
                theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} :
                Filter.Tendsto μs F (nhds μ) ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => (μs i).toWeakDualBCNN f) F (nhds (μ.toWeakDualBCNN f))
                theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} :
                Filter.Tendsto μs F (nhds μ) ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))
                theorem MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds 0)) (f : BoundedContinuousFunction Ω NNReal) :
                Filter.Tendsto (fun (i : γ) => (μs i).testAgainstNN f) F (nhds 0)

                If the total masses of finite measures tend to zero, then the measures tend to zero. This formulation concerns the associated functionals on bounded continuous nonnegative test functions. See MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass for a formulation stating the weak convergence of measures.

                theorem MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds 0)) :

                If the total masses of finite measures tend to zero, then the measures tend to zero.

                theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_3} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} :
                Filter.Tendsto μs F (nhds μ) ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => ∫⁻ (x : Ω), (f x)(μs i)) F (nhds (∫⁻ (x : Ω), (f x)μ))

                A characterization of weak convergence in terms of integrals of bounded continuous nonnegative functions.

                The mapping toWeakDualBCNN from finite Borel measures to the weak dual of Ω →ᵇ ℝ≥0 is injective, if in the underlying space Ω, indicator functions of closed sets have decreasing approximations by sequences of continuous functions (in particular if Ω is pseudometrizable).

                theorem MeasureTheory.FiniteMeasure.embedding_toWeakDualBCNN (Ω : Type u_1) [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω] :
                Embedding MeasureTheory.FiniteMeasure.toWeakDualBCNN

                On topological spaces where indicators of closed sets have decreasing approximating sequences of continuous functions (HasOuterApproxClosed), the topology of weak convergence of finite Borel measures is Hausdorff (T2Space).

                Equations
                • =

                Bounded convergence results for finite measures #

                This section is about bounded convergence theorems for finite measures.

                theorem MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) {fs : BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ (n : ) (ω : Ω), (fs n) ω c) {f : ΩNNReal} (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun (n : ) => (fs n) ω) Filter.atTop (nhds (f ω))) :
                Filter.Tendsto (fun (n : ) => ∫⁻ (ω : Ω), ((fs n) ω)μ) Filter.atTop (nhds (∫⁻ (ω : Ω), (f ω)μ))

                A bounded convergence theorem for a finite measure: If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and tend pointwise to a limit, then their integrals (MeasureTheory.lintegral) against the finite measure tend to the integral of the limit.

                A related result with more general assumptions is MeasureTheory.tendsto_lintegral_nn_filter_of_le_const.

                theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] {μ : MeasureTheory.FiniteMeasure Ω} {fs : ιBoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω c) {f : BoundedContinuousFunction Ω NNReal} (fs_lim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (i : ι) => (fs i) ω) L (nhds (f ω))) :
                Filter.Tendsto (fun (i : ι) => μ.testAgainstNN (fs i)) L (nhds (μ.testAgainstNN 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 the pairing against non-negative continuous test functions (MeasureTheory.FiniteMeasure.testAgainstNN).

                A related result using MeasureTheory.lintegral for integration is MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const.

                theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {fs : BoundedContinuousFunction Ω NNReal} {c : NNReal} (fs_le_const : ∀ (n : ) (ω : Ω), (fs n) ω c) {f : BoundedContinuousFunction Ω NNReal} (fs_lim : ∀ (ω : Ω), Filter.Tendsto (fun (n : ) => (fs n) ω) Filter.atTop (nhds (f ω))) :
                Filter.Tendsto (fun (n : ) => μ.testAgainstNN (fs n)) Filter.atTop (nhds (μ.testAgainstNN f))

                A bounded convergence theorem for a finite measure: If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and tend pointwise to a limit, then their integrals (MeasureTheory.FiniteMeasure.testAgainstNN) against the finite measure tend to the integral of the limit.

                Related results:

                Weak convergence of finite measures with bounded continuous real-valued functions #

                In this section we characterize the weak convergence of finite measures by the usual (defining) condition that the integrals of all bounded continuous real-valued functions converge.

                theorem MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (h : ∀ (f : BoundedContinuousFunction Ω ), Filter.Tendsto (fun (i : γ) => ∫ (x : Ω), f x(μs i)) F (nhds (∫ (x : Ω), f xμ))) :
                Filter.Tendsto μs F (nhds μ)
                theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} :
                Filter.Tendsto μs F (nhds μ) ∀ (f : BoundedContinuousFunction Ω ), Filter.Tendsto (fun (i : γ) => ∫ (x : Ω), f x(μs i)) F (nhds (∫ (x : Ω), f xμ))

                A characterization of weak convergence in terms of integrals of bounded continuous real-valued functions.

                noncomputable def MeasureTheory.FiniteMeasure.map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) (f : ΩΩ') :

                The push-forward of a finite measure by a function between measurable spaces.

                Equations
                Instances For
                  @[simp]
                  theorem MeasureTheory.FiniteMeasure.toMeasure_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) (f : ΩΩ') :
                  (ν.map f) = MeasureTheory.Measure.map f ν
                  theorem MeasureTheory.FiniteMeasure.map_apply' {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) {f : ΩΩ'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) :
                  (ν.map f) A = ν (f ⁻¹' A)

                  Note that this is an equality of elements of ℝ≥0∞. See also MeasureTheory.FiniteMeasure.map_apply for the corresponding equality as elements of ℝ≥0.

                  theorem MeasureTheory.FiniteMeasure.map_apply_of_aemeasurable {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) {f : ΩΩ'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) :
                  (fun (s : Set Ω') => ((ν.map f) s).toNNReal) A = (fun (s : Set Ω) => (ν s).toNNReal) (f ⁻¹' A)
                  theorem MeasureTheory.FiniteMeasure.map_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.FiniteMeasure Ω) {f : ΩΩ'} (f_mble : Measurable f) {A : Set Ω'} (A_mble : MeasurableSet A) :
                  (fun (s : Set Ω') => ((ν.map f) s).toNNReal) A = (fun (s : Set Ω) => (ν s).toNNReal) (f ⁻¹' A)
                  @[simp]
                  theorem MeasureTheory.FiniteMeasure.map_add {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {f : ΩΩ'} (f_mble : Measurable f) (ν₁ : MeasureTheory.FiniteMeasure Ω) (ν₂ : MeasureTheory.FiniteMeasure Ω) :
                  (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f
                  @[simp]
                  theorem MeasureTheory.FiniteMeasure.map_smul {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {f : ΩΩ'} (c : NNReal) (ν : MeasureTheory.FiniteMeasure Ω) :
                  (c ν).map f = c ν.map f

                  The push-forward of a finite measure by a function between measurable spaces as a linear map.

                  Equations
                  Instances For
                    theorem MeasureTheory.FiniteMeasure.tendsto_map_of_tendsto_of_continuous {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {ι : Type u_3} {L : Filter ι} (νs : ιMeasureTheory.FiniteMeasure Ω) (ν : MeasureTheory.FiniteMeasure Ω) (lim : Filter.Tendsto νs L (nhds ν)) {f : ΩΩ'} (f_cont : Continuous f) :
                    Filter.Tendsto (fun (i : ι) => (νs i).map f) L (nhds (ν.map f))

                    If f : X → Y is continuous and Y is equipped with the Borel sigma algebra, then (weak) convergence of FiniteMeasures on X implies (weak) convergence of the push-forwards of these measures by f.

                    theorem MeasureTheory.FiniteMeasure.continuous_map {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace Ω'] [BorelSpace Ω'] {f : ΩΩ'} (f_cont : Continuous f) :
                    Continuous fun (ν : MeasureTheory.FiniteMeasure Ω) => ν.map f

                    If f : X → Y is continuous and Y is equipped with the Borel sigma algebra, then the push-forward of finite measures f* : FiniteMeasure X → FiniteMeasure Y is continuous (in the topologies of weak convergence of measures).

                    The push-forward of a finite measure by a continuous function between Borel spaces as a continuous linear map.

                    Equations
                    Instances For