Un-killed q-scale martingale is false under the exact Lévy process assumptions
ProvedAvramDividend.Classical.unbounded_scale_reward_unstopped_martingale_falseavram-dividendformal-counterargumentmartingalestoppingstrict-exit
The un-killed discounted q-scale reward cannot be a martingale for any positive discount and unbounded-variation spectrally negative Levy process, under precisely the same process and scale-function hypotheses as the currently Open chat04_unbounded_discounted_scale_martingale theorem. The Lévy structure already supplies a probability measure; Mathlib's IsFiniteMeasure.sigmaFiniteFiltration instance supplies the apparent sigma-finite filtration hypothesis of the established non-martingale theorem. Consequently the existing prerequisite's theorem statement is mathematically false at zero initial reserve and must be corrected to a stopped/killed formulation.
Preamble
import Theorems.Thm_AvramDividend_Classical_unbounded_discounted_scale_unstopped_martingale_impossible import Mathlib.Probability.Process.Filtration open AvramDividend.Classical MeasureTheory open scoped NNReal
Formal statement
theorem AvramDividend.Classical.unbounded_scale_reward_unstopped_martingale_false
{Ω : Type*} [mΩ : MeasurableSpace Ω]
{P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
(X : SpectrallyNegativeLevy P 𝓕)
(q : ℝ) (hq : 0 < q)
(W : ℝ → ℝ) (hW : IsScaleFunction X q W)
(hnbv : ¬ X.BoundedVariation) :
¬ Martingale
(fun t : ℝ≥0 => fun ω : Ω =>
Real.exp (-(q * (t : ℝ))) * W (X.X t ω)) 𝓕 P := by sorrySource
Proved unbounded_discounted_scale_unstopped_martingale_impossible, SpectrallyNegativeLevy.isProbability, Mathlib IsFiniteMeasure.sigmaFiniteFiltration.