  37  x ^ (s - 1)
  38
  39/-- Mellin integrand for a real kernel `f`. -/
  40def mellinIntegrand (f : ℝ → ℝ) (s x : ℝ) : ℝ :=
  41  f x * mellinKernel s x
  42
  43/-- The reflected Mellin parameter. -/
  44def mellinReflect (s : ℝ) : ℝ :=
  45  1 - s
  46
  47/-- Analytic package for a Mellin transform of `f`.
  48
  49`M` is not defined here by an integral. Instead, this structure records the
  50exact analytic assumptions that an integral definition must satisfy:
  51
  52* `realizes`: `M s` is the transform at `s`.
  53* `substitution`: the `x ↦ x⁻¹` change of variables is valid and turns the
  54  transform at `s` into the transform at `1-s`.
  55
  56The point of this split is honest accounting. The substitution theorem is the
  57first analytic bridge; the RS part then proves the reflection law from it. -/
  58structure MellinAdmissibleKernel (f : ℝ → ℝ) where
  59  M : ℝ → ℝ
  60  reciprocal : ReciprocalSymmetric f
  61  substitution :
  62    ∀ s : ℝ, M s = M (mellinReflect s)
  63
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.