MellinAdmissibleKernel

formal source

  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
  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