88theorem mellinIntegrand_after_inversion 89 {f : ℝ → ℝ} (hf : ReciprocalSymmetric f) 90 (s x : ℝ) (hx : 0 < x) : 91 f x⁻¹ * mellinKernel s x⁻¹ = 92 f x * x ^ (mellinReflect s) := by
proof body
Term-mode proof.
93 have hfx : f x⁻¹ = f x := (hf x hx).symm 94 rw [hfx] 95 unfold mellinKernel mellinReflect 96 exact congrArg (fun y => f x * y) (mellin_reflection_via_substitution s x hx) 97 98/-! ## 3. Reflection theorem -/ 99 100/-- If a Mellin transform package is admissible for a reciprocally symmetric 101kernel, then the transform is invariant under `s ↔ 1-s`. -/
depends on (12)
Lean names referenced from this declaration's body.