Evaluating cutoff prefix densities at lifetime one

Fix a cylinder test before invoking the lifetime identity. Continuity on both sides upgrades almost-everywhere equality to equality at lifetime one.

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.integrable_prefix_cutoff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b : NNReal) (hb : 0 < b) (H : Excursion → ℝ) (hH : Measurable H) (hHb : ∃ (C : ℝ), ∀ (e : Excursion), |H e| ≤ C) (χ : ℝ → ℝ) (hχ : Continuous χ) (hχc : HasCompactSupport χ) {s : ℝ} (hs : 0 < s) : MeasureTheory.Integrable (fun (e : Excursion) => H e * χ (↑e.path b) * qKernel θ s (↑e.path b)) (excursionTail θ ↑b)

Compact endpoint cutoffs make the positive-time prefix density integrable.

theorem BGW.StableTrees.integral_goodTimes_eq_density_at_one {θ : ℝ} (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) (χ : ℝ → ℝ) (hχ : Continuous χ) (hχc : HasCompactSupport χ) : ∫ (e : Excursion), (φ fun (i : Fin n) => ↑e.path (t i)) * χ (↑e.path b) ∂↑(unitExcursionLaw θ) = (Scalar.stableDensity θ 0)⁻¹ * ∫ (e : Excursion) in {e : Excursion | ↑b < ↑e.lifetime}, (φ fun (i : Fin n) => ↑e.path (t i)) * χ (↑e.path b) * qKernel θ (1 - ↑b) (↑e.path b) ∂excursionMeasure θ

Evaluation of the prefix density at lifetime one on good-time cutoff cylinders.