Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Any measure absolutely continuous with respect to time-Lebesgue times jump intensity has a diffuse time-coordinate marginal

Proved
AvramDividend.Classical.time_marginal_atomless_of_ac_volume_prod

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

absolute-continuityavram-classicaldiffuse-time-marginallevy-itono-simultaneous-jumpspoisson

Let ν be an s-finite Borel measure on jump sizes, and let η be any measure on real time×real jump-size space which is absolutely continuous with respect to Lebesgue-time × ν. The time-coordinate marginal of η is atomless: every singleton time has probability or measure zero. A fixed-time slice {t}×ℝ has product intensity zero since Lebesgue gives no mass to a singleton. Absolute continuity transfers this nullness to η; projecting to time identifies its singleton preimage with the slice. This is the key diffuse-time measure-theoretic prerequisite for canonical Poisson point-family arrival times under the normalised restriction of the product intensity to nonzero-mass partition pieces. For zero-mass pieces the canonical model may use a dummy Dirac point and they must instead be shown inactive almost surely.

Preamble
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.MeasureTheory.Measure.Prod
import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

open MeasureTheory Set
open scoped ENNReal
Formal statement
theorem AvramDividend.Classical.time_marginal_atomless_of_ac_volume_prod
    (ν : Measure ℝ) [SFinite ν]
    (η : Measure (ℝ × ℝ))
    (hη : η ≪ ((volume : Measure ℝ).prod ν)) :
    NullSingletonClass (η.map Prod.fst) := by sorry
Source
Pinned Mathlib MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.AbsolutelyContinuous, MeasureTheory.nullSingletonClass_volume (Mathlib.MeasureTheory.Measure.Lebesgue.Basic), Measure.map_apply. Canonical Lévy jump construction in LeanLevy/RandomMeasure/PoissonPointFamily.lean uses piece-normalised product intensities for point laws.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me