Prime number theorem for psi

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 20261018T200210Z-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.

1. hall have (∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A)) ∧ ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ))

   Leaves ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x, with hall : (∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A)) ∧ ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ)).

   Uses library LSeriesSummable LSeriesSummable f s indicates that the L-series of f converges absolutely at s. , ContinuousOn A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s. , LSeries The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise. , Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , Finset.range range n is the set of natural numbers less than n. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , ArithmeticFunction.vonMangoldt The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

   Lean, lines 12–38

     have hall : (∀ (f : ℕ → ℝ) (A : ℝ), (∀ n, 0 ≤ f n) →
             (∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (f n : ℂ)) s) →
             (∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
               ∀ s : ℂ, 1 < s.re → G s = LSeries (fun n => (f n : ℂ)) s - A / (s - 1)) →
             Filter.Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, f n) / (N : ℝ)) Filter.atTop (nhds A)) ∧ (∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
             ∀ s : ℂ, 1 < s.re → G s =
               LSeries (fun n => ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)) s - 1 / (s - 1)) := by
       refine ⟨?_, ?_⟩
       · -- First lemma.
         -- label: Wiener–Ikehara Tauberian theorem
         -- claim: $f\ge0$, $\sum f(n)n^{-s}$ converges for $\Re s>1$ and $F(s)-A/(s-1)$ extends continuously to $\Re s\ge1$ $\Rightarrow$ $\frac1N\sum_{n<N}f(n)\to A$
         -- Wiener (1932), Ikehara (1931); continuous-boundary form: Korevaar, Bull. AMS 39 (2002), Thm 4.2 / Tauberian Theory (2004) III.4.
         have h_wi : ∀ (f : ℕ → ℝ) (A : ℝ), (∀ n, 0 ≤ f n) →
             (∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (f n : ℂ)) s) →
             (∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
               ∀ s : ℂ, 1 < s.re → G s = LSeries (fun n => (f n : ℂ)) s - A / (s - 1)) →
             Filter.Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, f n) / (N : ℝ)) Filter.atTop (nhds A) := sorry
         exact h_wi
       · -- Second lemma.
         -- label: -ζ'/ζ minus the pole extends to Re s ≥ 1
         -- claim: $\sum_n \Lambda(n) n^{-s} - \frac{1}{s-1}$ extends continuously to $\Re s\ge 1$
         -- From ζ's simple pole of residue 1 at s = 1 and ζ(s) ≠ 0 on Re s ≥ 1 (Mathlib: riemannZeta_residue_one,
         -- riemannZeta_ne_zero_of_one_le_re, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div).
         have h_ext : ∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
             ∀ s : ℂ, 1 < s.re → G s =
               LSeries (fun n => ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)) s - 1 / (s - 1) := sorry
         exact h_ext

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 12–38 at f0dfc93f9827 ↗

   1. hall.s1 case

      Leaves ∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A).

      Lean, lines 20–29

          · -- First lemma.
            -- label: Wiener–Ikehara Tauberian theorem
            -- claim: $f\ge0$, $\sum f(n)n^{-s}$ converges for $\Re s>1$ and $F(s)-A/(s-1)$ extends continuously to $\Re s\ge1$ $\Rightarrow$ $\frac1N\sum_{n<N}f(n)\to A$
            -- Wiener (1932), Ikehara (1931); continuous-boundary form: Korevaar, Bull. AMS 39 (2002), Thm 4.2 / Tauberian Theory (2004) III.4.
            have h_wi : ∀ (f : ℕ → ℝ) (A : ℝ), (∀ n, 0 ≤ f n) →
                (∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (f n : ℂ)) s) →
                (∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
                  ∀ s : ℂ, 1 < s.re → G s = LSeries (fun n => (f n : ℂ)) s - A / (s - 1)) →
                Filter.Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, f n) / (N : ℝ)) Filter.atTop (nhds A) := sorry
            exact h_wi

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 20–29 at f0dfc93f9827 ↗

      1. hall.s1.h_wi hole ∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A) hole

         Leaves ∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A), with h_wi : ∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A).

         Uses library LSeriesSummable LSeriesSummable f s indicates that the L-series of f converges absolutely at s. , ContinuousOn A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s. , LSeries The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise. , Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , Finset.range range n is the set of natural numbers less than n. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. .

         Left open as a hole; its statement is erdos-1094--h3--h3--h1--h1--h1--h1 (open).

         Lean, lines 24–28

               have h_wi : ∀ (f : ℕ → ℝ) (A : ℝ), (∀ n, 0 ≤ f n) →
                   (∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (f n : ℂ)) s) →
                   (∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
                     ∀ s : ℂ, 1 < s.re → G s = LSeries (fun n => (f n : ℂ)) s - A / (s - 1)) →
                   Filter.Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N, f n) / (N : ℝ)) Filter.atTop (nhds A) := sorry

         targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 24–28 at f0dfc93f9827 ↗

   2. hall.s2 case

      Leaves ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ)).

      Lean, lines 30–38

          · -- Second lemma.
            -- label: -ζ'/ζ minus the pole extends to Re s ≥ 1
            -- claim: $\sum_n \Lambda(n) n^{-s} - \frac{1}{s-1}$ extends continuously to $\Re s\ge 1$
            -- From ζ's simple pole of residue 1 at s = 1 and ζ(s) ≠ 0 on Re s ≥ 1 (Mathlib: riemannZeta_residue_one,
            -- riemannZeta_ne_zero_of_one_le_re, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div).
            have h_ext : ∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
                ∀ s : ℂ, 1 < s.re → G s =
                  LSeries (fun n => ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)) s - 1 / (s - 1) := sorry
            exact h_ext

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 30–38 at f0dfc93f9827 ↗

      1. hall.s2.h_ext hole ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ)) hole

         Leaves ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ)), with h_ext : ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ)).

         Uses library ContinuousOn A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s. , LSeries The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise. , ArithmeticFunction.vonMangoldt The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. .

         Left open as a hole; its statement is erdos-1094--h3--h3--h1--h1--h1--h2 (open).

         Lean, lines 35–37

               have h_ext : ∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
                   ∀ s : ℂ, 1 < s.re → G s =
                     LSeries (fun n => ((ArithmeticFunction.vonMangoldt n : ℝ) : ℂ)) s - 1 / (s - 1) := sorry

         targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 35–37 at f0dfc93f9827 ↗

