OAI/Probability/SKValue/GroundState/ExponentialMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SKValueG.expOneProbability line 12
  2. instance OAI.SKValueG.expOneNoAtoms line 15
  3. lemma OAI.SKValueG.exp_one_density_real line 19
  4. lemma OAI.SKValueG.exp_one_pos_ae line 26
  5. lemma OAI.SKValueG.exp_one_integrable_iff line 34
  6. lemma OAI.SKValueG.exp_one_rpow_integrable line 47
  7. lemma OAI.SKValueG.abs_log_le_two_rpow line 53
  8. lemma OAI.SKValueG.exp_one_log_integrable line 66
  9. def OAI.SKValueG.gumbelLaw line 82
  10. instance OAI.SKValueG.gumbelProbability line 84
  11. lemma OAI.SKValueG.gumbel_cdf line 88
  12. lemma OAI.SKValueG.gumbel_integrable line 100
  13. lemma OAI.SKValueG.gumbel_exp_integrable line 104
  14. def OAI.SKValueG.gumbelMean line 113
  15. lemma OAI.SKValueG.prob_measure_eq_of_cdf line 115