OAI/Analysis/RotationWeights/RadixDigits.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CircleDigits.CircleX line 74
  2. def OAI.CircleDigits.denominator line 76
  3. lemma OAI.CircleDigits.denominator_zero line 78
  4. lemma OAI.CircleDigits.denominator_succ line 79
  5. lemma OAI.CircleDigits.denominator_pos line 82
  6. lemma OAI.CircleDigits.denominator_geometric line 85
  7. lemma OAI.CircleDigits.denominator_inv_bound line 91
  8. lemma OAI.CircleDigits.denominator_inv_tendsto line 97
  9. abbrev OAI.CircleDigits.Digits line 102
  10. def OAI.CircleDigits.digitTerm line 104
  11. def OAI.CircleDigits.expansion line 106
  12. def OAI.CircleDigits.endpoint line 108
  13. lemma OAI.CircleDigits.digitTerm_nonneg line 110
  14. lemma OAI.CircleDigits.digitTerm_le_inverse line 113
  15. lemma OAI.CircleDigits.digitTerm_summable line 121
  16. lemma OAI.CircleDigits.digitTerm_le_telescope line 127
  17. lemma OAI.CircleDigits.digitPartial_bound line 139
  18. lemma OAI.CircleDigits.expansion_nonneg line 146
  19. lemma OAI.CircleDigits.expansion_le_one line 149
  20. lemma OAI.CircleDigits.expansion_tail_bound line 153
  21. lemma OAI.CircleDigits.measurable_digitTerm line 172
  22. lemma OAI.CircleDigits.measurable_expansion line 175
  23. lemma OAI.CircleDigits.measurable_endpoint line 178
  24. lemma OAI.CircleDigits.expansion_mono line 181
  25. def OAI.CircleDigits.digitLaw line 192
  26. instance OAI.CircleDigits.(instance at line 194) line 194
  27. def OAI.CircleDigits.uniformDigits line 197
  28. instance OAI.CircleDigits.(instance at line 198) line 198
  29. lemma OAI.CircleDigits.integral_digitLaw line 201
  30. def OAI.CircleDigits.character line 208
  31. lemma OAI.CircleDigits.character_div_eq_one line 214
  32. lemma OAI.CircleDigits.character_div_mul line 234
  33. lemma OAI.CircleDigits.integral_digitLaw_character_zero line 241
  34. lemma OAI.CircleDigits.exists_nondividing_digit line 265
  35. lemma OAI.CircleDigits.character_sum line 289
  36. lemma OAI.CircleDigits.integral_digitPartial line 296
  37. lemma OAI.CircleDigits.integral_endpoint_character line 331
  38. lemma OAI.CircleDigits.continuous_integral line 358
  39. lemma OAI.CircleDigits.circle_measure_eq_of_fourier line 370
  40. lemma OAI.CircleDigits.endpoint_measurePreserving line 398
  41. def OAI.CircleDigits.prefixNumeral line 420
  42. def OAI.CircleDigits.scaledTail line 424
  43. def OAI.CircleDigits.gridFree line 427
  44. lemma OAI.CircleDigits.prefixNumeral_sum line 429
  45. lemma OAI.CircleDigits.scaledTail_bounds line 440
  46. lemma OAI.CircleDigits.scaledTail_coe line 450
  47. lemma OAI.CircleDigits.ae_gridFree line 457
  48. lemma OAI.CircleDigits.scaledTail_lt_one line 473
  49. lemma OAI.CircleDigits.scaledTail_repr line 481
  50. lemma OAI.CircleDigits.scaledTail_recurrence line 491
  51. lemma OAI.CircleDigits.digit_interval line 496
  52. lemma OAI.CircleDigits.recover_digit line 505
  53. lemma OAI.CircleDigits.scaledTail_tsum line 515
  54. lemma OAI.CircleDigits.scaledTail_mono line 525