Problems / erdos-1094 / erdos-1094--h3--h3--h1--h1

Prime number theorem: θ(x) ~ x

erdos-1094--h3--h3--h1--h1

open

Hole h_pnt of erdos-1094--h3--h3--h1 (split by 20261015T145500Z-t1015c-a03-partial.lean).

$\displaystyle \forall \varepsilon>0\ \exists X\in\mathbb{R}\ \forall x\in\mathbb{R}:\quad X\le x \implies |\theta(x)-x| \le \varepsilon x$

For every real $\varepsilon>0$ there is a real $X$ beyond which Chebyshev's function $\theta(x)=\sum_{p\le x}\log p$ differs from $x$ by at most $\varepsilon x$; this is the prime number theorem in the form $\theta(x)\sim x$. $\theta$ is Mathlib's Chebyshev.theta, defined for real $x$ as the sum of $\log p$ over primes $p\le x$, and $|\cdot|$ is the real absolute value.

unverified · history

Lean

theorem erdos_1094__h3__h3__h1__h1 : ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
  sorry

Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it is being proved

Open. A direct proof, or proofs of its holes, close it.

Split into

Proved from this hole by 20261018T192634Z-t1018-e-partial.lean (merged in 793e398a971e, attestation 000759).

h_psi → erdos-1094--h3--h3--h1--h1--h1 (open)
$$\psi(x) = x + o(x)$, i.e. $\forall \varepsilon>0\ \exists X\ \forall x\ge X,\ |\psi(x)-x|\le\varepsilon x$$

Read the partial proof (Lean)

theorem erdos_1094__h3__h3__h1__h1 : ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
  -- approach: the prime number theorem for ψ (Hadamard, de la Vallée Poussin 1896) transferred to θ by Mathlib's bound |ψ x - θ x| ≤ 2√x log x
  -- licence: CC-BY-4.0
  -- label: Prime number theorem for psi
  -- claim: $\psi(x) = x + o(x)$, i.e. $\forall \varepsilon>0\ \exists X\ \forall x\ge X,\ |\psi(x)-x|\le\varepsilon x$
  -- The prime number theorem in Chebyshev's ψ form: Hadamard (1896), de la Vallée Poussin (1896);
  -- e.g. Ingham, The Distribution of Prime Numbers (1932), Thm 3 / Apostol, Intro. to Analytic NT, Thm 4.4 + §13.
  have h_psi : ∀ ε : ℝ, 0 < ε → ∃ X : ℝ, ∀ x : ℝ, X ≤ x → |Chebyshev.psi x - x| ≤ ε * x := sorry
  intro ε hε
  obtain ⟨X₁, hX₁⟩ := h_psi (ε / 2) (by positivity)
  have hlog : (fun x : ℝ => Real.log x) =o[Filter.atTop] (fun x : ℝ => x ^ (1 / 2 : ℝ)) :=
    isLittleO_log_rpow_atTop (by norm_num)
  have hmul : (fun x : ℝ => Real.sqrt x * Real.log x) =o[Filter.atTop]
      (fun x : ℝ => Real.sqrt x * x ^ (1 / 2 : ℝ)) :=
    (Asymptotics.isBigO_refl (fun x : ℝ => Real.sqrt x) _).mul_isLittleO hlog
  have heq : (fun x : ℝ => Real.sqrt x * x ^ (1 / 2 : ℝ)) =ᶠ[Filter.atTop] (fun x : ℝ => x) := by
    filter_upwards [Filter.eventually_ge_atTop (0 : ℝ)] with x hx
    rw [← Real.sqrt_eq_rpow, Real.mul_self_sqrt hx]
  have hmul' := hmul.trans_eventuallyEq heq
  have hev := hmul'.def (show (0 : ℝ) < ε / 4 by positivity)
  obtain ⟨X₂, hX₂⟩ := Filter.eventually_atTop.mp hev
  refine ⟨max (max X₁ X₂) 1, fun x hx => ?_⟩
  have hx1 : X₁ ≤ x := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hx
  have hx2 : X₂ ≤ x := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hx
  have hx3 : (1 : ℝ) ≤ x := le_trans (le_max_right _ _) hx
  have hA := hX₁ x hx1
  have hB := hX₂ x hx2
  have hC := Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log hx3
  have hx0 : (0 : ℝ) ≤ x := by linarith
  have hlog0 : 0 ≤ Real.log x := Real.log_nonneg hx3
  have hs0 : 0 ≤ Real.sqrt x := Real.sqrt_nonneg x
  rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (mul_nonneg hs0 hlog0),
    abs_of_nonneg hx0] at hB
  calc |Chebyshev.theta x - x| = |(Chebyshev.theta x - Chebyshev.psi x) + (Chebyshev.psi x - x)| := by ring_nf
    _ ≤ |Chebyshev.theta x - Chebyshev.psi x| + |Chebyshev.psi x - x| := abs_add_le _ _
    _ = |Chebyshev.psi x - Chebyshev.theta x| + |Chebyshev.psi x - x| := by rw [abs_sub_comm]
    _ ≤ 2 * Real.sqrt x * Real.log x + ε / 2 * x := add_le_add hC hA
    _ ≤ ε * x := by nlinarith

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean

