Finite product probability-measure kernels

This file provides the basic theory of the finite product of probability measures over a finite index type, phrased directly over Mathlib's ProbabilityMeasure.pi: measurability of the product kernel, and Measure.bind-evaluation of the mixture it induces.

Measurability:

• measurable_probabilityMeasure_pi — the product combinator ProbabilityMeasure.pi : (Π i, ProbabilityMeasure (α i)) → ProbabilityMeasure (Π i, α i) is measurable.
• measurable_probabilityMeasure_pi_toMeasure — the measure-valued random product ω ↦ (ProbabilityMeasure.pi fun i => ν i ω).toMeasure is measurable, for measurable coordinate kernels ν i.
• aemeasurable_probabilityMeasure_pi_toMeasure — the same map is AEMeasurable from a.e.-measurable coordinate kernels (∀ i, AEMeasurable (ν i) μ); the _of_measurable corollary is the measurable-input form.
• the constant-coordinate (fun _ : Fin m => ν ω) specializations measurable_probabilityMeasure_pi_const_toMeasure and aemeasurable_probabilityMeasure_pi_const_toMeasure.

Bind-evaluation of the mixture μ.bind fun ω => (ProbabilityMeasure.pi fun i => ν i ω).toMeasure:

• bind_probabilityMeasure_pi_apply — evaluation on a measurable set as the integral of the product kernel, from a.e.-measurable coordinate kernels.
• bind_probabilityMeasure_pi_pi — evaluation on a measurable rectangle as the integral of the product of coordinate measures, with Fin m constant-coordinate forms bind_probabilityMeasure_pi_const_apply and bind_probabilityMeasure_pi_const_pi.

This file does not introduce a new product-kernel structure; the lemmas live directly over Mathlib's ProbabilityMeasure.pi. It advances TauCetiRoadmap/Exchangeability, Layer 1 (product kernels, conditional independence, mixtures), and is motivated by the product-kernel layer of cameronfreer/exchangeability (MeasureKernels.lean and the bind_pi_apply of DeFinetti/CommonEnding.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22), implemented using Mathlib's ProbabilityMeasure.pi, Measure.bind_apply, and Giry measurability API; the combinator generalizes Mathlib's binary ProbabilityMeasure.measurable_fun_prod to finite index types.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_pi {ι : Type u_2} [Fintype ι] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] : Measurable MeasureTheory.ProbabilityMeasure.pi

The finite product combinator ProbabilityMeasure.pi is a measurable map (Π i, ProbabilityMeasure (α i)) → ProbabilityMeasure (Π i, α i).

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_pi_toMeasure {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] (ν : (i : ι) → Ω → MeasureTheory.ProbabilityMeasure (α i)) (hν : ∀ (i : ι), Measurable (ν i)) : Measurable fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (i : ι) => ν i ω)

A finite product of measurable probability-measure kernels is a measurable measure-valued map: if each ν i : Ω → ProbabilityMeasure (α i) is measurable, then ω ↦ (ProbabilityMeasure.pi fun i => ν i ω).toMeasure is measurable.

theorem TauCeti.MeasureTheory.aemeasurable_probabilityMeasure_pi_toMeasure {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] {μ : MeasureTheory.Measure Ω} (ν : (i : ι) → Ω → MeasureTheory.ProbabilityMeasure (α i)) (hν : ∀ (i : ι), AEMeasurable (ν i) μ) : AEMeasurable (fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (i : ι) => ν i ω)) μ

A finite product of a.e.-measurable probability-measure kernels is an a.e.-measurable measure-valued map: if each ν i : Ω → ProbabilityMeasure (α i) is AEMeasurable, then so is ω ↦ (ProbabilityMeasure.pi fun i => ν i ω).toMeasure.

theorem TauCeti.MeasureTheory.aemeasurable_probabilityMeasure_pi_toMeasure_of_measurable {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] {μ : MeasureTheory.Measure Ω} (ν : (i : ι) → Ω → MeasureTheory.ProbabilityMeasure (α i)) (hν : ∀ (i : ι), Measurable (ν i)) : AEMeasurable (fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (i : ι) => ν i ω)) μ

