infinite product measure

Stream: maths

[Nick_adfor]

I want to use Lean to write a proof of the problem:

Let $(\Omega_i, \mathcal{F}_i, \mu_i)_{i \in I}$ be a family of $\sigma$-finite measure spaces. Can one discuss the existence of a product measure on the infinite product space $\prod_{i \in I} \Omega_i$ with respect to the product $\sigma$-algebra $\bigotimes_{i \in I} \mathcal{F}_i$ in the same way as when the index set $I = \mathbb{N}$?

I check some of the Mathlib code for Measure Theory and find that there seems not a definition about infinite product measure. So I may think the hardest part of formalization is about the proper definition of infinite product measure. I try a kind of formalization (not so mature).

Any suggestion is welcomed.

import Mathlib

open MeasureTheory
open scoped ENNReal

universe u v

section InfiniteProductMeasures

variable {I : Type u} (Ω : I → Type v)
  [∀ i, MeasurableSpace (Ω i)]
  (μ : ∀ i, Measure (Ω i)) [∀ i, SigmaFinite (μ i)]

/-! Basic Definitions -/

def ProdSpace := ∀ i, Ω i

instance : MeasurableSpace (ProdSpace Ω) :=
  ⨆ i, MeasurableSpace.comap (fun x : ProdSpace Ω => x i) inferInstance

structure FinCylinder where
  J : Finset I
  sets : ∀ i, Set (Ω i)
  sets_measurable : ∀ i, MeasurableSet (sets i)
  sets_full_outside : ∀ i ∉ J, sets i = Set.univ

def cylinderSet (C : FinCylinder Ω) : Set (ProdSpace Ω) :=
  {x | ∀ i, x i ∈ C.sets i}

noncomputable def cylinderMeasure (C : FinCylinder Ω) : ℝ≥0∞ :=
  ∏ i ∈ C.J, μ i (C.sets i)

-- Definition of "all but countably many are probability measures" condition
structure TailProbabilityCondition where
  J : Set I
  J_countable : Set.Countable J
  is_probability_outside : ∀ i ∉ J, μ i (Set.univ) = 1
  -- In fact, we need μ i to be probability measures, not just measure of whole space = 1
  is_probability_measure_outside : ∀ i ∉ J, IsProbabilityMeasure (μ i)

-- Condition: uncountably many factors have infinite total measure
structure UncountableInfiniteCondition where
  infinite_indices : Set I
  uncountable : ¬ Set.Countable infinite_indices
  has_infinite_measure : ∀ i ∈ infinite_indices, μ i (Set.univ) = ∞

/-!
Theorem 1: Countable index set case
When I is countable, a σ-finite product measure always exists
-/

theorem product_measure_exists_countable_index [Countable I] :
    ∃ (ν : Measure (ProdSpace Ω)),
      SigmaFinite ν ∧
      ∀ (C : FinCylinder Ω),
        ν {x : ProdSpace Ω | ∀ i, x i ∈ C.sets i} = ∏ i ∈ C.J, μ i (C.sets i) := by
  sorry

/-!
Theorem 2: Uncountable index set with "tail probability measure" condition
-/

theorem product_measure_exists_tail_probability
    (h : TailProbabilityCondition Ω μ) :
    ∃ (ν : Measure (ProdSpace Ω)),
      SigmaFinite ν ∧
      ∀ (C : FinCylinder Ω),
        ν {x : ProdSpace Ω | ∀ i, x i ∈ C.sets i} = ∏ i ∈ C.J, μ i (C.sets i) := by
  sorry

/-!
Theorem 3: Uncountable index set with uncountably many infinite-measure factors
This case is impossible
-/

theorem no_sigma_finite_product_uncountable_infinite
    (h : UncountableInfiniteCondition Ω μ) :
    ¬ ∃ (ν : Measure (ProdSpace Ω)),
        SigmaFinite ν ∧
        ∀ (C : FinCylinder Ω),
          ν {x : ProdSpace Ω | ∀ i, x i ∈ C.sets i} = ∏ i ∈ C.J, μ i (C.sets i) := by
  sorry

[Nick_adfor]

