Gaussian smoothing of an attracted step law

The characteristic-function defect is obtained at moving frequencies. The centering phase disappears on taking moduli. The exponent of the squared stable modulus is 2 * cos (π * θ / 2) * |t| ^ θ, which is negative for nonzero t. Ported from BGWLeaves/StableAnalysis/GaussianSmoothing.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

theorem BGW.StableTrees.Attraction.GaussianSmoothing.norm_sq_centeredScaledWalk_charFun (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (m a : ℝ) (n : ℕ) (t : ℝ) : ‖MeasureTheory.charFun (TransformConvergence.centeredScaledWalk ν m a n) t‖ ^ 2 = (‖TransformConvergence.stepCharFun ν (t / a)‖ ^ 2) ^ n

Removing the deterministic centering phase from the squared modulus.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.norm_sq_stableCF {θ : ℝ} (hθ : θ ≠ 0) (t : ℝ) : ‖Scalar.stableCF θ t‖ ^ 2 = Real.exp (2 * Real.cos (Real.pi * θ / 2) * |t| ^ θ)

The squared stable modulus, with its (negative) exponent explicit.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_one_sub_of_pow {x : ℕ → ℝ} {k : ℕ → ℕ} {L : ℝ} (hx : Filter.Tendsto x Filter.atTop (nhds 1)) (hp : Filter.Tendsto (fun (n : ℕ) => x n ^ k n) Filter.atTop (nhds (Real.exp L))) : Filter.Tendsto (fun (n : ℕ) => ↑(k n) * (1 - x n)) Filter.atTop (nhds (-L))

A power limit gives the first-order defect once the bases tend to one. The derivative is extended at one, so the bases are allowed to equal one.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_stepCharFun_norm_sq_pow_moving {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {t : ℕ → ℝ} {u : ℝ} (ht : Filter.Tendsto t Filter.atTop (nhds u)) : Filter.Tendsto (fun (n : ℕ) => (‖TransformConvergence.stepCharFun ν (t n / b n)‖ ^ 2) ^ n) Filter.atTop (nhds (Real.exp (2 * Real.cos (Real.pi * θ / 2) * |u| ^ θ)))

Attraction controls the squared one-step CF powers at moving frequencies.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_stepCharFun_defect_moving {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {t : ℕ → ℝ} {u : ℝ} (ht : Filter.Tendsto t Filter.atTop (nhds u)) : Filter.Tendsto (fun (n : ℕ) => ↑n * (1 - ‖TransformConvergence.stepCharFun ν (t n / b n)‖ ^ 2)) Filter.atTop (nhds (-2 * Real.cos (Real.pi * θ / 2) * |u| ^ θ))

The symmetrized characteristic-function defect, including moving frequencies. No step lower bound or first-moment hypothesis is needed for this implication.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_stepCharFun_defect {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑n * (1 - ‖TransformConvergence.stepCharFun ν (t / b n)‖ ^ 2)) Filter.atTop (nhds (-2 * Real.cos (Real.pi * θ / 2) * |t| ^ θ))

The fixed-frequency specialization used in Gaussian smoothing.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_stepCharFun_defect_subseq {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {j : ℕ → ℕ} (hj : Filter.Tendsto j Filter.atTop Filter.atTop) {t : ℕ → ℝ} {u : ℝ} (ht : Filter.Tendsto t Filter.atTop (nhds u)) : Filter.Tendsto (fun (n : ℕ) => ↑(j n) * (1 - ‖TransformConvergence.stepCharFun ν (t n / b (j n))‖ ^ 2)) Filter.atTop (nhds (-2 * Real.cos (Real.pi * θ / 2) * |u| ^ θ))

The defect limit also holds along arbitrary diverging time changes.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.eventually_stepCharFun_defect_le_on_Icc {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (R : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ n ≥ N, ∀ t ∈ Set.Icc (-R) R, ↑n * (1 - ‖TransformConvergence.stepCharFun ν (t / b n)‖ ^ 2) ≤ C

Compact-frequency boundedness, obtained from the moving-frequency defect limit.

noncomputable def BGW.StableTrees.Attraction.GaussianSmoothing.symmetrizedLaw (ν : MeasureTheory.Measure ℤ) : MeasureTheory.Measure ℝ

The law of the difference of two independent copies of the step.

Equations

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

instance BGW.StableTrees.Attraction.GaussianSmoothing.symmetrizedLaw_isProbabilityMeasure (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (symmetrizedLaw ν)

theorem BGW.StableTrees.Attraction.GaussianSmoothing.charFun_symmetrizedLaw (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (t : ℝ) : MeasureTheory.charFun (symmetrizedLaw ν) t = ↑(‖TransformConvergence.stepCharFun ν t‖ ^ 2)

The symmetrized CF is the squared modulus of the original CF.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.symmetrizedLaw_eq_map (ν : MeasureTheory.Measure ℤ) : symmetrizedLaw ν = MeasureTheory.Measure.map (fun (p : ℤ × ℤ) => ↑p.1 - ↑p.2) (ν.prod ν)

Product-law realization of the independent difference.

noncomputable def BGW.StableTrees.Attraction.GaussianSmoothing.smoothing (ν : MeasureTheory.Measure ℤ) (s : ℝ) : ℝ

Gaussian-smoothed squared-step defect.

Equations

• BGW.StableTrees.Attraction.GaussianSmoothing.smoothing ν s = ∫ (x : ℝ), 1 - Real.exp (-s * x ^ 2) ∂BGW.StableTrees.Attraction.GaussianSmoothing.symmetrizedLaw ν

theorem BGW.StableTrees.Attraction.GaussianSmoothing.integrable_smoothing (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {s : ℝ} (hs : 0 ≤ s) : MeasureTheory.Integrable (fun (x : ℝ) => 1 - Real.exp (-s * x ^ 2)) (symmetrizedLaw ν)

The smoothing integrand is bounded and integrable for every nonnegative parameter.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.smoothing_bounds (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {s : ℝ} (hs : 0 ≤ s) : 0 ≤ smoothing ν s ∧ smoothing ν s ≤ 1

The smoothing takes values in the unit interval.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.smoothing_mono (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] {s r : ℝ} (hs : 0 ≤ s) (hsr : s ≤ r) : smoothing ν s ≤ smoothing ν r

Smoothing is monotone, the property needed to interpolate between adjacent scales.

@[simp]

theorem BGW.StableTrees.Attraction.GaussianSmoothing.smoothing_zero (ν : MeasureTheory.Measure ℤ) : smoothing ν 0 = 0

theorem BGW.StableTrees.Attraction.GaussianSmoothing.norm_pow_sub_one_le {z : ℂ} (hz : ‖z‖ ≤ 1) (k : ℕ) : ‖z ^ k - 1‖ ≤ ↑k * ‖z - 1‖

Elementary telescoping bound on powers in the closed complex unit disk.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.one_sub_re_pow_le {z : ℂ} (hz : ‖z‖ = 1) (k : ℕ) : 1 - (z ^ k).re ≤ ↑k ^ 2 * (1 - z.re)

The pointwise quadratic integer-multiple bound behind CF domination.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.one_sub_re_charFun_nat_mul_le (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (t : ℝ) (k : ℕ) : 1 - (MeasureTheory.charFun μ (↑k * t)).re ≤ ↑k ^ 2 * (1 - (MeasureTheory.charFun μ t).re)

Quadratic control of the real CF defect at integer multiples.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.stepCharFun_defect_nat_mul_le (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (t : ℝ) (k : ℕ) : 1 - ‖TransformConvergence.stepCharFun ν (↑k * t)‖ ^ 2 ≤ ↑k ^ 2 * (1 - ‖TransformConvergence.stepCharFun ν t‖ ^ 2)

Integer-multiple control specialized to the symmetrized step law.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.eventually_stepCharFun_defect_le_quadratic {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ n ≥ N, ∀ (t : ℝ), ↑n * (1 - ‖TransformConvergence.stepCharFun ν (t / b n)‖ ^ 2) ≤ C * (1 + t ^ 2)

A global quadratic bound, uniform in the walk length after a fixed threshold.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.smoothing_eq_gaussian_integral (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (a : ℝ) : smoothing ν (a ^ 2) = ∫ (t : ℝ), 1 - ‖TransformConvergence.stepCharFun ν (a * t)‖ ^ 2 ∂ProbabilityTheory.gaussianReal 0 2

Gaussian Fourier smoothing, expressed against the probability law N(0,2).

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_smoothing {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (a : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑n * smoothing ν ((a / b n) ^ 2)) Filter.atTop (nhds (∫ (t : ℝ), -2 * Real.cos (Real.pi * θ / 2) * |a * t| ^ θ ∂ProbabilityTheory.gaussianReal 0 2))

Integrating the scaled CF defects gives the Gaussian integral limit.

noncomputable def BGW.StableTrees.Attraction.GaussianSmoothing.smoothingConstant (θ : ℝ) : ℝ

The positive finite smoothing constant; no Gamma evaluation is needed.

Equations

• BGW.StableTrees.Attraction.GaussianSmoothing.smoothingConstant θ = -2 * Real.cos (Real.pi * θ / 2) * ∫ (t : ℝ), |t| ^ θ ∂ProbabilityTheory.gaussianReal 0 2

theorem BGW.StableTrees.Attraction.GaussianSmoothing.smoothingConstant_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : 0 < smoothingConstant θ

Strict positivity of the Gaussian moment gives strict positivity of the constant.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_smoothing_rpow {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) (a : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑n * smoothing ν ((a / b n) ^ 2)) Filter.atTop (nhds (smoothingConstant θ * |a| ^ θ))

The Gaussian integral limit with its homogeneous constant factored out.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_smoothing_div_sq {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {r : ℝ} (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => ↑n * smoothing ν (r / b n ^ 2)) Filter.atTop (nhds (smoothingConstant θ * r ^ (θ / 2)))

The scale form consumed by the domain-of-attraction converse.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_nat_mul_smoothing_moving {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {j : ℕ → ℕ} (hj : Filter.Tendsto j Filter.atTop Filter.atTop) {a : ℕ → ℝ} {u : ℝ} (ha : Filter.Tendsto a Filter.atTop (nhds u)) : Filter.Tendsto (fun (n : ℕ) => ↑(j n) * smoothing ν ((a n / b (j n)) ^ 2)) Filter.atTop (nhds (smoothingConstant θ * |u| ^ θ))

Gaussian smoothing limits remain valid under moving scales and time changes.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.exists_scale_indices {b : ℕ → ℝ} (hb : Filter.Tendsto b Filter.atTop Filter.atTop) (hpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < b n) (hsucc : Filter.Tendsto (fun (n : ℕ) => b (n + 1) / b n) Filter.atTop (nhds 1)) {x : ℕ → ℝ} (hx : Filter.Tendsto x Filter.atTop Filter.atTop) : ∃ (j : ℕ → ℕ), Filter.Tendsto j Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => b (j n) / x n) Filter.atTop (nhds 1)

A sequence with asymptotically unit adjacent ratios has asymptotically exact first crossings, even if it is not monotone.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.tendsto_smoothing_ratio_inv_sq {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (x : ℝ) => smoothing ν (c / x ^ 2) / smoothing ν (1 / x ^ 2)) Filter.atTop (nhds (c ^ (θ / 2)))

Continuum scale ratios, first stated at infinity in the inverse scale variable.

theorem BGW.StableTrees.Attraction.GaussianSmoothing.smoothing_regularlyVarying_zero {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ m : ℝ} {b : ℕ → ℝ} (hb : IsStableAttracted ν θ m b) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (s : ℝ) => smoothing ν (c * s) / smoothing ν s) (nhdsWithin 0 (Set.Ioi 0)) (nhds (c ^ (θ / 2)))

Gaussian-smoothed converse: the smoothed symmetrized squared-step defect is regularly varying at zero from the right, with index θ / 2. This conclusion holds for arbitrary eventually positive attracting normings.