alphaInv_of_gap

formal source

 121-/
 122
 123/-- The alphaInv function parameterized by f_gap value. -/
 124noncomputable def alphaInv_of_gap (g : ℝ) : ℝ := alpha_seed * Real.exp (-(g / alpha_seed))
 125
 126/-- At the canonical f_gap, alphaInv_of_gap agrees with alphaInv. -/
 127theorem alphaInv_of_gap_at_canonical : alphaInv_of_gap f_gap = alphaInv := rfl
 128
 129/-- The derivative of alphaInv with respect to f_gap. -/
 130theorem deriv_alphaInv_of_gap (g : ℝ) :
 131    deriv alphaInv_of_gap g = -(alphaInv_of_gap g / alpha_seed) := by
 132  unfold alphaInv_of_gap
 133  -- h1: derivative of g → -(g/alpha_seed) is -(1/alpha_seed)
 134  have h_id : HasDerivAt (fun g : ℝ => g) 1 g := hasDerivAt_id g
 135  have h_div : HasDerivAt (fun g : ℝ => g / alpha_seed) (1 / alpha_seed) g :=
 136    h_id.div_const alpha_seed
 137  have h1 : HasDerivAt (fun g : ℝ => -(g / alpha_seed)) (-(1 / alpha_seed)) g :=
 138    h_div.neg
 139  -- h2: derivative of exp(-(g/alpha_seed))
 140  have h2 : HasDerivAt (fun g : ℝ => Real.exp (-(g / alpha_seed)))
 141      (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed))) g :=
 142    (Real.hasDerivAt_exp _).comp g h1
 143  -- h3: scale by alpha_seed
 144  have h3 : HasDerivAt (fun g : ℝ => alpha_seed * Real.exp (-(g / alpha_seed)))
 145      (alpha_seed * (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed)))) g :=
 146    h2.const_mul alpha_seed
 147  -- Simplify the derivative expression
 148  have heq : alpha_seed * (Real.exp (-(g / alpha_seed)) * (-(1 / alpha_seed)))
 149       = -(alpha_seed * Real.exp (-(g / alpha_seed)) / alpha_seed) := by
 150    field_simp
 151  rw [← heq]
 152  exact h3.deriv
 153
 154/-- The logarithmic derivative: d ln(α⁻¹)/d(f_gap) = -1/α_seed (constant). -/