2. s2 obtain (∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A)) ∧ ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ))

   Leaves ∀ (ε : ℝ), (0 : ℝ) < ε → ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x, with h_wi : ∀ (f : ℕ → ℝ) (A : ℝ), (∀ (n : ℕ), (0 : ℝ) ≤ f n) → (∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) → (∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) → Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A), h_ext : ∃ (G : ℂ → ℂ), ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧ ∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑((ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) : ℂ)) s - (1 : ℂ) / (s - (1 : ℂ)).

   Lean, line 39

     obtain ⟨h_wi, h_ext⟩ := hall

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 39 at f0dfc93f9827 ↗

3. hlim have Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑N : ℝ)) Filter.atTop (nhds (1 : ℝ))

   Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x, with hlim : Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑N : ℝ)) Filter.atTop (nhds (1 : ℝ)).

   Uses library ArithmeticFunction.vonMangoldt The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. , ArithmeticFunction.vonMangoldt_nonneg, ArithmeticFunction.LSeriesSummable_vonMangoldt The L-series of the von Mangoldt function Λ converges at s when re s > 1. .

   Lean, lines 41–43

     have hlim := h_wi (fun n => ArithmeticFunction.vonMangoldt n) 1
       (fun n => ArithmeticFunction.vonMangoldt_nonneg)
       (fun s hs => ArithmeticFunction.LSeriesSummable_vonMangoldt hs) h_ext

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 41–43 at f0dfc93f9827 ↗

4. hev have ∃ (N : ℕ), ∀ n ≥ N, dist ((∑ n ∈ Finset.range n, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑n : ℝ)) (1 : ℝ) < ε / (2 : ℝ)

   Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x, with hev : ∃ (N : ℕ), ∀ n ≥ N, dist ((∑ n ∈ Finset.range n, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑n : ℝ)) (1 : ℝ) < ε / (2 : ℝ).

   Uses library Metric.tendsto_atTop.

   Lean, line 44

     have hev := (Metric.tendsto_atTop.mp hlim) (ε / 2) (by positivity)

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 44 at f0dfc93f9827 ↗

