OAI/Probability/LogConcave/LowerBounds/LinearHistory.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.LowerBound.remainingHaar_bot line 22
  2. def OAI.LogConcaveSampling.LowerBound.linearHistory line 46
  3. lemma OAI.LogConcaveSampling.LowerBound.measurable_linearHistory line 53
  4. abbrev OAI.LogConcaveSampling.LowerBound.RevealState line 71
  5. abbrev OAI.LogConcaveSampling.LowerBound.RoundRandom line 74
  6. def OAI.LogConcaveSampling.LowerBound.roundRandomLaw line 76
  7. instance OAI.LogConcaveSampling.LowerBound.roundRandomLaw_probability line 79
  8. def OAI.LogConcaveSampling.LowerBound.initialRevealState line 83
  9. lemma OAI.LogConcaveSampling.LowerBound.measurable_initialRevealState line 86
  10. def OAI.LogConcaveSampling.LowerBound.revealStep line 91
  11. lemma OAI.LogConcaveSampling.LowerBound.measurable_revealStep line 106
  12. def OAI.LogConcaveSampling.LowerBound.HistoryConsistent line 141
  13. lemma OAI.LogConcaveSampling.LowerBound.initial_historyConsistent line 147
  14. lemma OAI.LogConcaveSampling.LowerBound.revealStep_historyConsistent line 153
  15. def OAI.LogConcaveSampling.LowerBound.completeRevealState line 177
  16. lemma OAI.LogConcaveSampling.LowerBound.measurable_completeRevealState line 181
  17. lemma OAI.LogConcaveSampling.LowerBound.revealStep_completion_law line 187
  18. theorem OAI.LogConcaveSampling.LowerBound.revealState_completion_law line 209
  19. def OAI.LogConcaveSampling.LowerBound.finishFrame line 234
  20. lemma OAI.LogConcaveSampling.LowerBound.measurable_finishFrame line 239
  21. def OAI.LogConcaveSampling.LowerBound.finishComplete line 247
  22. lemma OAI.LogConcaveSampling.LowerBound.measurable_finishComplete line 252
  23. lemma OAI.LogConcaveSampling.LowerBound.finishComplete_law line 259
  24. def OAI.LogConcaveSampling.LowerBound.finishCoordinate line 282
  25. lemma OAI.LogConcaveSampling.LowerBound.measurable_finishCoordinate line 287
  26. lemma OAI.LogConcaveSampling.LowerBound.finishCoordinate_mem line 295
  27. lemma OAI.LogConcaveSampling.LowerBound.finishCoordinate_correct line 307
  28. def OAI.LogConcaveSampling.LowerBound.powerHull line 334
  29. lemma OAI.LogConcaveSampling.LowerBound.powerHull_mono_base line 338
  30. lemma OAI.LogConcaveSampling.LowerBound.le_powerHull line 344
  31. lemma OAI.LogConcaveSampling.LowerBound.powerHull_le_succ line 349
  32. lemma OAI.LogConcaveSampling.LowerBound.powerHull_mono_degree line 355
  33. def OAI.LogConcaveSampling.LowerBound.tapeHull line 359
  34. lemma OAI.LogConcaveSampling.LowerBound.tapeHull_empty line 362
  35. lemma OAI.LogConcaveSampling.LowerBound.tapeHull_snoc line 365
  36. lemma OAI.LogConcaveSampling.LowerBound.powerHull_round_growth line 387
  37. lemma OAI.LogConcaveSampling.LowerBound.measurable_frameProjection line 406
  38. def OAI.LogConcaveSampling.LowerBound.roundGood line 411
  39. lemma OAI.LogConcaveSampling.LowerBound.measurableSet_roundGood line 422
  40. lemma OAI.LogConcaveSampling.LowerBound.ae_roundGood line 449
  41. def OAI.LogConcaveSampling.LowerBound.SpanConsistent line 464
  42. lemma OAI.LogConcaveSampling.LowerBound.revealStep_spanConsistent line 468
  43. lemma OAI.LogConcaveSampling.LowerBound.revealRun_historyConsistent line 487
  44. lemma OAI.LogConcaveSampling.LowerBound.revealRun_spanConsistent line 496
  45. def OAI.LogConcaveSampling.LowerBound.orbitHull line 515
  46. lemma OAI.LogConcaveSampling.LowerBound.orbitHull_mono line 518
  47. lemma OAI.LogConcaveSampling.LowerBound.map_orbitHull_le_succ line 524
  48. lemma OAI.LogConcaveSampling.LowerBound.span_range_le_orbitHull line 533
  49. lemma OAI.LogConcaveSampling.LowerBound.powerHull_le_orbitHull line 539