Coverage

Library: each row is a main result of the library.

Main results: 20.
lean-pkg’s claims ledger: ready (sha256:0d19b11488fb5018…).

Result	Claims	Lean declarations	Ledger	Note
Orthogonality and Gram values of the Neumann cosine modes	`neumann-cosine-lean/integral-mode-mul-mode`	`NeumannCosine.integral_mode_mul_mode`	verified	—
Closed form of the integral of four cosine modes	`neumann-cosine-lean/kernel-integrals-integral-cos-cos-cos-cos`	`NeumannCosine.KernelIntegrals.integral_cos_cos_cos_cos`	verified	—
Integral of a product of three cosine series against a cosine	`neumann-cosine-lean/product-identities-cos-cos-cos-cos-lp`	`NeumannCosine.ProductIdentities.cos_cos_cos_cos_lp`	verified	—
Integral of two cosine series against two sines	`neumann-cosine-lean/product-identities-two-cosines-two-sines-lp`	`NeumannCosine.ProductIdentities.two_cosines_two_sines_lp`	verified	—
Cosine coefficients of W^{2,1} Neumann functions are absolutely summable	`neumann-cosine-lean/coefficients-summable-norm-cosine-coeff`	`NeumannCosine.Coefficients.summable_norm_cosineCoeff`	verified	—
Pointwise cosine expansion of W^{2,1} Neumann functions	`neumann-cosine-lean/coefficients-has-sum-cosine-coeff`	`NeumannCosine.Coefficients.hasSum_cosineCoeff`	verified	—
The du Bois-Reymond lemma on an interval	`neumann-cosine-lean/sobolev-weak-derivative-ae-eq-const-of-integral-mul-deriv-eq-zero`	`NeumannCosine.Sobolev.WeakDerivative.ae_eq_const_of_integral_mul_deriv_eq_zero`	verified	—
W^{1,1} functions have an absolutely continuous representative	`neumann-cosine-lean/sobolev-weak-derivative-has-weak-deriv-ae-eq-primitive`	`NeumannCosine.Sobolev.WeakDerivative.HasWeakDeriv.ae_eq_primitive`	verified	—
Cosine expansion of H^2 functions with Neumann trace	`neumann-cosine-lean/sobolev-h2-neumann-h2-has-sum-cosine-coeff`	`NeumannCosine.Sobolev.H2Neumann.H2.hasSum_cosineCoeff`	verified	—
Cosine eigenbasis of the discrete Neumann Laplacian	`neumann-cosine-lean/discrete-laplacian-reflected-neg-laplacian-cosine-eigenpair` `neumann-cosine-lean/discrete-laplacian-discrete-cosine-mode-exhaustion` `neumann-cosine-lean/discrete-laplacian-discrete-cosine-modes-linear-independent`	`NeumannCosine.Discrete.Laplacian.reflectedNegLaplacian_cosine_eigenpair` `NeumannCosine.Discrete.Laplacian.discreteCosineMode_exhaustion` `NeumannCosine.Discrete.Laplacian.discreteCosineModes_linearIndependent`	verified verified verified	—
Discrete Neumann eigenvalues converge to the continuum ones	`neumann-cosine-lean/discrete-eigenvalues-discrete-neumann-eigenvalue-tendsto`	`NeumannCosine.Discrete.Eigenvalues.discreteNeumannEigenvalue_tendsto`	verified	—
Discrete modal minimum converges to the continuum infimum	`neumann-cosine-lean/discrete-modal-minimum-limit-discrete-modal-min-tendsto`	`NeumannCosine.Discrete.ModalMinimumLimit.discreteModalMin_tendsto`	verified	—
Normalized projections of the Neumann modes	`neumann-cosine-lean/integral-cos-int-mul-pi-div` `neumann-cosine-lean/normalized-integral-mode-mul-self` `neumann-cosine-lean/normalized-integral-mode-three-mul` `neumann-cosine-lean/normalized-integral-mode-pow-four`	`NeumannCosine.integral_cos_int_mul_pi_div` `NeumannCosine.normalized_integral_mode_mul_self` `NeumannCosine.normalized_integral_mode_three_mul` `NeumannCosine.normalized_integral_mode_pow_four`	verified verified verified verified	—
Closed forms of the three-cosine and cosine-sine kernels	`neumann-cosine-lean/kernel-integrals-integral-cos-sin-sin` `neumann-cosine-lean/kernel-integrals-integral-cos-cos-cos` `neumann-cosine-lean/kernel-integrals-integral-cos-cos-sin-sin`	`NeumannCosine.KernelIntegrals.integral_cos_sin_sin` `NeumannCosine.KernelIntegrals.integral_cos_cos_cos` `NeumannCosine.KernelIntegrals.integral_cos_cos_sin_sin`	verified verified verified	—
Product identities for absolutely summable cosine series	`neumann-cosine-lean/product-identities-cosine-sine-sine` `neumann-cosine-lean/product-identities-two-cosines-two-sines` `neumann-cosine-lean/product-identities-cos-cos-cos` `neumann-cosine-lean/product-identities-cos-cos-cos-cos` `neumann-cosine-lean/product-identities-cosine-sine-sine-lp` `neumann-cosine-lean/product-identities-cos-cos-cos-lp`	`NeumannCosine.ProductIdentities.cosine_sine_sine` `NeumannCosine.ProductIdentities.two_cosines_two_sines` `NeumannCosine.ProductIdentities.cos_cos_cos` `NeumannCosine.ProductIdentities.cos_cos_cos_cos` `NeumannCosine.ProductIdentities.cosine_sine_sine_lp` `NeumannCosine.ProductIdentities.cos_cos_cos_lp`	verified verified verified verified verified verified	—
Termwise integration of a cosine series	`neumann-cosine-lean/series-termwise-integral-has-sum-interval-integral-cosine`	`NeumannCosine.Series.TermwiseIntegral.hasSum_intervalIntegral_cosine`	verified	—
Quadratic decay of the cosine coefficients	`neumann-cosine-lean/coefficients-cosine-coeff-eq-neg-mul-second-deriv` `neumann-cosine-lean/coefficients-abs-cosine-coeff-le`	`NeumannCosine.Coefficients.cosineCoeff_eq_neg_mul_secondDeriv` `NeumannCosine.Coefficients.abs_cosineCoeff_le`	verified verified	—
Summable cosine coefficients of H^2 functions with Neumann trace	`neumann-cosine-lean/sobolev-h2-neumann-h2-summable-norm-cosine-coeff`	`NeumannCosine.Sobolev.H2Neumann.H2.summable_norm_cosineCoeff`	verified	—
Cosine projection of a divergence-form source	`neumann-cosine-lean/divergence-form-projection-abs-integral-source-add-deriv-mul-cos-le` `neumann-cosine-lean/divergence-form-projection-abs-integral-source-add-deriv-mul-cos-le-of-absolutely-continuous`	`NeumannCosine.DivergenceFormProjection.abs_integral_source_add_deriv_mul_cos_le` `NeumannCosine.DivergenceFormProjection.abs_integral_source_add_deriv_mul_cos_le_of_absolutelyContinuous`	verified verified	—
Discrete Neumann eigenvalues: sinc form, ordering and lower bound	`neumann-cosine-lean/discrete-eigenvalues-discrete-neumann-eigenvalue-eq-mul-sinc-sq` `neumann-cosine-lean/discrete-eigenvalues-discrete-neumann-eigenvalue-one-le` `neumann-cosine-lean/discrete-eigenvalues-discrete-neumann-eigenvalue-lower-bound` `neumann-cosine-lean/discrete-laplacian-discrete-neumann-eigenvalue-lt-of-lt`	`NeumannCosine.Discrete.Eigenvalues.discreteNeumannEigenvalue_eq_mul_sinc_sq` `NeumannCosine.Discrete.Eigenvalues.discreteNeumannEigenvalue_one_le` `NeumannCosine.Discrete.Eigenvalues.discreteNeumannEigenvalue_lower_bound` `NeumannCosine.Discrete.Laplacian.discreteNeumannEigenvalue_lt_of_lt`	verified verified verified verified	—

One line per main result of coverage.yaml. Ledger: the status lean-pkg claims ledger gives each claim, in the order of the claims; only verified means the recorded receipts close the claim.

Back to Verification.