Normalization of the densities of variables drawn in steps

In the forward passes of the paper, the variables are drawn in steps: at each step, new variables are drawn from a distribution which depends on the variables drawn at the earlier steps. Their joint density is a product of factors, one per step, which integrates to one because each factor integrates to one over the new variables of its step, given the earlier ones.

This is proved here for marginal integrals with respect to a product measure ∏ i, μ i on ∀ i, X i: the steps form a finite subset A of a linearly ordered type, the new variables of the step k are the coordinates in a finite set S k, and the factor f k of the step k does not depend on the coordinates of the later steps (lmarginal_biUnion_prod_eq_one). Sums are the case where μ i is the counting measure.

As a first instance, the density m_1(x_1) ∏_t m_{t+1}(x_t, x_{t+1}) of a Markov chain with an initial density m_1 and transition densities m_{t+1} integrates to one (lintegral_markovChain).

theorem CSMC.lmarginal_biUnion_prod_eq_one {δ : Type u_1} {X : δ → Type u_2} [(i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)} [DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] {ι : Type u_3} [LinearOrder ι] (A : Finset ι) {S : ι → Finset δ} (hS : (↑A).PairwiseDisjoint S) {f : ι → ((i : δ) → X i) → ENNReal} (hf : ∀ k ∈ A, Measurable (f k)) (hdep : ∀ k ∈ A, ∀ j ∈ A, k < j → DependsOn (f k) (↑(S j))ᶜ) (hnorm : ∀ k ∈ A, ∀ (x : (i : δ) → X i), (∫⋯∫⁻_S k, f k ∂μ) x = 1) (x : (i : δ) → X i) : (∫⋯∫⁻_A.biUnion S, fun (y : (i : δ) → X i) => ∏ k ∈ A, f k y ∂μ) x = 1

Let A be a finite set of steps in a linearly ordered type. For each step k, let S k be the coordinates drawn at the step k and f k a measurable factor which does not depend on the coordinates drawn at the later steps and whose marginal integral over S k is one. Then the marginal integral of ∏ k ∈ A, f k over the coordinates drawn at all the steps is one.

theorem CSMC.lintegral_markovChain {Y : Type u_3} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [MeasureTheory.SigmaFinite ν] {n : ℕ} {m₁ : Y → ENNReal} {m : Fin n → Y → Y → ENNReal} (hm₁ : Measurable m₁) (hm : ∀ (s : Fin n), Measurable (Function.uncurry (m s))) (h₁ : ∫⁻ (x : Y), m₁ x ∂ν = 1) (h : ∀ (s : Fin n) (x : Y), ∫⁻ (x' : Y), m s x x' ∂ν = 1) : (∫⁻ (x : Fin (n + 1) → Y), m₁ (x 0) * ∏ s : Fin n, m s (x s.castSucc) (x s.succ) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => ν) = 1

The density m_1(x_1) ∏_t m_{t+1}(x_t, x_{t+1}) of a Markov chain on Y with n + 1 time steps, with an initial density m_1 and transition densities m_{t+1} with respect to a σ-finite measure ν, integrates to one with respect to the product measure.