Infinite product of probability measures

This file provides a definition for the product measure of an arbitrary family of probability measures. Given μ : (i : ι) → Measure (X i) such that each μ i is a probability measure, Measure.infinitePi μ is the only probability measure ν over Π i, X i such that ν (Set.pi s t) = ∏ i ∈ s, μ i (t i), with s : Finset ι and such that ∀ i ∈ s, MeasurableSet (t i) (see eq_infinitePi and infinitePi_pi). We also provide a few results regarding integration against this measure.

Main definition

• Measure.infinitePi μ: The product measure of the family of probability measures μ.

Main statements

• eq_infinitePi: Any measure which gives to a finite product of sets the mass which is the product of their measures is the product measure.
• infinitePi_pi: the product measure gives to finite products of sets a mass which is the product of their masses.
• infinitePi_cylinder: infinitePi μ (cylinder s S) = Measure.pi (fun i : s ↦ μ i) S

Implementation notes

To construct the product measure we first use the kernel traj obtained via the Ionescu-Tulcea theorem to construct the measure over a product indexed by ℕ, which is infinitePiNat. This is an implementation detail and should not be used directly. Then we construct the product measure over an arbitrary type by extending piContent μ thanks to Carathéodory's theorem. The key lemma to do so is piContent_tendsto_zero, which states that piContent μ (A n) tends to zero if A is a non increasing sequence of sets satisfying ⋂ n, A n = ∅. We prove this lemma by reducing to the case of an at most countable product, in which case piContent μ is known to be a true measure (see piContent_eq_measure_pi and piContent_eq_infinitePiNat).

Tags

infinite product measure

theorem MeasureTheory.isProjectiveMeasureFamily_pi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] : IsProjectiveMeasureFamily fun (I : Finset ι) => Measure.pi fun (i : { x : ι // x ∈ I }) => μ ↑i

Consider a family of probability measures. You can take their products for any finite subfamily. This gives a projective family of measures.

noncomputable def MeasureTheory.piContent {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] : AddContent (measurableCylinders X)

Consider a family of probability measures. You can take their products for any finite subfamily. This gives an additive content on the measurable cylinders.

Equations

• MeasureTheory.piContent μ = MeasureTheory.projectiveFamilyContent ⋯

theorem MeasureTheory.piContent_cylinder {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {I : Finset ι} {S : Set ((i : { x : ι // x ∈ I }) → X ↑i)} (hS : MeasurableSet S) : (piContent μ) (cylinder I S) = (Measure.pi fun (i : { x : ι // x ∈ I }) => μ ↑i) S

theorem MeasureTheory.piContent_eq_measure_pi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] [Fintype ι] {s : Set ((i : ι) → X i)} (hs : MeasurableSet s) : (piContent μ) s = (Measure.pi μ) s

Product of measures indexed by ℕ

noncomputable def MeasureTheory.Measure.infinitePiNat {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] : Measure ((n : ℕ) → X n)

Infinite product measure indexed by ℕ. This is an auxiliary construction, you should use the generic product measure Measure.infinitePi.

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePiNat {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] : IsProbabilityMeasure (infinitePiNat μ)

theorem MeasureTheory.Measure.pi_prod_map_IocProdIoc {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) : map (IocProdIoc a b c) ((Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc a b }) => μ ↑i).prod (Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc b c }) => μ ↑i)) = Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc a c }) => μ ↑i

Let μ : (i : Ioc a c) → Measure (X i) be a family of measures. Up to an equivalence, (⨂ i : Ioc a b, μ i) ⊗ (⨂ i : Ioc b c, μ i) = ⨂ i : Ioc a c, μ i, where ⊗ denotes the product of measures.

