OAI/Combinatorics/Progressions/Fourier/FourierLawTransport.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.IntegerFourierAxis line 12
  2. def OAI.Erdos3.IntegerFourierAxis.ofEstimate line 48
  3. theorem OAI.Erdos3.integerGridCoefficient_norm_le_one line 80
  4. theorem OAI.Erdos3.integerGridCoefficient_full_cap line 86
  5. theorem OAI.Erdos3.short_side_scale_bound line 95
  6. def OAI.Erdos3.boundedIntegerFourierAxis line 101
  7. structure OAI.Erdos3.IntegerFourierBudget line 155
  8. def OAI.Erdos3.IntegerFourierBudget.Controls line 163
  9. def OAI.Erdos3.IntegerFourierAxis.budget line 182
  10. theorem OAI.Erdos3.IntegerFourierAxis.budget_controls line 190
  11. def OAI.Erdos3.weightedSliceFourierAxis line 205
  12. def OAI.Erdos3.largeScaleFourierAxis line 265
  13. def OAI.Erdos3.boundedCubeSliceFourierAxis line 333
  14. def OAI.Erdos3.shortCubeSliceFourierAxis line 348
  15. def OAI.Erdos3.smoothCubeFourierAxis line 370
  16. theorem OAI.Erdos3.integerGridCoefficient_eq_of_complexMean line 510
  17. theorem OAI.Erdos3.integerGridApproximation_eq_of_complexMean line 518
  18. theorem OAI.Erdos3.IntegerFourierBudget.controls_of_complexMean line 528