Product of infinitely-many probability measures

Stream: Is there code for X?

[Oliver Nash]

I'd like to be able to take the product of infinitely-many probability measures. Am I right in thinking we do not yet have this construction?

[Oliver Nash]

For example, the following works:

import Mathlib

open MeasureTheory

variable {ι : Type*} {α : ι → Type*}
  [∀ i, MeasurableSpace (α i)]
  (μ : (i : ι) → Measure (α i))
  [∀ i, IsProbabilityMeasure (μ i)]

variable [Fintype ι] -- This is what I would like to drop

noncomputable example : Measure ((i : ι) → α i) := Measure.pi μ

#synth IsProbabilityMeasure (Measure.pi μ)

but not if I drop the [Fintype ι].

[Rémy Degenne]

Not in Mathlib yet. It's in https://github.com/sgouezel/kolmogorov_extension4 (work of @Etienne Marion ), which depends on https://github.com/RemyDegenne/kolmogorov_extension4/ , and both need to make their way to Mathlib.

[Oliver Nash]

Oh excellent, great to know they're en route: thanks!