Quantitative Integral Comparison for Monotone Series IV: The Harmonic Sum via Weak Euler–Maclaurin Comparison
Fuente:
Zenodo
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Recurso digital |
| Pubblicazione: |
Zenodo
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866901820659466240 |
|---|---|
| author | Jefferson, Bob |
| author_facet | Jefferson, Bob |
| contents | <h2>Abstract</h2> <p>This project applies the weak Euler–Maclaurin framework developed in the previous paper of the series to the harmonic function <span><span>f(x)=1/xf(x)=1/x</span><span><span><span>f</span><span>(</span><span>x</span><span>)</span><span>=</span></span><span><span>1/</span><span>x</span></span></span></span>.</p> <p>The harmonic partial sums</p> <p><span><span><span>HN=∑k=1N1kH_N=\sum_{k=1}^{N}\frac{1}{k}</span><span><span><span><span>H</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>=</span></span><span><span><span><span><span><span><span><span>k</span><span>=</span>1</span></span><span>∑</span><span><span><span>N</span></span></span></span><span></span></span></span></span><span><span><span><span><span><span>k</span>1</span><span></span></span></span></span></span></span></span></span></span></p> <p>admit the decomposition</p> <p><span><span><span>HN=logN+1+1/N2+EN,H_N=\log N+\frac{1+1/N}{2}+E_N,</span><span><span><span><span>H</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>=</span></span><span><span>log</span><span>N</span><span>+</span></span><span><span><span><span><span><span>21<span>+</span>1/<span>N</span></span><span></span></span></span></span></span><span>+</span></span><span><span><span>E</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>,</span></span></span></span></span></p> <p>with explicit bounds</p> <p><span><span><span>0≤EN≤1−1/N2.0\le E_N\le\frac{1-1/N}{2}.</span><span><span><span>0</span><span>≤</span></span><span><span><span>E</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>≤</span></span><span><span><span><span><span><span>21<span>−</span>1/<span>N</span></span><span></span></span></span></span></span><span>.</span></span></span></span></span></p> <p>The result follows from a minimal discrete–continuous comparison principle requiring only monotonicity, convexity on unit intervals, and elementary properties of integrals. No derivative expansions or Bernoulli numbers are required.</p> <h2>Method</h2> <p>The argument specialises the weak Euler–Maclaurin comparison principle established in Paper III. The proof relies on three elementary analytic ingredients:</p> <p>• decomposition of the integral into unit intervals<br>• a convex trapezoid estimate on each unit interval<br>• summation of these local bounds to obtain a global discrepancy estimate</p> <p>Applying this framework to <span><span>f(x)=1/xf(x)=1/x</span><span><span><span>f</span><span>(</span><span>x</span><span>)</span><span>=</span></span><span><span>1/</span><span>x</span></span></span></span> yields a transparent structural description of the difference between the harmonic sum and the logarithmic integral.</p> <h2>Quantitative interpretation</h2> <p>The decomposition gives the explicit bounds</p> <p><span><span><span>1+1/N2≤HN−logN≤1.\frac{1+1/N}{2}\le H_N-\log N\le 1.</span><span><span><span><span><span><span><span>21<span>+</span>1/<span>N</span></span><span></span></span></span></span></span><span>≤</span></span><span><span><span>H</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>−</span></span><span><span>log</span><span>N</span><span>≤</span></span><span><span>1.</span></span></span></span></span></p> <p>Taking limits yields the elementary enclosure</p> <p><span><span><span>12≤γ≤1\frac12\le\gamma\le1</span><span><span><span><span><span><span><span>21</span><span></span></span></span></span></span><span>≤</span></span><span><span>γ</span><span>≤</span></span><span><span>1</span></span></span></span></span></p> <p>for the Euler–Mascheroni constant.</p> <p>Although these bounds are coarse compared with those obtainable from the full Euler–Maclaurin expansion, they arise from a framework requiring only monotonicity, convexity, and elementary integral comparisons.</p> <h2>Formal verification</h2> <p>All results are formally verified in Lean 4 using <strong>mathlib4</strong>.</p> <p>The accompanying Lean development proves:</p> <p>• the analytic identity <span><span>∫1N1x dx=logN\int_1^N \frac{1}{x}\,dx=\log N</span><span><span><span><span>∫</span><span><span><span><span><span><span>1</span></span><span><span>N</span></span></span><span></span></span></span></span></span><span><span><span><span><span><span><span><span>x</span></span></span><span><span>1</span></span></span><span></span></span></span></span></span><span>d</span><span>x</span><span>=</span></span><span><span>log</span><span>N</span></span></span></span><br>• the harmonic weak Euler–Maclaurin decomposition<br>• explicit bounds for the correction term <span><span>ENE_N</span><span><span><span><span>E</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span></span></span></span><br>• numerical bounds for the harmonic partial sums</p> <p>The formalisation exposes these results as reusable theorems in a Lean library for integral comparison estimates.</p> <h2>Repository contents</h2> <p>The archive includes:</p> <p>• Lean 4 source files implementing the formal proofs<br>• the accompanying research paper (LaTeX source and compiled PDF)<br>• engineering logs describing the Lean modules<br>• build instructions and project metadata</p> <p>The development builds with Lean 4 and mathlib4 using a pinned toolchain.</p> <h2>Scope</h2> <p>This project lies at the intersection of</p> <p>• classical analysis<br>• analytic number theory<br>• formal verification of mathematics</p> <p>and illustrates how discrete–continuous comparison principles can be specialised to classical functions while remaining compatible with machine-checked proof.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18937084 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Quantitative Integral Comparison for Monotone Series IV: The Harmonic Sum via Weak Euler–Maclaurin Comparison Jefferson, Bob harmonic series Euler–Maclaurin formula integral comparison Euler–Mascheroni constant monotone series convexity inequalities analytic number theory formal verification mathlib4 Lean theorem prover <h2>Abstract</h2> <p>This project applies the weak Euler–Maclaurin framework developed in the previous paper of the series to the harmonic function <span><span>f(x)=1/xf(x)=1/x</span><span><span><span>f</span><span>(</span><span>x</span><span>)</span><span>=</span></span><span><span>1/</span><span>x</span></span></span></span>.</p> <p>The harmonic partial sums</p> <p><span><span><span>HN=∑k=1N1kH_N=\sum_{k=1}^{N}\frac{1}{k}</span><span><span><span><span>H</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>=</span></span><span><span><span><span><span><span><span><span>k</span><span>=</span>1</span></span><span>∑</span><span><span><span>N</span></span></span></span><span></span></span></span></span><span><span><span><span><span><span>k</span>1</span><span></span></span></span></span></span></span></span></span></span></p> <p>admit the decomposition</p> <p><span><span><span>HN=logN+1+1/N2+EN,H_N=\log N+\frac{1+1/N}{2}+E_N,</span><span><span><span><span>H</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>=</span></span><span><span>log</span><span>N</span><span>+</span></span><span><span><span><span><span><span>21<span>+</span>1/<span>N</span></span><span></span></span></span></span></span><span>+</span></span><span><span><span>E</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>,</span></span></span></span></span></p> <p>with explicit bounds</p> <p><span><span><span>0≤EN≤1−1/N2.0\le E_N\le\frac{1-1/N}{2}.</span><span><span><span>0</span><span>≤</span></span><span><span><span>E</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>≤</span></span><span><span><span><span><span><span>21<span>−</span>1/<span>N</span></span><span></span></span></span></span></span><span>.</span></span></span></span></span></p> <p>The result follows from a minimal discrete–continuous comparison principle requiring only monotonicity, convexity on unit intervals, and elementary properties of integrals. No derivative expansions or Bernoulli numbers are required.</p> <h2>Method</h2> <p>The argument specialises the weak Euler–Maclaurin comparison principle established in Paper III. The proof relies on three elementary analytic ingredients:</p> <p>• decomposition of the integral into unit intervals<br>• a convex trapezoid estimate on each unit interval<br>• summation of these local bounds to obtain a global discrepancy estimate</p> <p>Applying this framework to <span><span>f(x)=1/xf(x)=1/x</span><span><span><span>f</span><span>(</span><span>x</span><span>)</span><span>=</span></span><span><span>1/</span><span>x</span></span></span></span> yields a transparent structural description of the difference between the harmonic sum and the logarithmic integral.</p> <h2>Quantitative interpretation</h2> <p>The decomposition gives the explicit bounds</p> <p><span><span><span>1+1/N2≤HN−logN≤1.\frac{1+1/N}{2}\le H_N-\log N\le 1.</span><span><span><span><span><span><span><span>21<span>+</span>1/<span>N</span></span><span></span></span></span></span></span><span>≤</span></span><span><span><span>H</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span><span>−</span></span><span><span>log</span><span>N</span><span>≤</span></span><span><span>1.</span></span></span></span></span></p> <p>Taking limits yields the elementary enclosure</p> <p><span><span><span>12≤γ≤1\frac12\le\gamma\le1</span><span><span><span><span><span><span><span>21</span><span></span></span></span></span></span><span>≤</span></span><span><span>γ</span><span>≤</span></span><span><span>1</span></span></span></span></span></p> <p>for the Euler–Mascheroni constant.</p> <p>Although these bounds are coarse compared with those obtainable from the full Euler–Maclaurin expansion, they arise from a framework requiring only monotonicity, convexity, and elementary integral comparisons.</p> <h2>Formal verification</h2> <p>All results are formally verified in Lean 4 using <strong>mathlib4</strong>.</p> <p>The accompanying Lean development proves:</p> <p>• the analytic identity <span><span>∫1N1x dx=logN\int_1^N \frac{1}{x}\,dx=\log N</span><span><span><span><span>∫</span><span><span><span><span><span><span>1</span></span><span><span>N</span></span></span><span></span></span></span></span></span><span><span><span><span><span><span><span><span>x</span></span></span><span><span>1</span></span></span><span></span></span></span></span></span><span>d</span><span>x</span><span>=</span></span><span><span>log</span><span>N</span></span></span></span><br>• the harmonic weak Euler–Maclaurin decomposition<br>• explicit bounds for the correction term <span><span>ENE_N</span><span><span><span><span>E</span><span><span><span><span><span><span>N</span></span></span><span></span></span></span></span></span></span></span></span><br>• numerical bounds for the harmonic partial sums</p> <p>The formalisation exposes these results as reusable theorems in a Lean library for integral comparison estimates.</p> <h2>Repository contents</h2> <p>The archive includes:</p> <p>• Lean 4 source files implementing the formal proofs<br>• the accompanying research paper (LaTeX source and compiled PDF)<br>• engineering logs describing the Lean modules<br>• build instructions and project metadata</p> <p>The development builds with Lean 4 and mathlib4 using a pinned toolchain.</p> <h2>Scope</h2> <p>This project lies at the intersection of</p> <p>• classical analysis<br>• analytic number theory<br>• formal verification of mathematics</p> <p>and illustrates how discrete–continuous comparison principles can be specialised to classical functions while remaining compatible with machine-checked proof.</p> |
| title | Quantitative Integral Comparison for Monotone Series IV: The Harmonic Sum via Weak Euler–Maclaurin Comparison |
| topic | harmonic series Euler–Maclaurin formula integral comparison Euler–Mascheroni constant monotone series convexity inequalities analytic number theory formal verification mathlib4 Lean theorem prover |
| url | https://doi.org/10.5281/zenodo.18937084 |