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

Chebyshev sum of log p over (k/2, 11k/20) is at least k/100

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

open

Hole h_cheb of erdos-1094--h3--h3 (split by 20261015T132200Z-t1015b-g-partial.lean).

$\displaystyle \exists K_3\in\mathbb{N}\ \forall k\in\mathbb{N}:\quad K_3<k \implies \frac{k}{100} \le \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p$

For all large $k$, the sum of $\log p$ over the primes $p$ with $k<2p$ and $20p<11k$ is at least $k/100$. The sum is over Finset.range k filtered by Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k (so $p<k$, which the second condition already forces), the logarithm is the real Real.log of the cast of $p$, and $k/100$ is real division of the cast of $k$.

unverified · history

Lean

theorem erdos_1094__h3__h3__h1 : ∃ (K₃ : ℕ),
  ∀ (k : ℕ),
    K₃ < k →
      (↑k : ℝ) / (100 : ℝ) ≤
        ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) := 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 20261015T145500Z-t1015c-a03-partial.lean (merged in e3fa48b9b09d, attestation 000554).

h_pnt → erdos-1094--h3--h3--h1--h1 (open)
$\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$

Read the partial proof (Lean)

theorem erdos_1094__h3__h3__h1 : ∃ (K₃ : ℕ),
  ∀ (k : ℕ),
    K₃ < k →
      (↑k : ℝ) / (100 : ℝ) ≤
        ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) := by
  have h_pnt : ∀ ε : ℝ, 0 < ε → ∃ X : ℝ, ∀ x : ℝ, X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
    sorry
  obtain ⟨X, hX⟩ := h_pnt (1 / 100) (by norm_num)
  refine ⟨2 * ⌈X⌉₊ + 2, fun k hk => ?_⟩
  set S := (Finset.range k).filter (fun p => p.Prime ∧ k < 2 * p ∧ 20 * p < 11 * k) with hS
  have hk1 : 1 ≤ k := by omega
  set A : ℝ := ((11 * k - 1 : ℕ) : ℝ) / 20 with hA
  set B : ℝ := (k : ℝ) / 2 with hB
  have hfA : ⌊A⌋₊ = (11 * k - 1) / 20 := by
    rw [hA]; exact_mod_cast Nat.floor_div_eq_div (11 * k - 1) 20
  have hfB : ⌊B⌋₊ = k / 2 := by
    rw [hB]; exact_mod_cast Nat.floor_div_eq_div k 2
  set TA := (Finset.Ioc 0 ⌊A⌋₊).filter Nat.Prime with hTA
  set TB := (Finset.Ioc 0 ⌊B⌋₊).filter Nat.Prime with hTB
  have hthA : Chebyshev.theta A = ∑ p ∈ TA, Real.log p := rfl
  have hthB : Chebyshev.theta B = ∑ p ∈ TB, Real.log p := rfl
  have hdisj : Disjoint TB S := by
    rw [Finset.disjoint_left]
    intro p hp hpS
    rw [hTB, Finset.mem_filter, Finset.mem_Ioc, hfB] at hp
    rw [hS, Finset.mem_filter] at hpS
    omega
  have hsub : TA ⊆ TB ∪ S := by
    intro p hp
    rw [hTA, Finset.mem_filter, Finset.mem_Ioc, hfA] at hp
    rw [Finset.mem_union, hTB, hS, Finset.mem_filter, Finset.mem_filter, Finset.mem_Ioc,
      Finset.mem_range, hfB]
    by_cases h : p ≤ k / 2
    · left; exact ⟨⟨hp.1.1, h⟩, hp.2⟩
    · right
      refine ⟨by omega, hp.2, by omega, by omega⟩
  have hle : Chebyshev.theta A ≤ Chebyshev.theta B + ∑ p ∈ S, Real.log p := by
    rw [hthA, hthB, ← Finset.sum_union hdisj]
    apply Finset.sum_le_sum_of_subset_of_nonneg hsub
    intro p _ _
    exact Real.log_natCast_nonneg p
  have hXc : X ≤ (⌈X⌉₊ : ℝ) := Nat.le_ceil X
  have hkR : (2 * (⌈X⌉₊ : ℝ) + 2) < k := by exact_mod_cast hk
  have hAX : X ≤ A := by
    have : ((11 * k - 1 : ℕ) : ℝ) = 11 * (k : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega)]; push_cast; ring
    rw [hA, this]
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    linarith
  have hBX : X ≤ B := by
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    rw [hB]; linarith
  have h1 := hX A hAX
  have h2 := hX B hBX
  rw [abs_le] at h1 h2
  have hAeq : A = (11 * (k : ℝ) - 1) / 20 := by
    rw [hA, Nat.cast_sub (by omega)]; push_cast; ring
  have hkpos : (1 : ℝ) ≤ k := by exact_mod_cast hk1
  have hk2 : (2 : ℝ) < k := by
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    linarith
  rw [hAeq] at h1 hle
  rw [hB] at h2 hle
  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/attempts/20261015T145500Z-t1015c-a03-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

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».Context

