Basic Probability Formalization in Lean

A lean proof that stationary policies can be optimal and can be computed using dynamic programming

See https://formalproofs.github.io/Probability

Lean

Most useful

• Overview of tactics: https://github.com/madvorak/lean4-tactics
• Comprehensive list of tactics: https://seasawher.github.io/mathlib4-help/tactics/
• Loogle: https://loogle.lean-lang.org/
• Moogle: https://www.moogle.ai/

Others

• Blueprint: https://github.com/PatrickMassot/leanblueprint
• Lean packages and extensions: https://reservoir.lean-lang.org/
• Notations: https://github.com/leanprover-community/lean4-mode/blob/master/data/abbreviations.json