Gaussian zero-cap boundary package from positive-barrier scale values

Proved

AvramDividend.Classical.zero_cap_boundary_value_package_gaussian_of_positive_scale_ratio

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

avram-dividendgaussianroot-prerequisitestochastic-reflectionzero-cap

For a standing spectrally negative Lévy process with positive Gaussian coefficient, the full zero-cap boundary estimate holds whenever the actual positive-barrier reflected dividend value equals W(a)/W'(a) at reciprocal barriers a. Gaussian C2 regularity, vanishing scale origin and the exact positive finite right slope 2/σ² are canonically Proved, and therefore supply all analytic zero-boundary hypotheses automatically. The only remaining premise is the missing stochastic positive-barrier identity; the conclusion is an actual proof of the zero-cap package under that condition.

Preamble

import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Tactic.Positivity
import Theorems.Thm_AvramDividend_Classical_scaleFunction_contDiff_two_of_gaussian
import Theorems.Thm_AvramDividend_Classical_scaleFunction_zero_origin_gaussian_without_standing
import Theorems.Thm_AvramDividend_Classical_scaleFunction_derivRightLimit_at_zero_eq_two_over_sigma
import Theorems.Thm_AvramDividend_Classical_barrierValue_zero_boundary_nonneg
import Theorems.Thm_AvramDividend_Classical_zero_cap_value_at_zero_upper_bound_of_boundary
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_zero_boundary_of_positive_ratio_and_finite_deriv_limit

open AvramDividend.Classical MeasureTheory Filter Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.zero_cap_boundary_value_package_gaussian_of_positive_scale_ratio
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hX : X.Standing)
    (q : ℝ) (hq : 0 < q) (W : ℝ → ℝ)
    (hW : IsScaleFunction X q W) (hσ : 0 < X.σ)
    (hscale : ∀ n : ℕ,
      barrierSupValue X (1 / ((n : ℝ) + 1)) q =
        ENNReal.ofReal (W (1 / ((n : ℝ) + 1)) /
          deriv W (1 / ((n : ℝ) + 1)))) :
    0 ≤ barrierValue W 0 0 ∧
      valueFunctionLe X q 0 0 ≤ ENNReal.ofReal (barrierValue W 0 0) := by sorry

Source

Canonical Gaussian C2 theorem 4c4d5e79-8440-49a7-a008-66422a4cd211, origin-zero theorem 20b1acb4-bfe6-483b-bceb-2f0bbd6b6842, right slope 62495c30-344f-4493-8c5c-065915fe8ac3 and zero-cap boundary transfer fb8027bb-7b35-43db-b240-15e57d3ba650.

View graph