OAI/Analysis/ProductSpaces/ExponentialMixture.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentProducts.exponentialVector line 16
  2. instance OAI.IndependentProducts.(instance at line 17) line 17
  3. lemma OAI.IndependentProducts.exponential_eval_hasLaw line 21
  4. lemma OAI.IndependentProducts.exponentialVector_positive line 25
  5. lemma OAI.IndependentProducts.exponential_vector_complexMGF line 30
  6. lemma OAI.IndependentProducts.exponential_vector_characteristic line 40
  7. def OAI.IndependentProducts.exponentialDifference line 54
  8. lemma OAI.IndependentProducts.exponential_difference_charFun line 57
  9. def OAI.IndependentProducts.exponentialVariance line 85
  10. def OAI.IndependentProducts.exponentialMixture line 88
  11. lemma OAI.IndependentProducts.exponentialVariance_nonneg line 91
  12. lemma OAI.IndependentProducts.measurable_exponentialVariance line 95
  13. lemma OAI.IndependentProducts.measurable_exponentialMixture line 99
  14. lemma OAI.IndependentProducts.gaussian_scaled_characteristic line 102
  15. lemma OAI.IndependentProducts.exponential_mixture_charFun line 119
  16. lemma OAI.IndependentProducts.exponential_difference_mixture line 160