Work on ETC - #32

Merged

RemyDegenne merged 11 commits into

mainfrom

Sep 29, 2025

Commits on Sep 28, 2025

small progress
RemyDegenne
committed
f62164a
Merge remote-tracking branch 'origin/main' into work
RemyDegenne
committed
05d330a
extract indepFun lemmas
RemyDegenne
committed
cacf71d

Commits on Sep 29, 2025

more subGaussian lemmas
RemyDegenne
committed
679bc72
use new subgaussian lemma
RemyDegenne
committed
73643a0
minor
RemyDegenne
committed
02f102c
extract aux lemma
RemyDegenne
committed
595aa27
add IdentDistrib.prod
RemyDegenne
committed
6fd8efd
deal with the very annoying measurability sorry
RemyDegenne
committed
be5fb37
generalize measurability lemma
RemyDegenne
committed
a15aed9
move lemmas
RemyDegenne
committed
4a5aa87