Scalar multiplication of Lebesgue measure moves inside stopped dividend-time integration

Proved

AvramDividend.Classical.paymentTimes_lintegral_smul_volume

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

avram-classicallebesguemeasure-theorystieltjeszero-barrier

For any prescribed payment-time set and measurable nonnegative payoff, integrating against a constant scalar multiple of Lebesgue measure equals integrating the scalar-multiplied payoff against Lebesgue measure. This is a deterministic measure identity used to identify finite-activity reflected dividends with their discounted drift reward.

Preamble

import Theorems.Thm_AvramDividend_Classical_paymentTimes_measurable
import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Mathlib.MeasureTheory.Integral.Lebesgue.Add

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.paymentTimes_lintegral_smul_volume
    (σ : ℝ≥0∞) (c : ℝ≥0∞) (w : ℝ → ℝ≥0∞) (hw : Measurable w) :
    (∫⁻ t in paymentTimes σ, w t ∂(c • volume)) =
    (∫⁻ t in paymentTimes σ, c * w t ∂volume) := by sorry

Source

Pinned Mathlib lintegral_smul_measure and lintegral_const_mul plus accepted paymentTimes_measurable.

View graph