Positive scale derivative forces strict right increments near the barrier

Proved

AvramDividend.Classical.positive_derivative_eventually_right_increment

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

avram-dividendderivativerenewal-upperright-neighbourhoodscale-function

For a real function differentiable at a, a strictly positive derivative d implies that W(a+epsilon) is strictly greater than W(a) for every sufficiently small positive epsilon. This is the local analytical step needed to justify the strict denominator and geometric ratio used in the upper stopped-renewal finite-difference quotient.

Preamble

import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.Order.OrderClosed
import Mathlib.Algebra.Order.GroupWithZero.Basic

open Filter Set
open scoped Topology

Formal statement

theorem AvramDividend.Classical.positive_derivative_eventually_right_increment
    (W : ℝ → ℝ) (a d : ℝ)
    (hD : HasDerivAt W d a) (hd : 0 < d) :
    ∀ᶠ ε in 𝓝[>] (0 : ℝ), W a < W (a + ε) := by sorry

Source

Pinned Mathlib HasDerivAt.tendsto_slope_zero_right and eventual positivity of the right difference quotient. Analytic prerequisite for AvramDividend.Classical.barrierSupValue_stopped_renewal_upper_bound (c6c3b1d0-2c2f-41ce-a5a0-2771efcc3a69).

View graph