Removing the inverse-clock localization

Eventual equality on the whole stopped interval transfers bounded martingale estimates by Fatou. The resulting maximal moment supplies an integrable domination for the means.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.ae_eventually_errStopTime_eq_min {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᶠ (n : ℕ) in Filter.atTop, supAuxLadderTime θ z f ≤ ↑n ∧ ∀ (s : NNReal), errStopTime n (supHitting θ z) s f = min s (supAuxLadderTime θ z f)

Eventually the epoch is the minimum with the auxiliary inverse, at every horizon.

theorem BGW.StableTrees.ae_eventually_sup_errStopTime_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) (X : NNReal → Skorokhod.DLoc → ℝ) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᶠ (n : ℕ) in Filter.atTop, ⨆ (s : ↑(Set.Iic ↑n)), X (errStopTime n (supHitting θ z) (↑s) f) f = ⨆ (s : ↑(Set.Iic (supAuxLadderTime θ z f))), X (↑s) f

Any stopped compact supremum eventually equals its supremum up to the inverse clock. This is equality of ranges, so it does not rely on conditional-completeness bounds.

theorem BGW.StableTrees.integral_sq_sup_errorMartingale_supAuxLadderTime_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => (⨆ (s : ↑(Set.Iic (supAuxLadderTime θ z f))), |errorMartingale θ ε (↑s) f|) ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), (⨆ (s : ↑(Set.Iic (supAuxLadderTime θ z f))), |errorMartingale θ ε (↑s) f|) ^ 2 ∂↑(stableLocalLaw θ) ≤ 4 * (4 * ↑z * supCorrectionBound θ ε + 12 * supCorrectionBound θ ε ^ 2)

The martingale maximum up to the finite inverse clock has a finite second moment.

theorem BGW.StableTrees.integral_sq_supOccupation_sub_supAuxLadderTime_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => (supOccupation ε f (supAuxLadderTime θ z f) - ↑z) ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), (supOccupation ε f (supAuxLadderTime θ z f) - ↑z) ^ 2 ∂↑(stableLocalLaw θ) ≤ 4 * ↑z * supCorrectionBound θ ε + 12 * supCorrectionBound θ ε ^ 2

Stopped energy at A^*_z: E (O_ε(A^*_z) - z)² ≤ 4 z V_ε + 12 V_ε².

theorem BGW.StableTrees.ae_errStopTime_le_supAuxLadderTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (n : ℕ) (s : NNReal), errStopTime n (supHitting θ z) s f ≤ supAuxLadderTime θ z f

Every localized epoch lies below the finite inverse, on one event for all indices.

theorem BGW.StableTrees.ae_bddAbove_errorMartingale_supAuxLadderTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), BddAbove (Set.range fun (s : ↑(Set.Iic (supAuxLadderTime θ z f))) => |errorMartingale θ ε (↑s) f|)

The inverse-time martingale supremum is a genuine bounded real supremum almost surely.

theorem BGW.StableTrees.integral_supOccupation_supAuxLadderTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supOccupation ε f (supAuxLadderTime θ z f)) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), supOccupation ε f (supAuxLadderTime θ z f) ∂↑(stableLocalLaw θ) = ↑z

Exact mean: E O_ε(A^*_z) = z (uniform integrability from the L² bound; A^*_z < ∞ and R_{A^*_z} = 0), with integrability.