Real scalar stable attraction

This module packages weak attraction of real iid sums, proves the convergence-of-types theorem for arbitrary eventually positive normalizers, and connects the real formulation to the existing integer walk and offspring stable-domain predicates.

References: W. Feller, An Introduction to Probability Theory and Its Applications, vol. II, ch. XVII; N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation (1987), §1.5 (Potter bounds).

structure BGW.StableTrees.IsRealStableAttracted (ν : MeasureTheory.ProbabilityMeasure ℝ) (θ : ℝ) (B : ℕ → ℝ) : Prop

Real scalar attraction (audit correction 1): B n > 0 only eventually; no monotonicity, no centering, and no moment assumption.

• index_mem : 1 < θ ∧ θ ≤ 2
• pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < B n
• converges : Filter.Tendsto (fun (n : ℕ) => Probability.RealWalk.scaledSumLaw ν B n) Filter.atTop (nhds (stableLaw θ))

theorem BGW.StableTrees.IsRealStableAttracted.congr_eventually {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B B' : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) (hBB' : ∀ᶠ (n : ℕ) in Filter.atTop, B n = B' n) : IsRealStableAttracted ν θ B'

Invariance under eventual equality of normalizers.

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_charFun_pow_moving {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {m : ℕ → ℕ} (hm : Filter.Tendsto m Filter.atTop Filter.atTop) {u : ℕ → ℝ} {u₀ : ℝ} (hu : Filter.Tendsto u Filter.atTop (nhds u₀)) : Filter.Tendsto (fun (j : ℕ) => MeasureTheory.charFun (↑ν) (u j / B (m j)) ^ m j) Filter.atTop (nhds (MeasureTheory.charFun (↑(stableLaw θ)) u₀))

Moving-argument characteristic-function convergence (Node 4): along m j → ∞ and u j → u₀, φ_ν (u j / B (m j)) ^ (m j) → φ_{stableLaw θ} u₀.

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_norming_ratio {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {m q : ℕ → ℕ} {c : ℝ} (hc : 0 < c) (hq : Filter.Tendsto q Filter.atTop Filter.atTop) (hmq : Filter.Tendsto (fun (j : ℕ) => ↑(m j) / ↑(q j)) Filter.atTop (nhds c)) : Filter.Tendsto (fun (j : ℕ) => B (m j) / B (q j)) Filter.atTop (nhds (c ^ (1 / θ)))

The ratio theorem (Node 4): no monotonicity, no lattice, no criticality.

Bridge from the integer predicate

noncomputable def BGW.StableTrees.castLaw (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.ProbabilityMeasure ℝ

The cast pushforward of an integer step law to ℝ.

Equations

• BGW.StableTrees.castLaw ν = ⟨MeasureTheory.Measure.map (fun (z : ℤ) => ↑z) ν, ⋯⟩

theorem BGW.StableTrees.sumLaw_castLaw (ν : MeasureTheory.Measure ℤ) [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) : ↑(Probability.RealWalk.sumLaw (castLaw ν) n) = MeasureTheory.Measure.map (fun (z : ℤ) => ↑z) (Attraction.intWalk ν n)

The real sum law of cast integer steps is the cast of the integer walk law.

theorem BGW.StableTrees.Attraction.IsStableAttracted.isRealStableAttracted {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} {B : ℕ → ℝ} (h : IsStableAttracted ν θ 0 B) : IsRealStableAttracted (castLaw ν) θ B

(b) The existing integer attraction predicate (Attraction/Defs.lean, centering 0) implies the real one for the cast step law, with the same normalizer; uses eq_stableLaw_of_laplace to identify the limit.

noncomputable def BGW.StableTrees.realOffspringStepLaw (μ : PMF ℕ) : MeasureTheory.ProbabilityMeasure ℝ

The real offspring step law K - 1, as a cast of stepLaw μ.

Equations

• BGW.StableTrees.realOffspringStepLaw μ = BGW.StableTrees.castLaw (BGW.StableTrees.stepLaw μ)

theorem BGW.StableTrees.StableDomain.isRealStableAttracted {μ : PMF ℕ} {θ : ℝ} {a : ℕ → ℝ} (h : StableDomain μ θ a) : IsRealStableAttracted (realOffspringStepLaw μ) θ a

(c) Offspring bridge, through stableDomain_isStableAttracted and (b).