OAI/Analysis/FourierLLogL/Compress/Params.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Choice of entropy parameters

Here j tends to infinity, d=2^j. We take h a power of two, comparable with log j.

  1. def OAI.FourierLLogL.Compress.Params.ell line 12
  2. def OAI.FourierLLogL.Compress.Params.slow line 13
  3. def OAI.FourierLLogL.Compress.Params.wide line 14
  4. def OAI.FourierLLogL.Compress.Params.height line 15
  5. def OAI.FourierLLogL.Compress.Params.sLen line 16
  6. def OAI.FourierLLogL.Compress.Params.sSeg line 17
  7. def OAI.FourierLLogL.Compress.Params.long line 18
  8. lemma OAI.FourierLLogL.Compress.Params.pow_pos_nat line 21
  9. lemma OAI.FourierLLogL.Compress.Params.slow_pos line 23
  10. lemma OAI.FourierLLogL.Compress.Params.ell_tendsto line 24
  11. lemma OAI.FourierLLogL.Compress.Params.slow_tendsto line 32
  12. lemma OAI.FourierLLogL.Compress.Params.wide_tendsto line 37
  13. lemma OAI.FourierLLogL.Compress.Params.evt_slow line 42
  14. lemma OAI.FourierLLogL.Compress.Params.eventually_pow_small line 62
  15. lemma OAI.FourierLLogL.Compress.Params.eventually_pow_small_slow line 72
  16. lemma OAI.FourierLLogL.Compress.Params.nat_pow_small_slow line 76
  17. def OAI.FourierLLogL.Compress.Params.base line 82
  18. def OAI.FourierLLogL.Compress.Params.capE line 83
  19. def OAI.FourierLLogL.Compress.Params.cap line 84
  20. lemma OAI.FourierLLogL.Compress.Params.wide_le_j line 87
  21. lemma OAI.FourierLLogL.Compress.Params.ell_le_h line 90
  22. lemma OAI.FourierLLogL.Compress.Params.h_le_wide line 91
  23. lemma OAI.FourierLLogL.Compress.Params.slow_le_j line 92
  24. lemma OAI.FourierLLogL.Compress.Params.base_le_cap line 94
  25. lemma OAI.FourierLLogL.Compress.Params.cap_power line 101
  26. lemma OAI.FourierLLogL.Compress.Params.below_base line 110
  27. lemma OAI.FourierLLogL.Compress.Params.t_expr line 125
  28. def OAI.FourierLLogL.Compress.Params.nSched line 140
  29. def OAI.FourierLLogL.Compress.Params.qSched line 141
  30. def OAI.FourierLLogL.Compress.Params.mSched line 142
  31. def OAI.FourierLLogL.Compress.Params.searchSched line 144
  32. lemma OAI.FourierLLogL.Compress.Params.nSched_scale line 197
  33. lemma OAI.FourierLLogL.Compress.Params.searchSched_loss line 200
  34. def OAI.FourierLLogL.Compress.Params.levelLow line 210
  35. def OAI.FourierLLogL.Compress.Params.levelHigh line 211
  36. def OAI.FourierLLogL.Compress.Params.stepLow line 212
  37. def OAI.FourierLLogL.Compress.Params.stepHigh line 213
  38. def OAI.FourierLLogL.Compress.Params.stepRows line 215
  39. lemma OAI.FourierLLogL.Compress.Params.index_budgets line 217
  40. lemma OAI.FourierLLogL.Compress.Params.array_spec line 260
  41. lemma OAI.FourierLLogL.Compress.Params.big_t_real line 313