Kendall adapter and Gamma analytic interface

The time-first Kendall kernel is adapted from the passage-time density theorem. Its survival kernel is identified with the passage-time tail, and is proved finite, positive, measurable, and jointly continuous on its natural domain. The Gamma factor inherits the corresponding regularity API.

Main declarations: qKernel (q_s(x) = (x/s) p_s(-x)), passageLaw_eq_qKernel, sizeTailKernelENN and sizeTailKernelENN_eq_passageLaw (G_r(x) = P(T_x > r)), the integrable dominator qKernel_le_of_ge, continuity and measurability lemmas, and gammaA with gammaA_mul_sizeTail.

References

• D. G. Kendall, Some problems in the theory of dams, J. Roy. Statist. Soc. Ser. B 19 (1957), 207–212.
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII (Corollary VII.3).

Definitions

noncomputable def BGW.StableTrees.qKernel (θ s x : ℝ) : ℝ

The Kendall density q_s(x) = (x/s) p_s(-x), time first, level second (real arguments, junk for s ≤ 0). Same function as kendallKernel θ x s.

Equations

• BGW.StableTrees.qKernel θ s x = x / s * BGW.StableTrees.stableDensityAt θ s (-x)

noncomputable def BGW.StableTrees.sizeTailKernelENN (θ r x : ℝ) : ENNReal

Survival (size-tail) kernel in the nonnegative-integral form ∫⁻_{s > r} q_s(x) ds (primary definition, never junk).

Equations

• BGW.StableTrees.sizeTailKernelENN θ r x = ∫⁻ (s : ℝ) in Set.Ioi r, ENNReal.ofReal (BGW.StableTrees.qKernel θ s x)

noncomputable def BGW.StableTrees.sizeTailKernel (θ r x : ℝ) : ℝ

Survival (size-tail) kernel G_r(x) = ∫_{s > r} q_s(x) ds as a real integral (equal to (sizeTailKernelENN θ r x).toReal for r ≥ 0, x ≥ 0, see ofReal_sizeTailKernel).

Equations

• BGW.StableTrees.sizeTailKernel θ r x = ∫ (s : ℝ) in Set.Ioi r, BGW.StableTrees.qKernel θ s x

noncomputable def BGW.StableTrees.gammaA (θ a x : ℝ) : ℝ

The Gamma factor Γ_a(x) = θ q_{1-a}(x) / G_{1-a}(x) of the path-only Γ identity.

Equations

• BGW.StableTrees.gammaA θ a x = θ * BGW.StableTrees.qKernel θ (1 - a) x / BGW.StableTrees.sizeTailKernel θ (1 - a) x

Adapter to the existing Kendall theorem

theorem BGW.StableTrees.qKernel_eq_kendallKernel (θ s x : ℝ) : qKernel θ s x = kendallKernel θ x s

qKernel is kendallKernel with the time argument first.

theorem BGW.StableTrees.qKernel_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {s x : ℝ} (hs : 0 < s) (hx : 0 ≤ x) : 0 ≤ qKernel θ s x

qKernel is nonnegative for x ≥ 0, s > 0.

theorem BGW.StableTrees.passageLaw_eq_qKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) (hx : 0 < x) : passageLaw θ x = MeasureTheory.volume.withDensity fun (s : ℝ) => ENNReal.ofReal (if 0 < s then qKernel θ s ↑x else 0)

Kendall's identity, time-first form. For x > 0, passageLaw θ x has density qKernel θ s x on s > 0 (and 0 elsewhere) w.r.t. Lebesgue measure on ℝ (a restatement of kendall).

Survival kernel: finiteness and identification

theorem BGW.StableTrees.sizeTailKernelENN_eq_passageLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {r : ℝ} (hr : 0 ≤ r) (x : NNReal) (hx : 0 < x) : sizeTailKernelENN θ r ↑x = (passageLaw θ x) (Set.Ioi r)

The tail is the passage-time tail: for r ≥ 0, x > 0, ∫⁻_{s>r} q_s(x) = P(T_x > r).

