OAI/NumberTheory/CubicMoment/Estimates/WideGramSeminormControl.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite seminorm control of the actual radial composition operator. The constant is chosen before the test profile, as required for shrinking cells.

  1. theorem OAI.CubicFirstMoment.schwartz_wideGramExp_comp_seminorm line 12
  2. theorem OAI.CubicFirstMoment.wideAnnularLogSchwartz_seminorm_control line 60