Finite evaluation laws determine a measure on ProbabilityMeasure α

A finite measure on ProbabilityMeasure α is determined by the laws of its finite evaluation families P ↦ (P (B 0), …, P (B (n-1))).

Main results

• Measure.ext_of_forall_map_probabilityMeasure_eval_eq — two measures on ProbabilityMeasure α agree as soon as every finite family of measurable sets induces the same pushforward law.
• IsZeroOneMeasure.exists_eq_dirac_probabilityMeasure — a nonzero zero-one law on ProbabilityMeasure α is a Dirac measure when the measurable space on α is countably generated.
• measurable_probabilityMeasure_apply_real, measurable_probabilityMeasure_toMeasure_apply, measurable_probabilityMeasure_toMeasure_apply_toReal and measurable_probabilityMeasure_eval_family — measurability of a fixed-set evaluation, in the ℝ≥0-coercion, ℝ≥0∞ and .toReal spellings, singly and as a family. They are public because a consumer of the extensionality theorem needs them to discharge the measurability hypotheses of results like Measure.map_apply and integral_map when working with those pushforwards.

Implementation

The Giry σ-algebra on Measure α is defined as an iSup of comaps of the individual evaluations μ ↦ μ s, so it is already the pullback of a product σ-algebra along the all-evaluations map; comap_iSup is all that is needed to see this. Transporting along Subtype.val and replacing the ℝ≥0∞-valued evaluations by their real-valued counterparts — each is measurable in terms of the other, so the two pullbacks coincide — puts the σ-algebra on ProbabilityMeasure α in the same form.

Once the σ-algebra is a pullback, equality of the two measures reduces to equality of their pushforwards under the all-evaluations map. Those pushforwards live on a product space, and the hypothesis says exactly that their restrictions to every finite set of coordinates agree — so both are projective limits of the same family and MeasureTheory.IsProjectiveLimit.unique concludes. No π-system is built here: that lemma already performs the measurableCylinders argument. The only work is reindexing a Finset of coordinates by Fin via Finset.equivFin.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_apply_real {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) : Measurable fun (P : MeasureTheory.ProbabilityMeasure α) => ↑(P s)

Evaluating a probability measure at a fixed measurable set is measurable, as a real-valued function of the measure.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_toMeasure_apply {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) : Measurable fun (P : MeasureTheory.ProbabilityMeasure α) => ↑P s

Evaluating a probability measure at a fixed measurable set is measurable, as an ℝ≥0∞-valued function of the underlying measure.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_toMeasure_apply_toReal {α : Type u_1} [MeasurableSpace α] {s : Set α} (hs : MeasurableSet s) : Measurable fun (P : MeasureTheory.ProbabilityMeasure α) => (↑P s).toReal

Evaluating a probability measure at a fixed measurable set is measurable, in the ((P : Measure α) s).toReal form.

Stated separately from measurable_probabilityMeasure_apply_real so that consumers whose goal is phrased through Measure.toReal need not cross the coercion themselves.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_eval_family {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} (B : ι → Set α) (hB : ∀ (i : ι), MeasurableSet (B i)) : Measurable fun (P : MeasureTheory.ProbabilityMeasure α) (i : ι) => ↑(P (B i))

A family of evaluations is measurable into the product.

theorem TauCeti.MeasureTheory.Measure.ext_of_forall_map_probabilityMeasure_eval_eq {α : Type u_1} [MeasurableSpace α] {π₁ π₂ : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)} [MeasureTheory.IsFiniteMeasure π₁] (h : ∀ (n : ℕ) (B : Fin n → Set α), (∀ (i : Fin n), MeasurableSet (B i)) → MeasureTheory.Measure.map (fun (P : MeasureTheory.ProbabilityMeasure α) (i : Fin n) => ↑(P (B i))) π₁ = MeasureTheory.Measure.map (fun (P : MeasureTheory.ProbabilityMeasure α) (i : Fin n) => ↑(P (B i))) π₂) : π₁ = π₂

Finite evaluation laws determine the measure. Two measures on ProbabilityMeasure α are equal as soon as, for every finite family B of measurable subsets of α, the pushforwards under the evaluation map P ↦ (P (B 0), …, P (B (n-1))) agree.

Only π₁ need be assumed finite: the n = 0 instance of the hypothesis equates the total masses.

theorem TauCeti.MeasureTheory.IsZeroOneMeasure.exists_eq_dirac_probabilityMeasure {α : Type u_1} [MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] {π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)} [NeZero π] [MeasureTheory.IsZeroOneMeasure π] : ∃ (P : MeasureTheory.ProbabilityMeasure α), π = MeasureTheory.Measure.dirac P

A nonzero zero-one law on ProbabilityMeasure α is a Dirac measure when the measurable space on α is countably generated.

Mathlib's IsZeroOneMeasure.exists_eq_dirac applies to a standard Borel carrier. The Giry measurable space on ProbabilityMeasure α is not currently equipped with such an instance, so we instead embed it measurably and injectively into a countable product of ℝ≥0∞: evaluate a probability measure on the countable set algebra generated by countableGeneratingSet α. The pushforward is a zero-one probability measure on a standard Borel product, hence Dirac; injectivity of the evaluation map then pulls that conclusion back.