mathlib3
feat(probability/subgaussian): define sub-Gaussian random variables
#15141
Open
Open
feat(probability/subgaussian): define sub-Gaussian random variables #15141
RemyDegenne
wants to merge
41 commits into
master
from
RD_subgaussian
add chernoff bound
328544aa
add left tail versions
79b7bd6d
independence of joint r.v.
f54cae01
move a lemma
0c6f4a4c
change names
a5a6793e
docstrings
fff66bc1
expand docstring
1e37849c
fix
d0e12f91
docstrings
616bd056
spaces
b1d4ab74
make variables implicit
be37190d
Merge remote-tracking branch 'origin/RD_indep_comp' into RD_subgaussian
ae0382c0
copy
98eff175
Merge remote-tracking branch 'origin/RD_chernoff_bound' into RD_subga…
2a612356
no sorry left
aff1b5ba
remove pos hypothesis
7e8f9433
move things
6d96d0eb
version with mean instead of sum
88bbb832
remove example
1a0618f2
replace big rw by tactics
f0ab1d51
move lemmas
26f5e263
Merge remote-tracking branch 'origin/RD_subgaussian' into RD_mgf_sum
b20788e8
remove subgaussian
617de097
move sum lemmas up
6834b24a
fix lint
d4c2ec6b
add file docstring
3449effa
add section
650cbacb
change names
1e2e5d00
change names
a4d9a518
move to_real_prob_le_one
ae1645cf
change names
880a3e29
docstrings
50dca103
Merge remote-tracking branch 'origin/RD_mgf_sum' into RD_subgaussian
5306d1e8
Merge remote-tracking branch 'origin/master' into RD_mgf_sum
22a1ed9c
fix
e61dedc3
Merge remote-tracking branch 'origin/RD_mgf_sum' into RD_subgaussian
225bf74f
open real
7253b291
remove some real.
3a251721
fix
1a92cee6
Merge remote-tracking branch 'origin/master' into RD_subgaussian
424a04e4
fix
c8f50cde
sgouezel
commented
on 2022-07-31
Reviewers
Assignees
No one assigned
Labels
WIP
t-measure-probability
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub