OAI/Geometry/PeriodicTiling/CircleWeylCriterion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PeriodicTilingThree.unitPeriodPositive line 13
  2. abbrev OAI.PeriodicTilingThree.UnitAddCircle line 15
  3. def OAI.PeriodicTilingThree.CircleFourierCancellation line 17
  4. theorem OAI.PeriodicTilingThree.circle_continuous_integrable line 21
  5. theorem OAI.PeriodicTilingThree.circle_integral_fourier line 25
  6. theorem OAI.PeriodicTilingThree.circle_integral_norm_le line 35
  7. theorem OAI.PeriodicTilingThree.circle_average_norm_le line 42
  8. def OAI.PeriodicTilingThree.circleAveragingSubmodule line 47
  9. theorem OAI.PeriodicTilingThree.fourier_mem_circleAveragingSubmodule line 81
  10. theorem OAI.PeriodicTilingThree.circle_averages_tendsto_integral line 94
  11. theorem OAI.PeriodicTilingThree.denseRange_of_circleFourierCancellation line 131