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

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

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

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

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)

The codebase is sorry-free. #print axioms on the main results — the Lévy–Khintchine representation, converse, uniqueness, and characterization, and the compound Poisson pathwise Itô formula and law identification — reports only propext, Classical.choice, and Quot.sound.

Building

Requires Lean 4 (v4.29.0-rc3) and mathlib.

lake build

Structure

LeanLevy/
├── Fourier/
│   ├── Bochner.lean
│   ├── MeasureFourier.lean
│   └── PositiveDefinite.lean
├── Probability/
│   ├── Characteristic.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
├── Representation/
│   └── BochnerGaussian.lean
└── Levy/
    ├── CharacteristicExponent.lean
    ├── CompensatedIntegral.lean
    ├── InfiniteDivisible.lean
    ├── LevyKhintchine.lean
    ├── LevyKhintchineProof.lean
    ├── LevyKhintchineUniqueness.lean
    └── LevyMeasure.lean