OAI/Probability/SKValue/GroundState/CascadeMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKValueG.CascadeShape line 12
  2. abbrev OAI.SKValueG.CascadeWidths line 13
  3. def OAI.SKValueG.cascadeLaw line 17
  4. instance OAI.SKValueG.cascadeLaw_probability line 21
  5. def OAI.SKValueG.CascadeScale line 29
  6. def OAI.SKValueG.cascadeMoment line 33
  7. lemma OAI.SKValueG.branchLaw_exp_integrable line 37
  8. lemma OAI.SKValueG.cascadeMoment_pos line 44
  9. lemma OAI.SKValueG.cascadeLaw_integrable line 54
  10. lemma OAI.SKValueG.cascadeLaw_exp_integrable line 62
  11. theorem OAI.SKValueG.cascadeLaw_exp_upper line 75
  12. theorem OAI.SKValueG.cascadeMoment_mem_closure line 91
  13. def OAI.SKValueG.cascadeMean line 113
  14. theorem OAI.SKValueG.cascadeMean_mem_closure line 117