OAI/NumberTheory/CubicMoment/Angular/AngularNoncubeReflectedIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full noncube integral estimate for the reflected radial kernel. This is deduced by conjugating the original smooth weight.

  1. theorem OAI.CubicFirstMoment.angular_noncube_mellin_reflected_integral_saving line 16