Measurability of the kernels of the selection rules

The entries of the Gibbs kernel, of the forced moves F_p and F_u, and of the coupling kernel C_{p,q} are measurable functions of the vectors p, u, and (p, q). So are the entries of the kernels K_T, K_{t,j,j}, and K_{t,j,j'} of the six selection rules. With the measurability of the weights and of the backward-sampling probabilities in the particle positions, it follows that the kernels of the six rules are measurable functions of the particle positions (MeasurableKernels), which is left implicit in the paper.

theorem CSMC.measurable_gibbs {ι : Type u_1} (i j : ι) : Measurable fun (p : ι → ℝ) => gibbs p i j

The entries of the Gibbs kernel are measurable functions of the probability vector.

theorem CSMC.measurable_forced {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i j : ι) : Measurable fun (p : ι → ℝ) => forced p i j

The entries of the forced move F_p are measurable functions of p.

theorem CSMC.measurable_forcedU {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i j : ι) : Measurable fun (u : ι → ℝ) => forcedU u i j

The entries of the forced move F_u are measurable functions of the vector u.

theorem CSMC.measurable_coupling {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i i' : ι) : Measurable fun (pq : (ι → ℝ) × (ι → ℝ)) => coupling pq.1 pq.2 i i'

The entries of the coupling kernel C_{p,q} are measurable functions of (p, q).

theorem CSMC.SelectionRule.measurable_finalKernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : SelectionRule) (i j : ι) : Measurable fun (W : ι → ℝ) => r.finalKernel W i j

The entries of the kernel K_T of each rule are measurable functions of the final weights.

theorem CSMC.SelectionRule.measurable_diagKernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : SelectionRule) (i j : ι) : Measurable fun (p : ι → ℝ) => r.diagKernel p i j

The entries of the kernel K_{t,j,j} of each rule are measurable functions of the probability vector B_t(·|j).

theorem CSMC.SelectionRule.measurable_offDiagKernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : SelectionRule) (i j : ι) : Measurable fun (pq : (ι → ℝ) × (ι → ℝ)) => r.offDiagKernel pq.1 pq.2 i j

The entries of the kernel K_{t,j,j'}, j ≠ j', of each rule are measurable functions of the pair of probability vectors (B_t(·|j), B_t(·|j')).

theorem CSMC.FeynmanKac.measurableKernels_ruleKernels {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {n : ℕ} (M : FeynmanKac μ n) (N : ℕ) (r : SelectionRule) : MeasurableKernels (M.ruleKernels N r)

The kernels of each selection rule are measurable functions of the particle positions.