OAI/Probability/SKRatio/Matrices/PowExponentialPair.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKRatioGaussian.pow_le_exponential_pairline 29 - lemma
OAI.SKRatioGaussian.subgaussian_abs_momentline 44 - lemma
OAI.SKRatioGaussian.stdGaussian_subgaussian_lipschitzline 71 - lemma
OAI.SKRatioGaussian.stdGaussian_abs_centered_momentline 87