Signed Laplace-transform uniqueness without continuity

Proved

AvramDividend.Classical.avram_laplace_ae_zero_of_signed_20261026

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

avram-classicallaplace-uniquenessroot-connectedsigned-functions

A signed residual with integrable exponential weights and zero Laplace integral at every parameter above b vanishes almost everywhere on the positive half-line. Splitting into R+|R| and |R| reduces the assertion to the established nonnegative Laplace uniqueness theorem. This removes the continuity and C2 assumptions of previous generator-residual identification results and can serve bounded- and unbounded-variation analytic branches.

Preamble

import Mathlib.MeasureTheory.Function.L1Space.Integrable
import Mathlib.Tactic.Linarith
import Theorems.Thm_avram_laplace_ae_eq_of_nonnegative_20261026
open AvramDividend.Classical MeasureTheory Set

Formal statement

/-- A signed function with zero Laplace transform on a real half-line
vanishes almost everywhere on positive arguments. -/
theorem AvramDividend.Classical.avram_laplace_ae_zero_of_signed_20261026
    (R : ℝ → ℝ) (b : ℝ)
    (hlap : ∀ θ : ℝ, b < θ →
      IntegrableOn (fun x : ℝ => Real.exp (-(θ * x)) * R x) (Ioi (0 : ℝ)) ∧
      (∫ x in Ioi (0 : ℝ), Real.exp (-(θ * x)) * R x) = 0) :
    ∀ᵐ x ∂((volume : Measure ℝ).restrict (Ioi (0 : ℝ))), R x = 0 := by sorry

Source

Proved AvramDividend.Classical.scaleFunction_generator_eq_q_ae_of_c_two_residual_vanishing, candidate 16533, and Proved avram_laplace_ae_eq_of_nonnegative_20261026, candidate 16513.

View graph