Jcost_mellin_reciprocal

formal source

  64/-! ## 2. First-principles RS inputs -/
  65
  66/-- The RS J-cost is a reciprocally symmetric Mellin kernel input. -/
  67theorem Jcost_mellin_reciprocal : ReciprocalSymmetric Cost.Jcost :=
  68  Jcost_reciprocal_symmetric
  69
  70/-- The Mellin kernel transforms under inversion exactly as the reflected
  71parameter requires. -/
  72theorem mellinKernel_inversion (s x : ℝ) (hx : 0 < x) :
  73    mellinKernel s x⁻¹ = x ^ (mellinReflect s) := by
  74  unfold mellinKernel mellinReflect
  75  exact mellin_reflection_via_substitution s x hx
  76
  77/-- Reciprocal symmetry identifies the integrand before and after the
  78inversion, up to the standard Mellin kernel reflection. -/
  79theorem mellinIntegrand_reflect_pointwise
  80    {f : ℝ → ℝ} (hf : ReciprocalSymmetric f)
  81    (s x : ℝ) (hx : 0 < x) :
  82    mellinIntegrand f s x =
  83      f x⁻¹ * mellinKernel s x := by
  84  unfold mellinIntegrand
  85  exact mellin_pullback_pointwise hf s x hx
  86
  87/-- Kernel form of the reflection after inversion. -/
  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
  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