Metropolized backward sampling for conditional sequential Monte Carlo: Lean formalization

The results of the paper Metropolized backward sampling for conditional sequential Monte Carlo by Adrien Corenflos, and of its supplementary material, are formalized in Lean 4 with Mathlib. Every result is proved, and depends only on the axioms propext, Classical.choice, and Quot.sound.

• Blueprint: the statements of the paper, each with its Lean statement and proof.
• Dependency graph of the blueprint.
• API documentation of the Lean code.