The math proof (It is also not so mature. I try to refer to https://math.stackexchange.com/questions/21945/infinite-product-of-measurable-spaces)

Theorem 1 (Countable Index Set)  

When the index set $I$ is countable, a $\sigma$-finite product measure always exists on the infinite product space. The construction proceeds by decomposing each $\sigma$-finite measure $\mu_i$ into a sum of finite measures $\mu_i = \sum_{k=1}^\infty \mu_i^{(k)}$. Each finite measure is normalized to a probability measure $P_i^{(k)} = \mu_i^{(k)}/\mu_i^{(k)}(\Omega_i)$. For every sequence $(k_1, k_2, \dots)$ of indices, the Kolmogorov extension theorem provides a probability product measure $\bigotimes_{i=1}^\infty P_i^{(k_i)}$ on the countable product. The desired $\sigma$-finite product measure is then obtained as a countable sum $\nu = \sum_{k_1,k_2,\dots} \left(\prod_i \mu_i^{(k_i)}(\Omega_i)\right) \cdot \bigotimes_i P_i^{(k_i)}$, which is $\sigma$-finite and coincides with the finite-dimensional product on every cylinder set.

Theorem 2 (Uncountable Index Set with Tail Probability Condition)  

For an uncountable index set $I$, a $\sigma$-finite product measure exists if and only if there is a countable subset $J \subset I$ such that $\mu_i$ is $\sigma$-finite for every $i \in J$ and $\mu_i$ is a probability measure (i.e., $\mu_i(\Omega_i)=1$) for every $i \notin J$.  
Necessity. Assume a $\sigma$-finite product measure $\nu$ exists. Write the product space as a countable union $\prod_i \Omega_i = \bigcup_{n=1}^\infty B_n$ with $\nu(B_n) < \infty$. Each $B_n$ belongs to the product $\sigma$-algebra, hence depends on at most countably many coordinates; let $J_n$ be this countable set of coordinates. The union $J = \bigcup_n J_n$ remains countable. For any $i \notin J$, the measure $\mu_i$ must satisfy $\mu_i(\Omega_i)=1$; otherwise, the cylinder $\Omega_i \times \prod_{j\neq i} \Omega_j$ would have infinite $\nu$-measure, contradicting the $\sigma$-finiteness of $\nu$.
Sufficiency. When such a countable set $J$ exists, construct the product measure in two steps. On the countable coordinates $J$, apply Theorem 1 to obtain a $\sigma$-finite product measure $\nu_J = \bigotimes_{i\in J} \mu_i$. On the remaining coordinates $I\setminus J$, all measures are probability measures; the Kolmogorov extension theorem yields a probability product measure $\nu_{I\setminus J} = \bigotimes_{i\notin J} \mu_i$. The tensor product $\nu = \nu_J \otimes \nu_{I\setminus J}$ is then a $\sigma$-finite measure on the full product space that satisfies the required cylinder condition.

Theorem 3 (Impossibility with Uncountably Many Infinite Factors)  

If the set $I_\infty = \{i\in I : \mu_i(\Omega_i)=\infty\}$ is uncountable, then no $\sigma$-finite product measure can exist on $\prod_{i\in I} \Omega_i$.  

Suppose, for contradiction, that such a measure $\nu$ exists. By $\sigma$-finiteness we have $\prod_i \Omega_i = \bigcup_{n=1}^\infty B_n$ with $\nu(B_n) < \infty$. Each $B_n$, being an element of the product $\sigma$-algebra, depends on at most countably many coordinates; denote this countable set by $J_n$. The union $J = \bigcup_n J_n$ is still countable. Since $I_\infty$ is uncountable, we can choose an index $i_0 \in I_\infty \setminus J$. Consider the cylinder $C = \Omega_{i_0} \times \prod_{i\neq i_0} \Omega_i$. By the definition of a product measure, $\nu(C) = \mu_{i_0}(\Omega_{i_0}) = \infty$. However, $C$ is covered by the sets $B_n$, each of finite measure, which would force $\nu(C) \le \sum_n \nu(B_n) < \infty$ – a contradiction. Hence no $\sigma$-finite $\nu$ satisfying the product condition can exist.

[Rémy Degenne]

We have a product measure over an infinite index, for probability measures: MeasureTheory.Measure.infinitePi

[Nick_adfor]

Very thanks. It might be my careless check:(

[Lua Viana Reis]

the Kolmogorov extension theorem provides a probability product measure

I don't think this proof works for probability measures, the KET needs some extra assumptions, no? (of topological nature)

The desired $\sigma$-finite product measure is then obtained as a countable sum

This is also not a countable sum, $\mathbb{N} \to \mathbb{N}$ is uncountable.

That said, it is a theorem that

$$\bigotimes_{i \in I}\mathcal{F}_i = \bigcup_{\substack{\alpha \subset I\\\alpha\text{ is countable}}}\pi_{\alpha}^{-1}\left(\bigotimes_{i \in \alpha}\mathcal{F}_i\right),$$

so generally speaking if you can define a countable product, then it should be possible to do uncountable too

[Nick_adfor]

There's a very terrible problem: the origin problem want to discuss omega_i in the "same" way, the "same" may mean KET in probability measure on countable set. However, one can see the problem does not contain any word about "probability", just "same". The problem might be from some probability book and needs
context so I'm trying to ask my professor to fix the problem statement.

We can check that the problem itself seems to have math error on countable set I. Theorem 1 and Theorem 2 are wrong because of count measure (count measure is sigma-infinite measure).

[Nick_adfor]

5bfb3c76-920b-44ca-ad8f-b15794bca2c7-output.lean.txt

Here's Aristotle.

[Lua Viana Reis]

(deleted)

[Lua Viana Reis]

(deleted)