Infinite-activity bounded-variation drift deficit strictly increases between all ordered countable observation-grid pairs almost surely
ProvedAvramDividend.Classical.bv_infinite_activity_deficit_strict_grid_pairsavram-classicalcountable-gridinfinite-activitypath-regularitystrict-increase
For any countable observation grid of nonnegative times, an actual bounded-variation spectrally negative Lévy process with infinite negative-jump activity has strictly increasing canonical drift deficit at every strictly ordered grid pair on a common probability-one event. Uses fixed-interval strict increment law and two applications of ae_all_iff.
Preamble
import Theorems.Thm_AvramDividend_Classical_bv_infinite_activity_drift_deficit_increment_strict_ae import Mathlib.MeasureTheory.OuterMeasure.AE open AvramDividend.Classical MeasureTheory Set open scoped NNReal ENNReal
Formal statement
theorem AvramDividend.Classical.bv_infinite_activity_deficit_strict_grid_pairs
{Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
{𝓕 : Filtration ℝ≥0 mΩ}
(X : SpectrallyNegativeLevy P 𝓕)
(hBV : X.BoundedVariation)
(hνinf : X.ν (Iio (0 : ℝ)) = ⊤)
(grid : ℕ → ℝ≥0) :
∀ᵐ ω ∂P, ∀ i j : ℕ, grid i < grid j →
X.drift * (grid i : ℝ) - X.X (grid i) ω <
X.drift * (grid j : ℝ) - X.X (grid j) ω := by sorrySource
Accepted bv_infinite_activity_drift_deficit_increment_strict_ae and Mathlib ae_all_iff.