log_alphaInv_eq

formal source

  99  exact Real.log_exp _
 100
 101/-- Equivalent: ln(α⁻¹) = ln(α_seed) - f_gap/α_seed. -/
 102theorem log_alphaInv_eq :
 103    Real.log alphaInv = Real.log alpha_seed - f_gap / alpha_seed := by
 104  have h := log_alphaInv_seed_ratio
 105  rw [Real.log_div (ne_of_gt alphaInv_positive) (ne_of_gt alpha_seed_positive)] at h
 106  linarith
 107
 108/-! ## Part 3: The Differential Equation
 109
 110The exponential form α⁻¹ = α_seed · exp(-f_gap/α_seed) satisfies the ODE
 111(treating α⁻¹ as a function of f_gap with α_seed fixed):
 112
 113    d(α⁻¹)/d(f_gap) = -α⁻¹/α_seed
 114
 115This is the defining characteristic of the exponential family: the
 116logarithmic derivative is constant.
 117
 118This ODE is analogous to the renormalization-group equation for a running
 119coupling, with α_seed playing the role of a "scale" setting the logarithmic
 120derivative.
 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