Documentation

MetropolizedBackwardSampling.PreviousState.BackwardAncestorsSampling

Backward passes from the ancestors after ancestor sampling #

In the supplementary material, the paragraph after Proposition S4 reads: the proof uses Algorithm S2.a only through b_T โˆผ W_T conditionally on (๐ฑ, a), which holds for all the kernels of Lemma S1, so that the invariance also holds with ancestor sampling in Algorithm S2.a.

In Algorithm S2.a, steps (a) and (b) of Algorithm S1 are run with c = b_t, that is, with the identity kernels. Here, they are run with c drawn from C(B_t(ยท|x_{t+1}))(b_t, ยท), for a function C from probability vectors p to Markov kernels reversible with respect to p, as are the kernels K_{t,j,j} of the six selection rules. With the Gibbs kernels of BS and FM-BS, this is ancestor sampling, as in Algorithm S1.b. They are followed by the backward pass from the ancestors, with the kernels of a selection rule. The resulting Markov kernel leaves ฯ€ invariant (invariant_csmcAncWith).

By Lemma S1 for C, (๐ฑ, a, b_{1:T}) has the density (S4) with K_{t,j,j} = C(B_t(ยท|j)). The backward pass depends on b_{1:T} only through b_T. The joint distribution of (๐ฑ, a) and of b_T does not depend on C (map_extMeasure_last_eq). The particle positions, the ancestor indices, and the indices of the output therefore have the same distribution as with the identity kernels, which is the density (S4) with the indices of the output in place of those of the reference and with the kernels K_{t,j,j} of the selection rule, by the proof of Proposition S4. Then xฬƒ_{1:T} โˆผ ฯ€ by the converse of Lemma S1.

source
noncomputable def CSMC.PreviousState.Model.algLawAncWith {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) โ„) (r : SelectionRule) :
ProbabilityTheory.Kernel (Traj X n) ((Pos X n N ร— Anc n N ร— Idx n N) ร— Idx n N)

The joint distribution, given the reference trajectory, of the particle positions, the ancestor indices, and the indices of the reference, (y, a, b), and of the indices l of the output, generated by Algorithm S2 with the resampling scheme resdist and the kernels of the selection rule r, with c drawn from C(B_t(ยท|x_{t+1}))(b_t, ยท) in place of c = b_t in Algorithm S2.a.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CSMC.PreviousState.Model.csmcAncWith {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) โ„) (r : SelectionRule) :
    ProbabilityTheory.Kernel (Traj X n) (Traj X n)

    The Markov kernel defined by Algorithm S2 with the resampling scheme resdist and the kernels of the selection rule r, with c drawn from C(B_t(ยท|x_{t+1}))(b_t, ยท) in place of c = b_t in Algorithm S2.a.

    Equations
    Instances For
      source
      theorem CSMC.PreviousState.Model.csmcAncWith_one {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) โ†’ โ„) (r : SelectionRule) :
      M.csmcAncWith resdist (fun (x : Fin N โ†’ โ„) => 1) r = M.csmcAnc resdist r

      With the identity kernels, c = b_t, as in Algorithm S2.a.

      source
      instance CSMC.PreviousState.Model.instIsSFiniteKernelTrajProdPosAncIdxAlgLawAncWith {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) โ„) (r : SelectionRule) :
      ProbabilityTheory.IsSFiniteKernel (M.algLawAncWith resdist C r)

      The joint distribution algLawAncWith is an s-finite kernel.

      source
      instance CSMC.PreviousState.Model.instIsSFiniteKernelTrajCsmcAncWith {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) โ„) (r : SelectionRule) :
      ProbabilityTheory.IsSFiniteKernel (M.csmcAncWith resdist C r)

      The kernel csmcAncWith is an s-finite kernel.

      source
      theorem CSMC.PreviousState.Model.map_target_compProd_algLawAncWith_eq {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) (r : SelectionRule) :
      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.2)) (M.target.compProd (M.algLawAncWith resdist C r)) = MeasureTheory.Measure.map (fun (v : ((Pos X n N ร— Anc n N) ร— Fin N) ร— Idx n N) => (v.1.1.1, v.1.1.2, v.2)) ((MeasureTheory.Measure.map (fun (w : Pos X n N ร— Anc n N ร— Idx n N) => ((w.1, w.2.1), w.2.2 (Fin.last n))) (M.extMeasure resdist C)).compProd (backwardPassAnc (M.ruleKernels N r) Prod.snd))

      If the resampling schemes satisfy the condition of Definition S1 and each C(p) is reversible with respect to p, the particle positions, the ancestor indices, and the indices of the output of algLawAncWith started from x_{1:T} โˆผ ฯ€ have the distribution of (๐ฑ, a) and of b_T under the density (S4) with K_{t,j,j} = C(B_t(ยท|j)), followed by the backward pass from the ancestors.

      source
      theorem CSMC.PreviousState.Model.map_target_compProd_algLawAncWith {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) (r : SelectionRule) :
      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.2)) (M.target.compProd (M.algLawAncWith resdist C r)) = M.extMeasure resdist r.diagKernel

      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 particle positions, the ancestor indices, and the indices of the output of algLawAncWith started from x_{1:T} โˆผ ฯ€ have the density (S4), with the indices of the output in place of those of the reference and with the kernels K_{t,j,j} of the selection rule.

      source
      theorem CSMC.PreviousState.Model.invariant_csmcAncWith {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) (r : SelectionRule) :
      (M.csmcAncWith resdist C r).Invariant M.target

      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 Markov kernel defined by Algorithm S2, with c drawn from C(B_t(ยท|x_{t+1}))(b_t, ยท) in place of c = b_t in Algorithm S2.a, leaves ฯ€ invariant.