The Vervaat image of the stable bridge

A single discrete offspring witness identifies the Vervaat bridge limit with the normalized Itô excursion law, by agreement of prefixes and the pinned terminal value.

1. Adapters to the sealed discrete bridge and prefix results

instance BGW.StableTrees.VervaatIto.instIsProbabilityMeasureForallFinNatOffspringVec (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (DiscreteBridge.offspringVec μ n)

theorem BGW.StableTrees.VervaatIto.tendsto_walkBridgeLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => DiscreteBridge.walkBridgeLaw μ B (q k) ⋯) Filter.atTop (nhds (stableBridgeLaw θ))

(K06 statement) Walk bridge invariance principle.

theorem BGW.StableTrees.VervaatIto.map_vervaatD_walkBridgeLaw {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) (hB : 0 < B n) : MeasureTheory.Measure.map Skorokhod.vervaatD ↑(DiscreteBridge.walkBridgeLaw μ B n hn) = ↑(DiscreteBridge.exactWalkLaw μ B n hn)

(K06 statement) Cyclic law: the Vervaat image of the discrete walk bridge is the exact-size Łukasiewicz path law.

theorem BGW.StableTrees.VervaatIto.tendsto_exactWalkLaw_prefix {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (k : ℕ) => DiscreteBridge.restrictLaw a ⋯ (DiscreteBridge.exactWalkLaw μ B (q k) ⋯)) Filter.atTop (nhds ((unitExcursionLaw θ).map (excursionRestrict a)))

(K07 statement) Exact-size walk prefixes: the restriction of the exact-size path law to [0,a] converges to the unit-excursion prefix.

2. The single witness

structure BGW.StableTrees.VervaatIto.DiscreteWitness (θ : ℝ) : Type

One witness for the whole identification: an offspring law, a norming, the stable domain proof and an unbounded admissible sequence of sizes, all chosen once.

• μ : PMF ℕ

  The offspring law.

• B : ℕ → ℝ

  The norming sequence.

• h : StableDomain self.μ θ self.B

  Attraction to the spectrally positive θ-stable law.

• q : ℕ → ℕ

  The sample sizes.

• hqtop : Filter.Tendsto self.q Filter.atTop Filter.atTop

  The sizes are unbounded.

• hq (k : ℕ) : Admissible self.μ (self.q k)

  The sizes are admissible: P(ζ = q k) ≠ 0.

theorem BGW.StableTrees.VervaatIto.exists_discreteWitness {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Nonempty (DiscreteWitness θ)

The witness exists for every 1 < θ ≤ 2 (exists_stableDomain, sizeProb_pos_iff: choose q k = 1 + d * (N + k + 1), d = Scalar.latticeSpan μ, beyond the lattice threshold N; then q k ≡ 1 mod d and N ≤ q k).

3. The Vervaat image and the full-path limit

noncomputable def BGW.StableTrees.VervaatIto.vervaatImage (θ : ℝ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)

The Vervaat image (stableBridgeLaw θ).map vervaatD as a probability measure.

Equations

• BGW.StableTrees.VervaatIto.vervaatImage θ = (BGW.StableTrees.stableBridgeLaw θ).map BGW.Skorokhod.vervaatD

theorem BGW.StableTrees.VervaatIto.tendsto_exactWalkLaw_vervaatImage {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (w : DiscreteWitness θ) : Filter.Tendsto (fun (k : ℕ) => DiscreteBridge.exactWalkLaw w.μ w.B (w.q k) ⋯) Filter.atTop (nhds (vervaatImage θ))

Full-path limit of the transformed walk bridge: along the witness the exact-size walk laws converge to the Vervaat image of the stable bridge. K06 convergence, the a.s. continuity of vervaatD at the bridge (stableBridgeLaw_ae_continuousAt_vervaatD), the continuous mapping theorem, and the cyclic law map_vervaatD_walkBridgeLaw. The terminal value of the paths is -1/B n; nothing is assumed about the limit at time 1.

4. Prefixes on a dense set of times and the terminal coordinate

def BGW.StableTrees.VervaatIto.timePoint (a : NNReal) (ha : a ≤ 1) : ↑(Set.Icc 0 1)

The time a ∈ [0,1] as a point of the domain of D 1 ℝ.

Equations

• BGW.StableTrees.VervaatIto.timePoint a ha = ⟨↑a, ⋯⟩

def BGW.StableTrees.VervaatIto.NoFixedDiscontinuity (P : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)) (t : ↑(Set.Icc 0 1)) : Prop

P has no fixed discontinuity at t: almost every path is continuous at t.

Equations

• BGW.StableTrees.VervaatIto.NoFixedDiscontinuity P t = (↑P {f : BGW.Skorokhod.D 1 ℝ | ¬ContinuousAt (⇑f) t} = 0)

theorem BGW.StableTrees.VervaatIto.countable_fixedDiscontinuities (P : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)) : {t : ↑(Set.Icc 0 1) | ¬NoFixedDiscontinuity P t}.Countable

