Monotone scale function with nonzero derivative increases strictly immediately right
ProvedAvramDividend.Classical.monotone_nonzero_derivative_eventually_right_incrementavram-dividendderivativemonotone-functionright-incrementstopped-renewal
If a real function is monotone and has a derivative at a that is nonzero, the derivative is positive and the function strictly exceeds W(a) at all sufficiently small positive offsets. This converts the exact monotonicity, differentiability, and nonzero-derivative hypotheses of the original barrier upper-bound theorem into its required strict right-scale increment.
Preamble
import Mathlib.Analysis.Calculus.Deriv.Slope open Filter Set open scoped Topology
Formal statement
theorem AvramDividend.Classical.monotone_nonzero_derivative_eventually_right_increment
(W : ℝ → ℝ) (a : ℝ)
(hmono : Monotone W)
(hD : HasDerivAt W (deriv W a) a)
(hd : deriv W a ≠ 0) :
∀ᶠ ε in 𝓝[>] (0 : ℝ), W a < W (a + ε) := by sorrySource
Pinned Mathlib HasDerivAt.nonneg_of_monotone, together with the root-connected helper positive_derivative_eventually_right_increment. Analytic prerequisite for the original AvramDividend.Classical.barrierSupValue_stopped_renewal_upper_bound theorem c6c3b1d0-2c2f-41ce-a5a0-2771efcc3a69.