OAI/Probability/LogConcave/OraclePrograms/Program.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LogConcaveSampling.OracleCompiler.Program line 14
  2. def OAI.LogConcaveSampling.OracleCompiler.Program.history line 24
  3. def OAI.LogConcaveSampling.OracleCompiler.Program.run line 32
  4. def OAI.LogConcaveSampling.OracleCompiler.Program.algorithm line 35
  5. lemma OAI.LogConcaveSampling.OracleCompiler.Program.algorithm_history line 41
  6. lemma OAI.LogConcaveSampling.OracleCompiler.Program.algorithm_run line 49
  7. lemma OAI.LogConcaveSampling.OracleCompiler.Program.history_tail line 55
  8. lemma OAI.LogConcaveSampling.OracleCompiler.Program.history_stable line 66
  9. def OAI.LogConcaveSampling.OracleCompiler.Program.mask line 78
  10. lemma OAI.LogConcaveSampling.OracleCompiler.Program.prefix_zero line 81
  11. lemma OAI.LogConcaveSampling.OracleCompiler.Program.prefix_full line 85
  12. lemma OAI.LogConcaveSampling.OracleCompiler.Program.prefix_succ line 89
  13. lemma OAI.LogConcaveSampling.OracleCompiler.Program.history_eq_prefix line 101
  14. lemma OAI.LogConcaveSampling.OracleCompiler.Program.history_spec line 109
  15. lemma OAI.LogConcaveSampling.OracleCompiler.Program.history_unique line 117
  16. lemma OAI.LogConcaveSampling.OracleCompiler.Program.measurable_prefix line 130
  17. lemma OAI.LogConcaveSampling.OracleCompiler.Program.measurable_history line 138
  18. lemma OAI.LogConcaveSampling.OracleCompiler.Program.measurable_run line 156
  19. def OAI.LogConcaveSampling.OracleCompiler.Program.leftTrace line 167
  20. def OAI.LogConcaveSampling.OracleCompiler.Program.rightTrace line 168
  21. lemma OAI.LogConcaveSampling.OracleCompiler.Program.measurable_leftTrace line 170
  22. lemma OAI.LogConcaveSampling.OracleCompiler.Program.measurable_rightTrace line 172
  23. lemma OAI.LogConcaveSampling.OracleCompiler.Program.leftTrace_append line 175
  24. lemma OAI.LogConcaveSampling.OracleCompiler.Program.rightTrace_append line 179
  25. lemma OAI.LogConcaveSampling.OracleCompiler.Program.leftTrace_prefix_left line 184
  26. lemma OAI.LogConcaveSampling.OracleCompiler.Program.leftTrace_prefix_right line 189
  27. lemma OAI.LogConcaveSampling.OracleCompiler.Program.rightTrace_prefix_right line 195
  28. def OAI.LogConcaveSampling.OracleCompiler.Program.seq line 200
  29. lemma OAI.LogConcaveSampling.OracleCompiler.Program.seq_history line 219
  30. lemma OAI.LogConcaveSampling.OracleCompiler.Program.seq_run line 233
  31. def OAI.LogConcaveSampling.OracleCompiler.Program.map line 241
  32. lemma OAI.LogConcaveSampling.OracleCompiler.Program.map_history line 247
  33. lemma OAI.LogConcaveSampling.OracleCompiler.Program.map_run line 256
  34. def OAI.LogConcaveSampling.OracleCompiler.Program.seedMap line 262
  35. lemma OAI.LogConcaveSampling.OracleCompiler.Program.seedMap_history line 271
  36. lemma OAI.LogConcaveSampling.OracleCompiler.Program.seedMap_run line 280
  37. def OAI.LogConcaveSampling.OracleCompiler.Program.pure line 287
  38. lemma OAI.LogConcaveSampling.OracleCompiler.Program.pure_run line 293
  39. def OAI.LogConcaveSampling.OracleCompiler.Program.oneQuery line 296
  40. lemma OAI.LogConcaveSampling.OracleCompiler.Program.oneQuery_run line 304
  41. def OAI.LogConcaveSampling.OracleCompiler.Program.castCap line 314
  42. lemma OAI.LogConcaveSampling.OracleCompiler.Program.castCap_run line 316
  43. def OAI.LogConcaveSampling.OracleCompiler.Program.iterate line 319
  44. lemma OAI.LogConcaveSampling.OracleCompiler.Program.iterate_run line 324
  45. def OAI.LogConcaveSampling.SeedCompiler.slotSum line 344
  46. def OAI.LogConcaveSampling.SeedCompiler.slotTransform line 346
  47. lemma OAI.LogConcaveSampling.SeedCompiler.slot_energy line 350
  48. def OAI.LogConcaveSampling.SeedCompiler.restored line 372
  49. lemma OAI.LogConcaveSampling.SeedCompiler.restored_apply line 380
  50. lemma OAI.LogConcaveSampling.SeedCompiler.dual_restored_left line 384
  51. lemma OAI.LogConcaveSampling.SeedCompiler.dual_restored_right line 399
  52. theorem OAI.LogConcaveSampling.SeedCompiler.restored_gaussian line 412
  53. def OAI.LogConcaveSampling.SeedCompiler.sqrtCoefficient line 433
  54. lemma OAI.LogConcaveSampling.SeedCompiler.sqrtCoefficient_equation line 436
  55. theorem OAI.LogConcaveSampling.SeedCompiler.sqrt_restored_gaussian line 444
  56. def OAI.LogConcaveSampling.SeedCompiler.ShiftInvariant line 455
  57. lemma OAI.LogConcaveSampling.SeedCompiler.absorption_pathwise line 459
  58. lemma OAI.LogConcaveSampling.SeedCompiler.normalized_shift_bound line 478
  59. theorem OAI.LogConcaveSampling.SeedCompiler.absorption_law line 488
  60. theorem OAI.LogConcaveSampling.SeedCompiler.restored_with_anchors line 505
  61. theorem OAI.LogConcaveSampling.SeedCompiler.absorption_with_anchors line 513
  62. lemma OAI.LogConcaveSampling.SeedCompiler.slotSum_transform line 541
  63. lemma OAI.LogConcaveSampling.SeedCompiler.slotTransform_comp line 551
  64. lemma OAI.LogConcaveSampling.SeedCompiler.slotTransform_square line 560
  65. lemma OAI.LogConcaveSampling.SeedCompiler.slotSum_energy_bound line 571
  66. lemma OAI.LogConcaveSampling.SeedCompiler.sqrtCoefficient_nonneg line 581
  67. lemma OAI.LogConcaveSampling.SeedCompiler.sqrtCoefficient_le_one line 585
  68. lemma OAI.LogConcaveSampling.SeedCompiler.slotTransform_positive line 590
  69. lemma OAI.LogConcaveSampling.SeedCompiler.sqrtCoefficient_eigenvalue line 608
  70. def OAI.LogConcaveSampling.SeedCompiler.inverseCoefficient line 616
  71. lemma OAI.LogConcaveSampling.SeedCompiler.inverseCoefficient_cancel line 619
  72. lemma OAI.LogConcaveSampling.SeedCompiler.inverse_slotTransform line 629
  73. lemma OAI.LogConcaveSampling.SeedCompiler.slotTransform_inverse line 635
  74. lemma OAI.LogConcaveSampling.SeedCompiler.inverse_slot_energy line 645