Repository navigation

Random sampling - #154

Merged

RemyDegenne merged 10 commits into

LeanMachineLearning:mainfrom

gaetanserre:randomSampling

Jul 31, 2026

Merged

Random sampling#154
RemyDegenne merged 10 commits into
LeanMachineLearning:mainfrom
gaetanserre:randomSampling

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