Empirical measures of sequences

This file defines the empirical probability measure of a nonempty finite population (empiricalMeasureOfFintype) and, as its κ := Fin (n + 1) case, of the first n + 1 terms of a sequence (empiricalMeasure), together with their evaluation, integration, and measurability API. The successor indexing is what supplies the Nonempty instance for the sequence form, so it needs no side condition, and it matches the shape used in limit theorems.

There is one construction, not two: the sequence form is defined as the specialization, so the two can never drift apart.

It also provides empiricalMeasureOfFintype for a population indexed by an arbitrary nonempty finite type. This is the finite-population form used by quantitative sampling arguments.

The construction is a uniform finite sum of Dirac measures. It is the process-level prerequisite for the empirical-measure form of de Finetti's theorem in the Exchangeability roadmap.

noncomputable def TauCeti.Probability.empiricalMeasureOfFintype {α : Type u_1} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] (x : κ → α) : MeasureTheory.ProbabilityMeasure α

The empirical probability measure of a nonempty finite population x : κ → α.

Unlike empiricalMeasure, its population can have an arbitrary nonempty finite index type rather than a natural-number prefix.

Equations

• TauCeti.Probability.empiricalMeasureOfFintype x = ⟨∑ i : κ, (↑(Fintype.card κ))⁻¹ • MeasureTheory.Measure.dirac (x i), ⋯⟩

@[simp]

theorem TauCeti.Probability.empiricalMeasureOfFintype_toMeasure {α : Type u_1} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] (x : κ → α) : ↑(empiricalMeasureOfFintype x) = ∑ i : κ, (↑(Fintype.card κ))⁻¹ • MeasureTheory.Measure.dirac (x i)

The measure underlying a finite empirical population is the normalized sum of its Dirac masses.

theorem TauCeti.Probability.empiricalMeasureOfFintype_apply {α : Type u_1} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] {x : κ → α} {s : Set α} (hs : MeasurableSet s) : ↑(empiricalMeasureOfFintype x) s = (↑(Fintype.card κ))⁻¹ * ∑ i : κ, s.indicator 1 (x i)

Evaluation of a finite empirical population on a measurable set is its empirical frequency.

theorem TauCeti.Probability.empiricalMeasureOfFintype_eq_map_uniformOn {α : Type u_1} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (x : κ → α) : ↑(empiricalMeasureOfFintype x) = MeasureTheory.Measure.map x (ProbabilityTheory.uniformOn Set.univ)

On a discrete finite index type, a finite empirical population is the pushforward of the uniform law on its indices.

theorem TauCeti.Probability.integral_empiricalMeasureOfFintype {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {x : κ → α} {f : α → E} (hf : MeasureTheory.StronglyMeasurable f) : ∫ (y : α), f y ∂↑(empiricalMeasureOfFintype x) = (↑(Fintype.card κ))⁻¹ • ∑ i : κ, f (x i)

Integrating against a finite empirical population is averaging over its values.

theorem TauCeti.Probability.lintegral_empiricalMeasureOfFintype {α : Type u_1} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] {x : κ → α} {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (y : α), f y ∂↑(empiricalMeasureOfFintype x) = (↑(Fintype.card κ))⁻¹ * ∑ i : κ, f (x i)

The Lebesgue integral against a finite empirical population is the average of the values.

theorem TauCeti.Probability.measurable_empiricalMeasureOfFintype {α : Type u_1} [MeasurableSpace α] {κ : Type u_4} [Fintype κ] [Nonempty κ] : Measurable empiricalMeasureOfFintype

Finite empirical distributions depend measurably on the population.

noncomputable def TauCeti.Probability.empiricalMeasure {α : Type u_1} [MeasurableSpace α] (x : ℕ → α) (n : ℕ) : MeasureTheory.ProbabilityMeasure α

The empirical probability measure of the first n + 1 terms of a sequence.

This is the κ := Fin (n + 1) case of empiricalMeasureOfFintype; the successor indexing is what supplies the Nonempty instance, so no side condition is needed.

Equations

• TauCeti.Probability.empiricalMeasure x n = TauCeti.Probability.empiricalMeasureOfFintype fun (i : Fin (n + 1)) => x ↑i

@[simp]

theorem TauCeti.Probability.empiricalMeasure_toMeasure {α : Type u_1} [MeasurableSpace α] (x : ℕ → α) (n : ℕ) : ↑(empiricalMeasure x n) = ∑ i ∈ Finset.range (n + 1), (↑(n + 1))⁻¹ • MeasureTheory.Measure.dirac (x i)

The measure underlying an empirical measure is the uniform finite sum of Dirac measures.

theorem TauCeti.Probability.empiricalMeasure_apply {α : Type u_1} [MeasurableSpace α] {x : ℕ → α} {n : ℕ} {s : Set α} (hs : MeasurableSet s) : ↑(empiricalMeasure x n) s = (↑(n + 1))⁻¹ * ∑ i ∈ Finset.range (n + 1), s.indicator 1 (x i)

Evaluation of an empirical measure on a measurable set is its empirical frequency.

theorem TauCeti.Probability.empiricalMeasure_apply_toReal {α : Type u_1} [MeasurableSpace α] {x : ℕ → α} {n : ℕ} {s : Set α} (hs : MeasurableSet s) : (↑(empiricalMeasure x n) s).toReal = (↑(n + 1))⁻¹ * ∑ i ∈ Finset.range (n + 1), s.indicator 1 (x i)

The real-valued form of empiricalMeasure_apply.

theorem TauCeti.Probability.empiricalMeasure_process_apply_toReal {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] {X : ℕ → Ω → α} {ω : Ω} {n : ℕ} {s : Set α} (hs : MeasurableSet s) : (↑(empiricalMeasure (fun (i : ℕ) => X i ω) n) s).toReal = (↑(n + 1))⁻¹ * ∑ i ∈ Finset.range (n + 1), (X i ⁻¹' s).indicator 1 ω

Evaluation of a path's empirical measure, written as indicators on the sample space.

theorem TauCeti.Probability.integral_empiricalMeasure {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {x : ℕ → α} {n : ℕ} {f : α → E} (hf : MeasureTheory.StronglyMeasurable f) : ∫ (y : α), f y ∂↑(empiricalMeasure x n) = (↑(n + 1))⁻¹ • ∑ i ∈ Finset.range (n + 1), f (x i)

Integrating against an empirical measure is averaging over the sampled values.

theorem TauCeti.Probability.lintegral_empiricalMeasure {α : Type u_1} [MeasurableSpace α] {x : ℕ → α} {n : ℕ} {f : α → ENNReal} (hf : Measurable f) : ∫⁻ (y : α), f y ∂↑(empiricalMeasure x n) = (↑(n + 1))⁻¹ * ∑ i ∈ Finset.range (n + 1), f (x i)

The Lebesgue integral against an empirical measure is the average of the sampled values.

theorem TauCeti.Probability.measurable_empiricalMeasure {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] {X : ℕ → Ω → α} (n : ℕ) (hX : ∀ i ∈ Finset.range (n + 1), Measurable (X i)) : Measurable fun (ω : Ω) => empiricalMeasure (fun (i : ℕ) => X i ω) n

Empirical measures depend measurably on a sequence of measurable observations.