OAI/Analysis/IrrationalRotation/Sampling/MixedRadixCircle.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.MixedRadix.denominator_radices line 10
  2. theorem OAI.Invariant233.MixedRadix.radices_ge_two line 18
  3. theorem OAI.Invariant233.MixedRadix.radices_pos line 28
  4. theorem OAI.Invariant233.MixedRadix.coordinate_eq_tailValue line 32
  5. theorem OAI.Invariant233.MixedRadix.coordinates_ordered line 39
  6. theorem OAI.Invariant233.MixedRadix.abs_coordinate_sub_raw_le line 48
  7. theorem OAI.Invariant233.MixedRadix.hybrid_apply_lt line 56
  8. theorem OAI.Invariant233.MixedRadix.hybrid_apply_ge line 59
  9. theorem OAI.Invariant233.MixedRadix.nonterminal_hybrid line 62
  10. theorem OAI.Invariant233.MixedRadix.hybrid_ordered line 70
  11. theorem OAI.Invariant233.MixedRadix.tailValue_hybrid line 76
  12. theorem OAI.Invariant233.MixedRadix.denominator_mul_hybrid_sub line 84
  13. theorem OAI.Invariant233.MixedRadix.hybrid_sub_eq_int_div line 93
  14. theorem OAI.Invariant233.MixedRadix.tendsto_ofDigits_hybrid line 101