cff-version: 1.2.0
message: If you use this software, please cite it as below, and record the exact commit you used.
title: 'NeumannCosine: Neumann cosine series on an interval and the discrete Neumann Laplacian in Lean 4'
type: software
authors:
- family-names: Chen
  given-names: Le
  affiliation: Auburn University
license: Apache-2.0
version: 0.1.0
date-released: '2026-10-20'
doi: 10.5281/zenodo.23488175
identifiers:
- type: doi
  value: 10.5281/zenodo.23488175
  description: Concept DOI (all versions; resolves to the latest release)
- type: doi
  value: 10.5281/zenodo.23488176
  description: Version DOI for v0.1.0
repository-code: https://github.com/chenle02/neumann-cosine-lean
abstract: Lean 4 library on Neumann cosine series on [0, L] and the discrete Neumann Laplacian.
  It proves orthogonality of the modes, closed forms for integrals of products of modes and of
  absolutely summable cosine series, absolute summability and pointwise convergence of cosine
  expansions under W^{2,1} or H^2 Neumann hypotheses, basic one-dimensional weak-derivative
  results, the cosine eigenbasis of the reflected three-point Laplacian, and convergence of
  discrete eigenvalues and modal minima to their continuum values.
keywords:
- Lean 4
- Mathlib
- formalization
- Fourier cosine series
- Neumann boundary condition
- discrete Laplacian
references:
- type: conference-paper
  title: The Lean Mathematical Library
  authors:
  - name: The mathlib Community
  collection-title: 'Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)'
  year: 2020
  doi: 10.1145/3372885.3373824
  repository-code: https://github.com/leanprover-community/mathlib4
- type: article
  title: 'Chemotaxis models with signal-dependent sensitivity and a logistic-type source, III: Bifurcation and spike-like solutions'
  authors:
  - family-names: Chen
    given-names: Le
  - family-names: Ruau
    given-names: Ian
  - family-names: Shen
    given-names: Wenxian
  year: 2026
  identifiers:
  - type: other
    value: arXiv:2610.20976
  url: https://arxiv.org/abs/2610.20976