HeckeStripGrowth.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The polynomial strip-growth field used by the Mellin proof follows from finite order, absolute convergence, and the functional equation. No polynomial strip bound is assumed in the input structure here.

lemma OAI.CubicFirstMoment.norm_idealDirichlet_le_zeta_two line 14
lemma OAI.CubicFirstMoment.hecke_left_boundary_bound line 28
structure OAI.CubicFirstMoment.PrimitiveHeckeFiniteOrderData line 71
Source documentation
Finite order is the weak growth statement supplied by the classical completed Hecke-function theory. Its conversion from the completed order-one bound is kept separate from the Phragmén–Lindelöf argument.
```
structure PrimitiveHeckeFiniteOrderData (χ χdual : EisensteinIdealExponent → ℂ)
    (A : ℝ) (ε : ℂ) (L Ldual : ℂ → ℂ) : Prop where
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
theorem OAI.CubicFirstMoment.PrimitiveHeckeFiniteOrderData.analyticData line 81
Source documentation
Polynomial strip growth follows from finite order and the completed functional equation, giving the bounds needed for the contour shift.
```
theorem PrimitiveHeckeFiniteOrderData.analyticData
    {χ χdual : EisensteinIdealExponent → ℂ}
    (hχ : ∀ ν, ‖χ ν‖ ≤ 1) (hχdual : ∀ ν, ‖χdual ν‖ ≤ 1)
    {A : ℝ} (hA : 0 < A) {ε : ℂ} {L Ldual : ℂ → ℂ}
    (data : PrimitiveHeckeFiniteOrderData χ χdual A ε L Ldual) :
    PrimitiveHeckeAnalyticData χ χdual A ε L Ldual := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.PrimitiveHeckeFiniteOrderData, OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData