OAI/NumberTheory/DuffinSchaeffer/Reductions.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Preliminary reductions for inhomogeneous Diophantine approximation.

  1. def OAI.WeakInhomogeneousDS.approximationSet line 14
  2. def OAI.WeakInhomogeneousDS.wellApproximated line 17
  3. def OAI.WeakInhomogeneousDS.rowCenters line 20
  4. def OAI.WeakInhomogeneousDS.rowRadius line 23
  5. def OAI.WeakInhomogeneousDS.totientMass line 25
  6. theorem OAI.WeakInhomogeneousDS.totientMass_eq_totient_mul_rowRadius line 28
  7. theorem OAI.WeakInhomogeneousDS.mul_rowRadius line 33
  8. theorem OAI.WeakInhomogeneousDS.norm_coe_lt_iff_exists_int line 38
  9. theorem OAI.WeakInhomogeneousDS.mem_approximationSet_iff line 47
  10. theorem OAI.WeakInhomogeneousDS.approximationSet_eq_thickening line 52
  11. theorem OAI.WeakInhomogeneousDS.approximationSet_eq_iUnion_Ioo line 77
  12. theorem OAI.WeakInhomogeneousDS.isOpen_approximationSet line 85
  13. theorem OAI.WeakInhomogeneousDS.approximationSet_empty_of_nonpos line 91
  14. theorem OAI.WeakInhomogeneousDS.approximationSet_mono line 97
  15. theorem OAI.WeakInhomogeneousDS.wellApproximated_eq_blimsup line 102
  16. theorem OAI.WeakInhomogeneousDS.measurableSet_wellApproximated line 108
  17. theorem OAI.WeakInhomogeneousDS.wellApproximated_mono line 114
  18. theorem OAI.WeakInhomogeneousDS.approximationSet_eq_univ_of_half_lt line 119
  19. theorem OAI.WeakInhomogeneousDS.thickening_rowCenters_one_div line 129
  20. theorem OAI.WeakInhomogeneousDS.ae_wellApproximated_of_infinite_large_widths line 135
  21. theorem OAI.WeakInhomogeneousDS.exists_infinite_large_widths_of_not_tendsto line 162
  22. theorem OAI.WeakInhomogeneousDS.ae_wellApproximated_of_not_tendsto_zero line 179
  23. theorem OAI.WeakInhomogeneousDS.totientMass_nonneg line 185
  24. theorem OAI.WeakInhomogeneousDS.totientMass_le line 189
  25. theorem OAI.WeakInhomogeneousDS.tendsto_totientMass_zero line 199
  26. theorem OAI.WeakInhomogeneousDS.rowRadius_bounds line 204
  27. theorem OAI.WeakInhomogeneousDS.tendsto_rowRadius_zero line 213
  28. theorem OAI.WeakInhomogeneousDS.exists_fixed_mass_block line 219
  29. theorem OAI.WeakInhomogeneousDS.exists_late_totient_mass_block line 269
  30. theorem OAI.WeakInhomogeneousDS.exists_late_small_totient_mass_block line 283
  31. theorem OAI.WeakInhomogeneousDS.exists_dyadic_tolerance line 299
  32. theorem OAI.WeakInhomogeneousDS.totient_divergence_of_mul_le line 317
  33. theorem OAI.WeakInhomogeneousDS.exists_dyadic_reduction line 336
  34. def OAI.WeakInhomogeneousDS.avoidedTail line 354
  35. theorem OAI.WeakInhomogeneousDS.mem_avoidedTail line 358
  36. theorem OAI.WeakInhomogeneousDS.measurableSet_avoidedTail line 362
  37. theorem OAI.WeakInhomogeneousDS.compl_wellApproximated line 367
  38. theorem OAI.WeakInhomogeneousDS.exists_positive_avoidedTail line 387
  39. theorem OAI.WeakInhomogeneousDS.exists_finite_measure_avoided_set line 400
  40. theorem OAI.WeakInhomogeneousDS.exists_disjoint_totient_mass_blocks line 431
  41. theorem OAI.WeakInhomogeneousDS.counterexample_reduction line 486