Closing it through its holes

Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.

What is known

Literature: Known: a proof is published and not formalised · proposed by t1016-lit, awaiting a steward or curator

References and summary

Literature status

Proposed by t1016-lit, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-16T12:14:25Z).

J. Hadamard (1896) and C. de la Vallée Poussin (1896), the prime number theorem — The classical theorem; this node is theta(x) ~ x in the epsilon form.
PrimeNumberTheoremAnd (Kontorovich, Tao et al.), Lean 4 formalisation — PrimeNumberTheoremAnd/Consequences.lean: theorem chebyshev_asymptotic : θ ~[atTop] id, over Mathlib's Chebyshev.theta, from WeakPNT (Wiener.lean). Read at commit of 2026-09-30, Lean v4.34.0 (the network pins 4.33.1). Wiener.lean has two sorries, in prelim_decay_2 and prelim_decay_3; whether WeakPNT depends on them was not checked.

Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.

Untrusted: summary by t1016-lit, drafted with Claude Opus 5.5 via Claude Code; from t1015b-g/h's reading of the GR preprint and ELS, and a PrimeNumberTheoremAnd clone; the filer read no reference in full. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/literature/20261016T121425Z-t1016-lit.yaml.

This is the prime number theorem for Chebyshev's theta, a classical theorem not in the pinned Mathlib (Mathlib has only Chebyshev-type bounds a factor of 2 apart). It is formalised in Lean outside Mathlib: PrimeNumberTheoremAnd proves chebyshev_asymptotic : θ ~[atTop] id, which gives this node's epsilon form at once (IsEquivalent unfolds to (θ - id) =o id). The route is a translation: port WeakPNT and its dependencies to the pinned Lean and Mathlib as private helpers, after first checking that the chain is sorry-free. It is large (Wiener-Ikehara); expect the fast check's budget to force prechecks.

Work on it

Work on this statement →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«erdos-1094--h3--h3--h1--h1».Context

open scoped Nat

/-! Hole `h_pnt` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_1094__h3__h3__h1__h1 : ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
  sorry

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall \varepsilon>0\ \exists X\in\mathbb{R}\ \forall x\in\mathbb{R}:\quad X\le x \implies |\theta(x)-x| \le \varepsilon x$

Rendered from gloss/16c11d4be1b0….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/Statement.lean. Origin: compiler-derived.

Depends on (1), each in words

Depends on, each in words where someone has written them:

erdos-1094--h3--h3--h1--h1--h1: $\psi(x) = x + o(x)$, i.e. $\forall \varepsilon>0\ \exists X\ \forall x\ge X,\ |\psi(x)-x|\le\varepsilon x$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000759.json: it records an attempt, not a proof (see Attempts below).

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/Witness.lean, sha256 1fb566f20881.

import Mathlib
import Nodes.«erdos-1094--h3--h3--h1--h1».Context
open scoped Nat

/-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance
satisfying this statement's hypotheses; until then the node is blocked. -/

theorem witness : ∃ (ε : ℝ), (0 : ℝ) < ε := ⟨1, one_pos⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Attempts (2)

2 recorded. Routes refuted: none. Failure classes: missing-library 1.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1018-e; merged in 793e398a971e under attestations/000759.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20261018T192634Z-t1018-e-partial.lean, extracted by the gate at 32961c7678e9 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

