hasDerivAt_sinhDivAlpha

formal source

 104    deriv (CostAlphaLog α) = fun t => sinh (α * t) / α :=
 105  funext fun t => (hasDerivAt_costAlphaLog α hα t).deriv
 106
 107private lemma hasDerivAt_sinhDivAlpha (α : ℝ) (hα : α ≠ 0) (t : ℝ) :
 108    HasDerivAt (fun s => sinh (α * s) / α) (cosh (α * t)) t := by
 109  have h1 : HasDerivAt (fun s => sinh (α * s)) (cosh (α * t) * α) t :=
 110    (hasDerivAt_sinh (α * t)).comp t (hasDerivAt_alpha_mul α t)
 111  convert h1.div_const α using 1
 112  field_simp
 113
 114/-- **Calibration Invariance**: G_α''(0) = 1 for every α ≠ 0.
 115    The unit-curvature condition is independent of the rescaling parameter. -/
 116theorem costAlphaLog_unit_curvature (α : ℝ) (hα : α ≠ 0) :
 117    deriv (deriv (CostAlphaLog α)) 0 = 1 := by
 118  rw [deriv_costAlphaLog_eq α hα, (hasDerivAt_sinhDivAlpha α hα 0).deriv,
 119      mul_zero, cosh_zero]
 120
 121/-! ## WLOG Theorem -/
 122
 123/-- **WLOG α = 1**: Every calibrated cost F_α is the canonical cost J under
 124    coordinate rescaling. The parameter α does not introduce a structurally
 125    new cost function.
 126
 127    Components:
 128    1. Rescaling identity: F_α(x) = (1/α²) · J(x^α)
 129    2. Recovery: F₁(x) = J(x)
 130    3. Group automorphism: (xy)^α = x^α · y^α
 131    4. Calibration invariance: G_α''(0) = 1 -/
 132theorem wlog_alpha_eq_one (α : ℝ) (hα : 0 < α) :
 133    (∀ x : ℝ, 0 < x → CostAlpha α x = (1 / α ^ 2) * Jcost (x ^ α))
 134    ∧ (∀ x : ℝ, 0 < x → CostAlpha 1 x = Jcost x)
 135    ∧ (∀ x y : ℝ, 0 < x → 0 < y → (x * y) ^ α = x ^ α * y ^ α)
 136    ∧ deriv (deriv (CostAlphaLog α)) 0 = 1 :=
 137  ⟨fun x hx => cost_alpha_rescaling α x hx,