Measurability of the shifted reserve's closed-horizon nonruin event
ProvedAvramDividend.Classical.chat04_shifted_lower_survival_measurablekilled-processmeasurabilitysurvivaltwo-sided-exit
Assuming an observation schedule covering reciprocal-natural time grids, the exact closed-horizon event that a Lévy reserve started at x remains nonnegative at every earlier time is measurable. This reformulates the already Proved lower-barrier survival filtration theorem with barrier -x and is needed to apply the killed L² bound and Vitali expectation-convergence lemma to the truly whole-history killed q-scale reward.
Preamble
import Theorems.Thm_AvramDividend_Classical_chat03_lower_survival_filtration_measurable import Mathlib.Tactic.Linarith open AvramDividend.Classical MeasureTheory Set open scoped NNReal
Formal statement
theorem AvramDividend.Classical.chat04_shifted_lower_survival_measurable
{Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
{𝓕 : Filtration ℝ≥0 mΩ}
(X : SpectrallyNegativeLevy P 𝓕)
(τ : ℕ → ℝ≥0)
(hCover : ∀ n : ℕ, 0 < n → ∀ k : ℕ,
∃ j : ℕ, τ j = (k : ℝ≥0) * (n : ℝ≥0)⁻¹)
(x : ℝ) (t : ℝ≥0) :
MeasurableSet {ω | ∀ s : ℝ≥0,
s ≤ t → 0 ≤ x + X.X s ω} := by sorrySource
Direct import of Proved chat03_lower_survival_filtration_measurable UUID 398891d8 and filtration monotonicity. Downstream: positive-reserve killed expected-scale initial continuity, then killed renewal a885f0b3, stopped exit 09663d0d.