CostAlpha

formal source

  31
  32/-- The α-parameterized cost in multiplicative coordinates:
  33    F_α(x) = (1/α²)(cosh(α ln x) − 1). -/
  34def CostAlpha (α x : ℝ) : ℝ :=
  35  CostAlphaLog α (log x)
  36
  37/-! ## Rescaling Identity -/
  38
  39/-- Core identity: cosh(α log x) − 1 = J(x^α) for x > 0.
  40    Proof uses x^α = exp(α log x), then Jcost ∘ exp = cosh − 1. -/
  41theorem cosh_log_eq_jcost_rpow (α x : ℝ) (hx : 0 < x) :
  42    cosh (α * log x) - 1 = Jcost (x ^ α) := by
  43  have h : x ^ α = exp (α * log x) := by
  44    rw [rpow_def_of_pos hx, mul_comm]
  45  rw [h, ← Jcost_exp_cosh]
  46
  47/-- **Rescaling Identity**: F_α(x) = (1/α²) · J(x^α). -/
  48theorem cost_alpha_rescaling (α x : ℝ) (hx : 0 < x) :
  49    CostAlpha α x = (1 / α ^ 2) * Jcost (x ^ α) := by
  50  unfold CostAlpha CostAlphaLog
  51  congr 1
  52  exact cosh_log_eq_jcost_rpow α x hx
  53
  54/-! ## α = 1 Recovery -/
  55
  56/-- Setting α = 1 gives F₁(x) = J(x) for x > 0. -/
  57theorem cost_alpha_one_eq_jcost (x : ℝ) (hx : 0 < x) :
  58    CostAlpha 1 x = Jcost x := by
  59  rw [cost_alpha_rescaling 1 x hx]
  60  simp [rpow_one]
  61
  62/-! ## Multiplicative Group Automorphism
  63
  64The rescaling φ_α : x ↦ x^α is a group homomorphism of (ℝ₊, ·).