OAI/Combinatorics/Progressions/Estimates/PeriodicIsometricAction.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.CircleFourier.ofReal_fejerPolynomial_eq line 12
  2. theorem OAI.Erdos3.CircleFourier.fejerAverage_eq_sum line 17
  3. def OAI.Erdos3.CircleFourier.circleFejerSum line 31
  4. theorem OAI.Erdos3.CircleFourier.circleFejerSum_eq_average line 34
  5. theorem OAI.Erdos3.CircleFourier.circleFejerSum_approximation line 41
  6. theorem OAI.Erdos3.CircleFourier.fejer_error_le_of_cutoff line 60
  7. theorem OAI.Erdos3.CircleFourier.exists_fejer_cutoff line 83
  8. theorem OAI.Erdos3.CircleFourier.fejer_cutoff_bound line 95
  9. def OAI.Erdos3.CircleFourier.fejerComponent line 130
  10. theorem OAI.Erdos3.CircleFourier.fejerComponent_vadd line 133
  11. theorem OAI.Erdos3.CircleFourier.fejerComponent_inherits_character line 139
  12. theorem OAI.Erdos3.CircleFourier.norm_fejerComponent_le line 146
  13. theorem OAI.Erdos3.CircleFourier.lipschitz_fejerComponent line 155
  14. theorem OAI.Erdos3.CircleFourier.exists_controlled_circle_decomposition line 167
  15. theorem OAI.Erdos3.CircleFourier.norm_fejerAverage_le line 214
  16. theorem OAI.Erdos3.CircleFourier.fejerAverage_sub line 227
  17. theorem OAI.Erdos3.CircleFourier.norm_fejerAverage_sub_average_le line 237
  18. theorem OAI.Erdos3.CircleFourier.norm_circleFejerSum_le line 245
  19. theorem OAI.Erdos3.CircleFourier.norm_circleFejerSum_sub_le line 250
  20. theorem OAI.Erdos3.CircleFourier.lipschitz_circleFejerSum line 258
  21. structure OAI.Erdos3.CircleFourier.IsometricCircleAction line 284
  22. def OAI.Erdos3.CircleFourier.IsometricCircleAction.toAddAction line 295
  23. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.toContinuousVAdd line 300
  24. def OAI.Erdos3.CircleFourier.IsometricCircleAction.component line 306
  25. def OAI.Erdos3.CircleFourier.IsometricCircleAction.smooth line 310
  26. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.smooth_eq_sum line 314
  27. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.component_character line 317
  28. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.component_lipschitz line 323
  29. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.component_norm_le line 330
  30. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.smooth_lipschitz line 336
  31. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.smooth_norm_le line 342
  32. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.smooth_error line 349
  33. theorem OAI.Erdos3.CircleFourier.realFlow_periodic line 371
  34. def OAI.Erdos3.CircleFourier.periodicFlowAct line 378
  35. theorem OAI.Erdos3.CircleFourier.periodicFlowAct_coe line 382
  36. theorem OAI.Erdos3.CircleFourier.periodicFlowAct_zero line 386
  37. theorem OAI.Erdos3.CircleFourier.periodicFlowAct_add line 392
  38. theorem OAI.Erdos3.CircleFourier.periodicFlowAct_isometry line 403
  39. theorem OAI.Erdos3.CircleFourier.periodicFlowAct_displacement line 411
  40. theorem OAI.Erdos3.CircleFourier.circleAct_joint_lipschitz line 422
  41. def OAI.Erdos3.CircleFourier.isometricCircleActionOfFlow line 445