def definition def or abbrev

`alphaInv_of_gap`

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

formal statement (Lean)

 124noncomputable def alphaInv_of_gap (g : ℝ) : ℝ := alpha_seed * Real.exp (-(g / alpha_seed))

Definition body.

 125
 126/-- At the canonical f_gap, alphaInv_of_gap agrees with alphaInv. -/

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

alphaInv_linear_rate in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_linear_term in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_of_gap_at_canonical in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
deriv_alphaInv_of_gap in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
logarithmic_derivative_constant in IndisputableMonolith.Constants.AlphaExponentialForm decl_use

Lean names referenced from this declaration's body.