Theorems · Theorem · number theory

WeakFEPair.f_modif_aux2

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) [CompleteSpace E] {s : ℂ},
  P.k < s.re → mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Compute the Mellin transform of the modifying term used to kill off the constants at 0 and ∞.

Defined in

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Cited by

1 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace