pith. machine review for the scientific record. sign in
theorem proved tactic proof

deriv_alphaInv_of_gap

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 130theorem deriv_alphaInv_of_gap (g : ℝ) :
 131    deriv alphaInv_of_gap g = -(alphaInv_of_gap g / alpha_seed) := by

proof body

Tactic-mode proof.

 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). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (27)

Lean names referenced from this declaration's body.