Characteristic-function convergence of the normalized walk

Under (H_α) (BGW.StableTrees.ScalarDomain μ α a), the laws of S_m / a_m (BGW.StableTrees.Scalar.scaledLaw) converge weakly to ν, whose characteristic function is exp((-iθ)^α) (BGW.StableTrees.Scalar.charFun_eq_stableCF).

• BGW.StableTrees.Scalar.tendsto_stepCF_pow: for times ψ j → ∞ and arguments s_j → t, φ(s_j / a_{ψ j})^{ψ j} → exp((-it)^α); the moving argument is handled by the uniform modulus |E e^{isY} - E e^{itY}| ≤ E min(2, |s-t||Y|) and the weak convergence of the bounded continuous test function min(2, δ|x|) (no tightness argument is needed).
• BGW.StableTrees.Scalar.tendsto_norm_stepCF_pow: the same for |φ|, with limit exp(cos(πα/2)|t|^α).

Adapted from PoissonDeclumping/Stable/Convergence.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

noncomputable def BGW.StableTrees.Scalar.scaledLaw (μ : PMF ℕ) (a : ℕ → ℝ) (m : ℕ) : MeasureTheory.Measure ℝ

The law of S_m / a_m on ℝ.

Equations

• BGW.StableTrees.Scalar.scaledLaw μ a m = MeasureTheory.Measure.map (fun (z : ℤ) => ↑z / a m) (BGW.StableTrees.walkLaw μ m)

instance BGW.StableTrees.Scalar.instIsProbabilityMeasureRealScaledLaw {μ : PMF ℕ} {a : ℕ → ℝ} (m : ℕ) : MeasureTheory.IsProbabilityMeasure (scaledLaw μ a m)

theorem BGW.StableTrees.Scalar.norm_cexp_mul_I_sub_le (s t x : ℝ) : ‖Complex.exp (↑s * ↑x * Complex.I) - Complex.exp (↑t * ↑x * Complex.I)‖ ≤ min 2 (|s - t| * |x|)

noncomputable def BGW.StableTrees.Scalar.bumpFn (δ : ℝ) : BoundedContinuousFunction ℝ ℝ

The bounded continuous function x ↦ min 2 (|δ| |x|).

Equations

• BGW.StableTrees.Scalar.bumpFn δ = BoundedContinuousFunction.ofNormedAddCommGroup (fun (x : ℝ) => min 2 (|δ| * |x|)) ⋯ 2 ⋯

theorem BGW.StableTrees.Scalar.bumpFn_apply (δ x : ℝ) : (bumpFn δ) x = min 2 (|δ| * |x|)

theorem BGW.StableTrees.Scalar.norm_charFun_sub_le (P : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure P] {s t δ : ℝ} (hst : |s - t| ≤ δ) : ‖MeasureTheory.charFun P s - MeasureTheory.charFun P t‖ ≤ ∫ (x : ℝ), (bumpFn δ) x ∂P

theorem BGW.StableTrees.Scalar.tendsto_integral_bumpFn (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν] : Filter.Tendsto (fun (δ : ℝ) => ∫ (x : ℝ), (bumpFn δ) x ∂ν) (nhds 0) (nhds 0)

theorem BGW.StableTrees.Scalar.tendsto_stepCF_pow {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {ψ : ℕ → ℕ} (hψ : Filter.Tendsto ψ Filter.atTop Filter.atTop) {s : ℕ → ℝ} {t : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds t)) : Filter.Tendsto (fun (j : ℕ) => stepCF μ (s j / a (ψ j)) ^ ψ j) Filter.atTop (nhds (stableCF α t))

Characteristic-function convergence along moving arguments. Under (H_α), for every sequence of times ψ j → ∞ and arguments s j → t, φ(s_j / a_{ψ j})^{ψ j} → exp((-it)^α).

theorem BGW.StableTrees.Scalar.tendsto_norm_stepCF_pow {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {ψ : ℕ → ℕ} (hψ : Filter.Tendsto ψ Filter.atTop Filter.atTop) {s : ℕ → ℝ} {t : ℝ} (hs : Filter.Tendsto s Filter.atTop (nhds t)) : Filter.Tendsto (fun (j : ℕ) => ‖stepCF μ (s j / a (ψ j))‖ ^ ψ j) Filter.atTop (nhds (Real.exp (Real.cos (Real.pi * α / 2) * |t| ^ α)))

The norm version: |φ(s_j / a_{ψ j})|^{ψ j} → exp(cos(πα/2) |t|^α).