1
Finite index sets
2
The forced move and the coupling kernel
3
Conditional sequential Monte Carlo
4
Validity
5
Comparison of the selection rules
6
Potential functions of the previous state and other resampling schemes
7
Formalization notes
▶
7.1
Indices and types
7.2
The model
7.3
The algorithms
7.4
The statements
Dependency graph
Metropolized backward sampling for conditional sequential Monte Carlo: Lean formalization
Adrien Corenflos
1
Finite index sets
2
The forced move and the coupling kernel
3
Conditional sequential Monte Carlo
4
Validity
5
Comparison of the selection rules
6
Potential functions of the previous state and other resampling schemes
7
Formalization notes
7.1
Indices and types
7.2
The model
7.3
The algorithms
7.4
The statements