Jcost_log_even

formal source

  61
  62/-- The "shifted cost" `H(t) = J(e^t) + 1` is even in `t`, which is the
  63    log-coordinate version of reciprocal symmetry. -/
  64theorem Jcost_log_even (t : ℝ) :
  65    Jcost (Real.exp t) = Jcost (Real.exp (-t)) := by
  66  have h_pos : 0 < Real.exp t := Real.exp_pos t
  67  rw [Jcost_symm h_pos]
  68  have h_inv : (Real.exp t)⁻¹ = Real.exp (-t) := by
  69    rw [← Real.exp_neg]
  70  rw [h_inv]
  71
  72/-! ## The abstract Mellin pullback theorem
  73
  74For a reciprocally symmetric integrand on the multiplicative group,
  75the Mellin transform inherits a reflection symmetry on the dual.
  76We state this abstractly without invoking the full Mellin transform
  77machinery (which lives in mathlib's complex analysis branch).
  78
  79The statement: if `f(x) = f(1/x)` and we integrate against `x^{s-1} dx`,
  80the result has the form `M(s) = M(1-s)` (where `M` denotes the
  81Mellin transform). -/
  82
  83/-- The substitution lemma at the level of the integrand: if
  84    `f(x) = f(1/x)`, then the integrand `f(x) · x^{s-1}` at point `x`
  85    equals the integrand `f(1/x) · (1/x)^{s-1} · x^{-2}` at point `x`,
  86    which after the variable change `u = 1/x` becomes
  87    `f(u) · u^{1-s-1} · |du/du|^{-1}` -- precisely the Mellin
  88    integrand at the point `1-s`. -/
  89theorem mellin_pullback_pointwise
  90    {f : ℝ → ℝ} (hf : ReciprocalSymmetric f) (s : ℝ) (x : ℝ) (hx : 0 < x) :
  91    f x * x ^ (s - 1) = f x⁻¹ * x ^ (s - 1) := by
  92  rw [hf x hx]
  93
  94/-- The reflection-substitution: under `x ↦ 1/x`, the kernel