OAI/NumberTheory/CubicMoment/Angular/AngularModelOuter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Summation of the actual angular lattice model over the level dyad. This is the model term in the low-height Type-I estimate.

  1. lemma OAI.CubicFirstMoment.angularSmoothModel_zero_of_not_squarefree line 12
  2. lemma OAI.CubicFirstMoment.angular_model_outer_power line 19
  3. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.angular_model_outer_bound line 27
  4. lemma OAI.CubicFirstMoment.angular_model_level_power line 85