Measure on an infinite product

Stream: mathlib4

[Yury G. Kudryashov]

I have an idea how we can merge two definitions of an indexed product of measures (finite product of σ-finite measures and an infinite product of probability measures) into one. We define the typeclass

-- todo: better name
class MeasureFamily {ι : Type*} {π : ι → Type*} [∀ i, MeasurableSpace (π i)] (μ : ∀ i, Measure (π i)) : Prop where
  sigmaFinite : ∀ i, SigmaFinite (μ i)
  isProbabilityMeasure : ∀ᶠ i in cofinite, IsProbabilityMeasure (μ i)

with an instance assuming [Finite ι] and an instance assuming [∀ i, IsProbabilityMeasure (μ i)].
Then we define one instance assuming [MeasureFamily μ] (we use the current construction for the non-probability finite product part and another construction for the probability part) and prove lemmas about it.

[Yury G. Kudryashov]

What do you think? I do understand that this is a nontrivial refactor.

[Yury G. Kudryashov]

If I try it, then how should I call the new typeclass?

[Kevin Buzzard]

Restricted infinite products are a generalisation of this. Here you have infinitely many spaces of infinite measure but each is equipped with a preferred subspace of measure 1. Each element in the restricted product must be outside the preferred subspace only finitely often but the finite bad set can depend on the element. So it's a direct limit of the construction you explain above.

[Yury G. Kudryashov]

What is the σ-algebra of measurable sets in this case?
We can have this definition but it can be added later because it leads to a measure on a different type, not the pi type.

[Yaël Dillies]

Yury G. Kudryashov said:

If I try it, then how should I call the new typeclass?

IsCofinitelyProbabilityMeasure? Not great...

[Sebastien Gouezel]

That's a good idea. But do we already have the product of infinitely many probability measures?

[Yury G. Kudryashov]

Not yet.