AngularDualContour.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Retained finite dual polynomials for fixed infinity type. The sole Gamma strip input is the bounded-strip consequence of NIST DLMF 5.11.9; there is no arithmetic moment or smooth-duality conclusion in that input.

def OAI.CubicFirstMoment.angularGammaFEQuotient line 14
def OAI.CubicFirstMoment.AngularGammaQuotientStripBound line 19
Source documentation
The fixed-shift specialization of the uniform vertical Stirling formula, DLMF 5.11.9.
```
def AngularGammaQuotientStripBound (k a : ℝ) : Prop :=
…
```
lemma OAI.CubicFirstMoment.differentiableOn_angularGammaFEQuotient line 23
def OAI.CubicFirstMoment.angularFiniteHeckeDual line 40
lemma OAI.CubicFirstMoment.differentiableOn_angularFiniteHeckeDual line 44

theorem OAI.CubicFirstMoment.angular_finite_dual_contour_shift line 58

Source documentation

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

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

Mentions: OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.angularFiniteHeckeDual

lemma OAI.CubicFirstMoment.angular_finite_dual_strip_growth line 112