OAI/Probability/Ballisticity/Estimates/SymmetrizedMgf.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.symmetrized_mgf line 22
  2. lemma OAI.DirectionalTransience.symmetrized_complexMGF line 27
  3. lemma OAI.DirectionalTransience.iid_difference_gaussian_mgf_product line 34
  4. lemma OAI.DirectionalTransience.iid_difference_gaussian_integrableExpSet line 40
  5. lemma OAI.DirectionalTransience.exp_mean_le_mgf line 50
  6. lemma OAI.DirectionalTransience.iid_difference_gaussian_mgf_bound line 63
  7. theorem OAI.DirectionalTransience.iid_difference_gaussian line 75
  8. lemma OAI.DirectionalTransience.map_iid_difference_linear line 127
  9. theorem OAI.DirectionalTransience.iid_difference_isGaussian line 142
  10. lemma OAI.DirectionalTransience.iid_difference_gaussian_centered_linear line 156