Skip to content

Add tutorial pages about probability - #90

Merged
RemyDegenne merged 3 commits into
mainfrom
doc
Apr 23, 2026
Merged

RemyDegenne merged 3 commits into
mainfrom
doc

Conversation

@RemyDegenne

@RemyDegenne RemyDegenne commented Apr 20, 2026 •

Copy link
Copy Markdown
Collaborator

Add 3 tutorial pages

  • basic probability, adapted from my blog post on the lean community website
  • Markov kernels (the section about composition is still TODO)
  • Stochastic processes and martingales. Still rough.

@RemyDegenne
RemyDegenne marked this pull request as ready for review April 23, 2026 13:41
@RemyDegenne
RemyDegenne merged commit 8594a37 into main Apr 23, 2026
1 check passed
@RemyDegenne
RemyDegenne deleted the doc branch April 23, 2026 13:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant