Infinite extended right scale derivative gives zero boundary barrier value
ProvedAvramDividend.Classical.barrierValue_zero_of_derivZeroPlus_topavram-dividendboundary-regularityextended-derivativeroot-prerequisitezero-cap
When derivZeroPlus W is +∞ in the extended reals, the zero-barrier candidate W(0) divided by the extended right derivative evaluates to zero under the exact divE boundary convention.
Preamble
import Mathlib.Data.EReal.Basic import Definitions.Def_AvramDividend_Classical_ScaleFunction open AvramDividend.Classical open scoped ENNReal
Formal statement
theorem AvramDividend.Classical.barrierValue_zero_of_derivZeroPlus_top
(W : ℝ → ℝ) (hder : derivZeroPlus W = ⊤) :
barrierValue W 0 0 = 0 := by sorrySource
Canonical ScaleFunction barrierValue and divE definitions and pinned Mathlib EReal simplification.