mathlib3
feat(probability/subgaussian): define sub-Gaussian random variables
#15141
Open
Overview
Commits
41
Changes
View On GitHub
Commits
  • add chernoff bound
    RemyDegenne committed 3 years ago
  • add left tail versions
    RemyDegenne committed 3 years ago
  • independence of joint r.v.
    RemyDegenne committed 3 years ago
  • move a lemma
    RemyDegenne committed 3 years ago
  • change names
    RemyDegenne committed 3 years ago
  • docstrings
    RemyDegenne committed 3 years ago
  • expand docstring
    RemyDegenne committed 3 years ago
  • fix
    RemyDegenne committed 3 years ago
  • docstrings
    RemyDegenne committed 3 years ago
  • spaces
    RemyDegenne committed 3 years ago
  • make variables implicit
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/RD_indep_comp' into RD_subgaussian
    RemyDegenne committed 3 years ago
  • copy
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/RD_chernoff_bound' into RD_subgaussian
    RemyDegenne committed 3 years ago
  • no sorry left
    RemyDegenne committed 3 years ago
  • remove pos hypothesis
    RemyDegenne committed 3 years ago
  • move things
    RemyDegenne committed 3 years ago
  • version with mean instead of sum
    RemyDegenne committed 3 years ago
  • remove example
    RemyDegenne committed 3 years ago
  • replace big rw by tactics
    RemyDegenne committed 3 years ago
  • move lemmas
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/RD_subgaussian' into RD_mgf_sum
    RemyDegenne committed 3 years ago
  • remove subgaussian
    RemyDegenne committed 3 years ago
  • move sum lemmas up
    RemyDegenne committed 3 years ago
  • fix lint
    RemyDegenne committed 3 years ago
  • add file docstring
    RemyDegenne committed 3 years ago
  • add section
    RemyDegenne committed 3 years ago
  • change names
    RemyDegenne committed 3 years ago
  • change names
    RemyDegenne committed 3 years ago
  • move to_real_prob_le_one
    RemyDegenne committed 3 years ago
  • change names
    RemyDegenne committed 3 years ago
  • docstrings
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/RD_mgf_sum' into RD_subgaussian
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into RD_mgf_sum
    RemyDegenne committed 3 years ago
  • fix
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/RD_mgf_sum' into RD_subgaussian
    RemyDegenne committed 3 years ago
  • open real
    RemyDegenne committed 3 years ago
  • remove some real.
    RemyDegenne committed 3 years ago
  • fix
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into RD_subgaussian
    RemyDegenne committed 3 years ago
  • fix
    RemyDegenne committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading