Repository navigation

feat: require Statlib, bump Mathlib to 2ddf59c - #298

Merged

RemyDegenne merged 7 commits into

mainfrom

require-statlib

Nov 13, 2026

Merged

feat: require Statlib, bump Mathlib to 2ddf59c#298
RemyDegenne merged 7 commits into
mainfrom
require-statlib

Commits on Nov 13, 2026
- chore: require Statlib and bump Mathlib to 2ddf59c
  
  RemyDegenne
  and
  claude
  committed
  d2388af
- fix(Tutorial): adapt the martingale convergence example to Mathlib
  
  RemyDegenne
  and
  claude
  committed
  aab284a
- refactor: use Statlib's copies of three KL and Radon-Nikodym lemmas
  
  RemyDegenne
  and
  claude
  committed
  5689645
- refactor: derive KL divergence results from Statlib
  
  RemyDegenne
  and
  claude
  committed
  99fdb87
- refactor: use Statlib's kernel measurable space, chain rule and convexity
  
  RemyDegenne
  and
  claude
  committed
  edad3c0
- chore: get Mathlib through Statlib
  
  RemyDegenne
  and
  claude
  committed
  628e9d0
- ci: bump Statlib instead of Mathlib
  
  RemyDegenne
  and
  claude
  committed
  93719c7