mellin_pullback_certificate

formal source

 131    module.  The full identification of `Θ_J`'s Mellin transform with
 132    `ξ` (the completed zeta function) requires complex-analytic
 133    machinery beyond the scope of this module. -/
 134theorem mellin_pullback_certificate :
 135    -- (1) J is reciprocally symmetric.
 136    ReciprocalSymmetric Jcost ∧
 137    -- (2) J(e^t) is even in t (log-coordinate reciprocal symmetry).
 138    (∀ (t : ℝ), Jcost (Real.exp t) = Jcost (Real.exp (-t))) ∧
 139    -- (3) The substitution x → 1/x converts the Mellin kernel x^{s-1}
 140    --     into the kernel x^{1-s} (after the Jacobian is accounted for).
 141    (∀ (s : ℝ) (x : ℝ), 0 < x → (x⁻¹ : ℝ) ^ (s - 1) = x ^ (1 - s)) ∧
 142    -- (4) For any reciprocally symmetric f, the integrand of its
 143    --     Mellin transform has the substitution-symmetry property.
 144    (∀ {f : ℝ → ℝ}, ReciprocalSymmetric f →
 145      ∀ (s : ℝ) (x : ℝ), 0 < x →
 146        f x * x ^ (s - 1) = f x⁻¹ * x ^ (s - 1)) :=
 147  ⟨Jcost_reciprocal_symmetric,
 148   Jcost_log_even,
 149   mellin_reflection_via_substitution,
 150   @mellin_pullback_pointwise⟩
 151
 152end
 153
 154end MellinPullback
 155end NumberTheory
 156end IndisputableMonolith