5. s5 obtain ∃ (N : ℕ), ∀ n ≥ N, dist ((∑ n ∈ Finset.range n, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑n : ℝ)) (1 : ℝ) < ε / (2 : ℝ)

   Leaves ∃ (X : ℝ), ∀ (x : ℝ), X ≤ x → |Chebyshev.psi x - x| ≤ ε * x, with N₀ : ℕ, hN₀ : ∀ n ≥ N₀, dist ((∑ n ∈ Finset.range n, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑n : ℝ)) (1 : ℝ) < ε / (2 : ℝ).

   Lean, line 45

     obtain ⟨N₀, hN₀⟩ := hev

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 45 at f0dfc93f9827 ↗

6. hx0 have (0 : ℝ) ≤ x

   Leaves |Chebyshev.psi x - x| ≤ ε * x, with hx0 : (0 : ℝ) ≤ x.

   Lean, lines 47–48

     have hx0 : 0 ≤ x := by have : (0:ℝ) ≤ N₀ := Nat.cast_nonneg _; have : 0 < 4 / ε := by positivity
                            linarith

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 47–48 at f0dfc93f9827 ↗

   1. hx0.s1 have (0 : ℝ) ≤ (↑N₀ : ℝ)

      Leaves (0 : ℝ) ≤ x, with this : (0 : ℝ) ≤ (↑N₀ : ℝ).

      Uses library Nat.cast_nonneg Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use. .

      Lean, line 47

        have hx0 : 0 ≤ x := by have : (0:ℝ) ≤ N₀ := Nat.cast_nonneg _; have : 0 < 4 / ε := by positivity

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 47 at f0dfc93f9827 ↗

   2. hx0.s2 have (0 : ℝ) < (4 : ℝ) / ε routine: positivity

      Leaves (0 : ℝ) ≤ x, with this : (0 : ℝ) < (4 : ℝ) / ε.

      Lean, line 47

        have hx0 : 0 ≤ x := by have : (0:ℝ) ≤ N₀ := Nat.cast_nonneg _; have : 0 < 4 / ε := by positivity

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 47 at f0dfc93f9827 ↗

7. hmx have (↑m : ℝ) ≤ x

   Leaves |Chebyshev.psi x - x| ≤ ε * x, with hmx : (↑m : ℝ) ≤ x.

   Uses library Nat.floor_le.

   Lean, line 50

     have hmx : (m : ℝ) ≤ x := Nat.floor_le hx0

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 50 at f0dfc93f9827 ↗

8. hxm have x < (↑m : ℝ) + (1 : ℝ)

   Leaves |Chebyshev.psi x - x| ≤ ε * x, with hxm : x < (↑m : ℝ) + (1 : ℝ).

   Uses library Nat.lt_floor_add_one.

   Lean, line 51

     have hxm : x < (m : ℝ) + 1 := Nat.lt_floor_add_one x

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 51 at f0dfc93f9827 ↗

