Documentation

MetropolizedBackwardSampling.PreviousState.Validity

The validity of Algorithm S1 #

Lemma S1 of the supplementary material is proved here: let x_{1:T} ∼ Ο€ and run steps (a) and (b) of Algorithm S1, with c drawn from C(B_t(Β·|x_{t+1}))(b_t, Β·) for kernels C(p) which are reversible with respect to p, as are the kernels K_{t,j,j} of the six selection rules. Then the joint distribution of x_{1:T} and of the variables (𝐱, a, b_{1:T}) of these steps is that of (x_1^{b_1}, …, x_T^{b_T}) and of (𝐱, a, b_{1:T}) with the density (S4).

In the proof, for each b, the reference trajectory is read off the particles with the indices b. The target density at (x_1^{b_1}, …, x_T^{b_T}) times the density of steps (a) and (b) is then the density (S4), by the pointwise identity target_mul_fwdDensity_eq_extDensity.

Proposition S1 is also proved here: given (𝐱, a), the pairs (b_t, l_t) form the backward Markov chain pairChain K, which does not change when the indices of the reference and of the output are exchanged, so that the Markov kernel defined by Algorithm S1 is reversible with respect to Ο€.

source
theorem CSMC.PreviousState.Model.lintegral_target_compProd_forwardPass {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) {f : Traj X n Γ— Pos X n N Γ— Anc n N Γ— Idx n N β†’ ENNReal} (hf : Measurable f) :
∫⁻ (z : Traj X n Γ— Pos X n N Γ— Anc n N Γ— Idx n N), f z βˆ‚M.target.compProd (M.forwardPass resdist C) = ∫⁻ (y : Fin (n + 1) Γ— Fin N β†’ X), βˆ‘ a : Anc n N, βˆ‘ b : Idx n N, M.normconst⁻¹ * ↑(unnormalizedTarget M.transdens₁ M.transdens M.pot₁ M.pot (trajOf y b)) * ↑(M.fwdDensity resdist C b y a) * f (trajOf y b, y, a, b) βˆ‚MeasureTheory.Measure.pi fun (x : Fin (n + 1) Γ— Fin N) => ΞΌ

Integrals with respect to the joint distribution of x_{1:T} ∼ Ο€ and of the variables (y, a, b) of steps (a) and (b) of Algorithm S1 are integrals over the particle positions of sums, over the ancestor indices and the indices of the reference, of the target density at (x_1^{b_1}, …, x_T^{b_T}) times the density of these steps times the integrand, evaluated at the reference trajectory (x_1^{b_1}, …, x_T^{b_T}).

source
theorem CSMC.PreviousState.Model.lintegral_extMeasure {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) {g : Pos X n N Γ— Anc n N Γ— Idx n N β†’ ENNReal} (hg : Measurable g) :
∫⁻ (w : Pos X n N Γ— Anc n N Γ— Idx n N), g w βˆ‚M.extMeasure resdist C = ∫⁻ (y : Fin (n + 1) Γ— Fin N β†’ X), βˆ‘ a : Anc n N, βˆ‘ b : Idx n N, M.extDensity resdist C y a b * g (y, a, b) βˆ‚MeasureTheory.Measure.pi fun (x : Fin (n + 1) Γ— Fin N) => ΞΌ

Integrals with respect to the distribution with the density (S4) are integrals over the particle positions of sums over the ancestor indices and the indices of the reference of the density (S4) times the integrand.

source
theorem CSMC.PreviousState.Model.measurable_traced {X : Type u_1} [MeasurableSpace X] {n N : β„•} :
Measurable fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => (trajOf w.1 w.2.2, w)

The map w ↦ (x, w), where x = (x_1^{b_1}, …, x_T^{b_T}) is the reference trajectory read off the particles with the indices of the reference, is measurable.

source
theorem CSMC.PreviousState.Model.target_compProd_forwardPass {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hC : βˆ€ (p : Fin N β†’ ℝ), IsProbVector p β†’ IsReversible p (C p)) (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) :
M.target.compProd (M.forwardPass resdist C) = MeasureTheory.Measure.map (fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => (trajOf w.1 w.2.2, w)) (M.extMeasure resdist C)

