Upper cap-linear discounted affine drift bounded by nonnegative drift
ProvedAvramDividend.Classical.avram_gfinite59_caplinear_affine_discount_drift_le_positive_partFor a nonnegative value at the cap-linear cutoff, nonnegative discount and a point above cutoff, the affine continuation contributes discounted drift at most the positive part of the original process drift. Direct deterministic scalar component of the original Gaussian upper-strip generator estimate; replaces a failed publisher specification with ambiguous process binders.
Preamble
import Mathlib noncomputable section
Formal statement
theorem AvramDividend.Classical.avram_gfinite59_caplinear_affine_discount_drift_le_positive_part
(c q wb b y : ℝ) (hq : 0 ≤ q)
(hwb : 0 ≤ wb) (hby : b ≤ y) :
c - q * (wb + (y - b)) ≤ max c 0 := by
sorry