Strict convexity of the q-scale function family in the discount
ProvedAvramDividend.Classical.unbounded_scale_discount_family_strictConvexOnavram-classicaldiscountscale-functionsensitivitystrict-convexity
For each positive reserve of an unbounded-variation spectrally negative Lévy process, the scale function indexed by every nonnegative discount is strictly convex as a real-valued function of the discount on [0,∞). The standard StrictConvexOn predicate supports downstream Jensen and slope arguments.
Preamble
import Mathlib.Analysis.Convex.Slope import Theorems.Thm_AvramDividend_Classical_unbounded_scale_discount_strict_convex_secants open AvramDividend.Classical MeasureTheory Set open scoped NNReal ENNReal
Formal statement
theorem AvramDividend.Classical.unbounded_scale_discount_family_strictConvexOn
{Ω : Type*} [mΩ : MeasurableSpace Ω]
{P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
(X : SpectrallyNegativeLevy P 𝓕) (hnbv : ¬ X.BoundedVariation)
(W : ℝ → ℝ → ℝ)
(hW : ∀ q : ℝ, 0 ≤ q → IsScaleFunction X q (W q)) :
∀ x : ℝ, 0 < x →
StrictConvexOn ℝ (Ici (0 : ℝ)) (fun q : ℝ => W q x) := by sorrySource
The verified strict increase of consecutive discount secant slopes and Mathlib's strictConvexOn_of_slope_strict_mono_adjacent criterion.