One-sided finite-difference quotient limits from HasDerivAt with nonzero derivative

Proved

AvramDividend.Classical.finite_difference_quotient_limit_of_hasDerivAt

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-differenceoptimal-dividendsscale-function

Let W : R -> R be differentiable at a with nonzero derivative. Then the two one-sided finite-difference quotients epsW(a-eps)/(W(a)-W(a-eps)) and epsW(a+eps)/(W(a+eps)-W(a)) both tend to W(a)/W'(a) as eps -> 0+. This is the pure-analysis bridge used in the sandwich passage for the reflected-barrier boundary value (Proposition 1 of Avram-Palmowski-Pistorius): once stopped-renewal lower/upper bounds squeeze the barrier value between these quotients, the limit identifies the scale ratio.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace AvramDividend.Classical

theorem finite_difference_quotient_limit_of_hasDerivAt
    (W : ℝ → ℝ) (a : ℝ)
    (hD : HasDerivAt W (deriv W a) a) (hd : deriv W a ≠ 0) :
    Filter.Tendsto (fun ε : ℝ => ε * W (a - ε) / (W a - W (a - ε)))
      (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (W a / deriv W a)) ∧
    Filter.Tendsto (fun ε : ℝ => ε * W (a + ε) / (W (a + ε) - W a))
      (nhdsWithin (0 : ℝ) (Set.Ioi 0)) (nhds (W a / deriv W a)) := by sorry

end AvramDividend.Classical

Source

Pure-analysis bridge for AvramDividend.Classical.barrierSupValue_eq_scale_ratio (a8d4c941) sandwich passage toward barrier_strategy_value (Proposition 1); extracted as an independently useful lemma with no stochastic premises

View graph