OAI/Geometry/PolarProducts/FourierIntegrals.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FourierPolynomial.Time line 15
  2. abbrev OAI.FourierPolynomial.μ line 16
  3. def OAI.FourierPolynomial.eval line 18
  4. theorem OAI.FourierPolynomial.continuous_eval line 21
  5. theorem OAI.FourierPolynomial.integral_fourier line 25
  6. theorem OAI.FourierPolynomial.integrable_continuous line 31
  7. theorem OAI.FourierPolynomial.integral_conj_fourier_mul line 35
  8. theorem OAI.FourierPolynomial.integral_conj_eval_mul line 41
  9. theorem OAI.FourierPolynomial.norm_sq_re line 72
  10. theorem OAI.FourierPolynomial.integral_norm_sq line 75
  11. theorem OAI.FourierPolynomial.coe_integral_norm_fourth line 86
  12. theorem OAI.WeightedSchur.two_mul_le_weighted line 116
  13. theorem OAI.WeightedSchur.sum_le line 121
  14. theorem OAI.WeightedSchur.reciprocal_pair_rows line 154
  15. theorem OAI.FourierPolynomial.integral_norm_fourth_le_pairs line 215
  16. theorem OAI.FourierPolynomial.positive_L4 line 238