Positive-reserve unit derivative of the zero-extended affine verification candidate

Proved

AvramDividend.Classical.affine_cutoff_deriv_eq_one_positive

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

counterexample-auditgradientoptimal-dividendsstochastic-verificationunbounded-variation

The candidate verification function equal to zero below reserve zero and z−1 for nonnegative reserves has derivative one at every strictly positive reserve. The proof uses its agreement with the affine function on a neighbourhood of any positive point. This discharges the gradient inequality in the Gaussian counterexample audit of the unbounded-variation stochastic verification theorem.

Preamble

import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Topology.Order.Basic
import Mathlib.Tactic

open Filter Set
open scoped Topology

Formal statement

theorem AvramDividend.Classical.affine_cutoff_deriv_eq_one_positive
    (y : ℝ) (hy : 0 < y) :
    deriv (fun z : ℝ => if z < 0 then 0 else z - 1) y = 1 := by sorry

Source

Avram, Palmowski and Pistorius (2007), Proposition 4(i), derivative HJB condition.

View graph