Progressive discounted heads for the raw auxiliary clock #
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.isStronglyProgressive_integral_head
{F : NNReal → Skorokhod.DLoc → ℝ}
(hF : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration F)
{w : ℝ → ℝ}
(hw : Measurable w)
:
MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) =>
∫ (s : ℝ) in Set.Ioc 0 ↑t, w s * F s.toNNReal f
A progressive real process has a progressive bounded-time integral. The integral is read as a totalized Bochner integral on every path.
theorem
BGW.StableTrees.isStronglyProgressive_discountedErrorMartingale
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{q ε : ℝ}
(hq : 0 < q)
(hε : 0 < ε)
:
MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) =>
discountedErrorMartingale θ q ε t f
The positive-rate error is progressive with the raw integration-by-parts head.