OAI/Combinatorics/BooleanFunctions/GaussianGain.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SquareRootDegree.GaussianGain.gaussian_sq_integral line 15
  2. theorem OAI.SquareRootDegree.GaussianGain.gaussian_sq_integrable line 21
  3. theorem OAI.SquareRootDegree.GaussianGain.gaussian_poly_integrable line 24
  4. theorem OAI.SquareRootDegree.GaussianGain.density_div_mass_bound line 28
  5. theorem OAI.SquareRootDegree.GaussianGain.density_tail_bound line 57
  6. def OAI.SquareRootDegree.GaussianGain.centralKernel line 82
  7. theorem OAI.SquareRootDegree.GaussianGain.centralKernel_continuous line 85
  8. theorem OAI.SquareRootDegree.GaussianGain.centralKernel_support line 90
  9. theorem OAI.SquareRootDegree.GaussianGain.centralKernel_compactSupport line 100
  10. theorem OAI.SquareRootDegree.GaussianGain.central_density_bound line 110
  11. theorem OAI.SquareRootDegree.GaussianGain.central_integral_bound line 157
  12. theorem OAI.SquareRootDegree.GaussianGain.density_integrable line 198
  13. theorem OAI.SquareRootDegree.GaussianGain.middle_mass_bound line 208
  14. def OAI.SquareRootDegree.GaussianGain.residual line 241
  15. theorem OAI.SquareRootDegree.GaussianGain.residual_nonneg line 243
  16. theorem OAI.SquareRootDegree.GaussianGain.residual_le_one line 246
  17. theorem OAI.SquareRootDegree.GaussianGain.residual_eq_zero line 250
  18. theorem OAI.SquareRootDegree.GaussianGain.quadratic_integrable line 253
  19. theorem OAI.SquareRootDegree.GaussianGain.residual_quadratic_integrable line 262
  20. theorem OAI.SquareRootDegree.GaussianGain.tail_integral_bound line 273
  21. def OAI.SquareRootDegree.GaussianGain.gridN line 326
  22. def OAI.SquareRootDegree.GaussianGain.width line 327
  23. def OAI.SquareRootDegree.GaussianGain.radius line 328
  24. def OAI.SquareRootDegree.GaussianGain.step line 329
  25. theorem OAI.SquareRootDegree.GaussianGain.gridN_pos line 331
  26. theorem OAI.SquareRootDegree.GaussianGain.width_pos line 332
  27. theorem OAI.SquareRootDegree.GaussianGain.step_pos line 333
  28. theorem OAI.SquareRootDegree.GaussianGain.step_small line 335
  29. theorem OAI.SquareRootDegree.GaussianGain.width_le_one line 336
  30. theorem OAI.SquareRootDegree.GaussianGain.grid_radius line 337
  31. theorem OAI.SquareRootDegree.GaussianGain.variance_numeric line 339
  32. theorem OAI.SquareRootDegree.GaussianGain.central_numeric line 342
  33. theorem OAI.SquareRootDegree.GaussianGain.tail_numeric line 357
  34. abbrev OAI.SquareRootDegree.GaussianGain.Leaves line 371
  35. def OAI.SquareRootDegree.GaussianGain.leafTest line 372
  36. def OAI.SquareRootDegree.GaussianGain.selectorTest line 373
  37. def OAI.SquareRootDegree.GaussianGain.beta line 374
  38. def OAI.SquareRootDegree.GaussianGain.mu line 375
  39. def OAI.SquareRootDegree.GaussianGain.sigma line 376
  40. def OAI.SquareRootDegree.GaussianGain.totalVariance line 377
  41. def OAI.SquareRootDegree.GaussianGain.otherVariance line 378
  42. theorem OAI.SquareRootDegree.GaussianGain.beta_pos line 380
  43. theorem OAI.SquareRootDegree.GaussianGain.mu_close line 381
  44. theorem OAI.SquareRootDegree.GaussianGain.sigma_nonneg line 383
  45. theorem OAI.SquareRootDegree.GaussianGain.sigma_bound line 384
  46. theorem OAI.SquareRootDegree.GaussianGain.otherVariance_nonneg line 385
  47. theorem OAI.SquareRootDegree.GaussianGain.otherVariance_bound line 387
  48. theorem OAI.SquareRootDegree.GaussianGain.otherVariance_le_one line 392
  49. def OAI.SquareRootDegree.GaussianGain.kernel line 395
  50. def OAI.SquareRootDegree.GaussianGain.J line 397
  51. theorem OAI.SquareRootDegree.GaussianGain.kernel_split_general line 399
  52. theorem OAI.SquareRootDegree.GaussianGain.kernel_split line 407
  53. theorem OAI.SquareRootDegree.GaussianGain.kernel_integrable line 411
  54. theorem OAI.SquareRootDegree.GaussianGain.J_lt_half line 419
  55. theorem OAI.SquareRootDegree.GaussianGain.J_nonneg line 436
  56. theorem OAI.SquareRootDegree.GaussianGain.positive_gaussian_deficit line 444