OAI/NumberTheory/CubicMoment/Theta/CubicThetaForcingProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The forcing profile is an entire function with values in the supremum-norm space on the fixed radial annulus.

  1. abbrev OAI.CubicFirstMoment.CubicThetaForcingBand line 12
  2. def OAI.CubicFirstMoment.cubicThetaForcingLog line 14
  3. def OAI.CubicFirstMoment.cubicThetaForcingA line 18
  4. def OAI.CubicFirstMoment.cubicThetaForcingB line 27
  5. def OAI.CubicFirstMoment.cubicThetaForcingProfile line 33
  6. theorem OAI.CubicFirstMoment.cubicThetaForcingProfile_analytic line 37
  7. lemma OAI.CubicFirstMoment.cubicThetaForcingProfile_apply line 45