Measurable-input corollary of aemeasurable_probabilityMeasure_pi_toMeasure.

theorem TauCeti.MeasureTheory.measurable_probabilityMeasure_pi_const_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_4} [MeasurableSpace α] {m : ℕ} (ν : Ω → MeasureTheory.ProbabilityMeasure α) (hν : Measurable ν) : Measurable fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)

Constant-coordinate specialization of measurable_probabilityMeasure_pi_toMeasure: the random product ω ↦ (ν ω)^{⊗ Fin m} is measurable.

theorem TauCeti.MeasureTheory.aemeasurable_probabilityMeasure_pi_const_toMeasure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {α : Type u_4} [MeasurableSpace α] {m : ℕ} (ν : Ω → MeasureTheory.ProbabilityMeasure α) (hν : AEMeasurable ν μ) : AEMeasurable (fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) μ

Constant-coordinate specialization of aemeasurable_probabilityMeasure_pi_toMeasure: the random product ω ↦ (ν ω)^{⊗ Fin m} is AEMeasurable from an a.e.-measurable directing kernel.

theorem TauCeti.MeasureTheory.bind_probabilityMeasure_pi_apply {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] {μ : MeasureTheory.Measure Ω} (ν : (i : ι) → Ω → MeasureTheory.ProbabilityMeasure (α i)) (hν : ∀ (i : ι), AEMeasurable (ν i) μ) {s : Set ((i : ι) → α i)} (hs : MeasurableSet s) : (μ.bind fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (i : ι) => ν i ω)) s = ∫⁻ (ω : Ω), ↑(MeasureTheory.ProbabilityMeasure.pi fun (i : ι) => ν i ω) s ∂μ

Bind-evaluation. Evaluating the mixture μ.bind fun ω => (ProbabilityMeasure.pi fun i => ν i ω).toMeasure on a measurable set s gives ∫⁻ ω, … s ∂μ, requiring only a.e.-measurability of each coordinate kernel ν i.

theorem TauCeti.MeasureTheory.bind_probabilityMeasure_pi_pi {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] {μ : MeasureTheory.Measure Ω} (ν : (i : ι) → Ω → MeasureTheory.ProbabilityMeasure (α i)) (hν : ∀ (i : ι), AEMeasurable (ν i) μ) (B : (i : ι) → Set (α i)) (hB : ∀ (i : ι), MeasurableSet (B i)) : (μ.bind fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (i : ι) => ν i ω)) (Set.univ.pi B) = ∫⁻ (ω : Ω), ∏ i : ι, ↑(ν i ω) (B i) ∂μ

Bind-evaluation on a rectangle. On a rectangle Set.univ.pi B, the mixture equals ∫⁻ ω, ∏ i, (ν i ω) (B i) ∂μ.

theorem TauCeti.MeasureTheory.bind_probabilityMeasure_pi_const_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {α : Type u_4} [MeasurableSpace α] {m : ℕ} (ν : Ω → MeasureTheory.ProbabilityMeasure α) (hν : AEMeasurable ν μ) {s : Set (Fin m → α)} (hs : MeasurableSet s) : (μ.bind fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) s = ∫⁻ (ω : Ω), ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω) s ∂μ

Constant-coordinate Fin m specialization of bind_probabilityMeasure_pi_apply.

theorem TauCeti.MeasureTheory.bind_probabilityMeasure_pi_const_pi {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {α : Type u_4} [MeasurableSpace α] {m : ℕ} (ν : Ω → MeasureTheory.ProbabilityMeasure α) (hν : AEMeasurable ν μ) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : (μ.bind fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) (Set.univ.pi B) = ∫⁻ (ω : Ω), ∏ i : Fin m, ↑(ν ω) (B i) ∂μ

Constant-coordinate Fin m specialization of bind_probabilityMeasure_pi_pi: the finite-block mixture identity the de Finetti common ending consumes.