Finite Lévy intensity of large positive jumps
ProvedAvramDividend.Classical.gaussian_levy_large_jump_finiteavram-classicalfinite-measuregaussianlarge-jumpslevy-integrabilitysigmafinite
For a positive jump-magnitude Lévy measure satisfying finite integral of min(1,z²) over positive magnitudes, the measure of jumps at least unit magnitude is finite. This is the large-jump part of the finite-annulus covering needed to derive sigma-finiteness of positive-magnitude pushforwards for Gaussian scale-function regularity.
Preamble
import Mathlib open MeasureTheory Set
Formal statement
theorem AvramDividend.Classical.gaussian_levy_large_jump_finite (μ : Measure ℝ)
(hlevy : (∫⁻ z in Ioi (0 : ℝ),
ENNReal.ofReal (min 1 (z ^ 2)) ∂μ) < ⊤) :
μ (Ici (1 : ℝ)) < ⊤ := by sorrySource
Lévy truncated-square condition; pinned Mathlib lintegral_mono_set, ae_restrict_mem, min_eq_left.