Feynman–Kac models with potential functions of the previous state

In Section S3 of the supplementary material, the potential functions are g_1 : X → (0, ∞) and g_t : X² → (0, ∞), 2 ≤ t ≤ T. The target distribution has density π(x_{1:T}) = m_1(x_1) g_1(x_1) ∏_{t ≥ 2} m_t(x_{t-1}, x_t) g_t(x_{t-1}, x_t) / Z (eq. (S2)), where Z ∈ (0, ∞). These data are the fields of the structure PreviousState.Model μ n, with the conventions of FeynmanKac μ n: pot s x x' is g_{t+1}(x, x') for the step s from time t = s.castSucc to time s.succ.

The normalized weights at the times t ≥ 2, W_t^i = g_t(x_{t-1}^{a_{t-1}^i}, x_t^i) / ∑_k g_t(x_{t-1}^{a_{t-1}^k}, x_t^k), depend on the ancestor indices. The backward-sampling probabilities B_t(i|x') of eq. (S3) are those of Lindsten and Schön (2013), with B_t(i|j) = B_t(i|x_{t+1}^j). Where the denominator of eq. (S3) vanishes, B_t(·|x') is defined as W_t, with the convention of FeynmanKac.bsprob for eq. (2).

It is proved here that π is a probability measure, and that the weights and the backward-sampling probabilities are probability vectors and, for fixed ancestor indices, measurable functions of the particle positions. The identities g_t(x_{t-1}^{a_{t-1}^i}, x_t^i) = W_t^i ∑_k g_t(x_{t-1}^{a_{t-1}^k}, x_t^k) and W_t^i m_{t+1}(x_t^i, x') g_{t+1}(x_t^i, x') = B_t(i|x') ∑_k W_t^k m_{t+1}(x_t^k, x') g_{t+1}(x_t^k, x') also hold.

def CSMC.PreviousState.unnormalizedTarget {X : Type u_1} {n : ℕ} (transdens₁ : X → NNReal) (transdens : Fin n → X → X → NNReal) (pot₁ : X → NNReal) (pot : Fin n → X → X → NNReal) (x : Traj X n) : NNReal

The numerator m_1(x_1) g_1(x_1) ∏_{t ≥ 2} m_t(x_{t-1}, x_t) g_t(x_{t-1}, x_t) of the target density (eq. (S2)).

Equations

• CSMC.PreviousState.unnormalizedTarget transdens₁ transdens pot₁ pot x = transdens₁ (x 0) * pot₁ (x 0) * ∏ s : Fin n, transdens s (x s.castSucc) (x s.succ) * pot s (x s.castSucc) (x s.succ)

structure CSMC.PreviousState.Model {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (n : ℕ) : Type u_1

A Feynman–Kac model with potential functions of the previous state, with T = n + 1 time steps on the measurable space X with the σ-finite measure μ (Section S3.1).

• transdens₁ : X → NNReal

  The initial density m_1.

• transdens : Fin n → X → X → NNReal

  The transition densities: transdens s x x' is m_{t+1}(x, x') for the step s from time t = s.castSucc to time s.succ.

• pot₁ : X → NNReal

  The potential function g_1.

• pot : Fin n → X → X → NNReal

  The potential functions of the previous state: pot s x x' is g_{t+1}(x, x') for the step s from time t = s.castSucc to time s.succ.

• measurable_transdens₁ : Measurable self.transdens₁

  The initial density is measurable.

• measurable_transdens (s : Fin n) : Measurable (Function.uncurry (self.transdens s))

  The transition densities are jointly measurable.

• measurable_pot₁ : Measurable self.pot₁

  The potential function g_1 is measurable.

• measurable_pot (s : Fin n) : Measurable (Function.uncurry (self.pot s))

  The potential functions g_t, t ≥ 2, are jointly measurable.

• lintegral_transdens₁ : ∫⁻ (x : X), ↑(self.transdens₁ x) ∂μ = 1

  m_1 is a probability density with respect to μ.

