Documentation

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Probability measures #

This file defines the type of probability 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 probability measures is equipped with the topology of convergence in distribution (weak convergence of measures). The topology of convergence in distribution is the coarsest topology w.r.t. which for every bounded continuous ℝ≥0-valued random variable X, the expected value of X depends continuously on the choice of probability measure. This is a special case of the topology of weak convergence of finite measures.

Main definitions #

The main definitions are

Main results #

TODO:

Implementation notes #

The topology of convergence in distribution on MeasureTheory.ProbabilityMeasure Ω is inherited weak convergence of finite measures via the mapping MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

Like MeasureTheory.FiniteMeasure Ω, the implementation of MeasureTheory.ProbabilityMeasure Ω 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 Ω.

References #

Tags #

convergence in distribution, convergence in law, weak convergence of measures, probability measure

Probability measures #

In this section we define the type of probability measures on a measurable space Ω, denoted by MeasureTheory.ProbabilityMeasure Ω.

If Ω is moreover a topological space and the sigma algebra on Ω is finer than the Borel sigma algebra (i.e. [OpensMeasurableSpace Ω]), then MeasureTheory.ProbabilityMeasure Ω is equipped with the topology of weak convergence of measures. Since every probability measure is a finite measure, this is implemented as the induced topology from the mapping MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

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

