Repository navigation

Random sampling - #154

Merged

RemyDegenne merged 10 commits into

LeanMachineLearning:mainfrom

gaetanserre:randomSampling

Jul 31, 2026

Commits on Jun 24, 2026

Convergence lemmas for `randomSampling`
gaetanserre
committed
0016684
dosctring
gaetanserre
committed
67cf9e6
imports
gaetanserre
committed
e8e8f65
mk_all
gaetanserre
committed
e395627
Linter
gaetanserre
committed
28386e3
fix import
gaetanserre
committed
6e177e7

Commits on Jun 27, 2026

Merge remote-tracking branch 'origin/main' into randomSampling
RemyDegenne
committed
3467d3b

Commits on Jul 30, 2026

Update LeanMachineLearning/ForMathlib/Topology/Instances/ENNReal/Lemmas.lean

gaetanserre
and
RemyDegenne
authored
94c1f9c
Imports and lint
gaetanserre
committed
3d0e6f6

Commits on Jul 31, 2026

reward -> feedback & actionS -> action
gaetanserre
committed
9586be3