Documentation

MetropolizedBackwardSampling.PreviousState.Marginal

The distribution of the particle positions and the ancestor indices under (S4) #

In the supplementary material, the paragraph after Lemma S1 reads: the density (S4) is the product of a function of (๐ฑ, a) and of W_T^{b_T} โˆ_t K_{t,b_{t+1},b_{t+1}}(a_t^{b_{t+1}}, b_t), which is a probability distribution of b_{1:T}. Hence the marginal density of (๐ฑ, a) does not depend on the selection rule. Conditionally on (๐ฑ, a), b_T โˆผ W_T and, for t = T - 1, โ€ฆ, 1, given also b_{t+1:T}, b_t โˆผ K_{t,b_{t+1},b_{t+1}}(a_t^{b_{t+1}}, ยท).

These claims are proved here for the density (S4) with K_{t,j,j} = C(B_t(ยท|j)), for every function C from probability vectors to Markov kernels, as are the kernels K_{t,j,j} of the six selection rules. The function of (๐ฑ, a) is posAncDensity. The distribution with this density is posAncMeasure. The conditional distribution of b_{1:T} given (๐ฑ, a) is the backward Markov chain refChain C, a Markov kernel (isMarkovKernel_refChain). The distribution (S4) is posAncMeasure followed by refChain C (map_extMeasure_eq_compProd). The marginal of (๐ฑ, a) is therefore posAncMeasure (map_extMeasure_posAnc), which does not depend on C.

The joint distribution of (๐ฑ, a) and of b_T does not depend on C either (map_extMeasure_last_eq): conditionally on (๐ฑ, a), b_T โˆผ W_T.

source
theorem CSMC.PreviousState.Model.measurable_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) โ†’ โ„} (hrm : โˆ€ (s : Fin n) (a : Fin N โ†’ Fin N), Measurable fun (xw : (Fin N โ†’ X) ร— (Fin N โ†’ โ„)) => resdist s xw.1 xw.2 a) :
Measurable fun (ya : Pos X n N ร— Anc n N) => M.posAncDensity resdist ya.1 ya.2

For resampling schemes which are measurable functions of the particles and the weights, the factor of the density (S4) which depends on the particle positions and the ancestor indices only is a measurable function of these.

source
noncomputable def CSMC.PreviousState.Model.posAncMeasure {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) โ†’ โ„) :
MeasureTheory.Measure (Pos X n N ร— Anc n N)

