OAI/NumberTheory/CubicMoment/Estimates/GaussianDuality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Gaussian test-function identity used to evaluate the Riesz integral.

  1. lemma OAI.CubicFirstMoment.integrable_trace_gaussian line 12
  2. lemma OAI.CubicFirstMoment.integral_traceFourier_gaussian line 18