# P2516: The sharp Dirichlet Poincare constant with two moment constraints

- ID: `P2516`
- Reference: `two-moment-poincare-constant`
- Page: https://theoremdb.org/statements/P2516
- Record maturity: Reviewed problem with recorded work

## Problem

Let \(\lambda_*\) be the infimum of \(\int_0^1|f'(x)|^2\,dx/\int_0^1|f(x)|^2\,dx\) over nonzero \(f\in H_0^1(0,1)\) satisfying \(\int_0^1 f(x)\,dx=\int_0^1 x f(x)\,dx=0\). Determine \(\lambda_*\) with a rigorous interval of width at most \(10^{-8}\).

### Context

This variational problem asks for the first Dirichlet energy level after imposing orthogonality to the functions \(1\) and \(x\).

### Problem setup

- **Definition (\(H_0^1(0,1)\)).** The space \(H_0^1(0,1)\) consists of square-integrable functions with square-integrable weak derivative and zero endpoint traces.
- **Remark.** The reciprocal of \(\lambda_*\) is the best constant in the corresponding constrained Poincaré inequality.

### What counts as a solution

- Derive a correct characteristic equation or validated variational scheme and certify \(\lambda_*\) inside an interval of width at most \(10^{-8}\).

## The answer

Exact Taylor bounds place lambda_* in an interval of width 7.189455132656e-10. [2](#reference-2)

**Review status:** Reproduced.

**Lean verification:** not Lean-verified.

### Verification

Take the rational endpoints
\[
z_-=\frac{44934094579}{10^{10}},\qquad
z_+=\frac{3510476139}{781250000}.
\]
For \(h(z)=\sin z-z\cos z\), Taylor's theorem gives rigorous enclosures by using the sine polynomial through degree 49 with error at most \(z^{51}/51!\), and the cosine polynomial through degree 48 with error at most \(z^{50}/50!\). Exact rational arithmetic gives
\[
h(z_-)>\frac3{10^{11}},\qquad h(z_+)<-\frac4{10^{11}}.
\]
The uniqueness proved in the spectral record isolates \(z_*\) between these endpoints. Squaring the positive interval and multiplying by four gives
\[
\frac{2019072855634517187241}{25000000000000000000}
<\lambda_*<
\frac{12323442722488347321}{152587890625000000}.
\]
In terminating decimals,
\[
\boxed{80.76291422538068748964<\lambda_*<80.76291422609963300291}.
\]
The exact width is
\[
\frac{449340945791}{625000000000000000000}
=0.0000000007189455132656<10^{-8}.
\]
Consequently the best constant \(C_*=1/\lambda_*\) obeys
\[
\frac{152587890625000000}{12323442722488347321}
<C_*<
\frac{25000000000000000000}{2019072855634517187241},
\]
or approximately \(0.01238192070682903136<C_*<0.01238192070693925431\).

## Work

### Proof and evidence for the resolution

**Computation 1 (The sharp eigenvalue is certified to ten decimal places).** Exact Taylor bounds place lambda_* in an interval of width 7.189455132656e-10.

Take the rational endpoints
\[
z_-=\frac{44934094579}{10^{10}},\qquad
z_+=\frac{3510476139}{781250000}.
\]
For \(h(z)=\sin z-z\cos z\), Taylor's theorem gives rigorous enclosures by using the sine polynomial through degree 49 with error at most \(z^{51}/51!\), and the cosine polynomial through degree 48 with error at most \(z^{50}/50!\). Exact rational arithmetic gives
\[
h(z_-)>\frac3{10^{11}},\qquad h(z_+)<-\frac4{10^{11}}.
\]
The uniqueness proved in the spectral record isolates \(z_*\) between these endpoints. Squaring the positive interval and multiplying by four gives
\[
\frac{2019072855634517187241}{25000000000000000000}
<\lambda_*<
\frac{12323442722488347321}{152587890625000000}.
\]
In terminating decimals,
\[
\boxed{80.76291422538068748964<\lambda_*<80.76291422609963300291}.
\]
The exact width is
\[
\frac{449340945791}{625000000000000000000}
=0.0000000007189455132656<10^{-8}.
\]
Consequently the best constant \(C_*=1/\lambda_*\) obeys
\[
\frac{152587890625000000}{12323442722488347321}
<C_*<
\frac{25000000000000000000}{2019072855634517187241},
\]
or approximately \(0.01238192070682903136<C_*<0.01238192070693925431\).

### Background and intake notes

- Original intake status: Status not established. No literature search was performed. Constrained Sturm-Liouville problems of this type are classical.
- A sine Galerkin truncation gives monotone upper bounds under exact constraint projection. A lower bound needs a residual estimate or a secular equation with certified root isolation.
- Simply deleting the first two sine modes is invalid because the moment constraints are not coordinate constraints in that basis.

### Supporting results

- **Claim 1** (reported): The minimum is the simple even eigenvalue 4z_*^2, where z_* is the unique zero of sin z-z cos z in (pi,3pi/2). [2](#reference-2)

### Prior approaches

- **Route 1** (supported): Classical sharp Poincare theory and Gaussian moment improvements supply context; the exact two-moment Dirichlet constant was not found. [3](#reference-3) [2](#reference-2) [1](#reference-1)

### Formalizations

- **Formalization 1** (reported): The approved theorem checks both rational Taylor endpoint inequalities, the two squared endpoints, the exact interval width, and the required 10^-8 bound. [2](#reference-2)

### Runnable artifacts

- **Artifact 1** (reproduced): A standard-library Python program proves both endpoint signs and the required lambda interval width using Fraction arithmetic.

### Computational notes

- Numerical constrained Ritz estimates with 4, 8, 20, 40, 80, and 160 sine modes were 80.9307560889, 80.7809865827, 80.7640276904, 80.7630526606, 80.7629315067, and 80.7629163851. The reciprocal of the 160-mode estimate is approximately 0.0123819203758. None of these decimals has a rigorous error certificate.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `two-moment-poincare-constant`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

1 declaration, with 0 open proof obligations.

### TheoremDB.TwoMomentPoincare.exactRationalCertificate

- State: source contains no sorry; verification pending
- Role: target declaration
- Lean world: `lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@24c58f96c6cba9e5150e04319a134c65cd13a0b2b4615f54dc2959b54ec2765d`

```lean
theorem TheoremDB.TwoMomentPoincare.exactRationalCertificate : ∀ (zLo zHi : ℚ), zLo = 449340945790 / 10 ^ 11 → zHi = 449340945792 / 10 ^ 11 → 3 / 10 ^ 11 < ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zLo ^ (2 * j + 1) / (Nat.factorial (2 * j + 1) : ℚ)) - zLo ^ 51 / (Nat.factorial 51 : ℚ)) - zLo * ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zLo ^ (2 * j) / (Nat.factorial (2 * j) : ℚ)) + zLo ^ 50 / (Nat.factorial 50 : ℚ)) ∧ ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zHi ^ (2 * j + 1) / (Nat.factorial (2 * j + 1) : ℚ)) + zHi ^ 51 / (Nat.factorial 51 : ℚ)) - zHi * ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zHi ^ (2 * j) / (Nat.factorial (2 * j) : ℚ)) - zHi ^ 50 / (Nat.factorial 50 : ℚ)) < -(4 / 10 ^ 11) ∧ 4 * zLo ^ 2 = 2019072855634517187241 / 25000000000000000000 ∧ 4 * zHi ^ 2 = 12323442722488347321 / 152587890625000000 ∧ 4 * zHi ^ 2 - 4 * zLo ^ 2 = 449340945791 / 625000000000000000000 ∧ 4 * zHi ^ 2 - 4 * zLo ^ 2 < 1 / 10 ^ 8
```

### Continue Lean verification

Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.

[Continue Lean verification with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20two-moment-poincare-constant%0A%0AExact%20title%3A%20The%20sharp%20Dirichlet%20Poincare%20constant%20with%20two%20moment%20constraints%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Ftwo-moment-poincare-constant%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>Jean-Philippe Bartier, Adrien Blanchet, Jean Dolbeault, and Miguel Escobedo, “Improved intermediate asymptotics for the heat equation”. Applied Mathematics Letters 24(1) (2011), 76-81. DOI 10.1016/j.aml.2010.08.020. Applied Mathematics Letters 24 (2011), Proposition 1 https://doi.org/10.1016/j.aml.2010.08.020
   - scholarly_publication; reference source; checked 2026-08-01
   - Source use: citation_only
   - For The sharp Dirichlet Poincare constant with two moment constraints, the reviewed source scope is Applied Mathematics Letters 24 (2011), Proposition 1. The packet makes no inference beyond that cited scope.
2. <a id="reference-2"></a>Nikolay Kuznetsov and Alexander Nazarov, “Sharp constants in the Poincaré, Steklov and related inequalities: a survey,” Mathematika 61(2) (2015), 328-344. DOI 10.1112/S0025579314000229. survey sections on sharp Poincare, Steklov, and related constants https://doi.org/10.1112/S0025579314000229
   - Also cited at Mathematika 61 (2015), 328-344
   - Also cited at Exact rational certificate tmpc-artifact-rational-root-certificate, together with tmpc-claim-spectral-reduction
   - Also cited at Complete variational, parity, min-max, and ODE proof supplied in this record
   - Also cited at formalization-target:tmpc-artifact-rational-root-certificate
   - scholarly_publication; reference source; checked 2026-08-01
   - Source use: citation_only
   - For The sharp Dirichlet Poincare constant with two moment constraints, this source supplies classical endpoint inequalities; it does not give the packet's two-moment exact constant.
   - Source named by the research packet.
3. <a id="reference-3"></a>Guiqiao Xu, Zehong Liu, and Wanting Lu, “A kind of sharp Wirtinger inequality”. Journal of Inequalities and Applications 2019(1) (2019), 166. DOI 10.1186/s13660-019-2121-8. Guiqiao Xu, Zehong Liu, and Wanting Lu, A kind of sharp Wirtinger inequality, Journal of Inequalities and Applications 2019:166, abstract and L2 eigenvalue discussion; Nikolay Kuznetsov and Alexander Nazarov, Mathematika 61 (2015), 328-344, DOI 10.1112/S0025579314000229; Jean-Philippe Bartier, Adrien Blanchet, Jean Dolbeault, and Miguel Escobedo, Applied Mathematics Letters 24 (2011), 76-81, Proposition 1, DOI 10.1016/j.aml.2010.08.020 https://doi.org/10.1186/s13660-019-2121-8
   - Also cited at Journal of Inequalities and Applications 2019, article 166
   - scholarly_publication; reference source; version of record; checked 2026-08-01
   - Source use: citation_only
   - For The sharp Dirichlet Poincare constant with two moment constraints, the reviewed source scope is Guiqiao Xu, Zehong Liu, and Wanting Lu, A kind of sharp Wirtinger inequality, Journal of Inequalities and Applications 2019:166, abstract and L2 eigenvalue discussion; Nikolay Kuznetsov and Alexander Nazarov, Mathematika 61 (2015), 328-344, DOI 10.1112/S0025579314000229; Jean-Philippe Bartier, Adrien Blanchet, Jean Dolbeault, and Miguel Escobedo, Applied Mathematics Letters 24 (2011), 76-81, Proposition 1, DOI 10.1016/j.aml.2010.08.020. The packet makes no inference beyond that cited scope.