OAI/Analysis/IrrationalRotation/Sampling/MixedRadix.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.MixedRadix.denominator_zero line 13
  2. theorem OAI.Invariant233.MixedRadix.denominator_succ line 16
  3. theorem OAI.Invariant233.MixedRadix.denominator_pos line 20
  4. theorem OAI.Invariant233.MixedRadix.term_nonneg line 24
  5. theorem OAI.Invariant233.MixedRadix.term_le_reciprocal_gap line 27
  6. theorem OAI.Invariant233.MixedRadix.sum_terms_le_reciprocal_gap line 42
  7. theorem OAI.Invariant233.MixedRadix.summable_terms line 54
  8. theorem OAI.Invariant233.MixedRadix.tsum_tail_le line 63
  9. theorem OAI.Invariant233.MixedRadix.ofDigits_nonneg line 71
  10. theorem OAI.Invariant233.MixedRadix.ofDigits_le_one line 74
  11. theorem OAI.Invariant233.MixedRadix.tailValue_nonneg line 78
  12. theorem OAI.Invariant233.MixedRadix.tailValue_le_one line 83
  13. theorem OAI.Invariant233.MixedRadix.ofDigits_mono line 91
  14. theorem OAI.Invariant233.MixedRadix.tailValue_mono line 97
  15. theorem OAI.Invariant233.MixedRadix.tailValue_rec line 105
  16. theorem OAI.Invariant233.MixedRadix.tailValue_mem_bin line 121
  17. theorem OAI.Invariant233.MixedRadix.abs_tailValue_sub_raw_le line 131
  18. theorem OAI.Invariant233.MixedRadix.abs_tailValue_sub_raw_le_of_floor line 148
  19. theorem OAI.Invariant233.MixedRadix.ofDigits_eq_prefix_add_tail line 155
  20. theorem OAI.Invariant233.MixedRadix.abs_ofDigits_sub_ofDigits_le line 161
  21. theorem OAI.Invariant233.MixedRadix.denominator_double line 176
  22. theorem OAI.Invariant233.MixedRadix.summable_reciprocal_denominator line 182
  23. theorem OAI.Invariant233.MixedRadix.reciprocal_denominator_tendsto_zero line 189
  24. theorem OAI.Invariant233.MixedRadix.continuous_ofDigits line 193
  25. theorem OAI.Invariant233.MixedRadix.tendsto_ofDigits_of_agree_prefix line 207
  26. theorem OAI.Invariant233.MixedRadix.prefixRank_zero line 219
  27. theorem OAI.Invariant233.MixedRadix.prefixRank_succ line 221
  28. theorem OAI.Invariant233.MixedRadix.prefixRank_lt_denominator line 224
  29. theorem OAI.Invariant233.MixedRadix.denominator_mul_prefix line 233
  30. theorem OAI.Invariant233.MixedRadix.denominator_mul_ofDigits line 247
  31. theorem OAI.Invariant233.MixedRadix.tailValue_eq_one_imp_next line 253
  32. theorem OAI.Invariant233.MixedRadix.tailValue_lt_one line 262
  33. theorem OAI.Invariant233.MixedRadix.fract_denominator_mul_ofDigits line 280
  34. theorem OAI.Invariant233.MixedRadix.floor_radix_mul_tailValue line 286
  35. theorem OAI.Invariant233.MixedRadix.floor_coordinate_recovers_digit line 297
  36. theorem OAI.Invariant233.MixedRadix.ofDigits_injective_on_nonterminal line 303
  37. theorem OAI.Invariant233.MixedRadix.prefixRank_canonicalDigits line 311
  38. theorem OAI.Invariant233.MixedRadix.canonical_prefix_error line 327
  39. theorem OAI.Invariant233.MixedRadix.ofDigits_canonicalDigits line 342
  40. theorem OAI.Invariant233.MixedRadix.prefixRank_congr line 358
  41. theorem OAI.Invariant233.MixedRadix.prefixRank_eq_iff line 365
  42. theorem OAI.Invariant233.MixedRadix.extendPrefix_apply_lt line 387
  43. theorem OAI.Invariant233.MixedRadix.finitePrefixRank_injective line 392
  44. theorem OAI.Invariant233.MixedRadix.finitePrefixRank_surjective line 400
  45. def OAI.Invariant233.MixedRadix.finitePrefixRankEquiv line 422
  46. theorem OAI.Invariant233.MixedRadix.finitePrefixRankEquiv_val line 432
  47. theorem OAI.Invariant233.MixedRadix.finitePrefixRankEquiv_canonicalDigits line 436
  48. theorem OAI.Invariant233.MixedRadix.measurable_canonicalDigits line 449
  49. theorem OAI.Invariant233.MixedRadix.measurable_ofDigits line 457
  50. theorem OAI.Invariant233.MixedRadix.ofDigits_mem_Ico line 460
  51. theorem OAI.Invariant233.MixedRadix.floor_denominator_mul_ofDigits line 465
  52. theorem OAI.Invariant233.MixedRadix.canonicalDigits_ofDigits line 474