A monotone nonnegative scale function vanishing at a has no Laplace mass below a

Proved

AvramDividend.Classical.laplace_integral_restrict_tail_of_monotone_zero

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

avram-classicalintegrationlaplace-transformm2m4strict-positivityunbounded-variation

A nonnegative nondecreasing W on the nonnegative real axis which is zero at a>0 must vanish on (0,a]. Consequently its Laplace integral on (0,∞) is equal to its integral on the tail (a,∞) for every real Laplace parameter, with no integrability premise.

Preamble

import Mathlib
open MeasureTheory Set Filter

Formal statement

namespace AvramDividend.Classical

theorem laplace_integral_restrict_tail_of_monotone_zero
    (W : ℝ → ℝ) (a β : ℝ)
    (ha : 0 < a)
    (hW : ∀ x : ℝ, 0 ≤ x → 0 ≤ W x)
    (hmono : MonotoneOn W (Ici 0))
    (hWa : W a = 0) :
    (∫ x in Ioi (0 : ℝ), Real.exp (-β * x) * W x) =
      ∫ x in Ioi a, Real.exp (-β * x) * W x := by
  sorry

end AvramDividend.Classical

Source

Deterministic set-integral restriction step for the unbounded-variation strict-positivity contradiction in Avram Dividend.

View graph