HeckeCompletedOrder.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Classical order-one completion as the weak analytic input. Thorner--Zaman, ANT 13 (2019), §2C, p.1049, Eq. (2-15), states that the completed primitive nonprincipal Hecke function is entire of order one. The coarse quadratic exponential majorant below is sufficient. The reciprocal Gamma strip bound is a weak consequence of the uniform vertical Stirling formula, DLMF 5.11.9, and its entire reciprocal (5.2.2). These inputs concern individual analytic functions, not arithmetic means.

def OAI.CubicFirstMoment.CompletedHeckeFiniteOrder line 21
Source documentation
An order-one completed function has this deliberately coarse quadratic exponential bound. The regular-point equality respects Lean's zero-valued Gamma at its poles.
```
def CompletedHeckeFiniteOrder (A : ℝ) (L : ℂ → ℂ) : Prop :=
…
```
def OAI.CubicFirstMoment.GammaInverseFiniteOrder line 27
Source documentation
Weak reciprocal-Gamma growth, on one bounded strip only.
```
def GammaInverseFiniteOrder (a b : ℝ) : Prop :=
…
```
lemma OAI.CubicFirstMoment.completed_hecke_decompletion line 31
theorem OAI.CubicFirstMoment.completed_hecke_finiteVerticalOrder line 50
Source documentation
Decompletion preserves finite order. This derives the growth hypothesis needed for Phragmén–Lindelöf from the published completion.
```
theorem completed_hecke_finiteVerticalOrder {A : ℝ} (hA : 0 < A)
    {L : ℂ → ℂ} (hL : Differentiable ℂ L)
    (hcomp : CompletedHeckeFiniteOrder A L) {a b : ℝ}
    (hGamma : GammaInverseFiniteOrder a b) : FiniteVerticalOrder L a b := by
…
```
Mentions: OAI.CubicFirstMoment.CompletedHeckeFiniteOrder, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.FiniteVerticalOrder

theorem OAI.CubicFirstMoment.primitiveHeckeAnalyticData_of_completed line 99

Source documentation

The completion and reciprocal Gamma bound imply the polynomial strip bounds for smooth duality.

theorem primitiveHeckeAnalyticData_of_completed
    {χ χdual : EisensteinIdealExponent → ℂ}
    (hχ : ∀ ν, ‖χ ν‖ ≤ 1) (hχdual : ∀ ν, ‖χdual ν‖ ≤ 1)
    {A : ℝ} (hA : 0 < A) {ε : ℂ} {L Ldual : ℂ → ℂ}
    (hL : Differentiable ℂ L)
    (hs : ∀ s : ℂ, 1 < s.re → L s = normDirichletSeries χ idealExponentNorm s)
    (hds : ∀ s : ℂ, 1 < s.re → Ldual s = normDirichletSeries χdual idealExponentNorm s)
    (hFE : HeckeFunctionalEquation A 0 ε L Ldual)
    (hcomp : CompletedHeckeFiniteOrder A L)
    (hGamma : ∀ m : ℕ, GammaInverseFiniteOrder (1/2-(m:ℝ)) 2) :
    PrimitiveHeckeAnalyticData χ χdual A ε L Ldual := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.normDirichletSeries, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.HeckeFunctionalEquation, OAI.CubicFirstMoment.CompletedHeckeFiniteOrder, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData