OAI/Probability/SKRatio/Matrices/GaussianSquareTails.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatioClock.Regression.integrable_bounded_lipschitz line 13
  2. lemma OAI.SKRatioClock.Regression.bounded_product_lipschitz line 20
  3. lemma OAI.SKRatioClock.Regression.gaussian_integrable_exp_quarter_sq line 40
  4. lemma OAI.SKRatioClock.Regression.iid_upper_deviation_of_log_mgf line 56
  5. def OAI.SKRatioClock.Regression.squareTail line 89
  6. lemma OAI.SKRatioClock.Regression.squareTail_nonneg line 91
  7. lemma OAI.SKRatioClock.Regression.squareTail_le line 95
  8. lemma OAI.SKRatioClock.Regression.measurable_squareTail line 99
  9. lemma OAI.SKRatioClock.Regression.integrable_exp_squareTail line 104
  10. lemma OAI.SKRatioClock.Regression.tendsto_squareTail_mgf line 112
  11. def OAI.SKRatioClock.Regression.ExponentialSquareTails line 132
  12. theorem OAI.SKRatioClock.Regression.iid_exponential_squareTails line 137
  13. theorem OAI.SKRatioClock.Regression.gaussian_exponential_squareTails line 178
  14. lemma OAI.SKRatioClock.Regression.squareTail_perturbation line 184
  15. theorem OAI.SKRatioClock.Regression.ExponentialSquareTails.l2_stability line 198
  16. lemma OAI.SKRatioClock.Regression.squareTail_add line 228
  17. lemma OAI.SKRatioClock.Regression.squareTail_antitone line 247
  18. theorem OAI.SKRatioClock.Regression.ExponentialSquareTails.add line 252
  19. lemma OAI.SKRatioClock.Regression.squareTail_mul line 286
  20. lemma OAI.SKRatioClock.Regression.ExponentialSquareTails.bounded_mul line 299
  21. def OAI.SKRatioClock.Regression.clippedSquare line 322
  22. lemma OAI.SKRatioClock.Regression.clippedSquare_bounds line 324
  23. lemma OAI.SKRatioClock.Regression.clippedSquare_error line 332
  24. lemma OAI.SKRatioClock.Regression.clippedSquare_lipschitz line 340
  25. lemma OAI.SKRatioClock.Regression.integrable_clippedSquare line 353
  26. lemma OAI.SKRatioClock.Regression.tendsto_integral_clippedSquare line 360
  27. theorem OAI.SKRatioClock.Regression.ExponentialEmpiricalConcentration.secondMoment line 377
  28. lemma OAI.SKRatioClock.Regression.exponentialSquareTails_of_bounded line 432