OAI/Geometry/PolarProducts/FourierPaths.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FourierPolynomial.real_inner_eq_complex_re line 14
  2. abbrev OAI.FourierPolynomial.Vector line 20
  3. abbrev OAI.FourierPolynomial.Coeff line 21
  4. def OAI.FourierPolynomial.mode line 23
  5. theorem OAI.FourierPolynomial.mode_apply line 27
  6. def OAI.FourierPolynomial.loop line 29
  7. theorem OAI.FourierPolynomial.loop_apply line 34
  8. theorem OAI.FourierPolynomial.loop_coord line 37
  9. def OAI.FourierPolynomial.loopCLM line 41
  10. theorem OAI.FourierPolynomial.loopCLM_apply line 55
  11. theorem OAI.FourierPolynomial.integral_loop_norm_sq line 57
  12. theorem OAI.FourierPolynomial.integral_loop_coord_sq line 67
  13. theorem OAI.FourierPolynomial.vector_norm_fourth_le line 83
  14. theorem OAI.FourierPolynomial.integral_loop_norm_fourth_le line 92
  15. theorem OAI.FourierPolynomial.fourierCoeff_eval line 131
  16. def OAI.FourierPolynomial.project line 147
  17. theorem OAI.FourierPolynomial.project_apply line 151
  18. theorem OAI.FourierPolynomial.project_loop line 154
  19. theorem OAI.FourierPolynomial.integral_fourier_mul_conj line 161
  20. theorem OAI.FourierPolynomial.integral_inner_loop line 169
  21. theorem OAI.FourierPolynomial.project_bessel line 223
  22. theorem OAI.FourierPolynomial.project_bounded line 245
  23. def OAI.FourierPolynomial.average line 267
  24. theorem OAI.FourierPolynomial.average_apply line 280
  25. def OAI.FourierPolynomial.potential line 282
  26. theorem OAI.FourierPolynomial.contDiff_potential line 285
  27. theorem OAI.FourierPolynomial.contDiff_gradient_function line 289
  28. def OAI.FourierPolynomial.gradLoop line 294
  29. theorem OAI.FourierPolynomial.hasGradientAt_potential line 299
  30. theorem OAI.FourierPolynomial.gradient_potential line 318