MellinContour.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Contour shifting for the Mellin integrals in the smooth Hecke sum. The horizontal edges are kept explicit until a uniform decay bound is available; no functional equation or dual-sum estimate is assumed here.

def OAI.CubicFirstMoment.closedVerticalStrip line 16
lemma OAI.CubicFirstMoment.mellin_rectangle_identity line 19

theorem OAI.CubicFirstMoment.mellin_contour_shift line 45

Source documentation

Vertical Mellin integrals agree after shifting through a holomorphic strip, once both horizontal edges vanish.

theorem mellin_contour_shift {a b : ℝ} (hab : a ≤ b)
    (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (closedVerticalStrip a b))
    (ha : Integrable (fun y : ℝ => f (a + (y : ℂ) * Complex.I)))
    (hb : Integrable (fun y : ℝ => f (b + (y : ℂ) * Complex.I)))
    (hTop : Tendsto (fun T : ℝ => ∫ x in a..b, f (x + (T : ℂ) * Complex.I))
      atTop (𝓝 0))
    (hBot : Tendsto (fun T : ℝ => ∫ x in a..b, f (x - (T : ℂ) * Complex.I))
      atTop (𝓝 0)) :
    (∫ y : ℝ, f (a + (y : ℂ) * Complex.I)) =
      ∫ y : ℝ, f (b + (y : ℂ) * Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.closedVerticalStrip

theorem OAI.CubicFirstMoment.mellin_contour_shift_of_majorant line 77

Source documentation

A common decaying majorant supplies both horizontal limits. This is the form used for a rapidly decreasing Mellin transform times an L-function of polynomial growth.

theorem mellin_contour_shift_of_majorant {a b : ℝ} (hab : a ≤ b)
    (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (closedVerticalStrip a b))
    (H : ℝ → ℝ) (hH : Integrable H)
    (hHtop : Tendsto H atTop (𝓝 0)) (hHbot : Tendsto H atBot (𝓝 0))
    (hbound : ∀ x ∈ Icc a b, ∀ t : ℝ, ‖f (x + (t : ℂ) * Complex.I)‖ ≤ H t) :
    (∫ y : ℝ, f (a + (y : ℂ) * Complex.I)) =
      ∫ y : ℝ, f (b + (y : ℂ) * Complex.I) := by
…

Mentions: OAI.CubicFirstMoment.closedVerticalStrip