Stopped means of the occupation error #
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.integral_errorMartingale_stopped
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{ε : ℝ}
(hε : 0 < ε)
(n : ℕ)
{σ : Skorokhod.DLoc → ENNReal}
(hσ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration σ)
(t : NNReal)
:
The stopped error has mean zero at every bounded horizon.
theorem
BGW.StableTrees.integral_supOccupation_stopped_le
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{ε : ℝ}
(hε : 0 < ε)
(n : ℕ)
{σ : Skorokhod.DLoc → ENNReal}
(hσ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration σ)
(t : NNReal)
:
∫ (f : Skorokhod.DLoc), supOccupation ε f (errStopTime n σ t f) - supAuxLocalTime θ f (errStopTime n σ t f) ∂↑(stableLocalLaw θ) = -∫ (f : Skorokhod.DLoc), occupationCorrection θ ε (errStopTime n σ t f) f ∂↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), supOccupation ε f (errStopTime n σ t f) ∂↑(stableLocalLaw θ) ≤ ∫ (f : Skorokhod.DLoc), supAuxLocalTime θ f (errStopTime n σ t f) ∂↑(stableLocalLaw θ) + 2 * supCorrectionBound θ ε
The mean occupation error is minus the mean correction, giving the stopped mean bound.