Lemma S1: if the resampling schemes satisfy the condition of Definition S1 and each C(p) is reversible with respect to p, the joint distribution of x_{1:T} ∼ Ο€ and of the variables (𝐱, a, b_{1:T}) of steps (a) and (b) of Algorithm S1, with c drawn from C(B_t(Β·|x_{t+1}))(b_t, Β·), is that of (x_1^{b_1}, …, x_T^{b_T}) and of (𝐱, a, b_{1:T}) with the density (S4).

source
theorem CSMC.PreviousState.Model.map_snd_target_compProd_forwardPass {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hC : βˆ€ (p : Fin N β†’ ℝ), IsProbVector p β†’ IsReversible p (C p)) (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) :
MeasureTheory.Measure.map Prod.snd (M.target.compProd (M.forwardPass resdist C)) = M.extMeasure resdist C

Lemma S1, second part: under the same hypotheses, (𝐱, a, b_{1:T}) has the density (S4).

source
instance CSMC.PreviousState.Model.instSFiniteProdPosAncIdxExtMeasureOfSigmaFinite {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ) (C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ) :
MeasureTheory.SFinite (M.extMeasure resdist C)

The distribution with the density (S4) is s-finite.

source
noncomputable def CSMC.PreviousState.Model.posAncDensity {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ) (y : Pos X n N) (a : Anc n N) :
ENNReal

