Finite measures

When the underlying σ-algebra is countably generated, singletons are measurable in FiniteMeasure α and in ProbabilityMeasure α.

On a finite measurable space, a probability measure is the sum of its singleton masses.

Narrow convergence of finite measures μs i → μ tests against a fixed bounded continuous function. It also passes to integrands fs i converging uniformly to a bounded continuous f: ∫ fs i dμs i → ∫ f dμ. This is what makes t ↦ ∫ u (t, x) dμₜ(x) continuous along a narrowly continuous curve of finite measures when u is bounded continuous and uniformly continuous in time.

Main results

• MeasureTheory.FiniteMeasure.instMeasurableSingletonClass
• MeasureTheory.ProbabilityMeasure.instMeasurableSingletonClass
• MeasureTheory.Measure.sum_singleton_eq_one
• MeasureTheory.Measure.measureReal_finset_eq_zero
• MeasureTheory.FiniteMeasure.tendsto_integral_of_tendstoUniformly: narrow convergence against uniformly convergent RCLike-valued integrands.
• MeasureTheory.FiniteMeasure.tendsto_integral_of_tendstoUniformlyOn_closedBall: the same for measures carried by a closed ball of a proper normed space, against RCLike-valued integrands that are only continuous, and converge uniformly, on the ball.

Implementation

The statement is really about finite measures; the probability-measure form is the subtype corollary. Countable generation is exactly what the proof consumes — StandardBorelSpace α implies it, but is stronger than needed.

A countable generating family need not be closed under intersection, so it is replaced by the set algebra it generates (MeasureTheory.generateSetAlgebra), which is still countable, is a π-system, and generates the same σ-algebra. A finite measure is then pinned down by its values there (ext_of_generate_finite, with Set.univ supplied by the algebra), so {μ} is the countable intersection of the equalizers {ν | ν s = μ s}. Each equalizer is measurable because evaluation at a fixed measurable set is.

instance MeasureTheory.FiniteMeasure.instMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] : MeasurableSingletonClass (FiniteMeasure α)

Singletons are measurable in the space of finite measures, when the σ-algebra on α is countably generated.

instance MeasureTheory.ProbabilityMeasure.instMeasurableSingletonClass {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass (FiniteMeasure α)] : MeasurableSingletonClass (ProbabilityMeasure α)

Singletons are measurable in the space of probability measures whenever they are measurable in the space of finite measures, as they are when the σ-algebra on α is countably generated (FiniteMeasure.instMeasurableSingletonClass).

theorem MeasureTheory.Measure.sum_singleton_eq_one {κ : Type u_2} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (ν : Measure κ) [IsProbabilityMeasure ν] : ∑ k : κ, ν {k} = 1

The singleton masses of a probability measure on a finite measurable space sum to one.

theorem MeasureTheory.Measure.measureReal_finset_eq_zero {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [IsFiniteMeasure μ] [MeasurableSingletonClass α] (s : Finset α) (hzero : ∀ i ∈ s, μ.real {i} = 0) : μ.real ↑s = 0

A finite measure vanishes on a finite set if it vanishes on every point of that set.

theorem MeasureTheory.FiniteMeasure.tendsto_integral_of_tendstoUniformly {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] {ι : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {l : Filter ι} {μs : ι → FiniteMeasure α} {μ : FiniteMeasure α} (hμ : Filter.Tendsto μs l (nhds μ)) {fs : ι → α → 𝕜} {f : BoundedContinuousFunction α 𝕜} (hf : TendstoUniformly fs (⇑f) l) (hfs : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (fs i) ↑(μs i)) : Filter.Tendsto (fun (i : ι) => ∫ (x : α), fs i x ∂↑(μs i)) l (nhds (∫ (x : α), f x ∂↑μ))

Narrow convergence against uniformly convergent integrands. If the finite measures μs i converge narrowly to μ and the RCLike-valued functions fs i, eventually almost everywhere strongly measurable, converge uniformly to a bounded continuous function f, then ∫ fs i dμs i converges to ∫ f dμ.

theorem MeasureTheory.FiniteMeasure.tendsto_integral_of_tendstoUniformlyOn_closedBall {E : Type u_2} {𝕜 : Type u_3} {ι : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] [MeasurableSpace E] [BorelSpace E] [RCLike 𝕜] {l : Filter ι} {μs : ι → FiniteMeasure E} {μ : FiniteMeasure E} (hμ : Filter.Tendsto μs l (nhds μ)) {r : ℝ} (hμsr : ∀ᶠ (i : ι) in l, ↑(μs i) (Metric.closedBall 0 r)ᶜ = 0) (hμr : ↑μ (Metric.closedBall 0 r)ᶜ = 0) {fs : ι → E → 𝕜} {f : E → 𝕜} (hfs : ∀ (i : ι), ContinuousOn (fs i) (Metric.closedBall 0 r)) (hf : ContinuousOn f (Metric.closedBall 0 r)) (hfsf : TendstoUniformlyOn fs f l (Metric.closedBall 0 r)) : Filter.Tendsto (fun (i : ι) => ∫ (x : E), fs i x ∂↑(μs i)) l (nhds (∫ (x : E), f x ∂↑μ))

Narrow convergence of measures carried by a closed ball. Let finite measures μs i on a proper real normed space converge narrowly to μ, all carried by the closed ball closedBall 0 r. If functions fs i, continuous on that ball, converge uniformly on it to a function f continuous on it, then ∫ fs i dμs i converges to ∫ f dμ. Nothing is assumed off the ball: there fs i and f may be unbounded or discontinuous.