Sampling a random population along a random selection

A population is a map x : κ → α, and a selection is an index map k : ι → κ; reading the selected entries gives the sample x ∘ k : ι → α. This file builds the law of that sample when the population and the selection are drawn independently: for a population law ρ : Measure (κ → α) and a selection law σ : Measure (ι → κ), samplePopulation σ ρ is the pushforward of σ.prod ρ along (k, x) ↦ x ∘ k.

Its evaluation and mixture lemmas take the population index countable with measurable singletons, which is what makes the reindexing map measurable for an arbitrary state space α. Finite sampling with and without replacement are the cases where σ is uniform on all index maps, respectively on the injective ones (TauCeti.Probability.sampleWithReplacement, TauCeti.Probability.sampleWithoutReplacement).

Main declarations

• measurable_reindexPopulation — measurability of the joint selection/population evaluation;
• samplePopulation — sample a random population along an independent random selection;
• samplePopulation_apply, samplePopulation_apply_population — its evaluation by conditioning on the selection or on the population;
• samplePopulation_eq_bind, samplePopulation_eq_bind_population — its form as a mixture, over the selection law or over the population law, of the samples with that input fixed.

theorem TauCeti.Probability.measurable_reindexPopulation {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [Countable κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] : Measurable fun (p : (ι → κ) × (κ → α)) (i : ι) => p.2 (p.1 i)

Reindexing a population by a simultaneously supplied selection of its indices is measurable.

The measurable-space hypothesis on the population index is discrete: it lets the variable index be split into countably many measurable fibres.

noncomputable def TauCeti.Probability.samplePopulation {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] (σ : MeasureTheory.Measure (ι → κ)) (ρ : MeasureTheory.Measure (κ → α)) : MeasureTheory.Measure (ι → α)

Sampling a random population along an independent random selection of its indices.

First draw a population x : κ → α with law ρ; independently draw an index map k : ι → κ with law σ; then return the sample i ↦ x (k i). Sampling without replacement (sampleWithoutReplacement) and with replacement (sampleWithReplacement) are the cases where σ is uniform on the injective index maps, respectively on all of them.

The definition is the pushforward Measure.map of σ.prod ρ along (k, x) ↦ x ∘ k. Following Measure.map, when that map is not almost everywhere measurable the result is an arbitrary Dirac mass, or zero if σ.prod ρ = 0. When the population index is countable with measurable singletons the map is measurable for an arbitrary α (measurable_reindexPopulation), and the evaluation and mixture lemmas below assume this.

theorem TauCeti.Probability.samplePopulation_def {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] (σ : MeasureTheory.Measure (ι → κ)) (ρ : MeasureTheory.Measure (κ → α)) : samplePopulation σ ρ = MeasureTheory.Measure.map (fun (p : (ι → κ) × (κ → α)) (i : ι) => p.2 (p.1 i)) (σ.prod ρ)

The defining pushforward form of samplePopulation.

instance TauCeti.Probability.isFiniteMeasure_samplePopulation {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] (σ : MeasureTheory.Measure (ι → κ)) (ρ : MeasureTheory.Measure (κ → α)) [MeasureTheory.IsFiniteMeasure σ] [MeasureTheory.IsFiniteMeasure ρ] : MeasureTheory.IsFiniteMeasure (samplePopulation σ ρ)

Sampling a finite population law along a finite selection law gives a finite law.

instance TauCeti.Probability.isProbabilityMeasure_samplePopulation {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] (σ : MeasureTheory.Measure (ι → κ)) (ρ : MeasureTheory.Measure (κ → α)) [MeasureTheory.IsProbabilityMeasure σ] [MeasureTheory.IsProbabilityMeasure ρ] : MeasureTheory.IsProbabilityMeasure (samplePopulation σ ρ)

Sampling a probability population along a probability selection law is a probability law.

theorem TauCeti.Probability.measurable_readPopulation {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (x : κ → α) : Measurable fun (k : ι → κ) (i : ι) => x (k i)

Reading a fixed population along a varying selection is measurable.

@[simp]

theorem TauCeti.Probability.samplePopulation_dirac {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (σ : MeasureTheory.Measure (ι → κ)) [MeasureTheory.SFinite σ] (x : κ → α) : samplePopulation σ (MeasureTheory.Measure.dirac x) = MeasureTheory.Measure.map (fun (k : ι → κ) (i : ι) => x (k i)) σ

Sampling a deterministic population is the pushforward of the selection law by reading that population at the selected indices.

theorem TauCeti.Probability.samplePopulation_apply {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] {σ : MeasureTheory.Measure (ι → κ)} {ρ : MeasureTheory.Measure (κ → α)} [MeasureTheory.SFinite ρ] {A : Set (ι → α)} (hA : MeasurableSet A) : (samplePopulation σ ρ) A = ∫⁻ (k : ι → κ), ρ ((fun (x : κ → α) (i : ι) => x (k i)) ⁻¹' A) ∂σ

Evaluating a sampled law by conditioning first on the selection: it averages the laws of the selected entries of the population over the selection law.

theorem TauCeti.Probability.samplePopulation_apply_population {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] {σ : MeasureTheory.Measure (ι → κ)} [MeasureTheory.SFinite σ] {ρ : MeasureTheory.Measure (κ → α)} [MeasureTheory.SFinite ρ] {A : Set (ι → α)} (hA : MeasurableSet A) : (samplePopulation σ ρ) A = ∫⁻ (x : κ → α), σ ((fun (k : ι → κ) (i : ι) => x (k i)) ⁻¹' A) ∂ρ

Evaluating a sampled law by conditioning first on the population: it averages, over the population law, the selection probability of the event.

theorem TauCeti.Probability.samplePopulation_eq_bind {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (σ : MeasureTheory.Measure (ι → κ)) (ρ : MeasureTheory.Measure (κ → α)) [MeasureTheory.SFinite ρ] : samplePopulation σ ρ = σ.bind fun (k : ι → κ) => MeasureTheory.Measure.map (fun (x : κ → α) (i : ι) => x (k i)) ρ

Sampling a random population is the mixture, over the selection law, of reading each fixed selection off the random population.

theorem TauCeti.Probability.samplePopulation_eq_bind_population {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} {κ : Type u_3} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (σ : MeasureTheory.Measure (ι → κ)) [MeasureTheory.SFinite σ] (ρ : MeasureTheory.Measure (κ → α)) [MeasureTheory.SFinite ρ] : samplePopulation σ ρ = ρ.bind fun (x : κ → α) => MeasureTheory.Measure.map (fun (k : ι → κ) (i : ι) => x (k i)) σ

Sampling a random population is the mixture, over the population law, of sampling each fixed population along the selection law.