Equations
Instances For
    Equations

    Coercion from MeasureTheory.ProbabilityMeasure Ω to MeasureTheory.Measure Ω.

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

      A probability measure can be interpreted as a measure.

      Equations
      • MeasureTheory.ProbabilityMeasure.instCoeMeasure = { coe := MeasureTheory.ProbabilityMeasure.toMeasure }
      theorem MeasureTheory.ProbabilityMeasure.toMeasure_injective {Ω : Type u_1} [MeasurableSpace Ω] :
      Function.Injective MeasureTheory.ProbabilityMeasure.toMeasure
      Equations
      theorem MeasureTheory.ProbabilityMeasure.coeFn_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) :
      μ = fun (s : Set Ω) => (μ s).toNNReal
      theorem MeasureTheory.ProbabilityMeasure.coeFn_mk {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ) :
      μ, = fun (s : Set Ω) => (μ s).toNNReal
      @[simp]
      theorem MeasureTheory.ProbabilityMeasure.mk_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ) (s : Set Ω) :
      μ, s = (μ s).toNNReal

      A probability measure can be interpreted as a finite measure.

      Equations
      • μ.toFiniteMeasure = μ,
      Instances For
        @[simp]
        @[simp]
        theorem MeasureTheory.ProbabilityMeasure.apply_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) {s₁ : Set Ω} {s₂ : Set Ω} (h : s₁ s₂) :
        μ s₁ μ s₂

        The topology of weak convergence on MeasureTheory.ProbabilityMeasure Ω. This is inherited (induced) from the topology of weak convergence of finite measures via the inclusion MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

        Equations
        • MeasureTheory.ProbabilityMeasure.instTopologicalSpace = TopologicalSpace.induced MeasureTheory.ProbabilityMeasure.toFiniteMeasure inferInstance
        theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] :
        Continuous MeasureTheory.ProbabilityMeasure.toFiniteMeasure

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

        Equations
        • MeasureTheory.ProbabilityMeasure.toWeakDualBCNN = MeasureTheory.FiniteMeasure.toWeakDualBCNN MeasureTheory.ProbabilityMeasure.toFiniteMeasure
        Instances For
          @[simp]
          theorem MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) :
          μ.toWeakDualBCNN = μ.toFiniteMeasure.testAgainstNN
          @[simp]
          theorem MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (f : BoundedContinuousFunction Ω NNReal) :
          μ.toWeakDualBCNN f = (∫⁻ (ω : Ω), (f ω)μ).toNNReal
          theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_embedding (Ω : Type u_2) [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] :
          Embedding MeasureTheory.ProbabilityMeasure.toFiniteMeasure
          theorem MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {δ : Type u_2} (F : Filter δ) {μs : δMeasureTheory.ProbabilityMeasure Ω} {μ₀ : MeasureTheory.ProbabilityMeasure Ω} :
          Filter.Tendsto μs F (nhds μ₀) Filter.Tendsto (MeasureTheory.ProbabilityMeasure.toFiniteMeasure μs) F (nhds μ₀.toFiniteMeasure)
          theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.ProbabilityMeasure Ω} {μ : MeasureTheory.ProbabilityMeasure Ω} :
          Filter.Tendsto μs F (nhds μ) ∀ (f : BoundedContinuousFunction Ω NNReal), Filter.Tendsto (fun (i : γ) => ∫⁻ (ω : Ω), (f ω)(μs i)) F (nhds (∫⁻ (ω : Ω), (f ω)μ))

          A characterization of weak convergence of probability measures by the condition that the integrals of every continuous bounded nonnegative function converge to the integral of the function against the limit measure.

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

          The characterization of weak convergence of probability measures by the usual (defining) condition that the integrals of every continuous bounded function converge to the integral of the function against the limit measure.

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

          Equations
          • =

          Normalization of finite measures to probability measures #

          This section is about normalizing finite measures to probability measures.

          The weak convergence of finite measures to nonzero limit measures is characterized by the convergence of the total mass and the convergence of the normalized probability measures.

          Normalize a finite measure so that it becomes a probability measure, i.e., divide by the total mass.

          Equations
          Instances For
            @[simp]
            theorem MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (s : Set Ω) :
            μ s = μ.mass * μ.normalize s
            theorem MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) :
            μ = μ.mass μ.normalize.toFiniteMeasure
            theorem MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (nonzero : μ 0) (s : Set Ω) :
            μ.normalize s = μ.mass⁻¹ * μ s
            theorem MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (nonzero : μ 0) :
            μ.normalize.toFiniteMeasure = μ.mass⁻¹ μ
            theorem MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) (nonzero : μ 0) :
            μ.normalize = μ.mass⁻¹ μ
            @[simp]
            theorem ProbabilityMeasure.toFiniteMeasure_normalize_eq_self {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.ProbabilityMeasure Ω) :
            μ.toFiniteMeasure.normalize = μ
            theorem MeasureTheory.FiniteMeasure.average_eq_integral_normalize {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (nonzero : μ 0) (f : ΩE) :
            MeasureTheory.average (μ) f = ∫ (ω : Ω), f ωμ.normalize

            Averaging with respect to a finite measure is the same as integrating against MeasureTheory.FiniteMeasure.normalize.

            theorem MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) [TopologicalSpace Ω] (f : BoundedContinuousFunction Ω NNReal) :
            μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f
            theorem MeasureTheory.FiniteMeasure.normalize_testAgainstNN {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) [TopologicalSpace Ω] (nonzero : μ 0) (f : BoundedContinuousFunction Ω NNReal) :
            μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f
            theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize)) (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass)) (f : BoundedContinuousFunction Ω NNReal) :
            Filter.Tendsto (fun (i : γ) => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))
            theorem MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto μs F (nhds μ)) (nonzero : μ 0) (f : BoundedContinuousFunction Ω NNReal) :
            Filter.Tendsto (fun (i : γ) => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (nhds (μ.normalize.toFiniteMeasure.testAgainstNN f))
            theorem MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize)) (mass_lim : Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass)) :
            Filter.Tendsto μs F (nhds μ)

            If the normalized versions of finite measures converge weakly and their total masses also converge, then the finite measures themselves converge weakly.

            theorem MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto μs F (nhds μ)) (nonzero : μ 0) :
            Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize)

            If finite measures themselves converge weakly to a nonzero limit measure, then their normalized versions also converge weakly.

            theorem MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto {Ω : Type u_1} [Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ} {μs : γMeasureTheory.FiniteMeasure Ω} (nonzero : μ 0) :
            Filter.Tendsto (fun (i : γ) => (μs i).normalize) F (nhds μ.normalize) Filter.Tendsto (fun (i : γ) => (μs i).mass) F (nhds μ.mass) Filter.Tendsto μs F (nhds μ)

            The weak convergence of finite measures to a nonzero limit can be characterized by the weak convergence of both their normalized versions (probability measures) and their total masses.

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

            The push-forward of a probability measure by a measurable function.

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

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

              theorem MeasureTheory.ProbabilityMeasure.map_apply_of_aemeasurable {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : ΩΩ'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) :
              (ν.map f_aemble) A = ν (f ⁻¹' A)
              theorem MeasureTheory.ProbabilityMeasure.map_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] (ν : MeasureTheory.ProbabilityMeasure Ω) {f : ΩΩ'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) :
              (ν.map f_aemble) A = ν (f ⁻¹' A)
              theorem MeasureTheory.ProbabilityMeasure.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.ProbabilityMeasure Ω) (ν : MeasureTheory.ProbabilityMeasure Ω) (lim : Filter.Tendsto νs L (nhds ν)) {f : ΩΩ'} (f_cont : Continuous f) :
              Filter.Tendsto (fun (i : ι) => (νs i).map ) L (nhds (ν.map ))

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

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

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