OAI/Probability/LogConcave/LowerBounds/PrefixSpace.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.LowerBound.complementary_gaussian_direction_law line 20
  2. theorem OAI.LogConcaveSampling.LowerBound.projected_gaussian_direction_law line 43
  3. def OAI.LogConcaveSampling.LowerBound.prefixSpace line 58
  4. theorem OAI.LogConcaveSampling.LowerBound.mem_prefixSpace line 64
  5. def OAI.LogConcaveSampling.LowerBound.coordinateVector line 67
  6. theorem OAI.LogConcaveSampling.LowerBound.coordinateVector_apply line 69
  7. theorem OAI.LogConcaveSampling.LowerBound.coordinateVector_norm line 73
  8. theorem OAI.LogConcaveSampling.LowerBound.inner_coordinateVector line 76
  9. theorem OAI.LogConcaveSampling.LowerBound.prefixSpace_zero line 80
  10. lemma OAI.LogConcaveSampling.LowerBound.prefixSpace_mono line 85
  11. lemma OAI.LogConcaveSampling.LowerBound.coordinateVector_orthogonal_prefix line 90
  12. lemma OAI.LogConcaveSampling.LowerBound.prefixSpace_succ line 97
  13. def OAI.LogConcaveSampling.LowerBound.prefixProject line 124
  14. theorem OAI.LogConcaveSampling.LowerBound.prefixProject_apply line 127
  15. theorem OAI.LogConcaveSampling.LowerBound.continuous_prefixProject line 130
  16. lemma OAI.LogConcaveSampling.LowerBound.prefixProject_mem line 138
  17. lemma OAI.LogConcaveSampling.LowerBound.sub_prefixProject_mem_orthogonal line 143
  18. lemma OAI.LogConcaveSampling.LowerBound.prefixProject_eq_projection line 154
  19. instance OAI.LogConcaveSampling.LowerBound.subspaceHaar_invInvariant line 169
  20. def OAI.LogConcaveSampling.LowerBound.gaussianSection line 184
  21. theorem OAI.LogConcaveSampling.LowerBound.measurable_gaussianSection line 188
  22. def OAI.LogConcaveSampling.LowerBound.gaussianForward line 193
  23. theorem OAI.LogConcaveSampling.LowerBound.measurable_gaussianForward line 197
  24. theorem OAI.LogConcaveSampling.LowerBound.gaussianForward_law line 203
  25. def OAI.LogConcaveSampling.LowerBound.gaussianBackward line 232
  26. theorem OAI.LogConcaveSampling.LowerBound.measurable_gaussianBackward line 236
  27. theorem OAI.LogConcaveSampling.LowerBound.gaussianBackward_law line 241
  28. lemma OAI.LogConcaveSampling.LowerBound.gaussianBackward_sends line 270
  29. def OAI.LogConcaveSampling.LowerBound.remainingHaar line 289
  30. instance OAI.LogConcaveSampling.LowerBound.remainingHaar_probability line 292
  31. lemma OAI.LogConcaveSampling.LowerBound.remainingHaar_fixes line 297
  32. def OAI.LogConcaveSampling.LowerBound.ambientBackward line 303
  33. lemma OAI.LogConcaveSampling.LowerBound.measurable_ambientBackward line 307
  34. lemma OAI.LogConcaveSampling.LowerBound.ambientBackward_law line 312
  35. lemma OAI.LogConcaveSampling.LowerBound.ambientBackward_mem line 328
  36. lemma OAI.LogConcaveSampling.LowerBound.ambientBackward_sends line 333
  37. def OAI.LogConcaveSampling.LowerBound.prefixUnit line 340
  38. lemma OAI.LogConcaveSampling.LowerBound.norm_prefixUnit line 343
  39. abbrev OAI.LogConcaveSampling.LowerBound.Frames line 346
  40. def OAI.LogConcaveSampling.LowerBound.frameCompletion line 348
  41. lemma OAI.LogConcaveSampling.LowerBound.measurable_frameCompletion line 351
  42. def OAI.LogConcaveSampling.LowerBound.flagDirection line 356
  43. lemma OAI.LogConcaveSampling.LowerBound.measurable_flagDirection line 359
  44. lemma OAI.LogConcaveSampling.LowerBound.norm_flagDirection line 363
  45. def OAI.LogConcaveSampling.LowerBound.inverseFrameUpdate line 366
  46. lemma OAI.LogConcaveSampling.LowerBound.measurable_inverseFrameUpdate line 371
  47. theorem OAI.LogConcaveSampling.LowerBound.inverseFrameUpdate_law line 380
  48. lemma OAI.LogConcaveSampling.LowerBound.remainingHaar_map_inv line 405
  49. lemma OAI.LogConcaveSampling.LowerBound.frameCompletion_swap line 415
  50. def OAI.LogConcaveSampling.LowerBound.forwardFrameUpdate line 419
  51. lemma OAI.LogConcaveSampling.LowerBound.measurable_forwardFrameUpdate line 422
  52. theorem OAI.LogConcaveSampling.LowerBound.forwardFrameUpdate_law line 429
  53. def OAI.LogConcaveSampling.LowerBound.frameSpace line 458
  54. lemma OAI.LogConcaveSampling.LowerBound.mem_frameSpace line 461
  55. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_mul line 474
  56. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_sup line 479
  57. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_line line 482
  58. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_fixed line 487
  59. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_mono line 497
  60. lemma OAI.LogConcaveSampling.LowerBound.complementSection_frameSpace line 500
  61. lemma OAI.LogConcaveSampling.LowerBound.flagSection_frameSpace line 509
  62. lemma OAI.LogConcaveSampling.LowerBound.vector_mem_flagDirection line 516
  63. lemma OAI.LogConcaveSampling.LowerBound.flagDirection_mem_span line 534
  64. def OAI.LogConcaveSampling.LowerBound.extendFrame line 551
  65. lemma OAI.LogConcaveSampling.LowerBound.measurable_extendFrame line 555
  66. lemma OAI.LogConcaveSampling.LowerBound.inverseFrameUpdate_eq line 562
  67. lemma OAI.LogConcaveSampling.LowerBound.forwardFrameUpdate_eq line 565
  68. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_extendFrame line 568
  69. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_le_extendFrame line 574
  70. lemma OAI.LogConcaveSampling.LowerBound.mem_frameSpace_extendFrame line 579
  71. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_extendFrame_le line 584
  72. lemma OAI.LogConcaveSampling.LowerBound.ae_frameGaussian_nonzero line 602
  73. def OAI.LogConcaveSampling.LowerBound.filledObservation line 612
  74. lemma OAI.LogConcaveSampling.LowerBound.measurable_filledObservation line 615
  75. lemma OAI.LogConcaveSampling.LowerBound.mem_frameSpace_of_projection_zero line 620
  76. lemma OAI.LogConcaveSampling.LowerBound.mem_frameSpace_filledExtend line 630
  77. lemma OAI.LogConcaveSampling.LowerBound.frameSpace_filledExtend_le line 637