← Mathematical handbook

The derivative identity for the whole positive parameter interval

theorem Papers.Rockel2026XiBlest.formula_tail (b : ℝ) (hb : 0 ≤ b) : xiFormula b = 8 * b ^ 2 * (7 - 3 * b) / 105 + ∫ (p : ↑unitInterval × ↑unitInterval), Verification.xiTail b |Verification.squareDelta p| ∧ nuFormula b = 4 * b * (28 - 9 * b) / 105 + ∫ (p : ↑unitInterval × ↑unitInterval), Verification.nuTail b |Verification.squareDelta p|

noncomputable def Papers.Rockel2026XiBlest.boundaryDerivative (b : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.Rockel2026XiBlest.formula_hasDerivAt (b : ℝ) (hb : 0 < b) : HasDerivAt xiFormula (b * boundaryDerivative b) b ∧ HasDerivAt nuFormula (boundaryDerivative b) b

theorem Papers.Rockel2026XiBlest.formula_derivative_identity (b : ℝ) (hb : 0 < b) : deriv nuFormula b = deriv xiFormula b / b

Lemma 4.5 / equation (7), including b=1.

theorem Papers.Rockel2026XiBlest.formula_zero_limits : Filter.Tendsto xiFormula (nhds 0) (nhds 0) ∧ Filter.Tendsto nuFormula (nhds 0) (nhds 0)