Bounded stopped energy at the auxiliary inverse clock

The strict hitting representative agrees almost surely with the finite auxiliary ladder time. On the same event the stopped clock is bounded by its level, and the localization eventually disappears on the whole interval up to the ladder time.

The stopped mean bound uses the centered error martingale of BGW.StableTrees.SupremumCorrection. The imported mesh lemmas and dominated convergence give the bounded-epoch energy estimate with constants 4 and 12. Nonnegativity of the centered correction allows the clock-increment term to be discarded in the grid inequality.

References

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

theorem BGW.StableTrees.occupationCorrection_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (t : NNReal) (f : Skorokhod.DLoc) : 0 ≤ occupationCorrection θ ε t f

The centered correction is nonnegative on every reflected state. The index-two constant cancels upon centering, just as it does for the other indices.

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

The stopping representative of A^*_z is A^*_z, almost surely, and is finite (ae_supLadder_geometry and ae_supLadder_eq_aux).

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

Up to the stopping epoch τ = σ ∧ t ∧ cutoff_n, M^* ≤ z (monotone, M^*(A^*_z) = z), simultaneously in n, t.

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

The localization is removed for large parameters: almost surely, eventually in n, errStopTime n (supHitting θ z) s f = s for every s ≤ A^*_z, and at s = n it equals A^*_z.

theorem BGW.StableTrees.integral_supOccupation_errStopTime_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) (n : ℕ) (t : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supOccupation ε f (errStopTime n (supHitting θ z) t f)) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), supOccupation ε f (errStopTime n (supHitting θ z) t f) ∂↑(stableLocalLaw θ) ≤ ↑z + 2 * supCorrectionBound θ ε

Mean occupation at the stopped epoch (E[O_ε(τ)] ≤ z + 2 V_ε), with integrability (0 ≤ O_ε(τ) ≤ τ/ε ≤ n/ε).

theorem BGW.StableTrees.ae_occupationCorrection_zero_dSupAux {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (ε : ℝ) (T : NNReal), (fun (s : ℝ) => occupationCorrection θ ε s.toNNReal f) =ᵐ[(supAuxStieltjes θ f).measure.restrict (Set.Ioc 0 ↑T)] 0

The centered correction vanishes almost everywhere for the auxiliary Stieltjes measure on every bounded positive interval, simultaneously for all widths.

theorem BGW.StableTrees.ae_occupationCorrection_supAuxLadderTime_eq_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (ε : ℝ) (z : NNReal), occupationCorrection θ ε (supAuxLadderTime θ z f) f = 0

At the finite auxiliary ladder time the centered correction vanishes, for all widths and levels on one event of full probability.

theorem BGW.StableTrees.tendsto_stopped_energy_bound {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : Filter.Tendsto (fun (ε : ℝ) => 104 * (↑z * supCorrectionBound θ ε + supCorrectionBound θ ε ^ 2)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The energy bound vanishes with ε (V_ε → 0, fixed z).

theorem BGW.StableTrees.monotone_errStopTime (n : ℕ) (σ : Skorokhod.DLoc → ENNReal) (f : Skorokhod.DLoc) : Monotone fun (s : NNReal) => errStopTime n σ s f

The bounded stopping epoch is monotone in its deterministic horizon.

theorem BGW.StableTrees.continuous_errStopTime (n : ℕ) (σ : Skorokhod.DLoc → ENNReal) (f : Skorokhod.DLoc) : Continuous fun (s : NNReal) => errStopTime n σ s f

As a function of the deterministic horizon the finite stopping epoch is continuous.

theorem BGW.StableTrees.integral_sq_errorMartingale_stopped_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) (n : ℕ) (t : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => errorMartingale θ ε (errStopTime n (supHitting θ z) t f) f ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), errorMartingale θ ε (errStopTime n (supHitting θ z) t f) f ^ 2 ∂↑(stableLocalLaw θ) ≤ 4 * ↑z * supCorrectionBound θ ε + 12 * supCorrectionBound θ ε ^ 2

Energy estimate E D_τ² ≤ 4 z V_ε + 12 V_ε² at τ = A_z ∧ t ∧ cutoff_n (summation by parts for the error martingale D against the finite-variation C = O - M^*; the dM^* term vanishes since w = 0 on {R = 0}).