OAI/Probability/SKValue/GroundState/EmpiricalPower.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.rpow_le_add_one line 12
  2. lemma OAI.SKValueG.integrable_rpow_le_one line 21
  3. lemma OAI.SKValueG.integral_rpow_le line 31
  4. lemma OAI.SKValueG.nonneg_integrals_tendsto_of_upper line 39
  5. theorem OAI.SKValueG.expected_rpow_empiricalMean_tendsto line 57
  6. def OAI.SKValueG.gumbelExpMoment line 95
  7. lemma OAI.SKValueG.gumbelExpMoment_pos line 97
  8. lemma OAI.SKValueG.gumbelSmooth_exp line 102
  9. lemma OAI.SKValueG.finite_centered_max_exp_moment line 109
  10. lemma OAI.SKValueG.empirical_branch_exp_identity line 120
  11. theorem OAI.SKValueG.marked_branching_exponential_limit line 132
  12. theorem OAI.SKValueG.marked_branching_exponential_upper line 150