The normalized prefix-density candidate at good horizons

Increasing endpoint cutoffs give mass equal to the stable density at zero. Bounded convergence then removes the cutoffs from every good-time cylinder test.

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.lintegral_prefix_density_mass_of_good {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b : NNReal) (hb : b ∈ Set.Ioo 0 1) (hbgood : NoFixedJumpUnit θ b) : ∫⁻ (e : Excursion), ENNReal.ofReal (qKernel θ (1 - ↑b) (↑e.path b)) ∂excursionTail θ ↑b = ENNReal.ofReal (Scalar.stableDensity θ 0)

At a good horizon the prefix density has mass equal to the stable density at zero.

noncomputable def BGW.StableTrees.prefixDensityMeasure (θ : ℝ) (a : NNReal) : MeasureTheory.Measure Excursion

The unnormalized Kendall-weighted excursion survival measure.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.measurable_prefixDensity (θ : ℝ) (a : NNReal) : Measurable fun (e : Excursion) => ENNReal.ofReal (qKernel θ (1 - ↑a) (↑e.path a))

Measurability of the prefix density.

theorem BGW.StableTrees.prefixDensityMeasure_univ_of_good {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (hgood : NoFixedJumpUnit θ a) : (prefixDensityMeasure θ a) Set.univ = ENNReal.ofReal (Scalar.stableDensity θ 0)

Good-horizon normalization of the unnormalized density measure.

theorem BGW.StableTrees.isFiniteMeasure_prefixDensityMeasure_of_good {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (hgood : NoFixedJumpUnit θ a) : MeasureTheory.IsFiniteMeasure (prefixDensityMeasure θ a)

Finiteness of the density measure at a good horizon.

theorem BGW.StableTrees.tendsto_integral_prefixCutoff (μ : MeasureTheory.Measure Excursion) [MeasureTheory.IsFiniteMeasure μ] (a : NNReal) (F : Excursion → ℝ) (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (e : Excursion), |F e| ≤ C) : Filter.Tendsto (fun (n : ℕ) => ∫ (e : Excursion), F e * prefixCutoff n (↑e.path a) ∂μ) Filter.atTop (nhds (∫ (e : Excursion), F e ∂μ))

Removing endpoint cutoffs under a finite excursion measure.

theorem BGW.StableTrees.integral_goodTimes_eq_prefixDensityMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b : NNReal) (hb : b ∈ Set.Ioo 0 1) (hbgood : NoFixedJumpUnit θ b) {n : ℕ} (t : Fin n → NNReal) (ht : ∀ (i : Fin n), t i ≤ b) (hgood : ∀ (i : Fin n), NoFixedJumpUnit θ (t i)) (φ : (Fin n → ℝ) → ℝ) (hφ : Continuous φ) (hφb : ∃ (C : ℝ), ∀ (x : Fin n → ℝ), |φ x| ≤ C) : ∫ (e : Excursion), φ fun (i : Fin n) => ↑e.path (t i) ∂↑(unitExcursionLaw θ) = (Scalar.stableDensity θ 0)⁻¹ * ∫ (e : Excursion), φ fun (i : Fin n) => ↑e.path (t i) ∂prefixDensityMeasure θ b

Good-time cylinder integrals without the endpoint cutoff.