Finite small negative jump square moment from Lévy integrability

Proved

AvramDividend.Classical.finite_small_negative_jump_square_moment

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

avram-classicallevy-jump-measurem2m4second-momentunbounded-variation

Finite Lévy integral of min(1,y squared) implies finite second moment of the jump measure on the small negative interval (-1,0).

Preamble

import Mathlib
open MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

namespace AvramDividend.Classical

theorem finite_small_negative_jump_square_moment
    (ν : Measure ℝ)
    (hν : (∫⁻ y : ℝ, ENNReal.ofReal (min 1 (y ^ 2)) ∂ν) < ⊤) :
    (∫⁻ y in Ioo (-1 : ℝ) 0, ENNReal.ofReal (y ^ 2) ∂ν) < ⊤ := by
  sorry

end AvramDividend.Classical

Source

Direct restriction of the canonical Lévy integrability condition, using y squared at most one on (-1,0).

View graph