OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreSections.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite core cutoffs are norms of genuine compact smooth cubic sections. Thus they supply actual local test sections, including at every point of the compact core.

  1. lemma OAI.CubicFirstMoment.cubicThetaCoreSeed_support line 13
  2. def OAI.CubicFirstMoment.cubicThetaCoreSection line 26
  3. lemma OAI.CubicFirstMoment.cubicThetaCoreSection_on_sheet line 31
  4. lemma OAI.CubicFirstMoment.cubicThetaCoreSeed_eq_bump line 37
  5. lemma OAI.CubicFirstMoment.cubicThetaCoreSection_norm line 60
  6. lemma OAI.CubicFirstMoment.cubicThetaCoreSection_finite_cover line 94