infotheo

Here are 2 public repositories matching this topic...

F1uctus / kalman.v

The Kalman filter formalized in Rocq/MathComp: discrete Riccati theory (monotonicity, convergence, a unique stabilizing DARE solution), with executable OCaml extraction via CoqEAL.

extraction estimation dare math-comp typst riccati-equations infotheo linear-estimation rocq-prover coqeal efficient-algebra

Updated Jul 17, 2026
Rocq Prover

F1uctus / rocq2typst

Star

Extract Rocq definitions to clean Typst markup.

extraction opam code-generation math-rendering math-comp infotheo rocq

Updated Jul 12, 2026
Rocq Prover

Improve this page

Add a description, image, and links to the infotheo topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the infotheo topic, visit your repo's landing page and select "manage topics."

Learn more

Provide feedback

Saved searches

Use saved searches to filter your results more quickly