Centered walk transforms and convergence of types

The A1 transform identities are followed by A2 convergence of types for arbitrary eventually positive normings. No monotonicity, step lower bound, or moment assumption is needed for A2. In particular all results apply with centering mean ν.

The scale-ratio proof adapts BGW.StableTrees.Scalar.Normalization and the private proof in BGW.StableTrees.Attraction.LocalLimit: compactify the ratio as u / (1 + u), then identify subsequential limits using moving characteristic functions and the strictly negative stable modulus exponent. The two-norming version also allows a change of time with positive limiting time ratio.

Divergence follows separately: attraction supplies a frequency with one-step CF modulus strictly below one. On a convergent bounded subsequence of scales, moving frequencies turn the normalized CF moduli into powers of that fixed modulus. These powers tend to zero, contradicting the strictly positive stable CF modulus. Ported from BGWLeaves/StableAnalysis/TransformConvergence.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

noncomputable def BGW.StableTrees.Attraction.TransformConvergence.stepCharFun (ν : MeasureTheory.Measure ℤ) (t : ℝ) : ℂ

The characteristic function of one integer-valued step, viewed as a real random variable.

Equations

• BGW.StableTrees.Attraction.TransformConvergence.stepCharFun ν t = MeasureTheory.charFun (MeasureTheory.Measure.map (fun (z : ℤ) => ↑z) ν) t

noncomputable def BGW.StableTrees.Attraction.TransformConvergence.stepLaplace (ν : MeasureTheory.Measure ℤ) (s : ℝ) : ℝ

The uncentered Laplace transform of one step.

Equations

• BGW.StableTrees.Attraction.TransformConvergence.stepLaplace ν s = ∫ (z : ℤ), Real.exp (-s * ↑z) ∂ν

noncomputable def BGW.StableTrees.Attraction.TransformConvergence.intWalkCharFun (ν : MeasureTheory.Measure ℤ) (n : ℕ) (t : ℝ) : ℂ

The characteristic function of the n-fold convolution of an integer-valued step law.

Equations

• BGW.StableTrees.Attraction.TransformConvergence.intWalkCharFun ν n t = MeasureTheory.charFun (MeasureTheory.Measure.map (fun (z : ℤ) => ↑z) (BGW.StableTrees.Attraction.intWalk ν n)) t

theorem BGW.StableTrees.Attraction.TransformConvergence.intWalkCharFun_eq_pow (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) (t : ℝ) : intWalkCharFun ν n t = stepCharFun ν t ^ n

noncomputable def BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk (ν : MeasureTheory.Measure ℤ) (m a : ℝ) (n : ℕ) : MeasureTheory.Measure ℝ

The law of the centered walk divided by a positive scale. It is written as two affine maps so that the scale and centering contributions to the characteristic function are explicit.

Equations

• One or more equations did not get rendered due to their size.

