OAI/Computability/MinUncut/Estimates/Basic.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.GaussianHermite.γ line 14
  2. def OAI.MinUncut.GaussianHermite.he line 16
  3. lemma OAI.MinUncut.GaussianHermite.integrable_poly line 18
  4. lemma OAI.MinUncut.GaussianHermite.integrable_poly_density line 27
  5. lemma OAI.MinUncut.GaussianHermite.density_derivative line 46
  6. lemma OAI.MinUncut.GaussianHermite.stein_poly line 61
  7. def OAI.MinUncut.GaussianHermite.hePoly line 88
  8. lemma OAI.MinUncut.GaussianHermite.hePoly_eval line 90
  9. lemma OAI.MinUncut.GaussianHermite.hePoly_zero line 93
  10. lemma OAI.MinUncut.GaussianHermite.hePoly_succ line 95
  11. lemma OAI.MinUncut.GaussianHermite.derivative_hePoly line 98
  12. lemma OAI.MinUncut.GaussianHermite.hePoly_adjoint line 107
  13. lemma OAI.MinUncut.GaussianHermite.he_zero line 129
  14. lemma OAI.MinUncut.GaussianHermite.he_mean_succ line 131
  15. lemma OAI.MinUncut.GaussianHermite.he_product line 134
  16. lemma OAI.MinUncut.GaussianHermite.measure_eq_of_moments line 156
  17. lemma OAI.MinUncut.GaussianHermite.memLp_poly line 188
  18. lemma OAI.MinUncut.GaussianHermite.memLp_exp line 194
  19. lemma OAI.MinUncut.GaussianHermite.memLp_positivePart line 202
  20. lemma OAI.MinUncut.GaussianHermite.weighted_finite line 210
  21. lemma OAI.MinUncut.GaussianHermite.weighted_expSet line 215
  22. lemma OAI.MinUncut.GaussianHermite.integral_weighted line 225
  23. lemma OAI.MinUncut.GaussianHermite.ae_zero_of_integral_poly_eq_zero line 233
  24. def OAI.MinUncut.GaussianHermite.heSequence line 270
  25. lemma OAI.MinUncut.GaussianHermite.heSequence_span line 275
  26. lemma OAI.MinUncut.GaussianHermite.ae_zero_of_integral_he_eq_zero line 282
  27. def OAI.MinUncut.GaussianHermite.H line 301
  28. lemma OAI.MinUncut.GaussianHermite.sqrt_factorial_pos line 303
  29. lemma OAI.MinUncut.GaussianHermite.memLp_H line 306
  30. lemma OAI.MinUncut.GaussianHermite.H_product line 311
  31. lemma OAI.MinUncut.GaussianHermite.integral_inner_toLp line 321
  32. def OAI.MinUncut.GaussianHermite.Hvec line 329
  33. lemma OAI.MinUncut.GaussianHermite.Hvec_orthonormal line 331
  34. lemma OAI.MinUncut.GaussianHermite.eq_zero_of_inner_Hvec_eq_zero line 336
  35. def OAI.MinUncut.GaussianHermite.hermiteBasis line 356
  36. abbrev OAI.MinUncut.GaussianHermite.γpi line 368
  37. lemma OAI.MinUncut.GaussianHermite.memLp_polyProd line 370
  38. def OAI.MinUncut.GaussianHermite.polyProdMap line 377
  39. lemma OAI.MinUncut.GaussianHermite.polyProdMap_apply line 383
  40. def OAI.MinUncut.GaussianHermite.orthPolyMap line 387
  41. lemma OAI.MinUncut.GaussianHermite.heLeadingUnit line 402
  42. lemma OAI.MinUncut.GaussianHermite.ortho_polyProd_of_heProd line 407
  43. lemma OAI.MinUncut.GaussianHermite.memLp_exp_linear line 419
  44. lemma OAI.MinUncut.GaussianHermite.memLp_mvpoly line 438
  45. lemma OAI.MinUncut.GaussianHermite.ortho_mvpoly_of_polyProd line 447
  46. def OAI.MinUncut.GaussianHermite.linearPoly line 464
  47. lemma OAI.MinUncut.GaussianHermite.eval_linearPoly line 467
  48. lemma OAI.MinUncut.GaussianHermite.weighted_linear_expSet line 478
  49. lemma OAI.MinUncut.GaussianHermite.ae_zero_of_integral_mvpoly_eq_zero line 491
  50. def OAI.MinUncut.GaussianHermite.psi line 539
  51. lemma OAI.MinUncut.GaussianHermite.continuous_H line 541
  52. lemma OAI.MinUncut.GaussianHermite.memLp_psi line 545
  53. lemma OAI.MinUncut.GaussianHermite.psi_product line 551
  54. lemma OAI.MinUncut.GaussianHermite.heProd_eq line 564
  55. lemma OAI.MinUncut.GaussianHermite.ae_zero_of_integral_psi_eq_zero line 571
  56. def OAI.MinUncut.GaussianHermite.psiVec line 582
  57. lemma OAI.MinUncut.GaussianHermite.psiVec_orthonormal line 584
  58. lemma OAI.MinUncut.GaussianHermite.eq_zero_of_inner_psiVec_eq_zero line 589
  59. def OAI.MinUncut.GaussianHermite.productHermiteBasis line 603
  60. def OAI.MinUncut.GaussianHermite.affinePoly line 615
  61. lemma OAI.MinUncut.GaussianHermite.eval_affinePoly line 616
  62. lemma OAI.MinUncut.GaussianHermite.derivative_affinePoly line 618
  63. lemma OAI.MinUncut.GaussianHermite.integrable_he_affine line 621
  64. lemma OAI.MinUncut.GaussianHermite.integrable_mul_he_affine line 626
  65. lemma OAI.MinUncut.GaussianHermite.stein_he_affine line 632
  66. lemma OAI.MinUncut.GaussianHermite.he_one line 640
  67. lemma OAI.MinUncut.GaussianHermite.he_recurrence line 644
  68. lemma OAI.MinUncut.GaussianHermite.he_noise line 649
  69. lemma OAI.MinUncut.GaussianHermite.H_noise line 677
  70. lemma OAI.MinUncut.GaussianHermite.psi_noise line 683
  71. lemma OAI.MinUncut.GaussianHermite.charFunDual_gamma line 689
  72. lemma OAI.MinUncut.GaussianHermite.charFunDual_gammaPi line 695
  73. def OAI.MinUncut.GaussianHermite.rotation line 707
  74. lemma OAI.MinUncut.GaussianHermite.rotation_apply line 714
  75. lemma OAI.MinUncut.GaussianHermite.rotation_involutive line 718
  76. lemma OAI.MinUncut.GaussianHermite.rotation_preserves line 729
  77. def OAI.MinUncut.GaussianHermite.noise line 766
  78. lemma OAI.MinUncut.GaussianHermite.measurable_noise line 769
  79. lemma OAI.MinUncut.GaussianHermite.psi_integrable line 776
  80. lemma OAI.MinUncut.GaussianHermite.continuous_psi line 779
  81. lemma OAI.MinUncut.GaussianHermite.noise_bound line 783
  82. lemma OAI.MinUncut.GaussianHermite.noise_coefficient line 789
  83. lemma OAI.MinUncut.GaussianHermite.he_rotation_moment line 836
  84. lemma OAI.MinUncut.GaussianHermite.sqrt_factorial_succ line 851
  85. lemma OAI.MinUncut.GaussianHermite.H_rotation_moment line 856
  86. lemma OAI.MinUncut.GaussianHermite.psi_rotation_moment line 865
  87. def OAI.MinUncut.GaussianHermite.score line 888
  88. lemma OAI.MinUncut.GaussianHermite.measurable_score line 891
  89. lemma OAI.MinUncut.GaussianHermite.coordinate_integrable line 898
  90. lemma OAI.MinUncut.GaussianHermite.score_bound line 901
  91. lemma OAI.MinUncut.GaussianHermite.memLp_score line 917
  92. lemma OAI.MinUncut.GaussianHermite.score_coefficient line 922
  93. def OAI.MinUncut.GaussianHermite.coeff line 976
  94. def OAI.MinUncut.GaussianHermite.degree line 978
  95. def OAI.MinUncut.GaussianHermite.bump line 980
  96. lemma OAI.MinUncut.GaussianHermite.degree_bump line 982
  97. lemma OAI.MinUncut.GaussianHermite.bump_injective line 990