OAI/Combinatorics/Progressions/Polynomial/PhaseBandCoordinateLifts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.torusPhaseLinear_realLattice_integral line 12
  2. theorem OAI.Erdos3.realMarkedParameterElement_scaled_integer_mem line 29
  3. theorem OAI.Erdos3.marked_phase_correction_coordinate_norm_le line 47
  4. theorem OAI.Erdos3.exists_marked_phase_band_representatives line 85
  5. theorem OAI.Erdos3.torusPhaseLinear_eq_of_close line 209
  6. theorem OAI.Erdos3.torusPhaseLinear_eq_in_band_of_near line 225
  7. theorem OAI.Erdos3.torusPhaseLinear_group_lipschitz line 241
  8. theorem OAI.Erdos3.torusPhaseLinear_group_lipschitz_exp line 260
  9. theorem OAI.Erdos3.exists_nearby_phase_band_lift line 276
  10. def OAI.Erdos3.phaseBandCoordinateConstant line 317
  11. def OAI.Erdos3.phaseBandQuotientConstant line 320
  12. theorem OAI.Erdos3.phase_band_quotient_dist_le line 324