 152  exact h3.deriv
 153
 154/-- The logarithmic derivative: d ln(α⁻¹)/d(f_gap) = -1/α_seed (constant). -/
 155theorem logarithmic_derivative_constant (g : ℝ) :
 156    deriv (fun g => Real.log (alphaInv_of_gap g)) g = -(1 / alpha_seed) := by
 157  have hpos : 0 < alphaInv_of_gap g := by
 158    unfold alphaInv_of_gap
 159    exact mul_pos alpha_seed_positive (Real.exp_pos _)
 160  have h_log_eq : ∀ g, Real.log (alphaInv_of_gap g) =
 161      Real.log alpha_seed + (-(g / alpha_seed)) := by
 162    intro g
 163    unfold alphaInv_of_gap
 164    rw [Real.log_mul (ne_of_gt alpha_seed_positive) (ne_of_gt (Real.exp_pos _)), Real.log_exp]
 165  -- deriv of (Real.log α_seed + (-(g / α_seed))) = deriv of (-(g/α_seed)) = -1/α_seed
 166  have h_fun_eq : (fun g => Real.log (alphaInv_of_gap g)) =
 167      (fun g => Real.log alpha_seed + (-(g / alpha_seed))) := by
 168    funext g
 169    exact h_log_eq g
 170  rw [h_fun_eq]
 171  have h_const_derivable : HasDerivAt (fun _ : ℝ => Real.log alpha_seed) 0 g :=
 172    hasDerivAt_const g _
 173  have h_lin_derivable : HasDerivAt (fun g => -(g / alpha_seed)) (-(1 / alpha_seed)) g := by
 174    have h1 : HasDerivAt (fun g : ℝ => g) 1 g := hasDerivAt_id g
 175    have h2 : HasDerivAt (fun g : ℝ => g / alpha_seed) (1 / alpha_seed) g :=
 176      h1.div_const alpha_seed
 177    exact h2.neg
 178  have : HasDerivAt (fun g => Real.log alpha_seed + (-(g / alpha_seed))) (0 + -(1 / alpha_seed)) g :=
 179    h_const_derivable.add h_lin_derivable
 180  rw [zero_add] at this
 181  exact this.deriv
 182
 183/-! ## Part 4: Inheritance from J-Cost Log Structure
 184
 185The J-cost J(x) = cosh(ln x) - 1 has Taylor expansion in log coordinates:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.