The path-only Gamma identity

The remaining lifetime gives the size-tail identity. Gamma weighting cancels its survival kernel and the unit prefix density supplies the normalization.

Main results

• levyExcLaw_prefix_eq_withDensity_tail: the unit prefix law is the Gamma-weighted tail prefix measure.
• lintegral_gamma_identity_path: the Gamma identity for nonnegative measurable path tests.
• gamma_identity_path: the Gamma identity for bounded signed path tests.
• integral_gammaA_tail_eq_one: the Gamma weight integrates to one against the tail prefix.
• excursionTail_size_tail: the size-tail identity for the excursion tail measure.

References

• T. Duquesne, A limit theorem for the contour process of conditioned Galton--Watson trees, Ann. Probab. 31 (2003), 996--1027; path-prefix absolute continuity.
• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.
• T. Duquesne, Path decompositions for real Lévy processes, Ann. Inst. H. Poincaré Probab. Statist. 39 (2003), 339–370.
• T. Duquesne and J.-F. Le Gall, Random Trees, Lévy Processes and Spatial Branching Processes, Astérisque 281 (2002).
• I. Kortchemski, A simple proof of Duquesne's theorem on contour processes of conditioned Galton--Watson trees, arXiv:1109.4138, Proposition 2.3 (path part).

noncomputable def BGW.StableTrees.tailPrefix (θ : ℝ) (a : NNReal) : MeasureTheory.Measure (Skorokhod.D ↑a ℝ)

Law of the excursion prefix under the normalized lifetime tail.

Equations

• BGW.StableTrees.tailPrefix θ a = MeasureTheory.Measure.map (BGW.StableTrees.excursionRestrict a) ↑(BGW.StableTrees.tailExcursionLaw θ)

noncomputable def BGW.StableTrees.evalEnd (a : NNReal) (x : Skorokhod.D ↑a ℝ) : ℝ

Endpoint coordinate of a compact path.

Equations

• BGW.StableTrees.evalEnd a x = x ⟨↑a, ⋯⟩

theorem BGW.StableTrees.evalEnd_excursionRestrict (a : NNReal) (e : Excursion) : evalEnd a (excursionRestrict a e) = ↑e.path a

Restriction preserves the endpoint value.

theorem BGW.StableTrees.measurable_evalEnd (a : NNReal) : Measurable (evalEnd a)

The endpoint coordinate is measurable.

theorem BGW.StableTrees.ae_evalEnd_pos_tailPrefix {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ∀ᵐ (x : Skorokhod.D ↑a ℝ) ∂tailPrefix θ a, 0 < evalEnd a x

Almost sure positivity of the endpoint under the tail prefix law.

theorem BGW.StableTrees.excursionTail_size_tail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (F : Skorokhod.D ↑a ℝ → ENNReal) (hF : Measurable F) : ∫⁻ (e : Excursion), F (excursionRestrict a e) ∂excursionTail θ 1 = ∫⁻ (e : Excursion), F (excursionRestrict a e) * sizeTailKernelENN θ (1 - ↑a) (↑e.path a) ∂excursionTail θ ↑a

Size-tail identity from the remaining lifetime and Kendall's tail kernel.

theorem BGW.StableTrees.measurable_gammaA_evalEnd (θ : ℝ) (a : NNReal) : Measurable fun (x : Skorokhod.D ↑a ℝ) => ENNReal.ofReal (gammaA θ (↑a) (evalEnd a x))

Measurability of the Gamma density on the prefix space.

theorem BGW.StableTrees.lintegral_gamma_identity_path {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (F : Skorokhod.D ↑a ℝ → ENNReal) (hF : Measurable F) : ∫⁻ (x : Skorokhod.D ↑a ℝ), F x ∂unitPrefix θ a = ∫⁻ (x : Skorokhod.D ↑a ℝ), F x * ENNReal.ofReal (gammaA θ (↑a) (evalEnd a x)) ∂tailPrefix θ a

Gamma-weighted tail prefix integrals equal unit-prefix integrals.

theorem BGW.StableTrees.levyExcLaw_prefix_eq_withDensity_tail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : unitPrefix θ a = (tailPrefix θ a).withDensity fun (x : Skorokhod.D ↑a ℝ) => ENNReal.ofReal (gammaA θ (↑a) (evalEnd a x))

The unit prefix is obtained by weighting the tail prefix by Gamma.

theorem BGW.StableTrees.integral_gammaA_tail_eq_one {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : MeasureTheory.Integrable (fun (x : Skorokhod.D ↑a ℝ) => gammaA θ (↑a) (evalEnd a x)) (tailPrefix θ a) ∧ ∫ (x : Skorokhod.D ↑a ℝ), gammaA θ (↑a) (evalEnd a x) ∂tailPrefix θ a = 1

Gamma is integrable under the tail prefix law and has expectation one.

theorem BGW.StableTrees.gamma_identity_path {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (F : Skorokhod.D ↑a ℝ → ℝ) (hF : Measurable F) (hb : ∃ (C : ℝ), ∀ (x : Skorokhod.D ↑a ℝ), |F x| ≤ C) : ∫ (x : Skorokhod.D ↑a ℝ), F x ∂unitPrefix θ a = ∫ (x : Skorokhod.D ↑a ℝ), F x * gammaA θ (↑a) (evalEnd a x) ∂tailPrefix θ a

Bounded signed path tests satisfy the Gamma identity.