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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.