OAI/Computability/MinUncut/Analysis/GaussianSmallBall.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.GaussianBudget.pdf_le_one line 11
  2. lemma OAI.MinUncut.GaussianBudget.small_ball line 20
  3. def OAI.MinUncut.GaussianBudget.betweenIndicator line 31
  4. lemma OAI.MinUncut.GaussianBudget.between_measurable line 33
  5. lemma OAI.MinUncut.GaussianBudget.between_integrable line 37
  6. lemma OAI.MinUncut.GaussianBudget.integral_between line 46
  7. lemma OAI.MinUncut.GaussianBudget.independent_small_ball line 53
  8. def OAI.MinUncut.GaussianBudget.signFailure line 77
  9. lemma OAI.MinUncut.GaussianBudget.signFailure_range line 79
  10. lemma OAI.MinUncut.GaussianBudget.signFailure_measurable line 83
  11. lemma OAI.MinUncut.GaussianBudget.signFailure_integrable line 89
  12. lemma OAI.MinUncut.GaussianBudget.signFailure_add_le line 98
  13. lemma OAI.MinUncut.GaussianBudget.signFailure_sumdiff_le line 112
  14. lemma OAI.MinUncut.GaussianBudget.signFailure_triangle line 128
  15. lemma OAI.MinUncut.GaussianBudget.integral_abs_le_sqrt_sq line 133
  16. lemma OAI.MinUncut.GaussianBudget.independent_sign_add line 142
  17. lemma OAI.MinUncut.GaussianBudget.inner_hasGaussianLaw line 155
  18. lemma OAI.MinUncut.GaussianBudget.inner_law line 158
  19. lemma OAI.MinUncut.GaussianBudget.inner_second_moment line 171
  20. lemma OAI.MinUncut.GaussianBudget.orthogonal_indep line 179
  21. lemma OAI.MinUncut.GaussianBudget.sign_inner_le line 187
  22. def OAI.MinUncut.GaussianBudget.score line 218
  23. abbrev OAI.MinUncut.GaussianBudget.vector line 219
  24. lemma OAI.MinUncut.GaussianBudget.score_inner line 221
  25. lemma OAI.MinUncut.GaussianBudget.toLp_preserving line 224
  26. lemma OAI.MinUncut.GaussianBudget.integral_score_sign line 228
  27. lemma OAI.MinUncut.GaussianBudget.sign_score_le line 235
  28. lemma OAI.MinUncut.GaussianBudget.signFailure_mul_right line 240
  29. lemma OAI.MinUncut.GaussianBudget.signFailure_mul line 243
  30. lemma OAI.MinUncut.GaussianBudget.norm_unit line 248
  31. lemma OAI.MinUncut.GaussianBudget.distance_normalize line 251
  32. lemma OAI.MinUncut.GaussianBudget.sign_inner_normalize_le line 270
  33. lemma OAI.MinUncut.GaussianBudget.sign_inner_common_norm line 277
  34. def OAI.MinUncut.FiniteGaussian.evenExp line 291
  35. def OAI.MinUncut.FiniteGaussian.densityPolynomial line 293
  36. def OAI.MinUncut.FiniteGaussian.error line 295
  37. lemma OAI.MinUncut.FiniteGaussian.taylor_exp line 297
  38. lemma OAI.MinUncut.FiniteGaussian.evenExp_error line 307
  39. lemma OAI.MinUncut.FiniteGaussian.density_bounds line 335
  40. lemma OAI.MinUncut.FiniteGaussian.density_positive line 349
  41. lemma OAI.MinUncut.FiniteGaussian.exists_error line 355
  42. def OAI.MinUncut.FiniteGaussian.coefficient line 364
  43. def OAI.MinUncut.FiniteGaussian.primitive line 365
  44. def OAI.MinUncut.FiniteGaussian.qIntegral line 367
  45. lemma OAI.MinUncut.FiniteGaussian.density_sum line 369
  46. lemma OAI.MinUncut.FiniteGaussian.continuous_density line 379
  47. lemma OAI.MinUncut.FiniteGaussian.qIntegral_cast line 383
  48. lemma OAI.MinUncut.FiniteGaussian.qIntegral_pos line 396
  49. def OAI.MinUncut.FiniteGaussian.endpoint line 403
  50. def OAI.MinUncut.FiniteGaussian.midpoint line 404
  51. def OAI.MinUncut.FiniteGaussian.cellWeight line 406
  52. lemma OAI.MinUncut.FiniteGaussian.endpoint_zero line 409
  53. lemma OAI.MinUncut.FiniteGaussian.endpoint_end line 410
  54. lemma OAI.MinUncut.FiniteGaussian.endpoint_lt line 416
  55. lemma OAI.MinUncut.FiniteGaussian.cellWeight_pos line 424
  56. lemma OAI.MinUncut.FiniteGaussian.sum_cellWeight line 428
  57. lemma OAI.MinUncut.FiniteGaussian.endpoint_mono line 444
  58. def OAI.MinUncut.FiniteGaussian.cell line 451
  59. lemma OAI.MinUncut.FiniteGaussian.cell_subset line 454
  60. lemma OAI.MinUncut.FiniteGaussian.exists_cell line 464
  61. lemma OAI.MinUncut.FiniteGaussian.disjoint_cells line 472
  62. lemma OAI.MinUncut.FiniteGaussian.midpoint_distance line 481
  63. def OAI.MinUncut.FiniteGaussian.cube line 495
  64. def OAI.MinUncut.FiniteGaussian.cubeCell line 496
  65. def OAI.MinUncut.FiniteGaussian.gridPoint line 497
  66. lemma OAI.MinUncut.FiniteGaussian.cubeCell_measurable line 499
  67. lemma OAI.MinUncut.FiniteGaussian.cube_measurable line 502
  68. lemma OAI.MinUncut.FiniteGaussian.cubeCell_subset line 506
  69. lemma OAI.MinUncut.FiniteGaussian.cube_union line 512
  70. lemma OAI.MinUncut.FiniteGaussian.cubeCell_disjoint line 522
  71. def OAI.MinUncut.FiniteGaussian.gridStep line 532
  72. lemma OAI.MinUncut.FiniteGaussian.gridStep_of_mem line 535
  73. lemma OAI.MinUncut.FiniteGaussian.gridStep_of_notMem line 546
  74. lemma OAI.MinUncut.FiniteGaussian.gridStep_range line 552
  75. lemma OAI.MinUncut.FiniteGaussian.gridStep_integrable line 561
  76. lemma OAI.MinUncut.FiniteGaussian.integral_gridStep line 565
  77. lemma OAI.MinUncut.FiniteGaussian.setIntegral_gridStep line 574
  78. abbrev OAI.MinUncut.FiniteGaussian.gaussianLaw line 585
  79. lemma OAI.MinUncut.FiniteGaussian.coordinate_sq_integrable line 588
  80. lemma OAI.MinUncut.FiniteGaussian.coordinate_second_moment line 592
  81. lemma OAI.MinUncut.FiniteGaussian.gaussian_cube_tail line 602
  82. def OAI.MinUncut.FiniteGaussian.thresholdBit line 638
  83. def OAI.MinUncut.FiniteGaussian.thresholdTable line 640
  84. lemma OAI.MinUncut.FiniteGaussian.thresholdBit_measurable line 643
  85. lemma OAI.MinUncut.FiniteGaussian.thresholdTable_measurable line 647
  86. lemma OAI.MinUncut.FiniteGaussian.tableTest_integrable line 652
  87. lemma OAI.MinUncut.FiniteGaussian.score_law line 659
  88. lemma OAI.MinUncut.FiniteGaussian.score_small_ball line 667
  89. lemma OAI.MinUncut.FiniteGaussian.score_grid_distance line 674
  90. lemma OAI.MinUncut.FiniteGaussian.threshold_change_small line 688
  91. lemma OAI.MinUncut.FiniteGaussian.tableTest_rounding_pointwise line 702