Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Euler Mascheroni Constant lb

eulerMascheroniConstant_lb

analytic number theory prime numbers asymptotics euler mascheroni bounds

Plain-language statement

For every integer $n\ge0$ , the corrected harmonic approximation $H_{n+1}-\log(n+1)-\frac{1}{2(n+1)}$ is a lower bound for the Euler–Mascheroni constant $\gamma$ .

Exact Lean statement

lemma eulerMascheroniConstant_lb (n : ℕ) :
    γ₁ (n + 1) ≤ eulerMascheroniConstant

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma eulerMascheroniConstant_lb (n : ℕ) :    γ₁ (n + 1) ≤ eulerMascheroniConstant := by  have key : γ₁ (n + 1) = eulerMascheroniSeq n + 1 / (2 * ((n : ℝ) + 1)) := by    simp only [γ₁, eulerMascheroniSeq]    rw [harmonic_succ]    push_cast    field_simp    ring  rw [key]  have h_lim : Filter.Tendsto (fun m => eulerMascheroniSeq m - eulerMascheroniSeq n) Filter.atTop (nhds (eulerMascheroniConstant - eulerMascheroniSeq n)) :=    Filter.Tendsto.sub Real.tendsto_eulerMascheroniSeq tendsto_const_nhds  have h_lim_bound : Filter.Tendsto (fun m => 1 / (2 * (n + 1) : ℝ) - 1 / (2 * (m + 1) : ℝ)) Filter.atTop (nhds (1 / (2 * (n + 1) : ℝ))) :=    le_trans (tendsto_const_nhds.sub <| tendsto_const_nhds.div_atTop <|      Filter.Tendsto.const_mul_atTop zero_lt_two <|      Filter.tendsto_id.atTop_add tendsto_const_nhds) <| by norm_num  have := h_lim_bound.comp tendsto_natCast_atTop_atTop  exact le_of_tendsto_of_tendsto this h_lim (Filter.eventually_atTop.mpr    ⟨n, by intros m hm; simpa using eulerMascheroniSeq_diff_lb n m hm⟩) |>    fun h => by norm_num at *; grind

Project: Prime Number Theorem and More
License: Apache-2.0
Commit: a93551347dce
Source: PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:99-117

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.0

Admissible bound mono

admissible_bound.mono

Plain-language statement

For positive parameters $A,B,C,R$ , the classical error-bound function $A\left(\frac{\log x}{R}\right)^B\exp\!\left(-C\sqrt{\frac{\log x}{R}}\right)$ is nonincreasing once $x\ge \exp\!\left(R(2B/C)^2\right)$ .

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Analytic On div Removable zero

AnalyticOn_divRemovable_zero

Plain-language statement

Let $f$ be analytic on an open set $s$ containing $0$ , and suppose $f(0)=0$ . Define $g(z)=f(z)/z$ for $z\ne0$ and $g(0)=f'(0)$ . Then the apparent singularity at $0$ is removable and $g$ is analytic throughout $s$ .

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Analytic On div Removable zero closed Ball

AnalyticOn_divRemovable_zero_closedBall

Plain-language statement

Suppose $R>0$ and $f$ is analytic on the closed disc $|z|\le R$ with $f(0)=0$ . Define $g(z)=f(z)/z$ for $z\ne0$ and $g(0)=f'(0)$ . Then $g$ is analytic on the entire closed disc, including at the removed singularity.

analytic number theoryprime numbersasymptotics

Source project: Prime Number Theorem and More

Person-level attribution pending.

View proof record