Finite truncated negative moment gives an s-finite measure

Proved

AvramDividend.Classical.sFinite_of_finite_truncated_negative_moment

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

avram-classicalbounded-variationlevy-measurem2m4renewal-resolvents-finite

Let ν be carried by (-∞,0). If the integral of min(-y,1) over negative y is finite, then ν is s-finite. Cover the negative half-line by (-∞,-1/(n+1)] and add [0,∞), which has zero ν-mass.

Preamble

import Mathlib
open MeasureTheory Set
open scoped ENNReal

Formal statement

namespace AvramDividend.Classical

/-- A measure carried by the negative half-line is s-finite when the truncated negative magnitude has finite integral. -/
theorem sFinite_of_finite_truncated_negative_moment
    (ν : Measure ℝ)
    (hIci : ν (Ici (0 : ℝ)) = 0)
    (hfin : (∫⁻ y in Iio (0 : ℝ), ENNReal.ofReal (min (-y) 1) ∂ν) < ⊤) :
    SFinite ν := by
  sorry

end AvramDividend.Classical

Source

Pinned Mathlib exists_nat_one_div_lt, MeasureTheory.meas_ge_le_lintegral_div, MeasureTheory.sigmaFinite_of_countable, and the SigmaFinite-to-SFinite instance.

View graph