Two models on a finite state space

The hypotheses of the results of the paper are satisfied by two models on the state space Fin 2 with the counting measure: a Feynman–Kac model with the uniform densities m_1 = m_{t+1}(x, ·) = 1/2 and the potential functions g_t(x) = x + 1, and a model of Section S3 with the same densities and the potential functions g_1(x) = x + 1 and g_{t+1}(x, x') = x + x' + 1. With two particles, Propositions 1 and S1 apply to the kernels of each selection rule, with Algorithm 1 and with Algorithm S1 and multinomial resampling, respectively.

theorem CSMC.Examples.lintegral_half : ∫⁻ (_x : Fin 2), ↑2⁻¹ ∂MeasureTheory.Measure.count = 1

The uniform density 1/2 integrates to one with respect to the counting measure on Fin 2.

theorem CSMC.Examples.lintegral_pi_count_ne_zero_ne_top {n : ℕ} {f : Traj (Fin 2) n → NNReal} (hf : ∀ (x : Traj (Fin 2) n), 0 < f x) : (∫⁻ (x : Fin (n + 1) → Fin 2), ↑(f x) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => MeasureTheory.Measure.count) ≠ 0 ∧ (∫⁻ (x : Fin (n + 1) → Fin 2), ↑(f x) ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => MeasureTheory.Measure.count) ≠ ⊤

A positive function on the trajectories has a positive and finite integral with respect to the product of the counting measures on Fin 2.

noncomputable def CSMC.Examples.discreteModel (n : ℕ) : FeynmanKac MeasureTheory.Measure.count n

The Feynman–Kac model on Fin 2 with the counting measure, the uniform densities 1/2, and the potential functions g_t(x) = x + 1.

Equations

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

noncomputable def CSMC.Examples.discretePreviousModel (n : ℕ) : PreviousState.Model MeasureTheory.Measure.count n

The model of Section S3 on Fin 2 with the counting measure, the uniform densities 1/2, and the potential functions g_1(x) = x + 1 and g_{t+1}(x, x') = x + x' + 1.

Equations

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

theorem CSMC.Examples.discreteModel_reversible (n : ℕ) (r : SelectionRule) : ProbabilityTheory.IsMarkovKernel ((discreteModel n).csmc ((discreteModel n).ruleKernels 2 r)) ∧ ((discreteModel n).csmc ((discreteModel n).ruleKernels 2 r)).IsReversible (discreteModel n).target ∧ ((discreteModel n).csmc ((discreteModel n).ruleKernels 2 r)).Invariant (discreteModel n).target

Proposition 1 applies to the model on Fin 2 with two particles: for each selection rule, the kernel of Algorithm 1 is a Markov kernel, reversible with respect to the target distribution, and leaves it invariant.

theorem CSMC.Examples.discretePreviousModel_reversible (n : ℕ) (r : SelectionRule) : ProbabilityTheory.IsMarkovKernel ((discretePreviousModel n).csmc (fun (x : Fin n) => PreviousState.multinomial) ((discretePreviousModel n).ruleKernels 2 r)) ∧ ((discretePreviousModel n).csmc (fun (x : Fin n) => PreviousState.multinomial) ((discretePreviousModel n).ruleKernels 2 r)).IsReversible (discretePreviousModel n).target

Proposition S1 applies to the model of Section S3 on Fin 2 with two particles and multinomial resampling: for each selection rule, the kernel of Algorithm S1 is a Markov kernel, reversible with respect to the target distribution.