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.

[Yaël Dillies]

@Yury G. Kudryashov, has anything moved on that front? @Kin Yau James Wong and I need the infinite product of probability measures to construct a (trivial) Gibbs measure

[Yury G. Kudryashov]

Not yet.

[Yury G. Kudryashov]

If you're going to work on this, I suggest that we talk about it first.

[Yaël Dillies]

Yeah, this is one of the first things we need for our project, so we need to work on this/convince you to do it for us

[Sébastien Gouëzel]

It has been done by Etienne Marion in his M1 internship with me, but it's not PRed to mathlib yet.

[Yaël Dillies]

Do you have any pointers for me?

[Peter Pfaffelhuber]

Yaël Dillies schrieb:

Yury G. Kudryashov, has anything moved on that front? Kin Yau James Wong and I need the infinite product of probability measures to construct a (trivial) Gibbs measure

Isn't this a simple example of the Kolmogorv Extension Theorem? @Rémy Degenne and I have worked this out, but still need to PR this to Mathlib. https://github.com/RemyDegenne/kolmogorov_extension4

[Yaël Dillies]

Yes it is

[Yaël Dillies]

@Peter Pfaffelhuber, I see MeasureTheory.independentFamily in your repo. However:

• Do we really need all those topological assumptions? I would the infinite product of probability doesn't require anything like that (but maybe I'm just ignorant).
• There's no API for it :sad:

[Rémy Degenne]

If you don't want topological assumptions, you need to restrict the index type. If you index over N, you don't need any assumption and can use the Ionescu-Tulcea theorem. This is what Etienne has done with Sébastien.

[Yaël Dillies]

I see. In our case, we care about ℤⁿ, so we would rather assume countability of the index type than topological stuff on the codomain

[Yaël Dillies]

Do you know where I can find Etienne's project?

[Yury G. Kudryashov]

About making different cases co-exist in Mathlib. I think that we should define the pi measure in some highly non-constructive way (e.g., the infimum of all measures such that for all s : ι → Set α with Set.Finite {i | μ i (s i) > 1}, the measure of Set.pi Set.univ s is ≥ tprod fun i ↦ μ i (s i) (not sure about > 1 vs ≠ 1; not sure if we need to require Countable ι, Set.Countable {i | s i ≠ univ}, or none). Then we can have a Prop-valued typeclass saying that a given family of measures admits a measure such that we have = tprod .... This way we can have instances with different assumptions and theorems assuming this TC.

[Sébastien Gouëzel]

You don't need topological assumptions for the product mesure, whatever the index set. Etienne has proved that. I'm currently getting the code in a reasonable state, should be ready today.

[Peter Pfaffelhuber]

This sounds like Corollary 8.25 in Kallenberg (Foundations of Modern Probability, 3rd edition). (If you have any dependency between coordinates, however, you will need some topological structure of the underlying spaces, as far as I know.)

[Rémy Degenne]

Sorry, I misread the thread and wrote nonsense. I meant that the extension theorem we used actually required assumptions in general.
The special case of the product measure is different.

[Sébastien Gouëzel]

You can find the definition of the general product measure in https://github.com/sgouezel/kolmogorov_extension4/blob/master/KolmogorovExtension4/MesureProduit2.lean. See productMeasure in this file, with some basic API after the definition.

[Yaël Dillies]

(now https://github.com/sgouezel/kolmogorov_extension4/blob/master/KolmogorovExtension4/ProductMeasure.lean)

[Etienne Marion]

#22555 just got merged, so infinite products of probability measures are now in Mathlib :tada: