OAI/Analysis/RotationWeights/Parameters.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.blockLength line 57
  2. def OAI.CircleSampling.blockEnd line 58
  3. def OAI.CircleSampling.polynomialWindow line 59
  4. def OAI.CircleSampling.dropSize line 60
  5. def OAI.CircleSampling.crossingBudget line 61
  6. def OAI.CircleSampling.bridgeSize line 62
  7. def OAI.CircleSampling.frequency line 63
  8. def OAI.CircleSampling.blocks line 65
  9. lemma OAI.CircleSampling.blockEnd_strictMono line 72
  10. lemma OAI.CircleSampling.blockEnd_ge line 73
  11. lemma OAI.CircleSampling.state_prefix line 74
  12. lemma OAI.CircleSampling.frequency_eq_state line 76
  13. lemma OAI.CircleSampling.frequency_block line 80
  14. lemma OAI.CircleSampling.frequency_zero line 85
  15. lemma OAI.CircleSampling.frequency_pos line 86
  16. lemma OAI.CircleSampling.frequency_dvd line 87
  17. lemma OAI.CircleSampling.frequency_strictMono line 90
  18. lemma OAI.CircleSampling.frequency_one_gt line 95
  19. lemma OAI.CircleSampling.polynomialWindow_zero line 97
  20. lemma OAI.CircleSampling.polynomialWindow_succ line 98
  21. lemma OAI.CircleSampling.polynomialWindow_pos line 99
  22. lemma OAI.CircleSampling.polynomialWindow_growth line 100
  23. lemma OAI.CircleSampling.polynomialWindow_gt_length line 102
  24. lemma OAI.CircleSampling.polynomialWindow_le_length line 104
  25. lemma OAI.CircleSampling.blockLength_strictMono line 106
  26. lemma OAI.CircleSampling.blockLength_ge line 108
  27. lemma OAI.CircleSampling.crossingBudget_mono line 109
  28. lemma OAI.CircleSampling.dropSize_ge_budget line 111
  29. lemma OAI.CircleSampling.dropSize_nonneg line 112
  30. lemma OAI.CircleSampling.exponent_prefix line 114
  31. lemma OAI.CircleSampling.polynomialWindow_geometric line 121
  32. lemma OAI.CircleSampling.frequency_block_ratio line 131
  33. lemma OAI.CircleSampling.frequency_radix_bound line 137
  34. def OAI.CircleSampling.modelFrequency line 149
  35. def OAI.CircleSampling.coordinateBlock line 150
  36. def OAI.CircleSampling.coordinateDrop line 151
  37. def OAI.CircleSampling.parameterAngle line 153
  38. lemma OAI.CircleSampling.parameterAngle_spec line 154
  39. lemma OAI.CircleSampling.block_phase line 156
  40. def OAI.CircleSampling.coordinatePhase line 167
  41. lemma OAI.CircleSampling.coordinatePhase_block line 169
  42. lemma OAI.CircleSampling.coordinatePhase_pos line 173
  43. lemma OAI.CircleSampling.window_inverse_bound line 180
  44. lemma OAI.CircleSampling.summable_window_inverse line 190
  45. lemma OAI.CircleSampling.tsum_window_inverse line 194
  46. lemma OAI.CircleSampling.sum_phase_block line 204
  47. lemma OAI.CircleSampling.summable_coordinatePhase line 212
  48. lemma OAI.CircleSampling.block_number_equiv line 226
  49. lemma OAI.CircleSampling.summable_block_reciprocal line 231
  50. lemma OAI.CircleSampling.dropSize_ge_window_sq line 237
  51. lemma OAI.CircleSampling.phase_drop_block_lower line 239
  52. lemma OAI.CircleSampling.not_summable_phase_drop line 257