9. hpsi have Chebyshev.psi x = ∑ n ∈ Finset.range (m + (1 : ℕ)), (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n

   Leaves |Chebyshev.psi x - x| ≤ ε * x, with hpsi : Chebyshev.psi x = ∑ n ∈ Finset.range (m + (1 : ℕ)), (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n.

   Uses library Chebyshev.psi The sum of ArithmeticFunction.vonMangoldt over integers n ≤ x. , Finset.range range n is the set of natural numbers less than n. , ArithmeticFunction.vonMangoldt The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. , Finset.Ioc The finset $(a, b]$ of elements x such that a < x and x ≤ b. , Finset.range_eq_Ico, Finset.sum_eq_sum_Ico_succ_bot.

   Lean, lines 52–57

     have hpsi : Chebyshev.psi x = ∑ n ∈ Finset.range (m + 1), ArithmeticFunction.vonMangoldt n := by
       show ∑ n ∈ Finset.Ioc 0 m, ArithmeticFunction.vonMangoldt n = _
       rw [Finset.range_eq_Ico, Finset.sum_eq_sum_Ico_succ_bot (by omega)]
       have hI : Finset.Ico (0 + 1) (m + 1) = Finset.Ioc 0 m := by
         ext n; simp only [Finset.mem_Ico, Finset.mem_Ioc]; omega
       rw [hI]; simp

   targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 52–57 at f0dfc93f9827 ↗

   1. hpsi.hI have Finset.Ico ((0 : ℕ) + (1 : ℕ)) (m + (1 : ℕ)) = Finset.Ioc (0 : ℕ) m

      Leaves ∑ n ∈ Finset.Ioc (0 : ℕ) m, (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n = (ArithmeticFunction.vonMangoldt : ℕ → ℝ) (0 : ℕ) + ∑ k ∈ Finset.Ico ((0 : ℕ) + (1 : ℕ)) (m + (1 : ℕ)), (ArithmeticFunction.vonMangoldt : ℕ → ℝ) k, with hI : Finset.Ico ((0 : ℕ) + (1 : ℕ)) (m + (1 : ℕ)) = Finset.Ioc (0 : ℕ) m.

      Uses library Finset.Ico The finset $[a, b)$ of elements x such that a ≤ x and x < b. , Finset.Ioc The finset $(a, b]$ of elements x such that a < x and x ≤ b. , Finset.mem_Ico, Finset.mem_Ioc.

      Lean, lines 55–56

          have hI : Finset.Ico (0 + 1) (m + 1) = Finset.Ioc 0 m := by
            ext n; simp only [Finset.mem_Ico, Finset.mem_Ioc]; omega

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 55–56 at f0dfc93f9827 ↗

10. hM have dist ((∑ n ∈ Finset.range (m + (1 : ℕ)), (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑(m + (1 : ℕ)) : ℝ)) (1 : ℝ) < ε / (2 : ℝ)

    Leaves |Chebyshev.psi x - x| ≤ ε * x, with hM : dist ((∑ n ∈ Finset.range (m + (1 : ℕ)), (ArithmeticFunction.vonMangoldt : ℕ → ℝ) n) / (↑(m + (1 : ℕ)) : ℝ)) (1 : ℝ) < ε / (2 : ℝ).

    Lean, lines 58–61

      have hM := hN₀ (m + 1) (by
        have : (N₀ : ℝ) < (m : ℝ) + 1 := by have : 0 < 4 / ε := by positivity
                                            linarith
        exact_mod_cast this.le)

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 58–61 at f0dfc93f9827 ↗

    1. hM.this have (↑N₀ : ℝ) < (↑m : ℝ) + (1 : ℝ)

       Leaves m + (1 : ℕ) ≥ N₀, with this : (↑N₀ : ℝ) < (↑m : ℝ) + (1 : ℝ).

       Lean, lines 59–60

           have : (N₀ : ℝ) < (m : ℝ) + 1 := by have : 0 < 4 / ε := by positivity
                                               linarith

       targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 59–60 at f0dfc93f9827 ↗

       1. hM.this.this have (0 : ℝ) < (4 : ℝ) / ε routine: positivity

          Leaves (↑N₀ : ℝ) < (↑m : ℝ) + (1 : ℝ), with this : (0 : ℝ) < (4 : ℝ) / ε.

          Lean, line 59

              have : (N₀ : ℝ) < (m : ℝ) + 1 := by have : 0 < 4 / ε := by positivity

          targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 59 at f0dfc93f9827 ↗

11. hMpos have (0 : ℝ) < (↑(m + (1 : ℕ)) : ℝ) routine: positivity

    Leaves |Chebyshev.psi x - x| ≤ ε * x, with hMpos : (0 : ℝ) < (↑(m + (1 : ℕ)) : ℝ).

    Lean, line 63

      have hMpos : (0 : ℝ) < ((m + 1 : ℕ) : ℝ) := by positivity

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 63 at f0dfc93f9827 ↗

12. hM' have |Chebyshev.psi x - (↑(m + (1 : ℕ)) : ℝ)| < ε / (2 : ℝ) * (↑(m + (1 : ℕ)) : ℝ)

    Leaves |Chebyshev.psi x - x| ≤ ε * x, with hM' : |Chebyshev.psi x - (↑(m + (1 : ℕ)) : ℝ)| < ε / (2 : ℝ) * (↑(m + (1 : ℕ)) : ℝ).

    Uses library Chebyshev.psi The sum of ArithmeticFunction.vonMangoldt over integers n ≤ x. , abs_div, abs_of_pos, div_lt_iff₀ See div_lt_iff₀' for a version with multiplication on the other side. .

    Lean, lines 65–69

      have hM' : |Chebyshev.psi x - ((m + 1 : ℕ) : ℝ)| < ε / 2 * ((m + 1 : ℕ) : ℝ) := by
        have h1 : Chebyshev.psi x / ((m + 1 : ℕ) : ℝ) - 1 = (Chebyshev.psi x - ((m + 1 : ℕ) : ℝ)) / ((m + 1 : ℕ) : ℝ) := by
          field_simp
        rw [h1, abs_div, abs_of_pos hMpos, div_lt_iff₀ hMpos] at hM
        exact hM

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 65–69 at f0dfc93f9827 ↗

    1. hM'.h1 have Chebyshev.psi x / (↑(m + (1 : ℕ)) : ℝ) - (1 : ℝ) = (Chebyshev.psi x - (↑(m + (1 : ℕ)) : ℝ)) / (↑(m + (1 : ℕ)) : ℝ) routine: field_simp

       Leaves |Chebyshev.psi x - (↑(m + (1 : ℕ)) : ℝ)| < ε / (2 : ℝ) * (↑(m + (1 : ℕ)) : ℝ), with h1 : Chebyshev.psi x / (↑(m + (1 : ℕ)) : ℝ) - (1 : ℝ) = (Chebyshev.psi x - (↑(m + (1 : ℕ)) : ℝ)) / (↑(m + (1 : ℕ)) : ℝ).

       Uses library Chebyshev.psi The sum of ArithmeticFunction.vonMangoldt over integers n ≤ x. .

       Lean, lines 66–67

           have h1 : Chebyshev.psi x / ((m + 1 : ℕ) : ℝ) - 1 = (Chebyshev.psi x - ((m + 1 : ℕ) : ℝ)) / ((m + 1 : ℕ) : ℝ) := by
             field_simp

       targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 66–67 at f0dfc93f9827 ↗

13. hx4 have (4 : ℝ) / ε + (1 : ℝ) ≤ x

    Leaves |Chebyshev.psi x - x| ≤ ε * x, with hx4 : (4 : ℝ) / ε + (1 : ℝ) ≤ x.

    Lean, lines 71–72

      have hx4 : 4 / ε + 1 ≤ x := by have : (0:ℝ) ≤ N₀ := Nat.cast_nonneg _
                                     linarith

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 71–72 at f0dfc93f9827 ↗

    1. hx4.this have (0 : ℝ) ≤ (↑N₀ : ℝ)

       Leaves (4 : ℝ) / ε + (1 : ℝ) ≤ x, with this : (0 : ℝ) ≤ (↑N₀ : ℝ).

       Uses library Nat.cast_nonneg Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use. .

       Lean, line 71

         have hx4 : 4 / ε + 1 ≤ x := by have : (0:ℝ) ≤ N₀ := Nat.cast_nonneg _

       targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 71 at f0dfc93f9827 ↗

14. h_x3b5x (hεx) have ε + (4 : ℝ) ≤ ε * x

    Leaves |Chebyshev.psi x - x| ≤ ε * x, with hεx : ε + (4 : ℝ) ≤ ε * x.

    Lean, lines 73–75

      have hεx : ε + 4 ≤ ε * x := by
        have h4 : ε * (4 / ε) = 4 := by field_simp
        nlinarith

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 73–75 at f0dfc93f9827 ↗

    1. h_x3b5x.h4 have ε * ((4 : ℝ) / ε) = (4 : ℝ) routine: field_simp

       Leaves ε + (4 : ℝ) ≤ ε * x, with h4 : ε * ((4 : ℝ) / ε) = (4 : ℝ).

       Lean, line 74

           have h4 : ε * (4 / ε) = 4 := by field_simp

       targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, line 74 at f0dfc93f9827 ↗

15. close term |Chebyshev.psi x - x| ≤ ε * x

    Closes the goal.

    Uses library abs_lt, abs_le.

    Lean, lines 76–78

      rw [abs_lt] at hM'
      rw [abs_le]
      constructor <;> nlinarith [hM'.1, hM'.2]

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean, lines 76–78 at f0dfc93f9827 ↗