open scoped Nat

/-! Hole `h_cheb` 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 : ∃ (K₃ : ℕ),
  ∀ (k : ℕ),
    K₃ < k →
      (↑k : ℝ) / (100 : ℝ) ≤
        ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) := 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 \exists K_3\in\mathbb{N}\ \forall k\in\mathbb{N}:\quad K_3<k \implies \frac{k}{100} \le \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p$

Rendered from gloss/953fcd1dba68….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/Statement.lean. Origin: skeleton-hole.

Depends on (1), each in words

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

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

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000554.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/Witness.lean, sha256 1aa8a1c1b9f3.

import Mathlib

open scoped Nat

theorem witness : True := trivial

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 (1)

1 recorded. Routes refuted: none. Failure classes: none.

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 t1015c-a03; merged in e3fa48b9b09d under attestations/000554.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/attempts/20261015T145500Z-t1015c-a03-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 20261015T145500Z-t1015c-a03-partial.lean, extracted by the gate at 067497e74a8b 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_pnt hole ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x hole
Leaves ∃ (K₃ : ℕ), ∀ (k : ℕ), K₃ < k → (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ), with h_pnt : ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ ε * x.
Uses library Chebyshev.theta.
Left open as a hole; its statement is erdos-1094--h3--h3--h1--h1 (open).
Lean, lines 14–15
```
  have h_pnt : ∀ ε : ℝ, 0 < ε → ∃ X : ℝ, ∀ x : ℝ, X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 14–15 at 6ba7fea98468 ↗
s2 obtain ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ (1 / 100 : ℝ) * x
Leaves ∃ (K₃ : ℕ), ∀ (k : ℕ), K₃ < k → (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ), with X : ℝ, hX : ∀ (x : ℝ), X ≤ x → |Chebyshev.theta x - x| ≤ (1 / 100 : ℝ) * x.
Lean, line 16
```
  obtain ⟨X, hX⟩ := h_pnt (1 / 100) (by norm_num)
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 16 at 6ba7fea98468 ↗
hk1 have (1 : ℕ) ≤ k routine: omega
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hk1 : (1 : ℕ) ≤ k.
Lean, line 19
```
  have hk1 : 1 ≤ k := by omega
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 19 at 6ba7fea98468 ↗
hfA have ⌊A⌋₊ = ((11 : ℕ) * k - (1 : ℕ)) / (20 : ℕ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hfA : ⌊A⌋₊ = ((11 : ℕ) * k - (1 : ℕ)) / (20 : ℕ).
Uses library Nat.floor_div_eq_div.
Lean, lines 22–23
```
  have hfA : ⌊A⌋₊ = (11 * k - 1) / 20 := by
    rw [hA]; exact_mod_cast Nat.floor_div_eq_div (11 * k - 1) 20
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 22–23 at 6ba7fea98468 ↗
hfB have ⌊B⌋₊ = k / (2 : ℕ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hfB : ⌊B⌋₊ = k / (2 : ℕ).
Uses library Nat.floor_div_eq_div.
Lean, lines 24–25
```
  have hfB : ⌊B⌋₊ = k / 2 := by
    rw [hB]; exact_mod_cast Nat.floor_div_eq_div k 2
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 24–25 at 6ba7fea98468 ↗
hthA have Chebyshev.theta A = ∑ p ∈ TA, Real.log (↑p : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hthA : Chebyshev.theta A = ∑ p ∈ TA, Real.log (↑p : ℝ).
Uses library Chebyshev.theta, Real.log, rfl.
Lean, line 28
```
  have hthA : Chebyshev.theta A = ∑ p ∈ TA, Real.log p := rfl
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 28 at 6ba7fea98468 ↗
hthB have Chebyshev.theta B = ∑ p ∈ TB, Real.log (↑p : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hthB : Chebyshev.theta B = ∑ p ∈ TB, Real.log (↑p : ℝ).
Uses library Chebyshev.theta, Real.log, rfl.
Lean, line 29
```
  have hthB : Chebyshev.theta B = ∑ p ∈ TB, Real.log p := rfl
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 29 at 6ba7fea98468 ↗
hdisj have Disjoint TB S
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hdisj : Disjoint TB S.
Uses library Disjoint, Finset.disjoint_left, Finset.mem_filter, Finset.mem_Ioc.
Lean, lines 30–35
```
  have hdisj : Disjoint TB S := by
    rw [Finset.disjoint_left]
    intro p hp hpS
    rw [hTB, Finset.mem_filter, Finset.mem_Ioc, hfB] at hp
    rw [hS, Finset.mem_filter] at hpS
    omega
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 30–35 at 6ba7fea98468 ↗
hsub have TA ⊆ TB ∪ S
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hsub : TA ⊆ TB ∪ S.
Uses library Finset.mem_filter, Finset.mem_Ioc, Finset.mem_union, Finset.mem_range.
Lean, lines 36–44
```
  have hsub : TA ⊆ TB ∪ S := by
    intro p hp
    rw [hTA, Finset.mem_filter, Finset.mem_Ioc, hfA] at hp
    rw [Finset.mem_union, hTB, hS, Finset.mem_filter, Finset.mem_filter, Finset.mem_Ioc,
      Finset.mem_range, hfB]
    by_cases h : p ≤ k / 2
    · left; exact ⟨⟨hp.1.1, h⟩, hp.2⟩
    · right
      refine ⟨by omega, hp.2, by omega, by omega⟩
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 36–44 at 6ba7fea98468 ↗
1. hsub.s1 case
  Leaves ((0 : ℕ) < p ∧ p ≤ k / (2 : ℕ)) ∧ Nat.Prime p ∨ p < k ∧ Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, with h : p ≤ k / (2 : ℕ).
  Uses library And.intro.
  Lean, line 42
  · left; exact ⟨⟨hp.1.1, h⟩, hp.2⟩
  targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 42 at 6ba7fea98468 ↗
2. hsub.s2 case
  Leaves ((0 : ℕ) < p ∧ p ≤ k / (2 : ℕ)) ∧ Nat.Prime p ∨ p < k ∧ Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, with h : ¬p ≤ k / (2 : ℕ).
  Uses library And.intro.
  Lean, lines 43–44
  · right refine ⟨by omega, hp.2, by omega, by omega⟩
  targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 43–44 at 6ba7fea98468 ↗
hle have Chebyshev.theta A ≤ Chebyshev.theta B + ∑ p ∈ S, Real.log (↑p : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hle : Chebyshev.theta A ≤ Chebyshev.theta B + ∑ p ∈ S, Real.log (↑p : ℝ).
Uses library Chebyshev.theta, Real.log, Finset.sum_union, Finset.sum_le_sum_of_subset_of_nonneg, Real.log_natCast_nonneg.
Lean, lines 45–49
```
  have hle : Chebyshev.theta A ≤ Chebyshev.theta B + ∑ p ∈ S, Real.log p := by
    rw [hthA, hthB, ← Finset.sum_union hdisj]
    apply Finset.sum_le_sum_of_subset_of_nonneg hsub
    intro p _ _
    exact Real.log_natCast_nonneg p
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 45–49 at 6ba7fea98468 ↗
hXc have X ≤ (↑⌈X⌉₊ : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hXc : X ≤ (↑⌈X⌉₊ : ℝ).
Uses library Nat.le_ceil.
Lean, line 50
```
  have hXc : X ≤ (⌈X⌉₊ : ℝ) := Nat.le_ceil X
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 50 at 6ba7fea98468 ↗
hkR have (2 : ℝ) * (↑⌈X⌉₊ : ℝ) + (2 : ℝ) < (↑k : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hkR : (2 : ℝ) * (↑⌈X⌉₊ : ℝ) + (2 : ℝ) < (↑k : ℝ).
Lean, line 51
```
  have hkR : (2 * (⌈X⌉₊ : ℝ) + 2) < k := by exact_mod_cast hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 51 at 6ba7fea98468 ↗
hAX have X ≤ A
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hAX : X ≤ A.
Lean, lines 52–57
```
  have hAX : X ≤ A := by
    have : ((11 * k - 1 : ℕ) : ℝ) = 11 * (k : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega)]; push_cast; ring
    rw [hA, this]
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    linarith
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 52–57 at 6ba7fea98468 ↗
1. hAX.s1 have (↑((11 : ℕ) * k - (1 : ℕ)) : ℝ) = (11 : ℝ) * (↑k : ℝ) - (1 : ℝ)
  Leaves X ≤ A, with this : (↑((11 : ℕ) * k - (1 : ℕ)) : ℝ) = (11 : ℝ) * (↑k : ℝ) - (1 : ℝ).
  Uses library Nat.cast_sub.
  Lean, lines 53–54
  have : ((11 * k - 1 : ℕ) : ℝ) = 11 * (k : ℝ) - 1 := by rw [Nat.cast_sub (by omega)]; push_cast; ring
  targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 53–54 at 6ba7fea98468 ↗
2. hAX.s2 have (0 : ℝ) ≤ (↑⌈X⌉₊ : ℝ)
  Leaves X ≤ ((11 : ℝ) * (↑k : ℝ) - (1 : ℝ)) / (20 : ℝ), with this : (0 : ℝ) ≤ (↑⌈X⌉₊ : ℝ).
  Uses library Nat.cast_nonneg.
  Lean, line 56
  have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
  targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 56 at 6ba7fea98468 ↗
hBX have X ≤ B
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hBX : X ≤ B.
Lean, lines 58–60
```
  have hBX : X ≤ B := by
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    rw [hB]; linarith
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 58–60 at 6ba7fea98468 ↗
1. hBX.this have (0 : ℝ) ≤ (↑⌈X⌉₊ : ℝ)
  Leaves X ≤ B, with this : (0 : ℝ) ≤ (↑⌈X⌉₊ : ℝ).
  Uses library Nat.cast_nonneg.
  Lean, line 59
  have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
  targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 59 at 6ba7fea98468 ↗
h1 have |Chebyshev.theta A - A| ≤ (1 / 100 : ℝ) * A
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with h1 : |Chebyshev.theta A - A| ≤ (1 / 100 : ℝ) * A.
Lean, line 61
```
  have h1 := hX A hAX
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 61 at 6ba7fea98468 ↗
h2 have |Chebyshev.theta B - B| ≤ (1 / 100 : ℝ) * B
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with h2 : |Chebyshev.theta B - B| ≤ (1 / 100 : ℝ) * B.
Lean, line 62
```
  have h2 := hX B hBX
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 62 at 6ba7fea98468 ↗
hAeq have A = ((11 : ℝ) * (↑k : ℝ) - (1 : ℝ)) / (20 : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hAeq : A = ((11 : ℝ) * (↑k : ℝ) - (1 : ℝ)) / (20 : ℝ).
Uses library Nat.cast_sub.
Lean, lines 64–65
```
  have hAeq : A = (11 * (k : ℝ) - 1) / 20 := by
    rw [hA, Nat.cast_sub (by omega)]; push_cast; ring
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 64–65 at 6ba7fea98468 ↗
hkpos have (1 : ℝ) ≤ (↑k : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hkpos : (1 : ℝ) ≤ (↑k : ℝ).
Lean, line 66
```
  have hkpos : (1 : ℝ) ≤ k := by exact_mod_cast hk1
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 66 at 6ba7fea98468 ↗
hk2 have (2 : ℝ) < (↑k : ℝ)
Leaves (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ), with hk2 : (2 : ℝ) < (↑k : ℝ).
Lean, lines 67–69
```
  have hk2 : (2 : ℝ) < k := by
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    linarith
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 67–69 at 6ba7fea98468 ↗
1. hk2.this have (0 : ℝ) ≤ (↑⌈X⌉₊ : ℝ)
  Leaves (2 : ℝ) < (↑k : ℝ), with this : (0 : ℝ) ≤ (↑⌈X⌉₊ : ℝ).
  Uses library Nat.cast_nonneg.
  Lean, line 68
  have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
  targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, line 68 at 6ba7fea98468 ↗
close term (↑k : ℝ) / (100 : ℝ) ≤ ∑ p ∈ S, Real.log (↑p : ℝ)
Closes the goal.
Lean, lines 70–72
```
  rw [hAeq] at h1 hle
  rw [hB] at h2 hle
  nlinarith
```
targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean, lines 70–72 at 6ba7fea98468 ↗

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

open scoped Nat

/-! Hole `h_cheb` 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 : ∃ (K₃ : ℕ),
  ∀ (k : ℕ),
    K₃ < k →
      (↑k : ℝ) / (100 : ℝ) ≤
        ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) := by
  have h_pnt : ∀ ε : ℝ, 0 < ε → ∃ X : ℝ, ∀ x : ℝ, X ≤ x → |Chebyshev.theta x - x| ≤ ε * x := by
    sorry
  obtain ⟨X, hX⟩ := h_pnt (1 / 100) (by norm_num)
  refine ⟨2 * ⌈X⌉₊ + 2, fun k hk => ?_⟩
  set S := (Finset.range k).filter (fun p => p.Prime ∧ k < 2 * p ∧ 20 * p < 11 * k) with hS
  have hk1 : 1 ≤ k := by omega
  set A : ℝ := ((11 * k - 1 : ℕ) : ℝ) / 20 with hA
  set B : ℝ := (k : ℝ) / 2 with hB
  have hfA : ⌊A⌋₊ = (11 * k - 1) / 20 := by
    rw [hA]; exact_mod_cast Nat.floor_div_eq_div (11 * k - 1) 20
  have hfB : ⌊B⌋₊ = k / 2 := by
    rw [hB]; exact_mod_cast Nat.floor_div_eq_div k 2
  set TA := (Finset.Ioc 0 ⌊A⌋₊).filter Nat.Prime with hTA
  set TB := (Finset.Ioc 0 ⌊B⌋₊).filter Nat.Prime with hTB
  have hthA : Chebyshev.theta A = ∑ p ∈ TA, Real.log p := rfl
  have hthB : Chebyshev.theta B = ∑ p ∈ TB, Real.log p := rfl
  have hdisj : Disjoint TB S := by
    rw [Finset.disjoint_left]
    intro p hp hpS
    rw [hTB, Finset.mem_filter, Finset.mem_Ioc, hfB] at hp
    rw [hS, Finset.mem_filter] at hpS
    omega
  have hsub : TA ⊆ TB ∪ S := by
    intro p hp
    rw [hTA, Finset.mem_filter, Finset.mem_Ioc, hfA] at hp
    rw [Finset.mem_union, hTB, hS, Finset.mem_filter, Finset.mem_filter, Finset.mem_Ioc,
      Finset.mem_range, hfB]
    by_cases h : p ≤ k / 2
    · left; exact ⟨⟨hp.1.1, h⟩, hp.2⟩
    · right
      refine ⟨by omega, hp.2, by omega, by omega⟩
  have hle : Chebyshev.theta A ≤ Chebyshev.theta B + ∑ p ∈ S, Real.log p := by
    rw [hthA, hthB, ← Finset.sum_union hdisj]
    apply Finset.sum_le_sum_of_subset_of_nonneg hsub
    intro p _ _
    exact Real.log_natCast_nonneg p
  have hXc : X ≤ (⌈X⌉₊ : ℝ) := Nat.le_ceil X
  have hkR : (2 * (⌈X⌉₊ : ℝ) + 2) < k := by exact_mod_cast hk
  have hAX : X ≤ A := by
    have : ((11 * k - 1 : ℕ) : ℝ) = 11 * (k : ℝ) - 1 := by
      rw [Nat.cast_sub (by omega)]; push_cast; ring
    rw [hA, this]
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    linarith
  have hBX : X ≤ B := by
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    rw [hB]; linarith
  have h1 := hX A hAX
  have h2 := hX B hBX
  rw [abs_le] at h1 h2
  have hAeq : A = (11 * (k : ℝ) - 1) / 20 := by
    rw [hA, Nat.cast_sub (by omega)]; push_cast; ring
  have hkpos : (1 : ℝ) ≤ k := by exact_mod_cast hk1
  have hk2 : (2 : ℝ) < k := by
    have : (0 : ℝ) ≤ ⌈X⌉₊ := Nat.cast_nonneg _
    linarith
  rw [hAeq] at h1 hle
  rw [hB] at h2 hle
  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 →