Time-zero expected q-scale continuity along bounded deterministic observation times

Proved

AvramDividend.Classical.chat04_positive_reserve_deterministic_scale_expectation_tendsto

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

expectation-convergencescale-functionstime-zerotwo-sided-exituniform-integrability

For any nonnegative discount q and positive initial reserve x, and any bounded deterministic sequence of times tending to zero, the expectation of exp(-q t) W(x+X_t) converges to W(x), provided the Lévy exponent exceeds q at a nonnegative θ. Uses the newly Proved uniform deterministic-horizon L² bound and an already Proved second-moment Vitali convergence lemma. This controls terminal-only q-scale expectation near time zero and supports the whole-history killed q-scale harmonicity input for the strict two-sided exit identity.

Preamble

import Theorems.Thm_AvramDividend_Classical_chat04_deterministic_horizon_scale_l2_uniform_bound
import Theorems.Thm_AvramDividend_Classical_chat04_positive_reserve_discounted_scale_tendsto_initial
import Theorems.Thm_AvramDividend_Classical_chat03_scale_function_borel_measurable
import Theorems.Thm_AvramDividend_Classical_nonnegative_integral_tendsto_of_uniform_second_moment
import Mathlib.MeasureTheory.Integral.Bochner.Basic

open MeasureTheory Filter Topology AvramDividend.Classical
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.chat04_positive_reserve_deterministic_scale_expectation_tendsto
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (hq : 0 ≤ q) (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (θ x : ℝ) (hθ : 0 ≤ θ) (hψ : q < X.ψ θ) (hx : 0 < x)
    (N : ℝ≥0) (t : ℕ → ℝ≥0) (htN : ∀ n, t n ≤ N)
    (ht0 : Filter.Tendsto t Filter.atTop (𝓝 0)) :
    Filter.Tendsto
      (fun n => ∫ ω, Real.exp (-(q * (t n : ℝ))) *
        W (x + X.X (t n) ω) ∂P)
      Filter.atTop (𝓝 (W x)) := by sorry

Source

Exact Proved import chain: deterministic horizon L² 19551a5a, positive reserve pathwise convergence 4940fc29, scale Borel measurability 45cbe3b4, uniform second moment expectation convergence bef79c38. Next: full-filter terminal-only expectation and unbounded killed harmonicity a885f0b3, then stopped exit 09663d0d.

View graph