OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialProductWindow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the constructed radial mean to the literal product window. The bounded dilation of its inner smooth weight is retained exactly.

  1. theorem OAI.CubicFirstMoment.cubicTheta_radial_productTypeICutoffWindow_bound line 13