OAI/Probability/SKValue/GroundState/BranchLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValueG.branchMax line 12
  2. lemma OAI.SKValueG.continuous_branchMax line 16
  3. def OAI.SKValueG.branchLaw line 20
  4. instance OAI.SKValueG.branchLaw_probability line 24
  5. lemma OAI.SKValueG.integrable_finiteMaximum_of_integrable line 29
  6. lemma OAI.SKValueG.branchMax_integrable line 36
  7. lemma OAI.SKValueG.branchLaw_integrable line 49
  8. lemma OAI.SKValueG.branchMax_exp_integrable line 55
  9. lemma OAI.SKValueG.branchLaw_integral line 81
  10. lemma OAI.SKValueG.branchLaw_exp_integral line 89
  11. lemma OAI.SKValueG.iid_sequence_law line 98
  12. lemma OAI.SKValueG.iid_finite_law line 102
  13. lemma OAI.SKValueG.integrable_exp_smaller line 119
  14. lemma OAI.SKValueG.iid_branchIntegral line 133
  15. lemma OAI.SKValueG.branchLaw_test line 142
  16. lemma OAI.SKValueG.gumbelSmooth_id line 152
  17. theorem OAI.SKValueG.branchLaw_test_tendsto line 157
  18. theorem OAI.SKValueG.branchLaw_mean_tendsto line 178
  19. theorem OAI.SKValueG.branchLaw_exp_tendsto line 185
  20. theorem OAI.SKValueG.branchLaw_exp_upper line 205