OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of the product squarefree model and its ordinary height mean for the actual stopped outer coefficient.

  1. def OAI.CubicFirstMoment.squarefreeProductModel line 14
  2. lemma OAI.CubicFirstMoment.squarefreeProductModel_collection line 19
  3. lemma OAI.CubicFirstMoment.continuous_squarefreeProductModel line 29
  4. lemma OAI.CubicFirstMoment.centered_product_eq_gauss_sub_model line 42
  5. lemma OAI.CubicFirstMoment.divisor_model_norm_bound line 59
  6. theorem OAI.CubicFirstMoment.stopped_product_model_norm line 79
  7. theorem OAI.CubicFirstMoment.stopped_product_model_height_mean line 113