Scalar walks and normalized stable attraction

The walk has offspring increments K - 1. Its stable-domain hypothesis states scalar weak convergence to a probability law with Laplace transform exp (λ ^ α), for 1 < α ≤ 2. It assumes neither a local limit estimate nor regular variation of the normalizing sequence.

Extracted from the scalar definitions in PoissonDeclumping/Statements/Defs.lean and PoissonDeclumping/Setup/Walk.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

def BGW.StableTrees.IsCritical (μ : PMF ℕ) : Prop

The offspring mean is one, including finiteness of the mean.

Equations

• BGW.StableTrees.IsCritical μ = (∑' (j : ℕ), ↑j * μ j = 1)

noncomputable def BGW.StableTrees.stepLaw (μ : PMF ℕ) : MeasureTheory.Measure ℤ

The law of one increment X = K - 1.

Equations

• BGW.StableTrees.stepLaw μ = MeasureTheory.Measure.map (fun (k : ℕ) => ↑k - 1) μ.toMeasure

noncomputable def BGW.StableTrees.walkLaw (μ : PMF ℕ) : ℕ → MeasureTheory.Measure ℤ

The law of the sum of n independent increments; the empty sum is zero.

Equations

• BGW.StableTrees.walkLaw μ 0 = MeasureTheory.Measure.dirac 0
• BGW.StableTrees.walkLaw μ m.succ = (BGW.StableTrees.walkLaw μ m).conv (BGW.StableTrees.stepLaw μ)

def BGW.StableTrees.SlowlyVarying (ℓ : ℝ → ℝ) : Prop

Ratio slow variation at infinity. Positivity and measurability are not part of this predicate; applications retain the needed hypotheses explicitly.

Equations

• BGW.StableTrees.SlowlyVarying ℓ = ∀ (a : ℝ), 0 < a → Filter.Tendsto (fun (x : ℝ) => ℓ (a * x) / ℓ x) Filter.atTop (nhds 1)

structure BGW.StableTrees.StableDomain (μ : PMF ℕ) (α : ℝ) (a : ℕ → ℝ) : Prop

Normalized scalar attraction to a spectrally positive stable law with Laplace exponent λ ^ α. The limit law is an existence hypothesis here. The normalizer is nondecreasing and positive for n ≥ 1.

• critical : IsCritical μ
• nondegenerate : μ 1 ≠ 1
• alpha_mem : 1 < α ∧ α ≤ 2
• monotone : Monotone a
• pos (n : ℕ) : 1 ≤ n → 0 < a n
• converges : ∃ (ν : MeasureTheory.Measure ℝ), MeasureTheory.IsProbabilityMeasure ν ∧ (∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ α)) ∧ ∀ (f : BoundedContinuousFunction ℝ ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), f x ∂MeasureTheory.Measure.map (fun (z : ℤ) => ↑z / a n) (walkLaw μ n)) Filter.atTop (nhds (∫ (x : ℝ), f x ∂ν))

def BGW.StableTrees.InStableDomain (μ : PMF ℕ) : Prop

Stable attraction for some index and normalizing sequence.

Equations

• BGW.StableTrees.InStableDomain μ = ∃ (α : ℝ) (a : ℕ → ℝ), BGW.StableTrees.StableDomain μ α a

noncomputable def BGW.StableTrees.walkProb (μ : PMF ℕ) (m i : ℤ) : ℝ

A walk point probability, extended to zero at negative integer times.

Equations

• BGW.StableTrees.walkProb μ m i = if 0 ≤ m then (BGW.StableTrees.walkLaw μ m.toNat).real {i} else 0