OAI/Geometry/PolarProducts/PeriodicFourier.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.L2Paths.integral_sq_le line 16
  2. theorem OAI.L2Paths.norm_sub_sq_le line 38
  3. theorem OAI.L2Paths.norm_sub_sq_le_global line 50
  4. theorem OAI.L2Paths.norm_bound line 65
  5. abbrev OAI.L2Paths.Segment line 91
  6. theorem OAI.L2Paths.exists_subsequence line 94
  7. abbrev OAI.L2Paths.Time line 126
  8. def OAI.L2Paths.restriction line 128
  9. theorem OAI.L2Paths.restriction_isometry line 132
  10. theorem OAI.L2Paths.exists_periodic_subsequence line 147
  11. abbrev OAI.PeriodicFourier.Time line 169
  12. abbrev OAI.PeriodicFourier.μ line 170
  13. def OAI.PeriodicFourier.coefficient line 173
  14. theorem OAI.PeriodicFourier.coefficient_apply line 187
  15. theorem OAI.PeriodicFourier.coefficient_ext line 189
  16. theorem OAI.PeriodicFourier.coefficient_const line 200
  17. theorem OAI.PeriodicFourier.constant_of_nonzero_coeff line 208
  18. theorem OAI.PeriodicFourier.continuous_lift line 218
  19. def OAI.PeriodicFourier.primitive line 222
  20. theorem OAI.PeriodicFourier.hasDerivAt_primitive line 224
  21. theorem OAI.PeriodicFourier.periodic_primitive line 229
  22. def OAI.PeriodicFourier.periodicPrimitive line 244
  23. theorem OAI.PeriodicFourier.periodicPrimitive_coe line 248
  24. theorem OAI.PeriodicFourier.coefficient_eq_on line 251
  25. theorem OAI.PeriodicFourier.derivative_coefficient line 256
  26. theorem OAI.PeriodicFourier.hasDerivAt_of_coefficients line 273