ReciprocalSymmetric

formal source

  51
  52/-- A function `f : ℝ → ℝ` is \emph{reciprocally symmetric} if
  53    `f(x) = f(1/x)` for every positive `x`. -/
  54def ReciprocalSymmetric (f : ℝ → ℝ) : Prop :=
  55  ∀ x : ℝ, 0 < x → f x = f x⁻¹
  56
  57/-- The Recognition Science cost function `J` is reciprocally symmetric. -/
  58theorem Jcost_reciprocal_symmetric : ReciprocalSymmetric Jcost := by
  59  intro x hx
  60  exact Jcost_symm hx
  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`