Feynman–Kac models

The model of Section 2.1 of the paper consists of a measurable space X with a σ-finite measure μ, a Markov chain on X with initial density m_1 and transition densities m_t(x_{t-1}, x_t), 2 ≤ t ≤ T, with respect to μ, and potential functions g_t : X → (0, ∞). 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) / Z (eq. (1)), where Z ∈ (0, ∞).

These data form the structure FeynmanKac μ n, with T = n + 1. The densities and the potential functions take values in [0, ∞). Their measurability, the normalization of the densities, the positivity of the potential functions, and the condition on Z are fields of the structure. The density m_{t+1}(x_t, ·) of the step s : Fin n from time s.castSucc to time s.succ is transdens s x_t.

The normalized weights W_t^i = g_t(x_t^i) / ∑_k g_t(x_t^k) and the backward-sampling probabilities B_t(i|j) of eq. (2) are also defined here. Where the denominator of eq. (2) vanishes, which happens on a null set under π̄, B_t(·|j) is defined as W_t, so that it is a probability vector for all particle positions.

The results proved here are that π is a probability measure, that the weights and the backward-sampling probabilities are probability vectors and measurable functions of the particle positions, and that g_t(x_t^i) = W_t^i ∑_k g_t(x_t^k) and W_t^i m_{t+1}(x_t^i, x_{t+1}^j) = B_t(i|j) ∑_k W_t^k m_{t+1}(x_t^k, x_{t+1}^j).

def CSMC.unnormalizedTarget {X : Type u_1} {n : ℕ} (transdens₁ : X → NNReal) (transdens : Fin n → X → X → NNReal) (pot : Fin (n + 1) → 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) of the target density (eq. (1)).

Equations

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

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

A Feynman–Kac model with T = n + 1 time steps on the measurable space X with the σ-finite measure μ (Section 2.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 : Fin (n + 1) → X → NNReal

  The potential functions g_t.

• 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 (t : Fin (n + 1)) : Measurable (self.pot t)

  The potential functions are 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 (t : Fin (n + 1)) (x : X) : 0 < self.pot t x

  The potential functions take values in (0, ∞).

• normconst_ne_zero : (∫⁻ (x : Fin (n + 1) → X), ↑(unnormalizedTarget self.transdens₁ self.transdens 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 x) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ) ≠ ⊤

  Z < ∞.

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

The normalizing constant Z of the target density.

Equations

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

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

The target distribution π of eq. (1).

Equations

• M.target = (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ).withDensity fun (x : Fin (n + 1) → X) => M.normconst⁻¹ * ↑(CSMC.unnormalizedTarget M.transdens₁ M.transdens M.pot x)

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

The normalized weight W_t^i = g_t(x_t^i) / ∑_k g_t(x_t^k) of the particle i at time t.

Equations

• M.weight y t i = ↑(M.pot t (y (t, i))) / ∑ k : Fin N, ↑(M.pot t (y (t, k)))

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

The backward-sampling probabilities of eq. (2): B_t(i|j) = W_t^i m_{t+1}(x_t^i, x_{t+1}^j) / ∑_k W_t^k m_{t+1}(x_t^k, x_{t+1}^j), with B_t(·|j) = W_t where the denominator vanishes.

Equations

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

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

The kernels of the selection rule r, as functions of the particle positions.

Equations

• M.ruleKernels N r y = r.kernels (M.weight y (Fin.last n)) (M.bsprob y)

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

The target distribution is a probability measure.

theorem CSMC.FeynmanKac.sum_pot_pos {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (t : Fin (n + 1)) : 0 < ∑ k : Fin N, ↑(M.pot t (y (t, k)))

With at least one particle, the sum ∑_k g_t(x_t^k) of the potentials at each time is positive.

theorem CSMC.FeynmanKac.weight_nonneg {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (y : Pos X n N) (t : Fin (n + 1)) (i : Fin N) : 0 ≤ M.weight y t i

The weights are nonnegative.

theorem CSMC.FeynmanKac.weight_toNNReal {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (y : Pos X n N) (t : Fin (n + 1)) (i : Fin N) : (M.weight y t i).toNNReal = M.pot t (y (t, i)) / ∑ k : Fin N, M.pot t (y (t, k))

The weight W_t^i as a nonnegative real number: g_t(x_t^i) / ∑_k g_t(x_t^k).

theorem CSMC.FeynmanKac.pot_eq_weight_mul {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (t : Fin (n + 1)) (i : Fin N) : M.pot t (y (t, i)) = (M.weight y t i).toNNReal * ∑ k : Fin N, M.pot t (y (t, k))

With at least one particle, g_t(x_t^i) = W_t^i ∑_k g_t(x_t^k).

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

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

theorem CSMC.FeynmanKac.isProbVector_bsprob {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (hN : 0 < N) (y : Pos X n N) (s : Fin n) (j : Fin N) : IsProbVector fun (i : Fin N) => M.bsprob y s i j

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

theorem CSMC.FeynmanKac.bsprob_eq_of_pos {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (y : Pos X n N) (s : Fin n) (i j : Fin N) (h : 0 < ∑ k : Fin N, M.weight y s.castSucc k * ↑(M.transdens s (y (s.castSucc, k)) (y (s.succ, j)))) : M.bsprob y s i j = M.weight y s.castSucc i * ↑(M.transdens s (y (s.castSucc, i)) (y (s.succ, j))) / ∑ k : Fin N, M.weight y s.castSucc k * ↑(M.transdens s (y (s.castSucc, k)) (y (s.succ, j)))

Where the denominator of eq. (2) is positive, B_t(i|j) is given by eq. (2).

theorem CSMC.FeynmanKac.bsprob_nonneg {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (y : Pos X n N) (s : Fin n) (i j : Fin N) : 0 ≤ M.bsprob y s i j

The backward-sampling probabilities are nonnegative.

theorem CSMC.FeynmanKac.weight_mul_transdens_eq {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (y : Pos X n N) (s : Fin n) (i j : Fin N) : M.weight y s.castSucc i * ↑(M.transdens s (y (s.castSucc, i)) (y (s.succ, j))) = M.bsprob y s i j * ∑ k : Fin N, M.weight y s.castSucc k * ↑(M.transdens s (y (s.castSucc, k)) (y (s.succ, j)))

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

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

The weights are measurable functions of the particle positions.

theorem CSMC.FeynmanKac.measurable_transdens_comp {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ 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.FeynmanKac.measurable_bsprob {X : Type u_1} [MeasurableSpace X] {n : ℕ} {μ : MeasureTheory.Measure X} (M : FeynmanKac μ n) {N : ℕ} (s : Fin n) (i j : Fin N) : Measurable fun (y : Pos X n N) => M.bsprob y s i j

The backward-sampling probabilities are measurable functions of the particle positions.