theorem BGW.StableTrees.sizeTailKernelENN_lt_top {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {r : ℝ} (hr : 0 ≤ r) {x : ℝ} (hx : 0 < x) : sizeTailKernelENN θ r x < ⊤

Finiteness of the survival kernel (it is at most 1), for r ≥ 0, x > 0.

theorem BGW.StableTrees.sizeTailKernelENN_lt_top_nnreal {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {r : ℝ} (hr : 0 ≤ r) {x : NNReal} (hx : 0 < x) : sizeTailKernelENN θ r ↑x < ⊤

Finiteness, x : ℝ≥0 form (same statement for the cast level).

theorem BGW.StableTrees.ofReal_sizeTailKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {r : ℝ} (hr : 0 ≤ r) {x : ℝ} (hx : 0 < x) : ENNReal.ofReal (sizeTailKernel θ r x) = sizeTailKernelENN θ r x

Conversion between the real and nonnegative-integral survival kernels (finite real-valued reading), for r ≥ 0, x > 0.

theorem BGW.StableTrees.continuousOn_qKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ContinuousOn (fun (z : ℝ × ℝ) => qKernel θ z.1 z.2) {z : ℝ × ℝ | 0 < z.1}

Joint continuity of q in (s, x) on s > 0 (adapter of kendallKernel_continuousOn).

theorem BGW.StableTrees.sizeTailKernel_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {r : ℝ} (hr : 0 < r) {x : ℝ} (hx : 0 < x) : 0 < sizeTailKernel θ r x

Positivity of the survival kernel: G_r(x) > 0 for r > 0, x > 0.

Continuity and local bounds

theorem BGW.StableTrees.qKernel_le_of_ge {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {r : ℝ} (hr : 0 < r) (X : ℝ) : ∃ (C : ℝ), ∀ (s : ℝ), r ≤ s → ∀ (x : ℝ), 0 ≤ x → x ≤ X → qKernel θ s x ≤ C * x * s ^ (-1 - 1 / θ)

Local integrable dominator (from Scalar.exists_stableDensity_le, q_s(x) = (x/s) p_s(-x) and p_s ≤ M s^{-1/θ}): for r > 0 and X ≥ 0 there is C (depending on θ, r, X) with q_s(x) ≤ C x s^{-1-1/θ} for all s ≥ r, 0 ≤ x ≤ X. The right side is integrable on s ≥ r (exponent -1-1/θ < -1), uniformly in x ≤ X.

theorem BGW.StableTrees.measurable_qKernel (θ : ℝ) : Measurable fun (z : ℝ × ℝ) => qKernel θ z.1 z.2

Measurability of q jointly in (s, x) on all of ℝ × ℝ.

theorem BGW.StableTrees.measurable_sizeTailKernelENN (θ : ℝ) : Measurable fun (z : ℝ × ℝ) => sizeTailKernelENN θ z.1 z.2

Measurability of the nonnegative size-tail kernel jointly in (r, x) (parametric lintegral of the jointly measurable measurable_qKernel).

theorem BGW.StableTrees.lintegral_qKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x : NNReal} (hx : 0 < x) : ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (qKernel θ s ↑x) = 1

Mass one of the Kendall density, in qKernel form (from lintegral_kendallKernel).

theorem BGW.StableTrees.continuousOn_sizeTailKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ContinuousOn (fun (z : ℝ × ℝ) => sizeTailKernel θ z.1 z.2) {z : ℝ × ℝ | 0 < z.1 ∧ 0 < z.2}

Joint continuity of the survival kernel in (r, x) on r > 0, x > 0, by dominated convergence with the integrable dominator of qKernel_le_of_ge.

theorem BGW.StableTrees.continuousOn_gammaA {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ContinuousOn (fun (z : ℝ × ℝ) => gammaA θ z.1 z.2) {z : ℝ × ℝ | z.1 < 1 ∧ 0 < z.2}

Continuity of Γ_a(x) jointly in (a, x) on a < 1, x > 0 (quotient of continuous functions with positive denominator sizeTailKernel_pos).

theorem BGW.StableTrees.measurable_gammaA (θ : ℝ) : Measurable fun (z : ℝ × ℝ) => gammaA θ z.1 z.2

Measurability of Γ jointly in (a, x).

theorem BGW.StableTrees.gammaA_mul_sizeTail {θ a x : ℝ} (h : 0 < sizeTailKernel θ (1 - a) x) : gammaA θ a x * sizeTailKernel θ (1 - a) x = θ * qKernel θ (1 - a) x

Defining identity of Γ: Γ_a(x) G_{1-a}(x) = θ q_{1-a}(x) when G_{1-a}(x) > 0.

theorem BGW.StableTrees.gammaA_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {a x : ℝ} (ha : a < 1) (hx : 0 < x) : 0 ≤ gammaA θ a x

Nonnegativity of Γ_a(x) for a < 1, x > 0.