First moments of the auxiliary clock

Compact square-mean convergence implies fixed-time convergence in mean. The arbitrary-rate resolvent bound then passes to the clock before recurrence is established.

References

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

theorem BGW.StableTrees.ae_supAuxLocalTime_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), 0 ≤ supAuxLocalTime θ f t

The clock is nonnegative at all times on one event.

theorem BGW.StableTrees.integrable_supAuxLocalTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supAuxLocalTime θ f T) ↑(stableLocalLaw θ)

The clock has integrable values at every deterministic time.

noncomputable def BGW.StableTrees.supAuxApproxError (θ ε : ℝ) (T : NNReal) (f : Skorokhod.DLoc) : ℝ

The compact approximation error used in the square-mean estimate.

Equations

• BGW.StableTrees.supAuxApproxError θ ε T f = ⨆ (t : ↑(Set.Iic T)), |BGW.StableTrees.supOccupation ε f ↑t - BGW.StableTrees.supAuxLocalTime θ f ↑t|

theorem BGW.StableTrees.ae_abs_sub_le_supAuxApproxError {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (T : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), |supOccupation ε f T - supAuxLocalTime θ f T| ≤ supAuxApproxError θ ε T f

The fixed-time error is bounded by the compact error on the continuous-path event.

theorem BGW.StableTrees.integral_abs_sub_le_supAuxApproxError {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (T : NNReal) : ∫ (f : Skorokhod.DLoc), |supOccupation ε f T - supAuxLocalTime θ f T| ∂↑(stableLocalLaw θ) ≤ δ + (∫ (f : Skorokhod.DLoc), supAuxApproxError θ ε T f ^ 2 ∂↑(stableLocalLaw θ)) / δ

An elementary square bound converts compact square error into fixed-time mean error.

theorem BGW.StableTrees.tendsto_integral_abs_supOccupation_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), |supOccupation ε f T - supAuxLocalTime θ f T| ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Fixed-time occupations converge in mean along the full positive-cutoff filter.

theorem BGW.StableTrees.tendsto_integral_supOccupation {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), supOccupation ε f T ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (f : Skorokhod.DLoc), supAuxLocalTime θ f T ∂↑(stableLocalLaw θ)))

The occupation means converge to the clock mean.

theorem BGW.StableTrees.integral_supAuxLocalTime_le_exp {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (T : NNReal) : ∫ (f : Skorokhod.DLoc), supAuxLocalTime θ f T ∂↑(stableLocalLaw θ) ≤ Real.exp (q * ↑T) * (q ^ (1 / θ) / q)

The arbitrary-rate first-moment growth bound passes to the clock.