Finite-dimensional increment laws of bridge prefixes

The increments on a strict prefix have the product stable law tilted by the density of the missing terminal increment. This supplies the finite-dimensional measure for the cyclic-invariance problem.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VIII (Vervaat's transformation and the uniform law of the minimum time); 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.map_increments_bridgePrefixLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) (n : ℕ) (t : Fin (n + 1) → ↑(Set.Icc 0 a)) (ht : StrictMono t) (ht0 : ↑(t 0) = 0) (htn : ↑(t (Fin.last n)) = a) : MeasureTheory.Measure.map (fun (f : Skorokhod.D a ℝ) (i : Fin n) => f (t i.succ) - f (t i.castSucc)) (bridgePrefixLaw θ a ⋯ ↑P) = (MeasureTheory.Measure.pi fun (i : Fin n) => ↑(stableLawAt θ (↑(t i.succ) - ↑(t i.castSucc)))).withDensity fun (x : Fin n → ℝ) => ENNReal.ofReal (stableDensityAt θ (1 - a) (-∑ i : Fin n, x i) / Scalar.stableDensity θ 0)

A strict-prefix increment vector has the independent increment law tilted by the transition density of the remaining increment to zero.

theorem BGW.StableTrees.map_pi_withDensity_sum_perm {ι : Type u_1} [Fintype ι] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SigmaFinite μ] {w : ℝ → ENNReal} (hw : Measurable w) (e : Equiv.Perm ι) : MeasureTheory.Measure.map (fun (x : ι → ℝ) (i : ι) => x (e i)) ((MeasureTheory.Measure.pi fun (x : ι) => μ).withDensity fun (x : ι → ℝ) => w (∑ i : ι, x i)) = (MeasureTheory.Measure.pi fun (x : ι) => μ).withDensity fun (x : ι → ℝ) => w (∑ i : ι, x i)

A product of identical increment laws tilted by a function of their sum is invariant under every coordinate permutation.

theorem BGW.StableTrees.map_increments_stableBridgeLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) (n : ℕ) (t : Fin (n + 1) → ↑(Set.Icc 0 a)) (ht : StrictMono t) (ht0 : ↑(t 0) = 0) (htn : ↑(t (Fin.last n)) = a) : MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) (i : Fin n) => f ⟨↑(t i.succ), ⋯⟩ - f ⟨↑(t i.castSucc), ⋯⟩) ↑(stableBridgeLaw θ) = (MeasureTheory.Measure.pi fun (i : Fin n) => ↑(stableLawAt θ (↑(t i.succ) - ↑(t i.castSucc)))).withDensity fun (x : Fin n → ℝ) => ENNReal.ofReal (stableDensityAt θ (1 - a) (-∑ i : Fin n, x i) / Scalar.stableDensity θ 0)

The finite-dimensional bridge increment density on a strict initial grid.