LeanLevy

A Lean 4 formalization of Lévy processes, built on top of mathlib.

What's here

Bochner API (LeanLevy/Representation/BochnerGaussian.lean)

• covMatrix: covariance matrix ψ(tᵢ - tⱼ) of a positive definite function, with covMatrix_is_psd
• bochner_identity: for continuous PD ψ with ψ(0)=1, ψ t = ∫ exp(I·t·x) ∂μ for the spectral measure μ (explicit-integral form of Bochner's theorem)

Fourier analysis (LeanLevy/Fourier/)

• Fourier transform of finite measures on ℝ, with boundedness, continuity, and value at zero
• Positive definite functions: definition, Schur product theorem, pointwise closure, characteristic function bridge
• Bochner's theorem, proved via Gaussian smoothing, Prokhorov compactness, and Lévy continuity

Characteristic functions (LeanLevy/Probability/Characteristic.lean)

• Characteristic function of probability measures
• Bochner positive semi-definiteness
• Multiplicativity under convolution

Poisson distribution (LeanLevy/Probability/Poisson.lean)

• Expectation, variance, second factorial moment
• Characteristic function: φ(ξ) = exp(r(exp(iξ) − 1))

Lévy's continuity theorem (LeanLevy/Probability/WeakConvergence.lean)

• Weak convergence of probability measures is equivalent to pointwise convergence of characteristic functions
• Tightness from convergence of characteristic functions

Stochastic processes (LeanLevy/Processes/StochasticProcess.lean)

• Independent and stationary increments
• Increment independence from the natural filtration
• The repo's HasIndependentIncrements predicate coincides definitionally with mathlib's HasIndepIncrements (hasIndependentIncrements_iff_hasIndepIncrements)

Finite-dimensional distributions (LeanLevy/Processes/FiniteDimensional.lean)

• Joint law at finitely many times as a pushforward measure
• Marginalization: restricting to a subset of times recovers the sub-distribution
• Projective consistency (IsProjectiveMeasureFamily)

Projective families (LeanLevy/Processes/ProjectiveFamily.lean)

• Bundled structure: measure family + consistency + probability
• Projection and composition lemmas (functoriality)
• Constructor from stochastic processes

Càdlàg paths (LeanLevy/Processes/Cadlag.lean)

• Right-continuity with left limits
• Monotone ℕ-valued functions are càdlàg when right-continuous
• Closure toolkit: IsCadlagAt.congr (the property is local — it depends only on the germ at 𝓝 t), IsCadlagAt.add/IsCadlag.add/IsCadlag.finsetSum (pointwise finite sums), isCadlag_stepIndicator (the right-continuous step t ↦ if c ≤ t then y else 0), Continuous.isCadlag, isCadlag_comp_nnrealCoe (precomposition with the coercion ℝ≥0 → ℝ), and isCadlag_of_tendstoUniformlyOn — a uniform-on-Iic T (for every T) limit of càdlàg functions ℝ → ℝ is càdlàg

Lévy processes (LeanLevy/Processes/LevyProcess.lean)

• Definition: independent increments, stationary increments, càdlàg paths, starts at zero
• Characteristic exponent and supporting lemmas (multiplicativity, non-vanishing, right-continuity)

Kolmogorov extension theorem (LeanLevy/Processes/Kolmogorov.lean)

• Existence and uniqueness of the projective limit measure on Polish spaces
• σ-additivity of the cylinder content via inner regularity and Tychonoff compactness

Poisson process (LeanLevy/Processes/PoissonProcess.lean)

• Defined as a counting process with independent, Poisson-distributed increments
• Constructed via the Kolmogorov extension theorem from its finite-dimensional distributions, whose projective consistency comes down to the convolution identity for Poisson laws
• Is a Lévy process

Characteristic exponent (LeanLevy/Levy/CharacteristicExponent.lean)

• Local log construction (branch-cut safe) and local-global exponent agreement
• Semigroup API: multiplicativity, power formulas, complex power law φ_t(ξ) = φ₁(ξ)^t
• Ceiling-sequence density lemma: right-continuous + continuous functions agreeing on ℕ/ℕ rationals are equal
• Lévy exponential formula F(t,ξ) = exp(tΨ(ξ)) with full continuity in t

Infinite divisibility (LeanLevy/Levy/InfiniteDivisible.lean)

• Iterated convolution, with characteristic function formula
• Poisson distribution is infinitely divisible
• Lévy process marginals are infinitely divisible

Lévy measures (LeanLevy/Levy/LevyMeasure.lean)

• IsLevyMeasure predicate: ν({0}) = 0 and ∫ min(1, x²) dν < ∞
• Finite mass on {x | ε ≤ |x|}, σ-finiteness
• IsLevyMeasure.smul: a finite scalar multiple c • ν (with c ≠ ∞) of a Lévy measure is again a Lévy measure

Compensated integrand (LeanLevy/Levy/CompensatedIntegral.lean)

• levyCompensatedIntegrand ξ x = exp(ixξ) − 1 − ixξ·1_{|x|<1}
• Pointwise norm bound, measurability, Bochner integrability under a Lévy measure
• integral_levyCompensatedIntegrand_eq_small_add_large: the compensated integral against a Lévy measure splits at radius 1 into the compensated small-jump integral ∫_{(−1,1)} (exp(ixξ) − 1 − ixξ) dν plus the plain large-jump integral ∫_{|x| ≥ 1} (exp(ixξ) − 1) dν

Lévy–Khintchine theorem (LeanLevy/Levy/LevyKhintchine.lean, LevyKhintchineProof.lean, LevyKhintchineUniqueness.lean)

• LevyKhintchineTriple: a drift, a Gaussian variance, and a Lévy measure, whose exponent is the Lévy–Khintchine formula ψ_T(ξ) = ibξ − σ²ξ²/2 + ∫ (e^{ixξ} − 1 − ixξ·1_{|x|<1}) dν
• levyKhintchine_representation: every infinitely divisible probability measure on ℝ has characteristic function exp(ψ_T) for some triple. The Lévy measure is only required to be σ-finite with ∫ min(1,x²) dν < ∞, so infinite-activity cases such as α-stable laws are covered (their infinite divisibility is not itself formalized here)
• The proof extracts Khintchine's canonical measure by a single Prokhorov argument applied to the min(1,x²)-tilted scaled measures, untilts it into the Lévy measure, and obtains the whole triple along one subsequence. The limit is identified at a split radius r ∈ (1/2, 1] chosen so that ν has no atom on the sphere; the resulting variance σ² = lim t⁻¹∫_{|x|<r} x² dμ_t − ∫_{|x|<r} x² dν keeps the small-jump second moment from being counted both in σ² and in the compensated integral
• levyKhintchine_converse: conversely, every triple is realised by an infinitely divisible law — ψ_T is continuous, vanishes at 0, is Hermitian and conditionally negative definite, so Schoenberg's theorem and Bochner's theorem produce a convolution semigroup whose time-1 member has characteristic function exp(ψ_T)
• LevyKhintchineTriple.ext_of_exponent_eq: the triple is determined by its exponent, via Sato's smearing argument — ψ_T(ξ) − ½∫_{[-1,1]} ψ_T(ξ+u) du is the characteristic function of a finite measure with a σ²/6 atom at the origin and density 1 − sinc against ν, from which σ², ν, and then the drift are recovered
• isInfinitelyDivisible_iff_exists_levyKhintchineTriple and existsUnique_levyKhintchineTriple: a probability measure on ℝ is infinitely divisible iff its characteristic function is exp(ψ_T) for a triple T, and that triple is unique (equal exponentials force equal exponents by a continuous-logarithm argument on the connected line)

Compound Poisson process (LeanLevy/Processes/CompoundPoisson.lean, CompoundPoissonLaw.lean)

• Construction: exists_isCompoundPoissonDriver — for any rate r > 0 and jump law ν', a driver (τ, Y) of i.i.d. exponential interarrival times and i.i.d. ν'-marks, jointly independent, on a canonical product space
• Sample paths: compoundPoisson_ae_isCadlag — the path t ↦ b·t + ∑_{n ≤ N(t)} Yₙ is almost surely càdlàg
• Pathwise Itô formula: compoundPoisson_pathwise_ito — for a C¹ function f, a purely pathwise change-of-variables identity f(Xₜ) − f(X₀) = ∫₀ᵗ f'(Xₛ)·b ds + ∑ jump terms, valid for these finite-activity paths with no stochastic integral (the drift part is an ordinary Riemann integral, the jumps a finite sum)
• Jump-count law: map_jumpCount_arrival — the number of jumps by time t is Poisson with mean r·t, obtained from the Gamma law of the arrival times and telescoping survival probabilities
• Characteristic function: charFun_map_compoundPoisson — the marginal at time t has characteristic function exp(t·(i b ξ + r·(charFun ν' ξ − 1))), by conditioning on the Poisson jump count and summing the generating series
• Lévy–Khintchine realization: compoundPoissonTriple is the triple (b + ∫_{|x|<1} x d(r·ν'), 0, r·ν'); charFun_map_compoundPoisson_eq_exponent shows the marginal's characteristic function is exp(t·ψ_T) for this triple, so compound Poisson processes realize exactly the finite-activity, zero-Gaussian Lévy–Khintchine triples, and isInfinitelyDivisible_map_compoundPoisson records that every marginal is infinitely divisible (via the converse Lévy–Khintchine theorem)

Poisson random measures (LeanLevy/RandomMeasure/PoissonPointFamily.lean, PoissonRandomMeasure.lean, PoissonCompensated.lean, TimeSpacePoisson.lean, PoissonFiltration.lean, PoissonMartingale.lean, LevyJumpLaw.lean)

For a σ-finite intensity measure m on a measurable space, the random measure is constructed, rather than axiomatized.

• Point family: prmPiece, prmPieceLaw partition the space into disjoint finite-mass pieces and normalize m on each; IsPoissonPointFamily bundles a family of piece counts and points, and exists_isPoissonPointFamily builds it in one shot with the counts and all points jointly independent, each count Poisson-distributed with the piece mass and each point drawn from the normalized piece law
• Per-piece identities: integral_pieceSum is Campbell's formula for a piece (E[∑ g(Xₙ)] = ∫ g dm), integral_sq_pieceSum its second moment, and integral_pieceProd_eq_exp the piece probability-generating-function identity E[∏ w(Xₙ)] = exp(m(piece)·(∫ w dm̂ − 1))
• Thinning: thinnedCount counts the points of a piece landing in a set; map_thinnedCount shows this count is Poisson with mean m(piece ∩ A), indepFun_thinnedCount_thinnedCount gives independence of the counts on two disjoint sets, and iIndepFun_thinnedCount gives mutual independence of the counts over a finite pairwise-disjoint family (with integral_prod_pow_thinnedCount and charFunDual_pi_thinnedCount the joint probability-generating and characteristic functions that factor across the pieces)
• The random measure: poissonRandomMeasure is a genuine Measure-valued random object, a countable sum of Dirac masses at the realized points, with poissonRandomMeasure_apply its evaluation and measurable_poissonRandomMeasure_apply measurability; map_poissonRandomMeasure_apply is the superposition law — the count N(A) on a finite-mass set is Poisson with mean m A — indepFun_poissonRandomMeasure_apply gives independence of the evaluations on two disjoint finite-mass sets, and iIndepFun_poissonRandomMeasure_apply gives mutual independence of the evaluations over a finite pairwise-disjoint family of finite-mass sets
• Lebesgue integration against the random measure: for a measurable g ≥ 0, lintegral_poissonRandomMeasure evaluates ∫⁻ g dN pathwise as the sum of g over the realized points; lintegral_poissonRandomMeasure_apply gives the evaluation mean ∫⁻ N(A) dμ = m A for a measurable set A (both sides may be ⊤); and lintegral_lintegral_poissonRandomMeasure is Campbell's formula — for a measurable g, the mean of ∫⁻ g dN over ω equals ∫⁻ g dm
• Compensated integral: compensatedPoissonSum is the centered sum ∑ f(Xₙ) − ∫ f dm; integral_compensatedPoissonSum shows it has mean zero and integral_sq_compensatedPoissonSum is Campbell's second formula, the L² isometry E[Ñ(f)²] = ∫ f² dm on L¹ ∩ L², with memLp_two_compensatedPoissonSum recording square-integrability; compensatedPoissonIntegral : Lp ℝ 2 m → Lp ℝ 2 μ extends the map to all of L²(m) by density, eLpNorm_compensatedPoissonIntegral being the isometry on the whole space, compensatedPoissonIntegral_eq_sum its agreement with the explicit sum on L¹ ∩ L², and integral_compensatedPoissonIntegral its mean-zero property on all of L²
• Time-indexed random measure: specializing to the mark space ℝ × E under the product intensity volume.prod m reads ℝ as time; poissonTimeCount is the running count of realized marks in (0, t] × A, map_poissonRandomMeasure_band is the band law (the count in (s, t] × A is Poisson with mean (t − s) · m A), map_poissonTimeCount its running-count specialization, poissonTimeCount_add its pathwise additivity over consecutive windows, and iIndepFun_poissonRandomMeasure_bands the independent-increments statement — counts over consecutive disjoint time bands are mutually independent
• Lévy specialization: with mark space ℝ and intensity volume.prod ν for a Lévy measure ν, memLp_two_smallJumpFun shows the small-jump test function 1_{(0,t] × (−1,1)}(s, x) · x is square-integrable, so levyCompensatedSmallJump is a genuine L²(μ) element at each time t; integral_levyCompensatedSmallJump gives it mean zero and eLpNorm_sq_levyCompensatedSmallJump its second moment t · ∫_{(−1,1)} x² dν, while map_levyLargeJumpCount shows the number of large jumps up to time t is Poisson with mean t · ν{|x| ≥ 1}
• Large-jump sum: at a fixed time t ≥ 0, levyLargeJumpSum is the sum of the jump sizes of the realized marks in the band (0, t] × {|x| ≥ 1}, defined as a series of piece sums that is almost surely a finite sum; measurable_levyLargeJumpSum is its measurability, levyLargeJumpSum_ae_eq_integral identifies it almost everywhere with the Bochner integral of the jump size against the random measure over the band, and levyLargeJumpSum_ae_eq_toReal_sub writes it almost everywhere as a difference of Lebesgue integrals of the positive and negative jump parts. integral_levyLargeJumpSum gives its mean t · ∫_{|x| ≥ 1} x dν under the hypothesis that the jump size is ν-integrable over {|x| ≥ 1}. charFun_map_levyLargeJumpSum identifies its law as compound Poisson: the characteristic function is exp(t · ∫_{|x| ≥ 1} (e^{ixξ} − 1) dν). These are statements about the time-t marginal, not about path regularity (for the almost-surely càdlàg sample paths of the large-jump sum, see ae_isCadlag_levyLargeJumpSum in the càdlàg-jump-process section below)
• Evaluation σ-algebras and filtration: prmEvalSigma K X m R is the σ-algebra generated by the finite-mass evaluations of the random measure inside a region R ⊆ E, and indep_prmEvalSigma records that the random measure is independently scattered — the evaluation σ-algebras of two disjoint regions are independent — resting on indepFun_poissonRandomMeasure_families, the independence of two finite families of finite-mass evaluation sets whose disjointness is required only across the families — each set of the first disjoint from each set of the second, with no disjointness needed within a family; iIndep_prmEvalSigma and iIndepFun_poissonRandomMeasure_families upgrade both to the mutual case — the evaluation σ-algebras of finitely many pairwise-disjoint regions are mutually independent, and finitely many finite families with cross-family disjointness only give mutually independent evaluation processes — built over the disjoint-index grouping lemmas of LeanLevy/Probability/IndependenceGrouping.lean (iIndepSets.piiUnionInter_of_pairwiseDisjoint, iIndep.biSup_of_pairwiseDisjoint, iIndepFun.setRestrict_of_pairwiseDisjoint, the mutual analogues of mathlib's binary grouping forms); measurable_lintegral_poissonRandomMeasure_prmEvalSigma shows that a Lebesgue integral of a region-supported function against the random measure is measurable with respect to that region's evaluation σ-algebra; reading ℝ as time, prmFiltration is the natural filtration whose value at time t is the evaluation σ-algebra of the prefix region (−∞, t] × E (prmFiltration_apply)
• Martingales: for the natural filtration prmFiltration over ℝ≥0, martingale_centeredPoissonTimeCount shows the centered running count (poissonTimeCount K X A t).toReal − t · (m A).toReal of a measurable finite-mass set A is a martingale, and martingale_levyCompensatedSmallJump shows the compensated small-jump process of a Lévy measure is a martingale — stated for levyCompensatedSmallJumpVersion, the prmFiltration-adapted representative that levyCompensatedSmallJumpVersion_ae_eq places almost everywhere equal to the L² element levyCompensatedSmallJump at each time; the martingale property is the conditional-expectation form of the independent-increment law and does not assert càdlàg paths, path regularity, or a process-level stochastic integral. At a fixed time t, indepFun_levyLargeJumpSum_levyCompensatedSmallJump shows the large-jump sum and the compensated small-jump integral are independent — their mark regions {|x| ≥ 1} and (−1, 1) are disjoint, so the corresponding bands scatter independently — with aestronglyMeasurable_levyLargeJumpSum_prmEvalSigma the almost-everywhere region-measurability of the large-jump sum that underlies it
• Small-jump law: for a Lévy measure ν and time t ≥ 0, charFun_map_levyCompensatedSmallJump identifies the law of the compensated small-jump integral levyCompensatedSmallJump — its characteristic function is exp(t · ∫_{(−1,1)} (e^{ixξ} − 1 − ixξ) dν), the compensated exponential of the small-jump band integral. It is assembled from charFun_map_compensatedBandSum, which for a measurable mark set A ⊆ (−1, 1) of finite ν-mass and t ≥ 0 gives the characteristic function exp(t · ∫_A (e^{ixξ} − 1 − ixξ) dν) of the compensated Poisson sum of the band test function over (0, t] × A, taken over an exhausting sequence of annuli whose integrals converge to the full small-jump band. These are statements about the time-t marginal, not about path regularity (for the càdlàg small-jump path and its per-time modification of this integral, see levySmallJumpPath in the càdlàg-jump-process section below)
• Assembled jump law (LevyJumpLaw.lean): at a fixed time t ≥ 0, charFun_map_levyJumpSum_eq_exponent identifies the marginal law of b · t + (large-jump sum) + (compensated small jumps) — its characteristic function is exp(t · ψ_T(ξ)), where ψ_T is the Lévy–Khintchine exponent of the pure-jump triple (b, 0, ν) with zero Gaussian variance. The disjoint mark bands {|x| ≥ 1} and (−1, 1) make the large-jump sum and the compensated small jumps independent, so their compound-Poisson and compensated exponentials multiply; the two band integrals reassemble the Lévy–Khintchine jump integral at split radius 1, and the deterministic drift supplies the linear term. isInfinitelyDivisible_map_levyJumpSum records that this same fixed-time marginal is infinitely divisible — it is the Lévy–Khintchine law of the t-scaled triple (t · b, 0, ENNReal.ofReal t • ν), again with zero Gaussian variance. These are statements about the single time-t marginal, not about the full process (for the full process — with independent stationary increments and càdlàg paths — see levyJumpPath and exists_isLevyProcess_pureJump in the càdlàg-jump-process section below)
• Jump process and its increments (LevyJumpLaw.lean): the three fixed-time ingredients are assembled into a single process levyJumpProcess, indexed by ℝ≥0, whose value at time t is the drift b · t plus the compound-Poisson large-jump sum plus the compensated small-jump integral. hasIndependentIncrements_levyJumpProcess shows its increments over any monotone ℝ≥0 time grid are mutually independent — each increment over a step (sₖ, sₖ₊₁] reads only the Poisson marks in its own time band (sₖ, sₖ₊₁] × ℝ, consecutive bands are pairwise disjoint, and disjoint regions scatter independently by iIndep_prmEvalSigma. hasStationaryIncrements_levyJumpProcess shows the increment over (s, s + h] has a law depending only on the length h. charFun_map_levyJumpProcess_sub computes that increment's characteristic function as exp ((t − s) · ψ_{(b,0,ν)}) for s ≤ t, where ψ_{(b,0,ν)} is the Lévy–Khintchine exponent of the pure-jump triple (b, 0, ν) with zero Gaussian variance; charFun_map_levyJumpProcess its time-t marginal exp (t · ψ_{(b,0,ν)}); and levyJumpProcess_zero_ae_eq that the process is almost everywhere 0 at time 0. exists_levyJumpProcess packages these into a realization: for every drift b and Lévy measure ν there is a probability space carrying a process with independent stationary increments, an a.e.-zero start, and marginal characteristic functions exp (t · ψ_{(b,0,ν)}). All of these are law-level statements over monotone ℝ≥0 grids: no path regularity (càdlàg) is claimed and the process is not asserted to be an IsLevyProcess — the realization holds in law only (for the càdlàg modification and the full IsLevyProcess realization, see levyJumpPath and exists_isLevyProcess_pureJump in the càdlàg-jump-process section below)

Càdlàg jump process (LeanLevy/RandomMeasure/LevyJumpPath.lean)

The pure-jump component is upgraded from a law-level object to a genuine process with regular sample paths, over the same Poisson-point family at intensity volume.prod ν.

• Pathwise band sums: bandJumpSum is the pathwise sum of the marks of the realized points in the window (0, t] × A (almost surely a finite sum when A has finite ν-mass); ae_isCadlag_bandJumpSum shows that almost every sample path t ↦ bandJumpSum K X A t ω is càdlàg — almost surely only finitely many pieces are active in each bounded window, where the path is a finite sum of right-continuous jump steps — and ae_isCadlag_levyLargeJumpSum is its large-jump specialization to the mark set {|x| ≥ 1}
• Compensated band paths and martingale: levyBandPath subtracts the linear compensator drift t · ∫_A x dν from the band sum; for a band A ⊆ (−1, 1) of finite ν-mass almost every path is càdlàg (ae_isCadlag_levyBandPath), and at each time t ≥ 0 the path agrees μ-almost everywhere with the compensated Poisson integral of the band test function 1_{(0,t] × A}(u, x) · x (levyBandPath_ae_eq_compensated). martingale_levyBandVersion shows the prmFiltration-adapted representative levyBandVersion is a martingale
• Maximal inequality: measure_countable_sup_levyBandPath_ge is a weak-type bound over a countable set of times D ⊆ [0, T] — the event that levyBandPath exceeds a level ε in absolute value at some time in D has measure at most √(T · ∫_A x² dν) / ε
• Geometric truncation: levyAnnulus n is the small-jump band (−1, 1) with a central hole of radius 1/(n+1); levyTruncationSeq_spec extracts a strictly increasing subsequence of annulus indices along which the tail second moment ∫_{(−1,1) ∖ levyAnnulus} x² dν decays at least geometrically (≤ 16⁻ʲ)
• Compensated small-jump path: levySmallJumpPath is the almost-sure uniform-on-compacts limit of the annulus compensated band paths — on the almost-sure good set levySmallJumpGoodSet it is that uniform limit (of càdlàg approximants), and off it the path is gated to 0. This unconditional gating makes it càdlàg for every ω (isCadlag_levySmallJumpPath), literally 0 at t = 0 (levySmallJumpPath_zero, a function equality), and measurable at each time (measurable_levySmallJumpPath). levySmallJumpPath_ae_eq identifies it as a modification of the L² small-jump integral levyCompensatedSmallJump at each fixed time t ≥ 0 — a per-time almost-everywhere equality whose null set may depend on t; no uniform-in-t statement is claimed
• The pure-jump process: levyJumpPath is the drift b · t plus the compound-Poisson large-jump sum plus the compensated small-jump path, indexed by ℝ≥0. It shares its drift and large-jump summands literally with the law-level levyJumpProcess, replacing only the L² small-jump element by the pathwise levySmallJumpPath. It starts at 0 for every ω (levyJumpPath_zero, a literal function equality), is a per-time modification of levyJumpProcess (levyJumpPath_ae_eq), has almost-surely càdlàg sample paths (ae_isCadlag_levyJumpPath), and marginal characteristic function exp(t · ψ_{(b,0,ν)}) (charFun_map_levyJumpPath) — the Lévy–Khintchine exponent of the pure-jump triple (b, 0, ν) with zero Gaussian variance — with the characteristic exponent identified by charExponent_levyJumpPath. isLevyProcess_levyJumpPath promotes it to a genuine IsLevyProcess: a literal zero start, almost-surely càdlàg paths, and independent and stationary increments inherited from levyJumpProcess through the per-time a.e. modification
• Headline realization: exists_isLevyProcess_pureJump — for every drift b and Lévy measure ν there is a probability space carrying a process X : ℝ≥0 → Ω → ℝ that is a genuine IsLevyProcess, whose time-slices X t are measurable, and whose marginal at time t has characteristic function exp(t · ψ_{(b,0,ν)}). This realizes every pure-jump triple (b, 0, ν) by a bona fide Lévy process. It does not assert the full Lévy–Itô decomposition, any uniqueness statement, or anything about a Brownian part: there is no Gaussian component (the variance slot is literally 0), no full decomposition with a Gaussian summand, and no stochastic calculus is developed

The codebase is sorry-free. #print axioms on the main results — the Lévy–Khintchine representation, converse, uniqueness, and characterization, the compound Poisson pathwise Itô formula and law identification, and the Poisson random measure superposition law, mutual independence over a finite disjoint family, compensated second-moment isometry and its L² extension, the time-indexed independent increments, the Lévy small-jump isometry and large-jump count law, Campbell's formula for the Lebesgue integral against the random measure, the compound-Poisson law of the large-jump sum and its independence from the compensated small-jump integral, the independent scattering of the evaluation σ-algebras and its mutual (finitely-many-disjoint-region) upgrade, the centered-count and compensated small-jump martingales, the compensated small-jump law and the assembled jump law realizing the zero-Gaussian Lévy–Khintchine exponent together with its infinite divisibility, the jump process's independent and stationary increments and its in-law realization of pure-jump Lévy triples, and the càdlàg pure-jump process's genuine IsLevyProcess structure (isLevyProcess_levyJumpPath) together with its realization of every pure-jump triple by a bona fide Lévy process with almost-surely càdlàg paths (exists_isLevyProcess_pureJump) — reports only propext, Classical.choice, and Quot.sound.

Building

Requires Lean 4 (v4.32.0) and mathlib.

lake build

Structure

LeanLevy/
├── Fourier/
│   ├── Bochner.lean
│   ├── MeasureFourier.lean
│   └── PositiveDefinite.lean
├── Probability/
│   ├── Characteristic.lean
│   ├── IndependenceGrouping.lean
│   ├── Poisson.lean
│   └── WeakConvergence.lean
├── Processes/
│   ├── Cadlag.lean
│   ├── CompoundPoisson.lean
│   ├── CompoundPoissonLaw.lean
│   ├── FiniteDimensional.lean
│   ├── ProjectiveFamily.lean
│   ├── Kolmogorov.lean
│   ├── LevyProcess.lean
│   ├── PiecewisePath.lean
│   ├── PoissonProcess.lean
│   └── StochasticProcess.lean
├── RandomMeasure/
│   ├── LevyJumpLaw.lean
│   ├── LevyJumpPath.lean
│   ├── PoissonCompensated.lean
│   ├── PoissonFiltration.lean
│   ├── PoissonMartingale.lean
│   ├── PoissonPointFamily.lean
│   ├── PoissonRandomMeasure.lean
│   └── TimeSpacePoisson.lean
├── Representation/
│   └── BochnerGaussian.lean
└── Levy/
    ├── CharacteristicExponent.lean
    ├── CompensatedIntegral.lean
    ├── InfiniteDivisible.lean
    ├── LevyKhintchine.lean
    ├── LevyKhintchineProof.lean
    ├── LevyKhintchineUniqueness.lean
    └── LevyMeasure.lean