OAI/Geometry/LatticeCovering/Folded.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.Folded.gamma1 line 23
  2. def OAI.SingleLatticeCovering.Folded.gamma line 24
  3. def OAI.SingleLatticeCovering.Folded.height line 25
  4. def OAI.SingleLatticeCovering.Folded.density line 26
  5. def OAI.SingleLatticeCovering.Folded.folded line 27
  6. def OAI.SingleLatticeCovering.Folded.bitValue line 28
  7. def OAI.SingleLatticeCovering.Folded.probability line 29
  8. def OAI.SingleLatticeCovering.Folded.wordMass line 31
  9. def OAI.SingleLatticeCovering.Folded.atom line 32
  10. def OAI.SingleLatticeCovering.Folded.alpha line 35
  11. lemma OAI.SingleLatticeCovering.Folded.gamma1_pos line 37
  12. lemma OAI.SingleLatticeCovering.Folded.density_pos line 40
  13. lemma OAI.SingleLatticeCovering.Folded.folded_pos line 43
  14. lemma OAI.SingleLatticeCovering.Folded.alpha_pos line 46
  15. lemma OAI.SingleLatticeCovering.Folded.alpha_lt_one line 47
  16. lemma OAI.SingleLatticeCovering.Folded.probability_sum line 51
  17. lemma OAI.SingleLatticeCovering.Folded.probability_pos line 57
  18. lemma OAI.SingleLatticeCovering.Folded.probability_le_one line 61
  19. lemma OAI.SingleLatticeCovering.Folded.wordMass_sum line 68
  20. lemma OAI.SingleLatticeCovering.Folded.folded_identity line 77
  21. lemma OAI.SingleLatticeCovering.Folded.gaussian_ratio line 87
  22. lemma OAI.SingleLatticeCovering.Folded.probability_true_logistic line 93
  23. lemma OAI.SingleLatticeCovering.Folded.one_sub_logistic line 102
  24. lemma OAI.SingleLatticeCovering.Folded.logistic_lower line 108
  25. lemma OAI.SingleLatticeCovering.Folded.probability_central line 113
  26. lemma OAI.SingleLatticeCovering.Folded.wordMass_le_exp_card line 133
  27. def OAI.SingleLatticeCovering.Folded.totalMass line 162
  28. def OAI.SingleLatticeCovering.Folded.logMean line 164
  29. lemma OAI.SingleLatticeCovering.Folded.continuous_gamma1 line 167
  30. lemma OAI.SingleLatticeCovering.Folded.continuous_density line 171
  31. lemma OAI.SingleLatticeCovering.Folded.gamma1_eq_gaussianPDF line 176
  32. lemma OAI.SingleLatticeCovering.Folded.gamma1_even line 180
  33. lemma OAI.SingleLatticeCovering.Folded.gamma1_int line 182
  34. lemma OAI.SingleLatticeCovering.Folded.gamma1_integrable line 186
  35. lemma OAI.SingleLatticeCovering.Folded.totalMass_eq_integral line 191
  36. lemma OAI.SingleLatticeCovering.Folded.totalMass_pos line 215
  37. lemma OAI.SingleLatticeCovering.Folded.totalMass_le_one line 224
  38. lemma OAI.SingleLatticeCovering.Folded.gamma1_le_inv_sqrt line 229
  39. lemma OAI.SingleLatticeCovering.Folded.density_upper line 235
  40. lemma OAI.SingleLatticeCovering.Folded.density_lower line 243
  41. lemma OAI.SingleLatticeCovering.Folded.gaussian_subgaussian line 267
  42. lemma OAI.SingleLatticeCovering.Folded.totalMass_eq_probability line 271
  43. lemma OAI.SingleLatticeCovering.Folded.totalMass_tail line 279
  44. lemma OAI.SingleLatticeCovering.Folded.gamma1_second_int line 304
  45. lemma OAI.SingleLatticeCovering.Folded.gamma1_second_integrable line 311
  46. lemma OAI.SingleLatticeCovering.Folded.integral_fold line 328
  47. def OAI.SingleLatticeCovering.Folded.foldMoment line 350
  48. lemma OAI.SingleLatticeCovering.Folded.continuous_foldMoment line 353
  49. lemma OAI.SingleLatticeCovering.Folded.foldMoment_integral_le line 361
  50. lemma OAI.SingleLatticeCovering.Folded.log_component line 370
  51. lemma OAI.SingleLatticeCovering.Folded.entropy_lower_pointwise line 377
  52. lemma OAI.SingleLatticeCovering.Folded.logMean_upper line 392
  53. lemma OAI.SingleLatticeCovering.Folded.logMean_lower line 406
  54. lemma OAI.SingleLatticeCovering.Folded.logMean_lower_of_half line 434
  55. def OAI.SingleLatticeCovering.Folded.law line 447
  56. lemma OAI.SingleLatticeCovering.Folded.measurable_weight line 451
  57. lemma OAI.SingleLatticeCovering.Folded.integral_law line 455
  58. lemma OAI.SingleLatticeCovering.Folded.law_isProbability line 465
  59. lemma OAI.SingleLatticeCovering.Folded.law_ae_mem line 478
  60. lemma OAI.SingleLatticeCovering.Folded.continuous_integrable_law line 484
  61. lemma OAI.SingleLatticeCovering.Folded.continuous_log_density line 492
  62. lemma OAI.SingleLatticeCovering.Folded.integral_log_density line 496
  63. lemma OAI.SingleLatticeCovering.Folded.log_density_bounds line 499
  64. lemma OAI.SingleLatticeCovering.Folded.log_density_memLp line 515
  65. lemma OAI.SingleLatticeCovering.Folded.log_density_variance line 525
  66. lemma OAI.SingleLatticeCovering.Concentration.chebyshev_real line 547
  67. lemma OAI.SingleLatticeCovering.Concentration.sum_memLp line 555
  68. lemma OAI.SingleLatticeCovering.Concentration.sum_mean line 560
  69. lemma OAI.SingleLatticeCovering.Concentration.sum_variance line 567
  70. lemma OAI.SingleLatticeCovering.Concentration.sum_chebyshev line 576
  71. lemma OAI.SingleLatticeCovering.Concentration.indicator_variance line 586
  72. lemma OAI.SingleLatticeCovering.Concentration.count_lower_tail line 597