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)) :=