Kernels under which a finite set of coordinates is redrawn

For an index type ι, a σ-finite measure μ on X, a finite set s of coordinates, and a map e : α → (ι → X), the measure updateKernel μ s e a is the image of the product measure μ^s under y ↦ Function.updateFinset (e a) s y: the coordinates outside s are those of e a, whereas those in s are independent with distribution μ. Integrals with respect to it are the marginal integrals ∫⋯∫⁻_s, f ∂μ of Mathlib, evaluated at e a.

The distributions of the variables generated by the forward passes of the paper have densities with respect to such a kernel, in which the coordinates outside s are those of the reference trajectory. If these coordinates are drawn from μ as well, the coordinates of the result are independent with distribution μ (lintegral_lintegral_updateKernel).

noncomputable def CSMC.updateKernel {α : Type u_1} {ι : Type u_2} {X : Type u_3} [MeasurableSpace α] [MeasurableSpace X] [DecidableEq ι] (μ : MeasureTheory.Measure X) (s : Finset ι) (e : α → ι → X) : ProbabilityTheory.Kernel α (ι → X)

The kernel under which the coordinates outside s are those of e a, whereas those in s are independent with distribution μ.

Equations

• One or more equations did not get rendered due to their size.

instance CSMC.instIsSFiniteKernelForallUpdateKernel {α : Type u_1} {ι : Type u_2} {X : Type u_3} [MeasurableSpace α] [MeasurableSpace X] [DecidableEq ι] (μ : MeasureTheory.Measure X) (s : Finset ι) (e : α → ι → X) : ProbabilityTheory.IsSFiniteKernel (updateKernel μ s e)

theorem CSMC.lintegral_updateKernel {α : Type u_1} {ι : Type u_2} {X : Type u_3} [MeasurableSpace α] [MeasurableSpace X] [DecidableEq ι] (μ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ] (s : Finset ι) {e : α → ι → X} (he : Measurable e) {f : (ι → X) → ENNReal} (hf : Measurable f) (a : α) : ∫⁻ (y : ι → X), f y ∂(updateKernel μ s e) a = (∫⋯∫⁻_s, f ∂fun (x : ι) => μ) (e a)

Integrals with respect to updateKernel μ s e a are marginal integrals over the coordinates in s, evaluated at e a.

theorem CSMC.lintegral_lintegral_updateKernel {ι : Type u_2} {X : Type u_3} [MeasurableSpace X] [DecidableEq ι] [Fintype ι] {δ : Type u_4} [Fintype δ] (μ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ] {s : Finset ι} {e : δ → ι} (he : Function.Injective e) (hs : ∀ (i : ι), i ∉ s ↔ i ∈ Set.range e) {g : (δ → X) → ι → X} (hg : Measurable g) (hge : ∀ (x : δ → X) (j : δ), g x (e j) = x j) {f : (δ → X) → (ι → X) → ENNReal} (hf : Measurable (Function.uncurry f)) : (∫⁻ (x : δ → X), ∫⁻ (y : ι → X), f x y ∂(updateKernel μ s g) x ∂MeasureTheory.Measure.pi fun (x : δ) => μ) = ∫⁻ (y : ι → X), f (fun (j : δ) => y (e j)) y ∂MeasureTheory.Measure.pi fun (x : ι) => μ

Let g insert a point x of δ → X at the coordinates e j, which are the coordinates outside s. If x is drawn from the product measure μ^δ and y from updateKernel μ s g x, then y has the distribution μ^ι, with x equal to j ↦ y (e j).