The distribution of the particle positions and the ancestor indices with the density posAncDensity, the factor of the density (S4) which depends on them only, with respect to the product of ฮผ on each particle position and of the counting measure on the ancestor indices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance CSMC.PreviousState.Model.instSFiniteProdPosAncPosAncMeasureOfSigmaFinite {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) โ†’ โ„) :
    MeasureTheory.SFinite (M.posAncMeasure resdist)

    The distribution posAncMeasure is s-finite.

    source
    theorem CSMC.PreviousState.Model.lintegral_posAncMeasure {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) {g : Pos X n N ร— Anc n N โ†’ ENNReal} (hg : Measurable g) :
    โˆซโป (ya : Pos X n N ร— Anc n N), g ya โˆ‚M.posAncMeasure resdist = โˆซโป (y : Fin (n + 1) ร— Fin N โ†’ X), โˆ‘ a : Anc n N, M.posAncDensity resdist y a * g (y, a) โˆ‚MeasureTheory.Measure.pi fun (x : Fin (n + 1) ร— Fin N) => ฮผ

    Integrals with respect to posAncMeasure are integrals over the particle positions of sums over the ancestor indices of posAncDensity times the integrand.

    source
    theorem CSMC.PreviousState.Model.measurable_refChainProb {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) {C : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„} (hCm : โˆ€ (i j : Fin N), Measurable fun (p : Fin N โ†’ โ„) => C p i j) (b : Idx n N) :
    Measurable fun (ya : Pos X n N ร— Anc n N) => M.weight ya.1 ya.2 (Fin.last n) (b (Fin.last n)) * โˆ s : Fin n, C (fun (i : Fin N) => M.bsprob ya.1 ya.2 s i (b s.succ)) (ya.2 s (b s.succ)) (b s.castSucc)

    For kernels C(p) whose entries are measurable functions of p, the probability W_T^{b_T} โˆ_t C(B_t(ยท|b_{t+1}))(a_t^{b_{t+1}}, b_t) of the indices b of the reference is a measurable function of the particle positions and the ancestor indices.

    source
    noncomputable def CSMC.PreviousState.Model.refChain {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) (C : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„) :
    ProbabilityTheory.Kernel (Pos X n N ร— Anc n N) (Idx n N)

    The backward Markov chain of the indices of the reference given the particle positions and the ancestor indices, under the density (S4) with K_{t,j,j} = C(B_t(ยท|j)): the kernel with mass function b โ†ฆ W_T^{b_T} โˆ_t C(B_t(ยท|b_{t+1}))(a_t^{b_{t+1}}, b_t), under which b_T โˆผ W_T and, for t = T - 1, โ€ฆ, 1, given b_{t+1:T}, b_t โˆผ C(B_t(ยท|b_{t+1}))(a_t^{b_{t+1}}, ยท).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CSMC.PreviousState.Model.instIsSFiniteKernelProdPosAncIdxRefChain {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) (C : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„) :
      ProbabilityTheory.IsSFiniteKernel (M.refChain C)

      The backward Markov chain refChain C is an s-finite kernel.

      source
      theorem CSMC.PreviousState.Model.lintegral_refChain {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) {C : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„} (hCm : โˆ€ (i j : Fin N), Measurable fun (p : Fin N โ†’ โ„) => C p i j) (ya : Pos X n N ร— Anc n N) (g : Idx n N โ†’ ENNReal) :
      โˆซโป (b : Idx n N), g b โˆ‚(M.refChain C) ya = โˆ‘ b : Idx n N, ENNReal.ofReal (M.weight ya.1 ya.2 (Fin.last n) (b (Fin.last n)) * โˆ s : Fin n, C (fun (i : Fin N) => M.bsprob ya.1 ya.2 s i (b s.succ)) (ya.2 s (b s.succ)) (b s.castSucc)) * g b

      Integrals with respect to refChain C are sums over the indices of the reference, weighted by W_T^{b_T} โˆ_t C(B_t(ยท|b_{t+1}))(a_t^{b_{t+1}}, b_t).

      source
      theorem CSMC.PreviousState.Model.isMarkovKernel_refChain {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) (hN : 0 < N) {C : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„} (hC : โˆ€ (p : Fin N โ†’ โ„), IsProbVector p โ†’ C p โˆˆ Matrix.rowStochastic โ„ (Fin N)) (hCm : โˆ€ (i j : Fin N), Measurable fun (p : Fin N โ†’ โ„) => C p i j) :
      ProbabilityTheory.IsMarkovKernel (M.refChain C)

      With at least one particle, if the kernels C(p) are Markov kernels for every probability vector p, the probabilities W_T^{b_T} โˆ_t C(B_t(ยท|b_{t+1}))(a_t^{b_{t+1}}, b_t) form a probability distribution of the indices b of the reference: refChain C is a Markov kernel.

      source
      theorem CSMC.PreviousState.Model.sum_prod_kernel_mul_last {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) (hN : 0 < N) {C : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„} (hC : โˆ€ (p : Fin N โ†’ โ„), IsProbVector p โ†’ C p โˆˆ Matrix.rowStochastic โ„ (Fin N)) (y : Pos X n N) (a : Anc n N) (F : Fin N โ†’ ENNReal) :
      โˆ‘ b : Idx n 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))) * F (b (Fin.last n)) = โˆ‘ bT : Fin N, F bT

      With at least one particle, if the kernels C(p) are Markov kernels for every probability vector p, the sum over the indices b of the reference of โˆ_t C(B_t(ยท|b_{t+1}))(a_t^{b_{t+1}}, b_t) times a function of b_T is the sum of this function over b_T.

      source
      theorem CSMC.PreviousState.Model.map_extMeasure_eq_compProd {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) โ†’ โ„} (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)) (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) => ((w.1, w.2.1), w.2.2)) (M.extMeasure resdist C) = (M.posAncMeasure resdist).compProd (M.refChain C)

      With at least one particle, if the kernels C(p) are Markov kernels for every probability vector p, the distribution (S4), with K_{t,j,j} = C(B_t(ยท|j)), is the distribution of (๐ฑ, a) with the density posAncDensity followed by the backward Markov chain refChain C of the indices of the reference.

      source
      theorem CSMC.PreviousState.Model.map_extMeasure_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) โ†’ โ„} (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)) (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) => (w.1, w.2.1)) (M.extMeasure resdist C) = M.posAncMeasure resdist

      With at least one particle, if the kernels C(p) are Markov kernels for every probability vector p, the marginal distribution of the particle positions and the ancestor indices under the density (S4), with K_{t,j,j} = C(B_t(ยท|j)), is posAncMeasure, which does not depend on C.

      source
      theorem CSMC.PreviousState.Model.lintegral_map_extMeasure_last {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) (hN : 0 < 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) โ„} (hC : โˆ€ (p : Fin N โ†’ โ„), IsProbVector p โ†’ C p โˆˆ Matrix.rowStochastic โ„ (Fin N)) (hCm : โˆ€ (i j : Fin N), Measurable fun (p : Fin N โ†’ โ„) => C p i j) {h : (Pos X n N ร— Anc n N) ร— Fin N โ†’ ENNReal} (hh : Measurable h) :
      โˆซโป (v : (Pos X n N ร— Anc n N) ร— Fin N), h v โˆ‚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) = โˆซโป (y : Fin (n + 1) ร— Fin N โ†’ X), โˆ‘ a : Anc n N, M.posAncDensity resdist y a * โˆ‘ bT : Fin N, ENNReal.ofReal (M.weight y a (Fin.last n) bT) * h ((y, a), bT) โˆ‚MeasureTheory.Measure.pi fun (x : Fin (n + 1) ร— Fin N) => ฮผ

      With at least one particle, if the kernels C(p) are Markov kernels for every probability vector p, integrals with respect to the joint distribution of (๐ฑ, a) and of b_T under the density (S4), with K_{t,j,j} = C(B_t(ยท|j)), are integrals over the particle positions of sums over the ancestor indices of posAncDensity times the sum over b_T of W_T^{b_T} times the integrand: conditionally on (๐ฑ, a), b_T โˆผ W_T.

      source
      theorem CSMC.PreviousState.Model.map_extMeasure_last_eq {X : Type u_1} [MeasurableSpace X] {n N : โ„•} {ฮผ : MeasureTheory.Measure X} (M : Model ฮผ n) (hN : 0 < 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 C' : (Fin N โ†’ โ„) โ†’ Matrix (Fin N) (Fin N) โ„} (hC : โˆ€ (p : Fin N โ†’ โ„), IsProbVector p โ†’ C p โˆˆ Matrix.rowStochastic โ„ (Fin N)) (hCm : โˆ€ (i j : Fin N), Measurable fun (p : Fin N โ†’ โ„) => C p i j) (hC' : โˆ€ (p : Fin N โ†’ โ„), IsProbVector p โ†’ C' p โˆˆ Matrix.rowStochastic โ„ (Fin N)) (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) => ((w.1, w.2.1), w.2.2 (Fin.last n))) (M.extMeasure resdist C) = 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')

      With at least one particle, if the kernels C(p) and C'(p) are Markov kernels for every probability vector p, the joint distribution of (๐ฑ, a) and of b_T is the same under the density (S4) with K_{t,j,j} = C(B_t(ยท|j)) as with K_{t,j,j} = C'(B_t(ยท|j)).