Stable division of an oscillating asymptotic expansion

Proved

EulerMascheroni.P2.oscillatory_transfer

by shivm · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

euler-mascheroniformalizationrational-approximation

If real s,u,v satisfy |s|≤1 and |u|≤1/2, then |(s+v)/(1+u)−s|≤2(|v|+|u|). The bound is additive and remains valid near zeros of s. It transfers a numerator expansion and a relative denominator error without assuming the oscillation is bounded away from zero.

Preamble

import Definitions.Def_eulerMascheroni_p2Approximation
open Filter Topology
open EulerMascheroni.P2

Formal statement

theorem EulerMascheroni.P2.oscillatory_transfer (s u v : ℝ) (hs : |s| ≤ 1) (hu : |u| ≤ 1/2) :
    |(s+v)/(1+u)-s| ≤ 2 * (|v|+|u|) := by sorry

Source

Van Assche–Wolfs, https://arxiv.org/html/2404.09799v3, section 5 for the family. Local p=2 proof draft SADDLE_DRAFT.md, sections 4–5. These are elementary supporting results and a conditional reduction, not novelty claims.

View graph