log_alphaInv_seed_ratio

formal source

  93-/
  94
  95/-- The log of the ratio alphaInv/alpha_seed equals -f_gap/alpha_seed. -/
  96theorem log_alphaInv_seed_ratio :
  97    Real.log (alphaInv / alpha_seed) = -(f_gap / alpha_seed) := by
  98  rw [alphaInv_seed_ratio]
  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. -/