OAI/Analysis/LipschitzHilbert/Fourier/ComplexBandAverage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Scalar complex packet averages on the actual line grid.

  1. theorem OAI.LipschitzHilbert.integral_complex_square line 16
  2. theorem OAI.LipschitzHilbert.schwartz_projection_deriv line 26
  3. theorem OAI.LipschitzHilbert.schwartz_projection_coe line 31
  4. theorem OAI.LipschitzHilbert.schwartz_re_memLp line 36
  5. theorem OAI.LipschitzHilbert.schwartz_im_memLp line 41
  6. def OAI.LipschitzHilbert.FiniteLineGrid.scalarAverage line 48
  7. theorem OAI.LipschitzHilbert.FiniteLineGrid.scalarAverage_re line 53
  8. theorem OAI.LipschitzHilbert.FiniteLineGrid.scalarAverage_im line 58
  9. theorem OAI.LipschitzHilbert.FiniteLineGrid.schwartz_projection_average_energy line 63
  10. theorem OAI.LipschitzHilbert.FiniteLineGrid.schwartz_primitive_average_energy line 81
  11. theorem OAI.LipschitzHilbert.FiniteLineGrid.schwartz_high_frequency_average line 103
  12. theorem OAI.LipschitzHilbert.FiniteLineGrid.schwartz_poincare line 124
  13. theorem OAI.LipschitzHilbert.FiniteLineGrid.schwartz_low_frequency_error line 174