Lean 4 / Mathlib library · release v0.1.0 · Apache-2.0

Neumann Cosine

Neumann cosine series on an interval $[0,L]$ and the discrete Neumann Laplacian: orthogonality, product integrals, summable coefficients and pointwise expansions under $W^{2,1}$ or $H^2$ Neumann data, and convergence of the discrete spectrum. Formalized in Lean 4 with Mathlib.

What is proved All Lean statements Get started

Not proved here.

No PDE theory: no existence, uniqueness or regularity theorem for any differential equation, and no semigroup.
No $L^2$ theory: completeness of the cosine system in $L^2(0,L)$ and Parseval’s identity for general $L^2$ functions are not proved. The expansions above need summable coefficients, which the library derives from $W^{2,1}$ or $H^2$ Neumann data.
No general bridge to Mathlib’s fourierCoeff. Coefficients.fourierCoeff_evenPeriodic covers only the even $2L$-periodic extension of a NeumannW21 function. A bridge for general integrable functions is planned for v0.2.
One dimension only: no domains in two or more dimensions.

Find your way

Results

What is proved

Each result with its exact compared Lean statement.

All Lean statements

Generated page: every result, its hypotheses, receipts and the checks that ran.

Coverage table

Every coverage row, its claims, inputs and notes.

Modules

What each Lean module contains.

Use and trust

Get started

Build, verify, and depend on the library from your own Lake project.

Trust and axioms

Permitted axioms and what the comparator checks.

Acknowledgments and citation

Authors and AI disclosure, lean-pkg, the Auburn University Easley Cluster, what it builds on, related work, and how to cite.

This library was first developed for the Chemotaxis III Lean companion. Its sibling library is scalar-pitchfork-lean. The two libraries are independent.