OAI/Combinatorics/Progressions/Fourier/RealQuarterTorusExtension.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.properCyclicCoordinateBound line 15
  2. theorem OAI.Erdos3.properCyclicCoordinateBound_nonneg line 18
  3. theorem OAI.Erdos3.exists_controlled_cyclic_torus_model line 24
  4. theorem OAI.Erdos3.properCyclicKernelBasisBound_le_exp line 60
  5. theorem OAI.Erdos3.properCyclicCoordinateBound_le_exp line 93
  6. def OAI.Erdos3.centeredCircleLift line 133
  7. theorem OAI.Erdos3.coe_centeredCircleLift line 136
  8. theorem OAI.Erdos3.centeredCircleLift_coe line 139
  9. def OAI.Erdos3.affineCyclicTorusLocalLift line 144
  10. theorem OAI.Erdos3.exists_localized_cyclic_torus_chart line 149
  11. theorem OAI.Erdos3.centeredCircleLift_eq_sub_floor line 218
  12. def OAI.Erdos3.affineCyclicTorusCarry line 232
  13. theorem OAI.Erdos3.affineCyclicTorusLocalLift_eq_sub_carry line 236
  14. theorem OAI.Erdos3.affineCyclicTorusCarry_identity line 242
  15. theorem OAI.Erdos3.affineCyclicTorusCarry_bound line 251
  16. theorem OAI.Erdos3.local_cyclic_torus_cell_count_le_exp line 274
  17. theorem OAI.Erdos3.local_cyclic_torus_total_loss_le line 294
  18. theorem OAI.Erdos3.local_cyclic_torus_density line 314
  19. theorem OAI.Erdos3.centeredCircleLift_abs_le_half line 344
  20. theorem OAI.Erdos3.norm_eq_abs_centeredCircleLift line 350
  21. theorem OAI.Erdos3.centeredCircleLift_dist line 358
  22. def OAI.Erdos3.centeredTorusLift line 372
  23. theorem OAI.Erdos3.centeredTorusLift_lipschitzOn line 375
  24. theorem OAI.Erdos3.exists_quarter_torus_extension line 397
  25. def OAI.Erdos3.realPeriodicTorusLift line 435
  26. theorem OAI.Erdos3.realPeriodicTorusLift_coe line 439
  27. theorem OAI.Erdos3.realPeriodicTorusLift_lipschitz line 446
  28. theorem OAI.Erdos3.realPeriodicTorusLift_range line 477
  29. theorem OAI.Erdos3.exists_real_quarter_torus_extension line 492