OAI/Analysis/RotationWeights/ActualDigits.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.coordinateRadix line 85
  2. def OAI.CircleSampling.bridgeWidth line 86
  3. def OAI.CircleSampling.rangeWidth line 87
  4. lemma OAI.CircleSampling.coordinateRadix_mul line 89
  5. lemma OAI.CircleSampling.coordinateRadix_cast line 91
  6. lemma OAI.CircleSampling.coordinateBlock_equiv line 94
  7. lemma OAI.CircleSampling.coordinateRadix_bound line 98
  8. lemma OAI.CircleSampling.blockLength_ge_twoHundred line 110
  9. lemma OAI.CircleSampling.bridgeSize_ge_one line 111
  10. lemma OAI.CircleSampling.bridgeWidth_bounds line 112
  11. lemma OAI.CircleSampling.rangeWidth_bounds line 119
  12. def OAI.CircleSampling.stageTagged line 126
  13. lemma OAI.CircleSampling.stageTagged_finite line 127
  14. lemma OAI.CircleSampling.summable_stageTagError line 137
  15. lemma OAI.CircleSampling.summable_kappa_sq line 147
  16. lemma OAI.CircleSampling.summable_coordinateKappaError line 159
  17. def OAI.CircleSampling.actualCoordinate line 180
  18. def OAI.CircleSampling.actualSystem line 192
  19. lemma OAI.CircleSampling.actual_radix_zero line 197
  20. lemma OAI.CircleSampling.actual_radix_succ line 198
  21. lemma OAI.CircleSampling.actual_denominator line 199
  22. lemma OAI.CircleSampling.actual_error_succ line 210
  23. lemma OAI.CircleSampling.summable_actual_error line 215
  24. lemma OAI.CircleSampling.ae_actual_order line 220
  25. lemma OAI.CircleSampling.actual_error_sum line 231
  26. def OAI.CircleSampling.marginalConstant line 272
  27. lemma OAI.CircleSampling.marginalConstant_pos line 273
  28. lemma OAI.CircleSampling.actual_hybrid_bound line 274
  29. def OAI.CircleDigits.hybrid line 289
  30. lemma OAI.CircleDigits.hybrid_order line 290
  31. lemma OAI.CircleDigits.hybrid_tail line 293
  32. lemma OAI.CircleDigits.hybrid_grid line 300
  33. lemma OAI.CircleDigits.hybrid_expansion_tendsto line 306
  34. lemma OAI.CircleDigits.hybrid_endpoint_tendsto line 320
  35. abbrev OAI.CircleSampling.ActualSamples line 331
  36. def OAI.CircleSampling.hybridChoice line 332
  37. def OAI.CircleSampling.firstEndpoint line 333
  38. def OAI.CircleSampling.lastEndpoint line 334
  39. def OAI.CircleSampling.hybridEndpoint line 335
  40. lemma OAI.CircleSampling.firstEndpoint_measurable line 336
  41. lemma OAI.CircleSampling.lastEndpoint_measurable line 337
  42. lemma OAI.CircleSampling.hybridEndpoint_measurable line 338
  43. lemma OAI.CircleSampling.hybrid_observe line 339
  44. lemma OAI.CircleSampling.actual_hybrid_grid line 345
  45. lemma OAI.CircleSampling.actual_hybrid_tendsto line 352
  46. lemma OAI.CircleSampling.ae_endpoint_good line 357
  47. lemma OAI.CircleSampling.ae_hybrid_coordinate_order line 361
  48. lemma OAI.CircleSampling.cappedDiagonal_eq_of_ratio_le line 378
  49. lemma OAI.CircleSampling.ae_hybrid_pair line 385
  50. def OAI.CircleSampling.actualPairLaw line 401
  51. lemma OAI.CircleSampling.actualPairLaw_uc line 403
  52. lemma OAI.CircleSampling.actualPairLaw_tendsto line 426
  53. lemma OAI.CircleSampling.actual_pair_identity line 439