theorem MeasureTheory.Measure.pi_prod_map_IicProdIoc {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] {a b : ℕ} : map (IicProdIoc a b) ((Measure.pi fun (i : { x : ℕ // x ∈ Finset.Iic a }) => μ ↑i).prod (Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc a b }) => μ ↑i)) = Measure.pi fun (i : { x : ℕ // x ∈ Finset.Iic b }) => μ ↑i

Let μ : (i : Iic b) → Measure (X i) be a family of measures. Up to an equivalence, (⨂ i : Iic a, μ i) ⊗ (⨂ i : Ioc a b, μ i) = ⨂ i : Iic b, μ i, where ⊗ denotes the product of measures.

theorem MeasureTheory.Measure.map_piSingleton {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [∀ (n : ℕ), SigmaFinite (μ n)] (n : ℕ) : map (⇑(MeasurableEquiv.piSingleton n)) (μ (n + 1)) = Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc n (n + 1) }) => μ ↑i

Let μ (i + 1) : Measure (X (i + 1)) be a measure. Up to an equivalence, μ i = ⨂ j : Ioc i (i + 1), μ i, where ⊗ denotes the product of measures.

theorem MeasureTheory.partialTraj_const_restrict₂ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] {a b : ℕ} : (ProbabilityTheory.Kernel.partialTraj (fun (n : ℕ) => ProbabilityTheory.Kernel.const ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (μ (n + 1))) a b).map (Finset.restrict₂ ⋯) = ProbabilityTheory.Kernel.const ((i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) (Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc a b }) => μ ↑i)

partialTraj κ a b is a kernel which up to an equivalence is equal to Kernel.id ×ₖ (κ a ⊗ₖ ... ⊗ₖ κ (b - 1)). This lemma therefore states that if the kernels κ are constant then their composition-product is the product measure.

theorem MeasureTheory.partialTraj_const {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] {a b : ℕ} : ProbabilityTheory.Kernel.partialTraj (fun (n : ℕ) => ProbabilityTheory.Kernel.const ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (μ (n + 1))) a b = (ProbabilityTheory.Kernel.id.prod (ProbabilityTheory.Kernel.const ((i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) (Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc a b }) => μ ↑i))).map (IicProdIoc a b)

partialTraj κ a b is a kernel which up to an equivalence is equal to Kernel.id ×ₖ (κ a ⊗ₖ ... ⊗ₖ κ (b - 1)). This lemma therefore states that if the kernel κ i is constant equal to μ i for all i, then up to an equivalence partialTraj κ a b = Kernel.id ×ₖ Kernel.const (⨂ μ i).

