OAI/Combinatorics/Progressions/Estimates/IteratedCircleAverageIntegral.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.CircleFourier.integral_circleCharacter line 13
  2. def OAI.Erdos3.CircleFourier.IsometricCircleAction.average line 26
  3. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_eq_integral line 30
  4. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_lipschitz line 35
  5. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_norm_le line 41
  6. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_const line 46
  7. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_invariant line 50
  8. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_unit_interval line 57
  9. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_sub line 75
  10. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_sub_norm_le line 85
  11. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_sum line 91
  12. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_equivariant line 100
  13. theorem OAI.Erdos3.CircleFourier.IsometricCircleAction.average_eigenfunction line 108
  14. def OAI.Erdos3.CircleFourier.iteratedCircleAverage line 129
  15. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_lipschitz line 134
  16. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_norm_le line 141
  17. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_unit_interval line 148
  18. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_sub_norm_le line 158
  19. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_sum line 168
  20. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_equivariant line 182
  21. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_invariant line 193
  22. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_eigenfunction line 212
  23. def OAI.Erdos3.CircleFourier.CircleAverageTuple line 245
  24. instance OAI.Erdos3.CircleFourier.circleAverageTupleMeasurableSpace line 249
  25. instance OAI.Erdos3.CircleFourier.circleAverageTupleTopologicalSpace line 255
  26. instance OAI.Erdos3.CircleFourier.circleAverageTupleSecondCountableTopology line 261
  27. instance OAI.Erdos3.CircleFourier.circleAverageTupleBorelSpace line 268
  28. instance OAI.Erdos3.CircleFourier.circleAverageTupleCompactSpace line 274
  29. def OAI.Erdos3.CircleFourier.circleAverageTupleMeasure line 280
  30. instance OAI.Erdos3.CircleFourier.circleAverageTupleMeasure_probability line 284
  31. def OAI.Erdos3.CircleFourier.iteratedCircleAction line 293
  32. theorem OAI.Erdos3.CircleFourier.continuous_iteratedCircleAction line 298
  33. theorem OAI.Erdos3.CircleFourier.continuous_iteratedCircleAction_parameter line 309
  34. theorem OAI.Erdos3.CircleFourier.integrable_iteratedCircleAction line 313
  35. theorem OAI.Erdos3.CircleFourier.iteratedCircleAverage_eq_integral line 320