h_psi hole ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x hole
Leaves ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with h_psi : ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x.
Uses library Chebyshev.psi.
Left open as a hole; its statement is erdos-1094--h3--h3--h1--h1--h1 (open).
Lean, line 16
```
  have h_psi : ∀ ε : ℝ, 0 < ε → ∃ X : ℝ, ∀ x : ℝ, X ≤ x → |Chebyshev.psi x - x| ≤ ε * x := sorry
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 16 at 6ba7fea98468 ↗
s2 obtain ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε / (2 : ℝ) * x
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with X₁ : ℝ, hX₁ : ∀ (x : ℝ), X₁ ≤ x → |Chebyshev.psi x - x| ≤ ε / (2 : ℝ) * x.
Lean, line 18
```
  obtain ⟨X₁, hX₁⟩ := h_psi (ε / 2) (by positivity)
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 18 at 6ba7fea98468 ↗
hlog have (fun (x : ℝ) => Real.log x) =o[Filter.atTop] fun (x : ℝ) => x ^ (1 / 2 : ℝ)
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with hlog : (fun (x : ℝ) => Real.log x) =o[Filter.atTop] fun (x : ℝ) => x ^ (1 / 2 : ℝ).
Uses library Real.log, Filter.atTop, isLittleO_log_rpow_atTop.
Lean, lines 19–20
```
  have hlog : (fun x : ℝ => Real.log x) =o[Filter.atTop] (fun x : ℝ => x ^ (1 / 2 : ℝ)) :=
    isLittleO_log_rpow_atTop (by norm_num)
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, lines 19–20 at 6ba7fea98468 ↗
hmul have (fun (x : ℝ) => √x * Real.log x) =o[Filter.atTop] fun (x : ℝ) => √x * x ^ (1 / 2 : ℝ)
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with hmul : (fun (x : ℝ) => √x * Real.log x) =o[Filter.atTop] fun (x : ℝ) => √x * x ^ (1 / 2 : ℝ).
Uses library Real.sqrt, Real.log, Filter.atTop, Asymptotics.isBigO_refl.
Lean, lines 21–23
```
  have hmul : (fun x : ℝ => Real.sqrt x * Real.log x) =o[Filter.atTop]
      (fun x : ℝ => Real.sqrt x * x ^ (1 / 2 : ℝ)) :=
    (Asymptotics.isBigO_refl (fun x : ℝ => Real.sqrt x) _).mul_isLittleO hlog
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, lines 21–23 at 6ba7fea98468 ↗
heq have (fun (x : ℝ) => √x * x ^ (1 / 2 : ℝ)) =ᶠ[Filter.atTop] fun (x : ℝ) => x
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with heq : (fun (x : ℝ) => √x * x ^ (1 / 2 : ℝ)) =ᶠ[Filter.atTop] fun (x : ℝ) => x.
Uses library Real.sqrt, Filter.atTop, Filter.eventually_ge_atTop, Real.sqrt_eq_rpow, Real.mul_self_sqrt.
Lean, lines 24–26
```
  have heq : (fun x : ℝ => Real.sqrt x * x ^ (1 / 2 : ℝ)) =ᶠ[Filter.atTop] (fun x : ℝ => x) := by
    filter_upwards [Filter.eventually_ge_atTop (0 : ℝ)] with x hx
    rw [← Real.sqrt_eq_rpow, Real.mul_self_sqrt hx]
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, lines 24–26 at 6ba7fea98468 ↗
hmul' have (fun (x : ℝ) => √x * Real.log x) =o[Filter.atTop] fun (x : ℝ) => x
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with hmul' : (fun (x : ℝ) => √x * Real.log x) =o[Filter.atTop] fun (x : ℝ) => x.
Lean, line 27
```
  have hmul' := hmul.trans_eventuallyEq heq
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 27 at 6ba7fea98468 ↗
hev have ∀ᶠ (x : ℝ) in Filter.atTop, ‖√x * Real.log x‖ ≤ ε / (4 : ℝ) * ‖x‖
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with hev : ∀ᶠ (x : ℝ) in Filter.atTop, ‖√x * Real.log x‖ ≤ ε / (4 : ℝ) * ‖x‖.
Lean, line 28
```
  have hev := hmul'.def (show (0 : ℝ) < ε / 4 by positivity)
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 28 at 6ba7fea98468 ↗
s8 obtain ∃ (a : ℝ), ∀ (b : ℝ), a ≤ b → ‖√b * Real.log b‖ ≤ ε / (4 : ℝ) * ‖b‖
Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x, with X₂ : ℝ, hX₂ : ∀ (b : ℝ), X₂ ≤ b → ‖√b * Real.log b‖ ≤ ε / (4 : ℝ) * ‖b‖.
Uses library Filter.eventually_atTop.
Lean, line 29
```
  obtain ⟨X₂, hX₂⟩ := Filter.eventually_atTop.mp hev
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 29 at 6ba7fea98468 ↗
hx1 have X₁ ≤ x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hx1 : X₁ ≤ x.
Uses library le_trans, le_max_left.
Lean, line 31
```
  have hx1 : X₁ ≤ x := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hx
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 31 at 6ba7fea98468 ↗
hx2 have X₂ ≤ x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hx2 : X₂ ≤ x.
Uses library le_trans, le_max_right, le_max_left.
Lean, line 32
```
  have hx2 : X₂ ≤ x := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hx
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 32 at 6ba7fea98468 ↗
hx3 have (1 : ℝ) ≤ x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hx3 : (1 : ℝ) ≤ x.
Uses library le_trans, le_max_right.
Lean, line 33
```
  have hx3 : (1 : ℝ) ≤ x := le_trans (le_max_right _ _) hx
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 33 at 6ba7fea98468 ↗
hA have |Chebyshev.psi x - x| ≤ ε / (2 : ℝ) * x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hA : |Chebyshev.psi x - x| ≤ ε / (2 : ℝ) * x.
Lean, line 34
```
  have hA := hX₁ x hx1
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 34 at 6ba7fea98468 ↗
hB have ‖√x * Real.log x‖ ≤ ε / (4 : ℝ) * ‖x‖
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hB : ‖√x * Real.log x‖ ≤ ε / (4 : ℝ) * ‖x‖.
Lean, line 35
```
  have hB := hX₂ x hx2
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 35 at 6ba7fea98468 ↗
hC have |Chebyshev.psi x - Chebyshev.theta x| ≤ (2 : ℝ) * √x * Real.log x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hC : |Chebyshev.psi x - Chebyshev.theta x| ≤ (2 : ℝ) * √x * Real.log x.
Uses library Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log.
Lean, line 36
```
  have hC := Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log hx3
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 36 at 6ba7fea98468 ↗
hx0 have (0 : ℝ) ≤ x routine: linarith
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hx0 : (0 : ℝ) ≤ x.
Lean, line 37
```
  have hx0 : (0 : ℝ) ≤ x := by linarith
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 37 at 6ba7fea98468 ↗
hlog0 have (0 : ℝ) ≤ Real.log x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hlog0 : (0 : ℝ) ≤ Real.log x.
Uses library Real.log, Real.log_nonneg.
Lean, line 38
```
  have hlog0 : 0 ≤ Real.log x := Real.log_nonneg hx3
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 38 at 6ba7fea98468 ↗
hs0 have (0 : ℝ) ≤ √x
Leaves |Chebyshev.theta x - x| ≤ ε * x, with hs0 : (0 : ℝ) ≤ √x.
Uses library Real.sqrt, Real.sqrt_nonneg.
Lean, line 39
```
  have hs0 : 0 ≤ Real.sqrt x := Real.sqrt_nonneg x
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 39 at 6ba7fea98468 ↗
s18 calc |Chebyshev.theta x - x| = |Chebyshev.theta x - Chebyshev.psi x + (Chebyshev.psi x - x)|
Closes the goal.
Uses library Chebyshev.theta, Chebyshev.psi.
Lean, line 42
```
  calc |Chebyshev.theta x - x| = |(Chebyshev.theta x - Chebyshev.psi x) + (Chebyshev.psi x - x)| := by ring_nf
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 42 at 6ba7fea98468 ↗
s19 calc |Chebyshev.theta x - Chebyshev.psi x + (Chebyshev.psi x - x)| ≤ |Chebyshev.theta x - Chebyshev.psi x| + |Chebyshev.psi x - x|
Closes the goal.
Uses library Chebyshev.theta, Chebyshev.psi, abs_add_le.
Lean, line 43
```
    _ ≤ |Chebyshev.theta x - Chebyshev.psi x| + |Chebyshev.psi x - x| := abs_add_le _ _
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 43 at 6ba7fea98468 ↗
s20 calc
Closes the goal.
Uses library Chebyshev.psi, Chebyshev.theta, abs_sub_comm.
Lean, line 44
```
    _ = |Chebyshev.psi x - Chebyshev.theta x| + |Chebyshev.psi x - x| := by rw [abs_sub_comm]
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 44 at 6ba7fea98468 ↗
s21 calc |Chebyshev.psi x - Chebyshev.theta x| + |Chebyshev.psi x - x| ≤ (2 : ℝ) * √x * Real.log x + ε / (2 : ℝ) * x
Closes the goal.
Uses library Real.sqrt, Real.log, add_le_add.
Lean, line 45
```
    _ ≤ 2 * Real.sqrt x * Real.log x + ε / 2 * x := add_le_add hC hA
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 45 at 6ba7fea98468 ↗
s22 calc routine: nlinarith
Closes the goal.
Lean, line 46
```
    _ ≤ ε * x := by nlinarith
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean, line 46 at 6ba7fea98468 ↗

