Search for a command to run...
This deposit contains the Lean 4 formal verification companion (BanachLevyComplete.lean, 2,439 lines) for the paper "Operator Factorization Beyond Hilbert Spaces: Representability Obstructions, Leibniz Defects, and Chaos Characterizations for Stable Lévy Processes" by Ramiro Fontes. The file has zero sorry declarations and zero axiom declarations. It integrates three layers: Part 1 — Poisson infrastructure: The symmetric γ-stable Lévy measure density with proved symmetry and nonnegativity. The Poisson mean identity E[Poisson(λ)] = λ and variance identity Var(Poisson(λ)) = λ, proved as theorems via a recurrence lemma and HasSum assembly. A canonical Poisson random variable constructed on (ℕ, poissonMeasure(λT)) with its distribution proved by Measure.map_id. Stable measure moment computations and the Blumenthal–Getoor dichotomy. Quadratic defect sharpness for the variance swap payoff. Part 2 — Lévy–Itô framework: The Itô formula for compound Poisson processes proved as a finite telescoping sum via Finset.sum_range_sub. A compound Poisson path defined as a concrete function, proved to start at zero and to have the correct terminal value. The compensated Poisson integral constructed as an L² limit of compound Poisson finite sums, with linearity inherited from finite-sum linearity and centering derived via tendsto_nhds_unique. Truncation convergence, centering, the predictable module structure, and chaos orthogonality derived from the compensated-integral interface. The first Poisson chaos realized concretely on (ℕ, poissonMeasure) with orthogonality proved via tsum_mul_left. The L² Cauchy estimate for the ε → 0 approximation proved, with the M → ∞ direction documented as requiring Lp (not L²) convergence. Part 3 — Banach energy space framework: The operator-covariant derivative D constructed via mk_dual (not axiomatized). The fluctuation factorization (Theorem A), representability obstruction, product rule with jump defect (Theorem B), and chaos characterization (Theorem C) verified. The centered obstruction witness derived from primitive stable-noise data: evenness from absolute-jump structure, positive variance from λ > 0 and T > 0 via mul_pos, nonzero from positive variance, and the obstruction from representability_obstruction. The Hilbert bridge showing the Banach framework specializes when the jump defect vanishes. The remaining primitive inputs are concentrated in two places: the Banach-side Lp-convergence layer for the compensated integral as M → ∞, and a full bottom-up Poisson-random-measure realization. These are isolated as explicit structure fields rather than hidden proof gaps. Together with the companion OperatorDerivative.lean (5,184 lines, zero sorry, one axiom) for the Hilbert paper, this constitutes 7,623 lines of formally verified stochastic calculus. To our knowledge, the Poisson mean and variance identities, the first Poisson chaos orthogonality, and the compound Poisson Itô formula via finite telescoping are among the first such formalized results in Lean 4.