theorem MathlibNt.SieveTheory.SuzukiMainTermNormalization.hasDerivAt_log_div_log {D x : ℝ} (hx : x ≠ 0) (hlogx : Real.log x ≠ 0) : HasDerivAt (fun (y : ℝ) => Real.log D / Real.log y) (-Real.log D / (x * Real.log x ^ 2)) x

Derivative used in Suzuki's change of variables t = log D / log x.

theorem MathlibNt.SieveTheory.SuzukiMainTermNormalization.stieltjesMainTerm_changeOfVariables {D w z s σ : ℝ} {H : ℝ → ℝ} (hD : 1 < D) (hs : 0 < s) (hsσ : s ≤ σ) (hz : z = D ^ (1 / s)) (hw : w = D ^ (1 / σ)) (hH : Continuous H) : ∫ (x : ℝ) in w..z, H (Real.log D / Real.log x) * (Real.log z / (x * Real.log x ^ 2)) = 1 / s * ∫ (t : ℝ) in s..σ, H t

Exact change of variables behind the dimension-one main term. This is the ordinary-integral form of the Stieltjes term -∫ H(log D/log x) d(log z/log x). The orientation is important: x : w → z corresponds to t : σ → s.