OAI/NumberTheory/CubicMoment/Angular/AngularHeckeGrowth.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial strip growth for the shifted completion Gamma(s+k). The input is the ordinary entire order-one completion, expressed by a coarse quadratic exponential bound. All strip bounds are derived.

  1. def OAI.CubicFirstMoment.ShiftedCompletedHeckeFiniteOrder line 13
  2. lemma OAI.CubicFirstMoment.shifted_completed_hecke_decompletion line 18
  3. theorem OAI.CubicFirstMoment.shifted_completed_finiteVerticalOrder line 39
  4. lemma OAI.CubicFirstMoment.angular_hecke_left_boundary line 91
  5. structure OAI.CubicFirstMoment.ShiftedPrimitiveHeckeAnalyticData line 144

    Source documentation

    Phragmen--Lindelof derives strip growth for the shifted completion from its entire order-one bound.

    structure ShiftedPrimitiveHeckeAnalyticData (χ χdual : EisensteinIdealExponent → ℂ)
    (A k : ℝ) (ε : ℂ) (L Ldual : ℂ → ℂ) : Prop where
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent

  6. theorem OAI.CubicFirstMoment.shifted_hecke_analyticData_of_completed line 154