HeckeDualContour.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Moving finite dual polynomials back to the symmetry line. The only new conditional analytic input is the bounded-strip polynomial estimate for the classical Gamma quotient, a specialization of NIST DLMF 5.11.9 (uniformly for bounded real parts). The half-integer-line estimate needed for the discarded tail was proved directly in GammaLeftLine.

def OAI.CubicFirstMoment.gammaFEQuotient line 17
Source documentation
The elementary quotient in the trivial infinity-type equation.
```
def gammaFEQuotient (s : ℂ) : ℂ := Complex.Gamma (1-s)/Complex.Gamma s
```
def OAI.CubicFirstMoment.GammaQuotientStripBound line 22
Source documentation
Small bounded-strip consequence of the uniform vertical Stirling formula, NIST DLMF (5.11.9), https://dlmf.nist.gov/5.11.E9. This concerns only the classical Gamma function, not an arithmetic sum.
```
def GammaQuotientStripBound (a : ℝ) : Prop :=
…
```
lemma OAI.CubicFirstMoment.differentiableOn_gammaFEQuotient line 26
lemma OAI.CubicFirstMoment.norm_conductor_power_strip line 40
def OAI.CubicFirstMoment.finiteNormDirichlet line 51
lemma OAI.CubicFirstMoment.differentiable_finiteNormDirichlet line 54
lemma OAI.CubicFirstMoment.norm_finiteNormDirichlet_le line 62
def OAI.CubicFirstMoment.finiteHeckeDual line 74
lemma OAI.CubicFirstMoment.differentiableOn_finiteHeckeDual line 78

theorem OAI.CubicFirstMoment.finite_hecke_dual_contour_shift line 92

Source documentation

The finite retained dual polynomial admits the actual contour move. Its coefficients are unchanged during the move.

theorem finite_hecke_dual_contour_shift {ι : Type*} (S : Finset ι)
    (a : ι → ℂ) (N : ι → ℝ) (hN : ∀ i ∈ S, 1 ≤ N i)
    (ε : ℂ) {A Z b : ℝ} (hA : 0 < A) (hZ : 1 ≤ Z) (hb : b ≤ 1/2)
    (hGamma : GammaQuotientStripBound b)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) (t : ℝ) :
    (∫ τ : ℝ, mellin W (b+(τ:ℂ)*Complex.I)*(Z:ℂ)^(b+(τ:ℂ)*Complex.I)*
      finiteHeckeDual S a N ε A (b+((τ-t:ℝ):ℂ)*Complex.I)) =
    ∫ τ : ℝ, mellin W ((1/2:ℂ)+(τ:ℂ)*Complex.I)*(Z:ℂ)^((1/2:ℂ)+(τ:ℂ)*Complex.I)*
      finiteHeckeDual S a N ε A ((1/2:ℂ)+((τ-t:ℝ):ℂ)*Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.GammaQuotientStripBound, OAI.CubicFirstMoment.finiteHeckeDual

lemma OAI.CubicFirstMoment.finite_hecke_dual_strip_growth line 146