mellin_pullback_pointwise

formal source

  86    which after the variable change `u = 1/x` becomes
  87    `f(u) · u^{1-s-1} · |du/du|^{-1}` -- precisely the Mellin
  88    integrand at the point `1-s`. -/
  89theorem mellin_pullback_pointwise
  90    {f : ℝ → ℝ} (hf : ReciprocalSymmetric f) (s : ℝ) (x : ℝ) (hx : 0 < x) :
  91    f x * x ^ (s - 1) = f x⁻¹ * x ^ (s - 1) := by
  92  rw [hf x hx]
  93
  94/-- The reflection-substitution: under `x ↦ 1/x`, the kernel
  95    transforms as if `s → 1 - s` after accounting for the Jacobian. -/
  96theorem mellin_reflection_via_substitution (s : ℝ) (x : ℝ) (hx : 0 < x) :
  97    (x⁻¹ : ℝ) ^ (s - 1) = x ^ (1 - s) := by
  98  rw [show s - 1 = -(1 - s) from by ring]
  99  rw [Real.rpow_neg (le_of_lt (inv_pos.mpr hx))]
 100  rw [Real.inv_rpow (le_of_lt hx) (1 - s)]
 101  rw [inv_inv]
 102
 103/-! ## The cost theta function
 104
 105The integer cost theta function `Θ_J(t) := Σ_{n ≥ 1} e^{-t · c(n)}`
 106has the Euler-product factorization
 107`Θ_J(t) = Π_p (1 - e^{-t J(p)})^{-1}`.
 108By reciprocal symmetry of `J` extended to rationals, `Θ_J` is
 109the prototype of a function whose Mellin transform inherits
 110the reflection symmetry. -/
 111
 112/-- The cost theta function as a formal series at parameter `t`.
 113    Sum over positive `t`; convergence is via `J(p) > 0` and
 114    rapid growth `J(p) ~ p/2`. -/
 115def costTheta (t : ℝ) (c : ℕ → ℝ) : ℝ :=
 116  ∑' n : ℕ, Real.exp (-t * c n)
 117
 118/-- The cost theta function is non-negative pointwise as a sum of
 119    exponentials, regardless of convergence (with the convention