Existence of an s-finite additive convolution-power sequence
ProvedAvramDividend.Classical.exists_sfinite_convolution_power_sequenceavram-classicalbounded-variationm2m4measure-convolutionrenewal-resolvent
Every s-finite measure on the additive real line has a recursively defined convolution-power sequence beginning with Dirac mass at zero. Every term remains s-finite because convolution preserves s-finiteness.
Preamble
import Mathlib open MeasureTheory
Formal statement
namespace AvramDividend.Classical
theorem exists_sfinite_convolution_power_sequence
(κ : Measure ℝ) [SFinite κ] :
∃ m : ℕ → Measure ℝ,
m 0 = Measure.dirac 0 ∧
(∀ n : ℕ, m (n + 1) = Measure.conv κ (m n)) ∧
(∀ n : ℕ, SFinite (m n)) := by
sorry
end AvramDividend.ClassicalSource
Pinned Mathlib additive measure convolution and its sfinite_mconv_of_sfinite instance; elementary recursion on natural numbers.