Tail transfer: from the offspring tail to the strict tail of the step law

Let μ be an offspring law with μ[j, ∞) = j ^ (-θ) * L j for j ≥ 1, L slowly varying. For ν = stepLaw μ (the law of K - 1) the strict tail T x = ν {z | x < z} satisfies T x = μ[⌊x⌋₊ + 2, ∞) for x ≥ 0; this module shows that T is regularly varying at infinity of index -θ (a consequence of the uniform convergence theorem) and eventually positive. Ported from BGWLeaves/StableAnalysis/TailTransfer.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

noncomputable def BGW.StableTrees.Attraction.TailTransfer.floorShift (x : ℝ) : ℝ

The index ⌊x⌋₊ + 2 as a real number.

Equations

• BGW.StableTrees.Attraction.TailTransfer.floorShift x = ↑(⌊x⌋₊ + 2)

theorem BGW.StableTrees.Attraction.TailTransfer.floorShift_pos (x : ℝ) : 0 < floorShift x

theorem BGW.StableTrees.Attraction.TailTransfer.le_floorShift {x : ℝ} : x + 1 ≤ floorShift x

theorem BGW.StableTrees.Attraction.TailTransfer.floorShift_le {x : ℝ} (hx : 0 ≤ x) : floorShift x ≤ x + 2

theorem BGW.StableTrees.Attraction.TailTransfer.tendsto_floorShift_atTop : Filter.Tendsto floorShift Filter.atTop Filter.atTop

theorem BGW.StableTrees.Attraction.TailTransfer.tendsto_floorShift_div : Filter.Tendsto (fun (x : ℝ) => floorShift x / x) Filter.atTop (nhds 1)

theorem BGW.StableTrees.Attraction.TailTransfer.tendsto_floorShift_ratio {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (x : ℝ) => floorShift (c * x) / floorShift x) Filter.atTop (nhds c)

The ratio ⌊c x⌋₊ + 2 over ⌊x⌋₊ + 2 tends to c.

theorem BGW.StableTrees.Attraction.TailTransfer.slow_ratio_tendsto {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) {ι : Type u_1} {l : Filter ι} {y r : ι → ℝ} {c : ℝ} (hc : 0 < c) (hy : Filter.Tendsto y l Filter.atTop) (hr : Filter.Tendsto r l (nhds c)) : Filter.Tendsto (fun (i : ι) => L (r i * y i) / L (y i)) l (nhds 1)

Slow variation along y i → ∞ and a scaling r i → c > 0.

theorem BGW.StableTrees.Attraction.TailTransfer.eventually_pos_of_slowlyVarying' {L : ℝ → ℝ} (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < L x

A nonnegative slowly varying function is eventually strictly positive.

theorem BGW.StableTrees.Attraction.TailTransfer.stepLaw_tail_eq (μ : PMF ℕ) {x : ℝ} (hx : 0 ≤ x) : (stepLaw μ).real {z : ℤ | x < ↑z} = (μ.toMeasure (Set.Ici (⌊x⌋₊ + 2))).toReal

For x ≥ 0, the strict tail of the step law K - 1 is the offspring tail at ⌊x⌋₊ + 2.

theorem BGW.StableTrees.Attraction.TailTransfer.stepLaw_tail_eq_rpow {μ : PMF ℕ} {θ : ℝ} {L : ℝ → ℝ} (htail : ∀ (j : ℕ), 1 ≤ j → (μ.toMeasure (Set.Ici j)).toReal = ↑j ^ (-θ) * L ↑j) {x : ℝ} (hx : 0 ≤ x) : (stepLaw μ).real {z : ℤ | x < ↑z} = floorShift x ^ (-θ) * L (floorShift x)

The strict tail of the step law in terms of L, for x ≥ 0.

theorem BGW.StableTrees.Attraction.TailTransfer.isRegVaryAtTop_stepLaw_tail {μ : PMF ℕ} {θ : ℝ} {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) (htail : ∀ (j : ℕ), 1 ≤ j → (μ.toMeasure (Set.Ici j)).toReal = ↑j ^ (-θ) * L ↑j) : MonotoneDensity.IsRegVaryAtTop (fun (x : ℝ) => (stepLaw μ).real {z : ℤ | x < ↑z}) (-θ)

Tail transfer. If μ[j,∞) = j^{-θ} L(j) for j ≥ 1 with L measurable, nonnegative and slowly varying, then the strict tail T x = P[K - 1 > x] is regularly varying at infinity of index -θ.

theorem BGW.StableTrees.Attraction.TailTransfer.stepLaw_tail_eventually_pos {μ : PMF ℕ} {θ : ℝ} {L : ℝ → ℝ} (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) (htail : ∀ (j : ℕ), 1 ≤ j → (μ.toMeasure (Set.Ici j)).toReal = ↑j ^ (-θ) * L ↑j) : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < (stepLaw μ).real {z : ℤ | x < ↑z}

The strict tail is eventually strictly positive.

theorem BGW.StableTrees.Attraction.TailTransfer.stepLaw_real_lt_neg_one (μ : PMF ℕ) : (stepLaw μ).real {z : ℤ | z < -1} = 0

The step law carries no mass below -1 (restated from stepLaw_lt_neg_one).