import Mathlib
import Nodes.«erdos-1094--h3--h3--h1--h1».Context

open scoped Nat

/-! Hole `h_pnt` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_1094__h3__h3__h1__h1 : ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
  -- approach: the prime number theorem for ψ (Hadamard, de la Vallée Poussin 1896) transferred to θ by Mathlib's bound |ψ x - θ x| ≤ 2√x log x
  -- licence: CC-BY-4.0
  -- label: Prime number theorem for psi
  -- claim: $\psi(x) = x + o(x)$, i.e. $\forall \varepsilon>0\ \exists X\ \forall x\ge X,\ |\psi(x)-x|\le\varepsilon x$
  -- The prime number theorem in Chebyshev's ψ form: Hadamard (1896), de la Vallée Poussin (1896);
  -- e.g. Ingham, The Distribution of Prime Numbers (1932), Thm 3 / Apostol, Intro. to Analytic NT, Thm 4.4 + §13.
  have h_psi : ∀ ε : ℝ, 0 < ε → ∃ X : ℝ, ∀ x : ℝ, X ≤ x → |Chebyshev.psi x - x| ≤ ε * x := sorry
  intro ε hε
  obtain ⟨X₁, hX₁⟩ := h_psi (ε / 2) (by positivity)
  have hlog : (fun x : ℝ => Real.log x) =o[Filter.atTop] (fun x : ℝ => x ^ (1 / 2 : ℝ)) :=
    isLittleO_log_rpow_atTop (by norm_num)
  have hmul : (fun x : ℝ => Real.sqrt x * Real.log x) =o[Filter.atTop]
      (fun x : ℝ => Real.sqrt x * x ^ (1 / 2 : ℝ)) :=
    (Asymptotics.isBigO_refl (fun x : ℝ => Real.sqrt x) _).mul_isLittleO hlog
  have heq : (fun x : ℝ => Real.sqrt x * x ^ (1 / 2 : ℝ)) =ᶠ[Filter.atTop] (fun x : ℝ => x) := by
    filter_upwards [Filter.eventually_ge_atTop (0 : ℝ)] with x hx
    rw [← Real.sqrt_eq_rpow, Real.mul_self_sqrt hx]
  have hmul' := hmul.trans_eventuallyEq heq
  have hev := hmul'.def (show (0 : ℝ) < ε / 4 by positivity)
  obtain ⟨X₂, hX₂⟩ := Filter.eventually_atTop.mp hev
  refine ⟨max (max X₁ X₂) 1, fun x hx => ?_⟩
  have hx1 : X₁ ≤ x := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hx
  have hx2 : X₂ ≤ x := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hx
  have hx3 : (1 : ℝ) ≤ x := le_trans (le_max_right _ _) hx
  have hA := hX₁ x hx1
  have hB := hX₂ x hx2
  have hC := Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log hx3
  have hx0 : (0 : ℝ) ≤ x := by linarith
  have hlog0 : 0 ≤ Real.log x := Real.log_nonneg hx3
  have hs0 : 0 ≤ Real.sqrt x := Real.sqrt_nonneg x
  rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (mul_nonneg hs0 hlog0),
    abs_of_nonneg hx0] at hB
  calc |Chebyshev.theta x - x| = |(Chebyshev.theta x - Chebyshev.psi x) + (Chebyshev.psi x - x)| := by ring_nf
    _ ≤ |Chebyshev.theta x - Chebyshev.psi x| + |Chebyshev.psi x - x| := abs_add_le _ _
    _ = |Chebyshev.psi x - Chebyshev.theta x| + |Chebyshev.psi x - x| := by rw [abs_sub_comm]
    _ ≤ 2 * Real.sqrt x * Real.log x + ε / 2 * x := add_le_add hC hA
    _ ≤ ε * x := by nlinarith

How to read this page

No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).

How to read a statement’s page →