A probability law on D[0,1] has at most countably many fixed discontinuities.

theorem BGW.StableTrees.VervaatIto.exists_dense_noFixedDiscontinuity_times (θ : ℝ) : ∃ (A : Set NNReal), (∀ a ∈ A, a ∈ Set.Ioo 0 1) ∧ Set.Ioo 0 1 ⊆ closure (NNReal.toReal '' A) ∧ ∀ a ∈ A, ∀ (ha : a ≤ 1), NoFixedDiscontinuity (vervaatImage θ) (timePoint a ha)

A dense set of cutoff times outside the fixed discontinuities of the Vervaat image (countable_fixedDiscontinuities and density of the complement of a countable set).

theorem BGW.StableTrees.VervaatIto.restrictLaw_vervaatImage_eq_unitPrefix {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (w : DiscreteWitness θ) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) (hcont : NoFixedDiscontinuity (vervaatImage θ) (timePoint a ⋯)) : DiscreteBridge.restrictLaw a ⋯ (vervaatImage θ) = (unitExcursionLaw θ).map (excursionRestrict a)

Equality of prefixes (K06 + K07 on the same witness w, which is exposed here and passed to tendsto_exactWalkLaw_vervaatImage hθ w): at every a ∈ (0,1) where the Vervaat image has no fixed discontinuity, its restriction to [0,a] is the unit-excursion prefix. The same sequence E_k = exactWalkLaw converges to both (CMT for restrict at continuity points and K07).

theorem BGW.StableTrees.VervaatIto.ae_vervaatImage_terminal_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(vervaatImage θ), f ⟨1, ⋯⟩ = 0

Both laws vanish a.s. at the terminal time (stableBridgeLaw_ae_vervaat_endpoints).

theorem BGW.StableTrees.VervaatIto.eq_of_restrict_eq_of_terminal_zero (P Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)) (A : Set NNReal) (hA : ∀ a ∈ A, a ∈ Set.Ioo 0 1) (hdense : Set.Ioo 0 1 ⊆ closure (NNReal.toReal '' A)) (h : ∀ (a : NNReal) (ha : a ∈ A), DiscreteBridge.restrictLaw a ⋯ P = DiscreteBridge.restrictLaw a ⋯ Q) (hP : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑P, f ⟨1, ⋯⟩ = 0) (hQ : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑Q, f ⟨1, ⋯⟩ = 0) : P = Q

Uniqueness with the terminal coordinate: two laws on D[0,1] that agree on the prefixes [0,a] for a in a set of times dense in (0,1), and are both a.s. 0 at time 1, are equal using ext_of_finiteDimensional: every finite collection of nonterminal times fits below a cutoff in A, and its joint law is obtained by adjoining the terminal constant 0.

5. C35

theorem BGW.StableTrees.VervaatIto.vervaatImage_eq_levyExcLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : vervaatImage θ = levyExcLaw θ

C35, probability-measure form: the Vervaat image of the stable bridge is the unit excursion law.

theorem BGW.StableTrees.VervaatIto.map_vervaatD_stableBridgeLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map Skorokhod.vervaatD ↑(stableBridgeLaw θ) = ↑(levyExcLaw θ)

C35 (K08 main theorem): for 1 < θ ≤ 2, the Vervaat transform of the stable bridge has the law of the normalized Itô excursion (levyExcLaw θ). Statement as in the blueprint.