OAI/Analysis/RotationWeights/TailBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleSampling.sum_drop_prefix line 85
  2. lemma OAI.CircleSampling.floor_abs_bound line 101
  3. lemma OAI.CircleSampling.exponent_prefix_bound line 116
  4. def OAI.CircleSampling.coefficientCap line 134
  5. lemma OAI.CircleSampling.coefficientCap_ge_one line 135
  6. lemma OAI.CircleSampling.modelF_prefix_bound line 136
  7. def OAI.CircleSampling.futureBad line 156
  8. lemma OAI.CircleSampling.futureBad_measurable line 159
  9. lemma OAI.CircleSampling.futureBad_bound line 165
  10. lemma OAI.CircleSampling.window_div_next line 193
  11. lemma OAI.CircleSampling.futureBad_tendsto line 202
  12. lemma OAI.CircleSampling.measure_small_positive_tendsto line 211
  13. def OAI.CircleSampling.endpointBad line 236
  14. def OAI.CircleSampling.projectionEvent line 238
  15. lemma OAI.CircleSampling.endpointBad_measurable line 240
  16. lemma OAI.CircleSampling.projectionEvent_measurable line 246
  17. lemma OAI.CircleSampling.endpointBad_tendsto line 249
  18. lemma OAI.CircleSampling.endpointBad_loss_tendsto line 257
  19. lemma OAI.CircleSampling.projectionEvent_mass line 261
  20. lemma OAI.CircleSampling.projectionEvent_mem line 275
  21. lemma OAI.CircleSampling.not_futureBad_iff line 286
  22. lemma OAI.CircleSampling.event_tail_margins line 298
  23. lemma OAI.CircleSampling.event_floor_tail line 322
  24. lemma OAI.CircleSampling.event_window_bounds line 356