• lintegral_transdens (s : Fin n) (x : X) : ∫⁻ (x' : X), ↑(self.transdens s x x') ∂μ = 1

  Each m_{t+1}(x, ·) is a probability density with respect to μ.

• pot₁_pos (x : X) : 0 < self.pot₁ x

  g_1 takes values in (0, ∞).

• pot_pos (s : Fin n) (x x' : X) : 0 < self.pot s x x'

  The potential functions g_t, t ≥ 2, take values in (0, ∞).

• normconst_ne_zero : (∫⁻ (x : Fin (n + 1) → X), ↑(unnormalizedTarget self.transdens₁ self.transdens self.pot₁ self.pot x) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ) ≠ 0

  Z ≠ 0.

• normconst_ne_top : (∫⁻ (x : Fin (n + 1) → X), ↑(unnormalizedTarget self.transdens₁ self.transdens self.pot₁ self.pot x) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ) ≠ ⊤

  Z < ∞.

noncomputable def CSMC.PreviousState.Model.normconst {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) : ENNReal

The normalizing constant Z of the target density.

Equations

• M.normconst = ∫⁻ (x : Fin (n + 1) → X), ↑(CSMC.PreviousState.unnormalizedTarget M.transdens₁ M.transdens M.pot₁ M.pot x) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ

noncomputable def CSMC.PreviousState.Model.target {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) : MeasureTheory.Measure (Traj X n)

The target distribution π of eq. (S2).

Equations

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

noncomputable def CSMC.PreviousState.Model.weight {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (y : Pos X n N) (a : Anc n N) (t : Fin (n + 1)) (i : Fin N) : ℝ

The normalized weights W_t^i: g_1(x_1^i) / ∑_k g_1(x_1^k) at time 1, and g_t(x_{t-1}^{a_{t-1}^i}, x_t^i) / ∑_k g_t(x_{t-1}^{a_{t-1}^k}, x_t^k) at the times t ≥ 2.

Equations

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

noncomputable def CSMC.PreviousState.Model.bsprobAt {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (y : Pos X n N) (a : Anc n N) (s : Fin n) (x' : X) (i : Fin N) : ℝ

The backward-sampling probabilities of eq. (S3): B_t(i|x') is W_t^i m_{t+1}(x_t^i, x') g_{t+1}(x_t^i, x') divided by its sum over i, with B_t(·|x') = W_t where this sum vanishes.

Equations

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

noncomputable def CSMC.PreviousState.Model.bsprob {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (y : Pos X n N) (a : Anc n N) (s : Fin n) : Matrix (Fin N) (Fin N) ℝ

The backward-sampling probabilities B_t(i|j) = B_t(i|x_{t+1}^j) (Section S3.1).

Equations

• M.bsprob y a s = Matrix.of fun (i j : Fin N) => M.bsprobAt y a s (y (s.succ, j)) i

noncomputable def CSMC.PreviousState.Model.ruleKernels {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) (N : ℕ) (r : SelectionRule) (ya : Pos X n N × Anc n N) : BackwardKernels (Fin N) n

The kernels of the selection rule r, defined as in the main text with the probabilities (S3), as functions of the particle positions and of the ancestor indices.

Equations

• M.ruleKernels N r ya = r.kernels (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2)

theorem CSMC.PreviousState.Model.isProbabilityMeasure_target {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) : MeasureTheory.IsProbabilityMeasure M.target

The target distribution is a probability measure.

theorem CSMC.PreviousState.Model.weight_zero {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (y : Pos X n N) (a : Anc n N) (i : Fin N) : M.weight y a 0 i = ↑(M.pot₁ (y (0, i))) / ∑ k : Fin N, ↑(M.pot₁ (y (0, k)))

The weights at time 1: W_1^i = g_1(x_1^i) / ∑_k g_1(x_1^k).

theorem CSMC.PreviousState.Model.weight_succ {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (y : Pos X n N) (a : Anc n N) (s : Fin n) (i : Fin N) : M.weight y a s.succ i = ↑(M.pot s (y (s.castSucc, a s i)) (y (s.succ, i))) / ∑ k : Fin N, ↑(M.pot s (y (s.castSucc, a s k)) (y (s.succ, k)))

The weights at the times t ≥ 2: W_t^i = g_t(x_{t-1}^{a_{t-1}^i}, x_t^i) / ∑_k g_t(x_{t-1}^{a_{t-1}^k}, x_t^k).

theorem CSMC.PreviousState.Model.weight_pos {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (a : Anc n N) (t : Fin (n + 1)) (i : Fin N) : 0 < M.weight y a t i

With at least one particle, the weights are positive.

theorem CSMC.PreviousState.Model.isProbVector_weight {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (a : Anc n N) (t : Fin (n + 1)) : IsProbVector (M.weight y a t)

With at least one particle, the weights at each time form a probability vector.

theorem CSMC.PreviousState.Model.pot₁_eq_weight_mul {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (a : Anc n N) (i : Fin N) : M.pot₁ (y (0, i)) = (M.weight y a 0 i).toNNReal * ∑ k : Fin N, M.pot₁ (y (0, k))

With at least one particle, g_1(x_1^i) = W_1^i ∑_k g_1(x_1^k).

theorem CSMC.PreviousState.Model.pot_eq_weight_mul {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (a : Anc n N) (s : Fin n) (i : Fin N) : M.pot s (y (s.castSucc, a s i)) (y (s.succ, i)) = (M.weight y a s.succ i).toNNReal * ∑ k : Fin N, M.pot s (y (s.castSucc, a s k)) (y (s.succ, k))

With at least one particle, g_t(x_{t-1}^{a_{t-1}^i}, x_t^i) = W_t^i ∑_k g_t(x_{t-1}^{a_{t-1}^k}, x_t^k) for t ≥ 2.

theorem CSMC.PreviousState.Model.isProbVector_bsprobAt {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (a : Anc n N) (s : Fin n) (x' : X) : IsProbVector (M.bsprobAt y a s x')

With at least one particle, each B_t(·|x') is a probability vector.

theorem CSMC.PreviousState.Model.weight_mul_eq_bsprobAt_mul {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (y : Pos X n N) (a : Anc n N) (s : Fin n) (x' : X) (i : Fin N) : M.weight y a s.castSucc i * (↑(M.transdens s (y (s.castSucc, i)) x') * ↑(M.pot s (y (s.castSucc, i)) x')) = M.bsprobAt y a s x' i * ∑ k : Fin N, M.weight y a s.castSucc k * (↑(M.transdens s (y (s.castSucc, k)) x') * ↑(M.pot s (y (s.castSucc, k)) x'))

W_t^i m_{t+1}(x_t^i, x') g_{t+1}(x_t^i, x') = B_t(i|x') ∑_k W_t^k m_{t+1}(x_t^k, x') g_{t+1}(x_t^k, x'), also where the sum vanishes.

theorem CSMC.PreviousState.Model.measurable_transdens_comp {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {α : Type u_2} [MeasurableSpace α] (s : Fin n) {f g : α → X} (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : α) => M.transdens s (f a) (g a)

The transition densities, evaluated at measurable functions, are measurable.

theorem CSMC.PreviousState.Model.measurable_pot_comp {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {α : Type u_2} [MeasurableSpace α] (s : Fin n) {f g : α → X} (hf : Measurable f) (hg : Measurable g) : Measurable fun (a : α) => M.pot s (f a) (g a)

The potential functions g_t, t ≥ 2, evaluated at measurable functions, are measurable.

theorem CSMC.PreviousState.Model.measurable_weight {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (a : Anc n N) (t : Fin (n + 1)) (i : Fin N) : Measurable fun (y : Pos X n N) => M.weight y a t i

For fixed ancestor indices, the weights are measurable functions of the particle positions.

theorem CSMC.PreviousState.Model.measurable_bsprob {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : Model μ n) {N : ℕ} (a : Anc n N) (s : Fin n) (i j : Fin N) : Measurable fun (y : Pos X n N) => M.bsprob y a s i j

For fixed ancestor indices, the backward-sampling probabilities B_t(i|j) are measurable functions of the particle positions.