A positive monotone integer limit yields an eventual normalised lower gap

Proved

AvramDividend.Classical.eventual_normalised_lower_of_monotone_integer_limit

by WillR · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicaleventual-growthlevy-exponentmonotone-limitnormalisation

Let J(θ) be nondecreasing for positive θ and suppose J(n+1) tends to A. If B is nonnegative, q is positive, and c+A is strictly positive, then beyond some positive real threshold every θ satisfies q/θ < c+J(θ)-B/θ. This is the exact real-parameter order bridge needed to turn integer compensated-jump convergence into eventual positivity of a zero-Gaussian Lévy exponent.

Preamble

import Mathlib

open Filter

Formal statement

theorem AvramDividend.Classical.eventual_normalised_lower_of_monotone_integer_limit
    (J : ℝ → ℝ) (c A B q : ℝ)
    (hJmono : ∀ θ₁ θ₂ : ℝ, 0 < θ₁ → θ₁ ≤ θ₂ → J θ₁ ≤ J θ₂)
    (hJlim : Filter.Tendsto (fun n : ℕ => J ((n : ℝ) + 1))
      Filter.atTop (nhds A))
    (hB : 0 ≤ B) (hd : 0 < c + A) (hq : 0 < q) :
    ∃ θ₀ : ℝ, 0 < θ₀ ∧ ∀ θ : ℝ, θ₀ ≤ θ →
      q / θ < c + J θ - B / θ := by sorry

Source

Elementary filter convergence and order arithmetic using the pinned Mathlib limit 1/(n+1)→0. The proof chooses one sufficiently large integer N and uses monotonicity of J plus denominator monotonicity for all real θ≥N+1.

View graph