The factor of the density (S4) which depends on the particle positions and the ancestor indices only: (Z N^T)⁻¹ {βˆ‘_i g_1(x_1^i)} ∏_n m_1(x_1^n) ∏_t r_t(a_t) ∏_t {βˆ‘_i g_{t+1}(x_t^{a_t^i}, x_{t+1}^i)} ∏_n m_{t+1}(x_t^{a_t^n}, x_{t+1}^n).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CSMC.PreviousState.Model.extDensity_eq_mul {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ) (C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ) (y : Pos X n N) (a : Anc n N) (b : Idx n N) :
    M.extDensity resdist C y a b = M.posAncDensity resdist y a * ENNReal.ofReal (M.weight y a (Fin.last n) (b (Fin.last n))) * ∏ s : Fin n, ENNReal.ofReal (C (fun (i : Fin N) => M.bsprob y a s i (b s.succ)) (a s (b s.succ)) (b s.castSucc))

    The density (S4) is the product of a function of the particle positions and the ancestor indices and of W_T^{b_T} ∏_t C(B_t(·|b_{t+1}))(a_t^{b_{t+1}}, b_t).

    source
    noncomputable def CSMC.PreviousState.Model.pairChain {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n) :
    ProbabilityTheory.Kernel (Pos X n N Γ— Anc n N) (Idx n N Γ— Idx n N)

    The backward Markov chain of the pairs (b_t, l_t) of indices of the reference and of the output, given the particle positions and the ancestor indices (proof of Proposition S1): the kernel with mass function (b, l) ↦ pathProb W_T B K b l, with the weights W_T and the probabilities (S3).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CSMC.PreviousState.Model.instIsSFiniteKernelProdPosAncIdxPairChain {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n) :
      ProbabilityTheory.IsSFiniteKernel (M.pairChain K)

      The backward Markov chain pairChain K is an s-finite kernel.

      source
      theorem CSMC.PreviousState.Model.measurable_pathProb {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hKm : MeasurableKernels K) (b l : Idx n N) :
      Measurable fun (ya : Pos X n N Γ— Anc n N) => pathProb (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya) b l

      For measurable kernels, the probabilities pathProb of pairChain K are measurable functions of the particle positions and the ancestor indices.

      source
      theorem CSMC.PreviousState.Model.lintegral_pairChain {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hKm : MeasurableKernels K) (ya : Pos X n N Γ— Anc n N) (g : Idx n N Γ— Idx n N β†’ ENNReal) :
      ∫⁻ (bl : Idx n N Γ— Idx n N), g bl βˆ‚(M.pairChain K) ya = βˆ‘ b : Fin (n + 1) β†’ Fin N, βˆ‘ l : Fin (n + 1) β†’ Fin N, ENNReal.ofReal (pathProb (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya) b l) * g (b, l)

      Integrals with respect to pairChain K are sums over the pairs (b, l), weighted by pathProb.

      source
      theorem CSMC.PreviousState.Model.lintegral_target_compProd_compProd {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hC : βˆ€ (p : Fin N β†’ ℝ), IsProbVector p β†’ IsReversible p (C p)) (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) {Ξ³ : Type u_2} [MeasurableSpace Ξ³] {Ξ· : ProbabilityTheory.Kernel (Traj X n Γ— Pos X n N Γ— Anc n N Γ— Idx n N) Ξ³} [ProbabilityTheory.IsSFiniteKernel Ξ·] {f : Traj X n Γ— (Pos X n N Γ— Anc n N Γ— Idx n N) Γ— Ξ³ β†’ ENNReal} (hf : Measurable f) :
      ∫⁻ (z : Traj X n Γ— (Pos X n N Γ— Anc n N Γ— Idx n N) Γ— Ξ³), f z βˆ‚M.target.compProd ((M.forwardPass resdist C).compProd Ξ·) = ∫⁻ (w : Pos X n N Γ— Anc n N Γ— Idx n N), ∫⁻ (c : Ξ³), f (trajOf w.1 w.2.2, w, c) βˆ‚Ξ· (trajOf w.1 w.2.2, w) βˆ‚M.extMeasure resdist C

      Integrals with respect to the joint distribution of x_{1:T} ∼ Ο€, of the variables (y, a, b) of steps (a) and (b) of Algorithm S1, and of a variable c drawn from a kernel Ξ· given these, are integrals, with respect to the distribution with the density (S4), of the integral with respect to Ξ·, at the reference trajectory (x_1^{b_1}, …, x_T^{b_T}).

      source
      theorem CSMC.PreviousState.Model.measurable_trajOf_fst {X : Type u_1} [MeasurableSpace X] {n N : β„•} :
      Measurable fun (w : (Pos X n N Γ— Anc n N) Γ— Idx n N) => trajOf w.1.1 w.2

      The trajectory of the particles with the indices l, as a function of the particle positions, the ancestor indices, and l, is measurable.

      source
      theorem CSMC.PreviousState.Model.sum_ofReal_weight_mul_prod_bsprob {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (hN : 0 < N) (y : Pos X n N) (a : Anc n N) :
      βˆ‘ b : Idx n N, ENNReal.ofReal (M.weight y a (Fin.last n) (b (Fin.last n)) * ∏ s : Fin n, M.bsprob y a s (b s.castSucc) (b s.succ)) = 1

      With at least one particle, the probabilities W_T^{b_T} ∏_t B_t(b_t|b_{t+1}) of the sequences of indices b sum to one, because W_T and the B_t(·|j) are probability vectors.

      source
      theorem CSMC.PreviousState.Model.map_target_compProd_algLaw_traced {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hKm : MeasurableKernels K) :
      MeasureTheory.Measure.map (fun (z : Traj X n Γ— (Pos X n N Γ— Anc n N Γ— Idx n N) Γ— Idx n N) => (z.1, (z.2.1.1, z.2.1.2.1), z.2.1.2.2, z.2.2)) (M.target.compProd (M.algLaw resdist K)) = MeasureTheory.Measure.map (fun (w : (Pos X n N Γ— Anc n N) Γ— Idx n N Γ— Idx n N) => (trajOf w.1.1 w.2.1, w)) ((MeasureTheory.Measure.map (fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => (w.1, w.2.1)) (M.extMeasure resdist gibbs)).compProd (M.pairChain K))

      Lemma 4 for Algorithm S1 (proof of Proposition S1): the joint distribution of x_{1:T} ∼ Ο€, of the particle positions and the ancestor indices (𝐱, a), and of the indices (b, l) of the reference and of the output of Algorithm S1, read as (x, ((𝐱, a), (b, l))), is that of (x_1^{b_1}, …, x_T^{b_T}) and of ((𝐱, a), (b, l)), where (𝐱, a) has its distribution under the density (S4) and, given (𝐱, a), (b, l) has the distribution of the backward Markov chain pairChain K.

      source
      theorem CSMC.PreviousState.Model.target_compProd_csmc {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hKm : MeasurableKernels K) :
      M.target.compProd (M.csmc resdist K) = MeasureTheory.Measure.map (fun (w : (Pos X n N Γ— Anc n N) Γ— Idx n N Γ— Idx n N) => (trajOf w.1.1 w.2.1, trajOf w.1.1 w.2.2)) ((MeasureTheory.Measure.map (fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => (w.1, w.2.1)) (M.extMeasure resdist gibbs)).compProd (M.pairChain K))

      The joint distribution of x_{1:T} ∼ Ο€ and of the output of Algorithm S1 is that of the trajectories (x_1^{b_1}, …, x_T^{b_T}) and (x_1^{l_1}, …, x_T^{l_T}), where (𝐱, a) has its distribution under the density (S4) and, given (𝐱, a), (b, l) has the distribution of the backward Markov chain pairChain K.

      source
      theorem CSMC.PreviousState.Model.pairChain_map_swap {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hK : βˆ€ (ya : Pos X n N Γ— Anc n N), Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya)) (hKm : MeasurableKernels K) :
      (M.pairChain K).map Prod.swap = M.pairChain K

      Under the hypotheses of Algorithm S1, pairChain K does not change when the indices of the reference and of the output are exchanged.

      source
      theorem CSMC.PreviousState.Model.isReversible_csmc {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hK : βˆ€ (ya : Pos X n N Γ— Anc n N), Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya)) (hKm : MeasurableKernels K) :
      (M.csmc resdist K).IsReversible M.target

      Proposition S1: for kernels K_T and K_{t,j,j'} as in Algorithm S1, the Markov kernel defined by Algorithm S1 is reversible with respect to Ο€.

      source
      theorem CSMC.PreviousState.Model.isProbabilityMeasure_extMeasure {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hC : βˆ€ (p : Fin N β†’ ℝ), IsProbVector p β†’ C p ∈ Matrix.rowStochastic ℝ (Fin N) ∧ IsReversible p (C p)) (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) :
      MeasureTheory.IsProbabilityMeasure (M.extMeasure resdist C)

      With at least one particle, if the resampling schemes satisfy the condition of Definition S1 and the kernels C(p) are Markov kernels reversible with respect to p, the distribution with the density (S4) is a probability measure.

      source
      theorem CSMC.PreviousState.Model.map_extMeasure_trajOf {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {C : (Fin N β†’ ℝ) β†’ Matrix (Fin N) (Fin N) ℝ} (hC : βˆ€ (p : Fin N β†’ ℝ), IsProbVector p β†’ C p ∈ Matrix.rowStochastic ℝ (Fin N) ∧ IsReversible p (C p)) (hCm : βˆ€ (i j : Fin N), Measurable fun (p : Fin N β†’ ℝ) => C p i j) :
      MeasureTheory.Measure.map (fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => trajOf w.1 w.2.2) (M.extMeasure resdist C) = M.target

      Converse of Lemma S1: under the same hypotheses, if (𝐱, a, b_{1:T}) has the density (S4), then (x_1^{b_1}, …, x_T^{b_T}) ∼ Ο€.

      source
      theorem CSMC.PreviousState.Model.isProbabilityMeasure_posAnc {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) :
      MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => (w.1, w.2.1)) (M.extMeasure resdist gibbs))

      With at least one particle, the distribution of the particle positions and the ancestor indices under the density (S4) with the Gibbs kernels is a probability measure.

      source
      theorem CSMC.PreviousState.Model.isMarkovKernel_pairChain {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (hN : 0 < N) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hK : βˆ€ (ya : Pos X n N Γ— Anc n N), Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya)) (hKm : MeasurableKernels K) :
      ProbabilityTheory.IsMarkovKernel (M.pairChain K)

      With at least one particle, for measurable kernels which satisfy the hypotheses of Algorithm S1, pairChain K is a Markov kernel.

      source
      theorem CSMC.PreviousState.Model.isMarkovKernel_csmc {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hK : βˆ€ (ya : Pos X n N Γ— Anc n N), Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya)) (hKm : MeasurableKernels K) :
      ProbabilityTheory.IsMarkovKernel (M.csmc resdist K)

      With at least one particle, for measurable kernels which satisfy the hypotheses of Algorithm S1, the kernel of Algorithm S1 is a Markov kernel.

      source
      theorem CSMC.PreviousState.Model.invariant_csmc {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hK : βˆ€ (ya : Pos X n N Γ— Anc n N), Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya)) (hKm : MeasurableKernels K) :
      (M.csmc resdist K).Invariant M.target

      With at least one particle, for measurable kernels which satisfy the hypotheses of Algorithm S1, the kernel of Algorithm S1 leaves Ο€ invariant.

      source
      theorem CSMC.PreviousState.Model.isProbVector_bsprob {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (hN : 0 < N) (y : Pos X n N) (a : Anc n N) (s : Fin n) (j : Fin N) :
      IsProbVector fun (i : Fin N) => M.bsprob y a s i j

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

      source
      theorem CSMC.PreviousState.Model.admissible_ruleKernels {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (hN : 0 < N) (r : SelectionRule) (ya : Pos X n N Γ— Anc n N) :
      Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (M.ruleKernels N r ya)

      The kernels of the selection rules, with the probabilities (S3), satisfy the hypotheses of Algorithm S1 at all particle positions and ancestor indices.

      source
      theorem CSMC.PreviousState.Model.pathProb_nonneg' {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) (hN : 0 < N) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hK : βˆ€ (ya : Pos X n N Γ— Anc n N), Admissible (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya)) (ya : Pos X n N Γ— Anc n N) (b l : Idx n N) :
      0 ≀ pathProb (M.weight ya.1 ya.2 (Fin.last n)) (M.bsprob ya.1 ya.2) (K ya) b l

      With at least one particle, for kernels which satisfy the hypotheses of Algorithm S1, the probabilities pathProb of pairChain K are nonnegative.

      source
      theorem CSMC.PreviousState.Model.map_target_compProd_algLaw {X : Type u_1} [MeasurableSpace X] {n N : β„•} {ΞΌ : MeasureTheory.Measure X} (M : Model ΞΌ n) [MeasureTheory.SigmaFinite ΞΌ] (hN : 0 < N) {resdist : Fin n β†’ (Fin N β†’ X) β†’ (Fin N β†’ ℝ) β†’ (Fin N β†’ Fin N) β†’ ℝ} (hr : βˆ€ (s : Fin n), IsUnbiasedResampling (resdist s)) (hrm : βˆ€ (s : Fin n) (a : Fin N β†’ Fin N), Measurable fun (xw : (Fin N β†’ X) Γ— (Fin N β†’ ℝ)) => resdist s xw.1 xw.2 a) {K : Pos X n N Γ— Anc n N β†’ BackwardKernels (Fin N) n} (hKm : MeasurableKernels K) :
      MeasureTheory.Measure.map (fun (z : Traj X n Γ— (Pos X n N Γ— Anc n N Γ— Idx n N) Γ— Idx n N) => ((z.2.1.1, z.2.1.2.1), z.2.1.2.2, z.2.2)) (M.target.compProd (M.algLaw resdist K)) = (MeasureTheory.Measure.map (fun (w : Pos X n N Γ— Anc n N Γ— Idx n N) => (w.1, w.2.1)) (M.extMeasure resdist gibbs)).compProd (M.pairChain K)

      Lemma 4 for Algorithm S1: the joint distribution of the particle positions and the ancestor indices, and of the indices of the reference and of the output, of Algorithm S1 started from x_{1:T} ∼ Ο€ is that of (𝐱, a) under the density (S4) followed by pairChain K.