OAI/Analysis/ProductSpaces/ExponentialExcess.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IndependentProducts.exponential_eval_memLp line 16
2. lemma OAI.IndependentProducts.exponential_positive_eval_memLp line 20
3. lemma OAI.IndependentProducts.exponential_positive_eval_mean line 25
4. lemma OAI.IndependentProducts.exponential_positive_eval_second line 34
5. lemma OAI.IndependentProducts.exponentialVariance_tail line 44
6. lemma OAI.IndependentProducts.integrable_exponentialVariance line 58
7. lemma OAI.IndependentProducts.integrable_exponentialMixture line 62
8. lemma OAI.IndependentProducts.excess_scaled_lower line 76
9. lemma OAI.IndependentProducts.exponential_mixture_excess line 84
10. lemma OAI.IndependentProducts.integrable_exponential_linear line 125
11. lemma OAI.IndependentProducts.exponential_scalar_excess_unit line 130
12. lemma OAI.IndependentProducts.excess_threshold_scale line 169
13. lemma OAI.IndependentProducts.exponential_scalar_excess line 176