OAI/Combinatorics/Progressions/Estimates/UniformCommutingCircleDecomposition.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.CircleFourier.iteratedCircleSmooth line 13
  2. theorem OAI.Erdos3.CircleFourier.iteratedCircleSmooth_lipschitz line 18
  3. theorem OAI.Erdos3.CircleFourier.iteratedCircleSmooth_norm_le line 25
  4. theorem OAI.Erdos3.CircleFourier.iteratedCircleSmooth_error line 33
  5. theorem OAI.Erdos3.CircleFourier.iteratedCircleSmooth_orbit_error line 52
  6. def OAI.Erdos3.CircleFourier.iteratedCircleComponent line 80
  7. theorem OAI.Erdos3.CircleFourier.iteratedCircleComponent_lipschitz line 86
  8. theorem OAI.Erdos3.CircleFourier.iteratedCircleComponent_norm_le line 94
  9. theorem OAI.Erdos3.CircleFourier.iteratedCircleComponent_character line 102
  10. abbrev OAI.Erdos3.CircleFourier.FejerChoice line 130
  11. theorem OAI.Erdos3.CircleFourier.sum_fin_tuple_cons line 132
  12. theorem OAI.Erdos3.CircleFourier.iteratedCircleSmooth_eq_sum line 139
  13. theorem OAI.Erdos3.CircleFourier.card_fejerChoices line 167
  14. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.component_sub line 187
  15. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.component_norm_sub_le line 200
  16. theorem OAI.Erdos3.CircleFourier.iteratedCircleComponent_norm_sub_le line 216
  17. theorem OAI.Erdos3.CircleFourier.iteratedCircleComponent_equivariant line 242
  18. theorem OAI.Erdos3.CircleFourier.exists_controlled_finite_circle_decomposition line 253
  19. theorem OAI.Erdos3.CircleFourier.exists_controlled_commuting_circle_decomposition line 334
  20. theorem OAI.Erdos3.CircleFourier.exists_uniform_controlled_commuting_circle_operators line 389
  21. theorem OAI.Erdos3.CircleFourier.exists_uniform_controlled_commuting_circle_decomposition line 503