theorem MeasureTheory.Measure.isProjectiveLimit_infinitePiNat {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] : IsProjectiveLimit (infinitePiNat μ) fun (I : Finset ℕ) => Measure.pi fun (i : { x : ℕ // x ∈ I }) => μ ↑i

theorem MeasureTheory.Measure.infinitePiNat_map_restrict {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] (I : Finset ℕ) : map I.restrict (infinitePiNat μ) = Measure.pi fun (i : { x : ℕ // x ∈ I }) => μ ↑i

Restricting the product measure to a product indexed by a finset yields the usual product measure.

theorem MeasureTheory.Measure.piContent_eq_infinitePiNat {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → Measure (X n)) [hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)] {A : Set ((n : ℕ) → X n)} (hA : A ∈ measurableCylinders X) : (piContent μ) A = (infinitePiNat μ) A

Product of infinitely many probability measures

theorem MeasureTheory.Measure.infinitePiNat_map_piCongrLeft {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] (e : ℕ ≃ ι) {s : Set ((i : ι) → X i)} (hs : s ∈ measurableCylinders X) : (map (⇑(MeasurableEquiv.piCongrLeft X e)) (infinitePiNat fun (n : ℕ) => μ (e n))) s = (piContent μ) s

If we push the product measure forward by a reindexing equivalence, we get a product measure on the reindexed product in the sense that it coincides with piContent μ over measurable cylinders. See infinitePi_map_piCongrLeft for a general version.

theorem MeasureTheory.piContent_tendsto_zero {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {A : ℕ → Set ((i : ι) → X i)} (A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X) (A_anti : Antitone A) (A_inter : ⋂ (n : ℕ), A n = ∅) : Filter.Tendsto (fun (n : ℕ) => (piContent μ) (A n)) Filter.atTop (nhds 0)

This is the key theorem to build the product of an arbitrary family of probability measures: the piContent of a decreasing sequence of cylinders with empty intersection converges to 0.

This implies the σ-additivity of piContent (see addContent_iUnion_eq_sum_of_tendsto_zero), which allows to extend it to the σ-algebra by Carathéodory's theorem.

theorem MeasureTheory.isSigmaSubadditive_piContent {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] : (piContent μ).IsSigmaSubadditive

The projectiveFamilyContent associated to a family of probability measures is σ-subadditive.

noncomputable def MeasureTheory.Measure.infinitePi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] : Measure ((i : ι) → X i)

The product measure of an arbitrary family of probability measures. It is defined as the unique extension of the function which gives to cylinders the measure given by the associated product measure.

Equations

• MeasureTheory.Measure.infinitePi μ = (MeasureTheory.piContent μ).measure ⋯ ⋯ ⋯

theorem MeasureTheory.Measure.isProjectiveLimit_infinitePi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] : IsProjectiveLimit (infinitePi μ) fun (I : Finset ι) => Measure.pi fun (i : { x : ι // x ∈ I }) => μ ↑i

The product measure is the projective limit of the partial product measures. This ensures uniqueness and expresses the value of the product measure applied to cylinders.

theorem MeasureTheory.Measure.infinitePi_map_restrict {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {I : Finset ι} : map I.restrict (infinitePi μ) = Measure.pi fun (i : { x : ι // x ∈ I }) => μ ↑i

Restricting the product measure to a product indexed by a finset yields the usual product measure.

instance MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] : IsProbabilityMeasure (infinitePi μ)

theorem MeasureTheory.Measure.eq_infinitePi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {ν : Measure ((i : ι) → X i)} (hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ i ∈ s, MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)) : ν = infinitePi μ

To prove that a measure is equal to the product measure it is enough to check that it it gives the same measure to measurable boxes.

theorem MeasureTheory.Measure.infinitePi_pi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Finset ι} {t : (i : ι) → Set (X i)} (mt : ∀ i ∈ s, MeasurableSet (t i)) : (infinitePi μ) ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)

theorem MeasureTheory.Measure.infinitePi_map_piCongrLeft {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {α : Type u_3} (e : α ≃ ι) : map (⇑(MeasurableEquiv.piCongrLeft X e)) (infinitePi fun (i : α) => μ (e i)) = infinitePi μ

If we push the product measure forward by a reindexing equivalence, we get a product measure on the reindexed product.

theorem MeasureTheory.Measure.infinitePi_eq_pi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] [Fintype ι] : infinitePi μ = Measure.pi μ

theorem MeasureTheory.Measure.infinitePi_cylinder {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Finset ι} {S : Set ((i : { x : ι // x ∈ s }) → X ↑i)} (mS : MeasurableSet S) : (infinitePi μ) (cylinder s S) = (Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i) S

theorem MeasureTheory.integral_restrict_infinitePi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι} {f : ((i : { x : ι // x ∈ s }) → X ↑i) → E} (hf : AEStronglyMeasurable f (Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i)) : ∫ (y : (i : ι) → X i), f (s.restrict y) ∂Measure.infinitePi μ = ∫ (y : (i : { x : ι // x ∈ s }) → X ↑i), f y ∂Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i

theorem MeasureTheory.lintegral_restrict_infinitePi {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Finset ι} {f : ((i : { x : ι // x ∈ s }) → X ↑i) → ENNReal} (hf : Measurable f) : ∫⁻ (y : (i : ι) → X i), f (s.restrict y) ∂Measure.infinitePi μ = ∫⁻ (y : (i : { x : ι // x ∈ s }) → X ↑i), f y ∂Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i

theorem MeasureTheory.integral_infinitePi_of_piFinset {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι} {f : ((i : ι) → X i) → E} (mf : StronglyMeasurable f) (x : (i : ι) → X i) : ∫ (y : (i : ι) → X i), f y ∂Measure.infinitePi μ = ∫ (y : (i : { x : ι // x ∈ s }) → X ↑i), f (Function.updateFinset x s y) ∂Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i

theorem MeasureTheory.lintegral_infinitePi_of_piFinset {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] [DecidableEq ι] {s : Finset ι} {f : ((i : ι) → X i) → ENNReal} (mf : Measurable f) (x : (i : ι) → X i) : ∫⁻ (y : (i : ι) → X i), f y ∂Measure.infinitePi μ = (∫⋯∫⁻_s, f ∂μ) x