Slow variation

Ported from BGWLeaves/StableAnalysis/SlowVariation.lean of the author's arXiv:1110.2163v4 formalization (local snapshot of 6 November 2026).

theorem BGW.StableTrees.Attraction.SlowVariation.additive_uniform_convergence {g : ℝ → ℝ} (hg : Measurable g) (hslow : ∀ (u : ℝ), Filter.Tendsto (fun (t : ℝ) => g (t + u) - g t) Filter.atTop (nhds 0)) {K : ℝ} (hK : 0 ≤ K) {ε : ℝ} (hε : 0 < ε) : ∃ (T : ℝ), ∀ (t : ℝ), T ≤ t → ∀ (u : ℝ), |u| ≤ K → |g (t + u) - g t| < ε

Measurable additive Uniform Convergence Theorem, on every bounded interval of shifts. No local boundedness or continuity of g is assumed.

theorem BGW.StableTrees.Attraction.SlowVariation.slow_uniform_log {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) {K : ℝ} (hK : 0 ≤ K) {ε : ℝ} (hε : 0 < ε) : ∃ (T : ℝ), ∀ (t : ℝ), T ≤ t → ∀ (u : ℝ), |u| ≤ K → |Real.log (L (Real.exp (t + u))) - Real.log (L (Real.exp t))| < ε

Uniform convergence of logarithmic ratios on bounded logarithmic scales.

theorem BGW.StableTrees.Attraction.SlowVariation.slow_uniform_convergence {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) {a b : ℝ} (ha : 0 < a) (_hab : a ≤ b) {ε : ℝ} (hε : 0 < ε) : ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → ∀ r ∈ Set.Icc a b, |L (r * x) / L x - 1| < ε

Multiplicative UCT: ratio convergence is uniform on each compact interval of positive scaling factors.

theorem BGW.StableTrees.Attraction.SlowVariation.slow_potter_nat {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 1 < C ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (x : ℝ), 1 ≤ x → 1 / C * x ^ (-ε) ≤ L (↑n * x) / L ↑n ∧ L (↑n * x) / L ↑n ≤ C * x ^ ε

Potter bounds with a single constant and threshold for all large integer base points and all real scaling factors at least one.

theorem BGW.StableTrees.Attraction.SlowVariation.slow_rpow_mul_tendsto_atTop {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (x : ℝ) => x ^ ε * L x) Filter.atTop Filter.atTop

The positive power dominates every measurable slowly varying function.

theorem BGW.StableTrees.Attraction.SlowVariation.slow_rpow_neg_mul_tendsto_zero {L : ℝ → ℝ} (hmeas : Measurable L) (hnn : ∀ (x : ℝ), 0 < x → 0 ≤ L x) (hL : SlowlyVarying L) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (x : ℝ) => x ^ (-ε) * L x) Filter.atTop (nhds 0)

Every negative power times a measurable slowly varying function tends to zero.