instance BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_isProbabilityMeasure (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (m a : ℝ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (centeredScaledWalk ν m a n)

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_eq_map (ν : MeasureTheory.Measure ℤ) (m a : ℝ) (n : ℕ) : centeredScaledWalk ν m a n = MeasureTheory.Measure.map (fun (z : ℤ) => (↑z - ↑n * m) / a) (intWalk ν n)

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_change_scale (ν : MeasureTheory.Measure ℤ) (m a b : ℝ) (n : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : centeredScaledWalk ν m a n = MeasureTheory.Measure.map (fun (x : ℝ) => b / a * x) (centeredScaledWalk ν m b n)

Rescaling the same centered walk changes its law by the corresponding scalar map.

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_charFun_change_scale (ν : MeasureTheory.Measure ℤ) (m a b : ℝ) (n : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) (t : ℝ) : MeasureTheory.charFun (centeredScaledWalk ν m a n) t = MeasureTheory.charFun (centeredScaledWalk ν m b n) (t * (b / a))

noncomputable def BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalkProb (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (m : ℝ) (a : ℕ → ℝ) (n : ℕ) : MeasureTheory.ProbabilityMeasure ℝ

The normalized walk regarded as a bundled probability measure.

Equations

• BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalkProb ν m a n = ⟨BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk ν m (a n) n, ⋯⟩

theorem BGW.StableTrees.Attraction.IsStableAttracted.tendsto_centeredScaledWalkProb {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a : ℕ → ℝ} (h : IsStableAttracted ν θ m a) : ∃ (Q : MeasureTheory.ProbabilityMeasure ℝ), (∀ (s : ℝ), 0 < s → ∫ (x : ℝ), Real.exp (-s * x) ∂↑Q = Real.exp (s ^ θ)) ∧ Filter.Tendsto (fun (n : ℕ) => TransformConvergence.centeredScaledWalkProb ν m a n) Filter.atTop (nhds Q)

Weak convergence in IsStableAttracted is exactly convergence of the bundled normalized walk laws.

theorem BGW.StableTrees.Attraction.IsStableAttracted.tendsto_centeredScaledWalk_charFun_moving {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a : ℕ → ℝ} (h : IsStableAttracted ν θ m a) {s : ℕ → ℝ} {t : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds t)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.charFun (TransformConvergence.centeredScaledWalk ν m (a n) n) (s n)) Filter.atTop (nhds (Scalar.stableCF θ t))

Weak convergence also controls characteristic functions at moving frequencies.

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_integrable_negExp (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (m a s : ℝ) (n : ℕ) (ha : 0 < a) (hs : 0 ≤ s) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-s * x)) (centeredScaledWalk ν m a n)

Every nonnegative negative-exponential moment of the centered scaled walk is finite. The one-step lower bound makes the step Laplace integrand bounded almost everywhere.

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_laplace (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hstep : ν {z : ℤ | z < -1} = 0) (m a s : ℝ) (n : ℕ) (ha : 0 < a) (hs : 0 ≤ s) : ∫ (x : ℝ), Real.exp (-s * x) ∂centeredScaledWalk ν m a n = stepLaplace ν (s / a) ^ n * Real.exp (s * ↑n * m / a)

Laplace transform of the centered scaled walk. Here stepLaplace is the uncentered one-step transform, so the last exponential is the deterministic centering factor.

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_integral_eq_zero (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (hν : MeasureTheory.Integrable (fun (z : ℤ) => ↑z) ν) (m a : ℝ) (n : ℕ) (hm : m = mean ν) : ∫ (x : ℝ), x ∂centeredScaledWalk ν m a n = 0

The first moment of the centered scaled walk is zero.

theorem BGW.StableTrees.Attraction.TransformConvergence.centeredScaledWalk_charFun (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (m a : ℝ) (n : ℕ) (t : ℝ) : MeasureTheory.charFun (centeredScaledWalk ν m a n) t = Complex.exp (-↑(t * ↑n * m / a) * Complex.I) * stepCharFun ν (t / a) ^ n

Characteristic function of the scaled, centered walk.

theorem BGW.StableTrees.Attraction.TransformConvergence.tendsto_div_of_tendsto_div (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a b : ℕ → ℝ} (h : IsStableAttracted ν θ m a) (hb : IsStableAttracted ν θ m b) {m' : ℕ → ℕ} {κ : ℝ} (hκ : 0 < κ) (hm' : Filter.Tendsto (fun (n : ℕ) => ↑(m' n) / ↑n) Filter.atTop (nhds κ)) : Filter.Tendsto (fun (n : ℕ) => a n / b (m' n)) Filter.atTop (nhds (κ ^ (-(1 / θ))))

Convergence of types for two eventually positive normings, allowing a change of time.

theorem BGW.StableTrees.Attraction.TransformConvergence.tendsto_div_of_tendsto_div' (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a b : ℕ → ℝ} (h : IsStableAttracted ν θ m a) (hb : IsStableAttracted ν θ m b) {m' : ℕ → ℕ} {κ : ℝ} (hκ : 0 < κ) (hm' : Filter.Tendsto (fun (n : ℕ) => ↑(m' n) / ↑n) Filter.atTop (nhds κ)) : Filter.Tendsto (fun (n : ℕ) => b (m' n) / a n) Filter.atTop (nhds (κ ^ (1 / θ)))

The reciprocal form: b (m' n) / a n tends to κ ^ (1 / θ).

theorem BGW.StableTrees.Attraction.TransformConvergence.regularlyVaryingSeq (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a : ℕ → ℝ} (h : IsStableAttracted ν θ m a) : RegularlyVaryingSeq (1 / θ) a

Every stable norming is regularly varying with index 1 / θ.

theorem BGW.StableTrees.Attraction.TransformConvergence.tendsto_succ_div (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a : ℕ → ℝ} (h : IsStableAttracted ν θ m a) : Filter.Tendsto (fun (n : ℕ) => a (n + 1) / a n) Filter.atTop (nhds 1)

Successive scales are asymptotically equal, even for a nonmonotone norming.

theorem BGW.StableTrees.Attraction.TransformConvergence.norming_ratio_tendsto_one (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a b : ℕ → ℝ} (ha : IsStableAttracted ν θ m a) (hb : IsStableAttracted ν θ m b) : Filter.Tendsto (fun (n : ℕ) => a n / b n) Filter.atTop (nhds 1)

Any two eventually positive normings giving the same normalized stable law are equivalent.

theorem BGW.StableTrees.Attraction.TransformConvergence.tendsto_atTop (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {a : ℕ → ℝ} (h : IsStableAttracted ν θ m a) : Filter.Tendsto a Filter.atTop Filter.atTop

Every eventually positive stable norming diverges, without a monotonicity assumption. A bounded subsequence of scales has a convergent further subsequence; the frequencies t * a n then converge, whereas the corresponding one-step CF powers tend to zero.