Quadratic upper bound for the negative Levy-Khintchine jump integral

Proved

AvramDividend.Classical.negative_jump_lk_integral_upper

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

avram-classicallevy-khintchinem2m4quadratic-boundunbounded-variation

For nonnegative theta, the negative-jump Levy-Khintchine integral is bounded above by theta squared times the small-jump second moment.

Preamble

import Mathlib
open MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

namespace AvramDividend.Classical

theorem negative_jump_lk_integral_upper
    (ν : Measure ℝ) (θ : ℝ) (hθ : 0 ≤ θ)
    (hint : IntegrableOn
      (fun y : ℝ => Real.exp (θ * y) - 1 -
        θ * y * (Ioo (-1 : ℝ) 1).indicator 1 y)
      (Iio (0 : ℝ)) ν)
    (hy2 : IntegrableOn (fun y : ℝ => y ^ 2) (Ioo (-1 : ℝ) 0) ν) :
    (∫ y in Iio (0 : ℝ),
      (Real.exp (θ * y) - 1 -
        θ * y * (Ioo (-1 : ℝ) 1).indicator 1 y) ∂ν) ≤
      θ ^ 2 * ∫ y in Ioo (-1 : ℝ) 0, y ^ 2 ∂ν := by
  sorry

end AvramDividend.Classical

Source

Split at -1. The large-jump contribution is nonpositive, while the compensated small-jump remainder is bounded by theta squared times y squared.

View graph