OAI/Probability/GaussianPropeller/OneCell.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.OneCell.nonneg_of_deriv_nonneg line 29
  2. lemma OAI.GaussianPropeller.OneCell.exp_neg_le_quadratic line 37
  3. lemma OAI.GaussianPropeller.OneCell.exp_neg_ge_cubic line 48
  4. lemma OAI.GaussianPropeller.OneCell.exp_neg_le_quartic line 61
  5. lemma OAI.GaussianPropeller.OneCell.exp_neg_sq_upper line 74
  6. def OAI.GaussianPropeller.OneCell.Q line 78
  7. def OAI.GaussianPropeller.OneCell.P line 79
  8. def OAI.GaussianPropeller.OneCell.P' line 80
  9. def OAI.GaussianPropeller.OneCell.P'' line 82
  10. lemma OAI.GaussianPropeller.OneCell.hasDerivAt_P line 85
  11. lemma OAI.GaussianPropeller.OneCell.hasDerivAt_P' line 92
  12. lemma OAI.GaussianPropeller.OneCell.P''_nonpos line 99
  13. lemma OAI.GaussianPropeller.OneCell.concaveOn_P line 109
  14. lemma OAI.GaussianPropeller.OneCell.P_global_upper line 115
  15. def OAI.GaussianPropeller.OneCell.density line 136
  16. def OAI.GaussianPropeller.OneCell.gaussianConst line 137
  17. def OAI.GaussianPropeller.OneCell.tail line 138
  18. lemma OAI.GaussianPropeller.OneCell.density_integrable line 140
  19. lemma OAI.GaussianPropeller.OneCell.mul_density_integrable line 145
  20. lemma OAI.GaussianPropeller.OneCell.sq_density_integrable line 149
  21. lemma OAI.GaussianPropeller.OneCell.hasDerivAt_density line 155
  22. lemma OAI.GaussianPropeller.OneCell.tendsto_density line 160
  23. lemma OAI.GaussianPropeller.OneCell.tail_first_moment line 166
  24. lemma OAI.GaussianPropeller.OneCell.tail_zero line 175
  25. lemma OAI.GaussianPropeller.OneCell.tail_sub line 182
  26. lemma OAI.GaussianPropeller.OneCell.gaussianConst_bounds line 187
  27. lemma OAI.GaussianPropeller.OneCell.tendsto_mul_density line 199
  28. lemma OAI.GaussianPropeller.OneCell.tail_second_moment line 207
  29. def OAI.GaussianPropeller.OneCell.densityUpper line 218
  30. def OAI.GaussianPropeller.OneCell.densityLower line 219
  31. def OAI.GaussianPropeller.OneCell.densityPrimitive line 220
  32. def OAI.GaussianPropeller.OneCell.densityLowerPrimitive line 221
  33. lemma OAI.GaussianPropeller.OneCell.integral_density_upper line 223
  34. lemma OAI.GaussianPropeller.OneCell.integral_density_lower line 240
  35. lemma OAI.GaussianPropeller.OneCell.tail_second_bound line 259
  36. lemma OAI.GaussianPropeller.OneCell.normalized_excess_small line 274
  37. lemma OAI.GaussianPropeller.OneCell.normalized_excess_large line 295
  38. lemma OAI.GaussianPropeller.OneCell.normalized_excess_bound line 323
  39. lemma OAI.GaussianPropeller.OneCell.integral_gaussianReal_std line 329
  40. lemma OAI.GaussianPropeller.OneCell.integral_excess_gaussian line 337
  41. lemma OAI.GaussianPropeller.OneCell.gaussian_excess_bound line 353
  42. lemma OAI.GaussianPropeller.OneCell.map_unit_inner_gaussian line 362
  43. lemma OAI.GaussianPropeller.OneCell.projection_rearrangement line 369
  44. lemma OAI.GaussianPropeller.OneCell.cell_norm_sq_le line 396
  45. lemma OAI.GaussianPropeller.OneCell.normalized_cell_probability line 432