English
Let P be a WeakFEPair. If either s ≠ 0 or f₀ = 0, and either s ≠ k or g₀ = 0, then DifferentiableAt ℂ P.Λ s.
Русский
Пусть P — слабый FEP-пар. При условии (s ≠ 0 или f₀ = 0) и (s ≠ k или g₀ = 0) Λ дифференцируема в точке s.
LaTeX
$$$((s \\neq 0) \\lor (P.f_0 = 0)) \\rightarrow ( (s \\neq P.k) \\lor (P.g_0 = 0) ) \\rightarrow \\mathrm{DifferentiableAt}_{\\mathbb{C}}(P.\\Lambda)(s)$$$
Lean4
/-- Relation between `Λ s` and the Mellin transform of `f - f₀`, where the latter is defined. -/
theorem hasMellin [CompleteSpace E] {s : ℂ} (hs : P.k < s.re) : HasMellin (P.f · - P.f₀) s (P.Λ s) :=
by
have hc1 : MellinConvergent (P.f · - P.f₀) s :=
let ⟨_, ht⟩ := exists_gt s.re
mellinConvergent_of_isBigO_rpow (P.hf_int.sub (locallyIntegrableOn_const _)) (P.hf_top _) ht P.hf_zero' hs
refine ⟨hc1, ?_⟩
have hc2 : HasMellin P.f_modif s (P.Λ₀ s) := P.toStrongFEPair.hasMellin s
have hc3 : mellin (fun x ↦ f_modif P x - f P x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀ :=
P.f_modif_aux2 hs
have := (hasMellin_sub hc2.1 hc1).2
simp_rw [← sub_add, hc3, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', ← sub_sub] at this
exact this
