Open Proof Network

Problems / erdos-1094 / erdos-1094--h3--h3--h2

Sander equidistribution: Σ({n/p} − 1/2) log p = o(k)

erdos-1094--h3--h3--h2

open

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

$\displaystyle \forall C\in\mathbb{N},\ \varepsilon>0\ \exists K_4\ \forall n,k\in\mathbb{N}:\quad K_4<k,\ \ k^2\le C\cdot n\cdot\lfloor\log_2 k\rfloor,\ \ n<k^2 \implies \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \Bigl(\Bigl\{\frac{n}{p}\Bigr\}-\frac12\Bigr)\log p\Bigr| \le \varepsilon k$

For every constant $C$ and every real $\varepsilon>0$ there is a threshold $K_4$ such that for all $k>K_4$ and all $n<k^2$ with $k^2\le C\,n\lfloor\log_2 k\rfloor$, the sum over primes $p$ with $k<2p$ and $20p<11k$ of $(\{n/p\}-\tfrac12)\log p$ has absolute value at most $\varepsilon k$. Here $\{n/p\}$ is Int.fract of the real quotient of the casts, $\log$ is Real.log, the sum runs over Finset.range k filtered by the three conditions, and the range hypotheses are in $\mathbb{N}$ where Nat.log 2 k is $\lfloor\log_2 k\rfloor$ (and $0$ for $k\le 1$), a natural number, so the right-hand side is a product of naturals.

unverified · history

Lean
theorem erdos_1094__h3__h3__h2 : ∀ (C : ℕ) (ε : ℝ),
  (0 : ℝ) < ε →
    ∃ (K₄ : ℕ),
      ∀ (n k : ℕ),
        K₄ < k →
          k * k ≤ C * (n * Nat.log (2 : ℕ) k) →
            n < k * k →
              |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
                    (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤
                ε * (↑k : ℝ) := 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 20261015T145123Z-t1015c-a02-partial.lean (merged in 40aad8949bad, attestation 000552).

  • h_l51 → erdos-1094--h3--h3--h2--h1 (open)

    $\displaystyle \forall C\in\mathbb{N},\ \delta>0\ \exists K_5\ \forall n,k\in\mathbb{N},\ K_5<k,\ k^2\le C n\lfloor\log_2 k\rfloor,\ n<k^2,\ \forall \sigma\in[0,1]:\quad \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}}\ [\{n/p\}<\sigma]\,\log p \;-\; \sigma \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p\Bigr| \le \delta k$

Read the partial proof (Lean)
private lemma floor_count (M : ℕ) (hM : 0 < M) (f : ℝ) (h0 : 0 ≤ f) (h1 : f < 1) :
    f - 1 / M ≤ (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M, (if (j : ℝ) / M ≤ f then (1 : ℝ) else 0) ∧
    (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M, (if (j : ℝ) / M ≤ f then (1 : ℝ) else 0) ≤ f := by
  have hMr : (0 : ℝ) < M := by exact_mod_cast hM
  set m := ⌊(M : ℝ) * f⌋₊ with hm
  have hmf : (m : ℝ) ≤ M * f := Nat.floor_le (by positivity)
  have hfm : M * f < m + 1 := Nat.lt_floor_add_one _
  have hmM : m ≤ M := by
    have : (m : ℝ) < M := by nlinarith
    exact_mod_cast this.le
  have key : ∀ j : ℕ, ((j : ℝ) / M ≤ f ↔ j ≤ m) := by
    intro j
    rw [div_le_iff₀ hMr, hm, Nat.le_floor_iff (by positivity), mul_comm]
  have hsum : ∑ j ∈ Finset.Icc 1 M, (if (j : ℝ) / M ≤ f then (1 : ℝ) else 0) = m := by
    simp_rw [key]
    rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one]
    have : (Finset.Icc 1 M).filter (fun j => j ≤ m) = Finset.Icc 1 m := by
      ext j; simp only [Finset.mem_filter, Finset.mem_Icc]; omega
    rw [this, Nat.card_Icc]; simp
  rw [hsum]
  constructor
  · rw [div_mul_eq_mul_div, one_mul, le_div_iff₀ hMr, sub_mul, one_div, inv_mul_cancel₀ hMr.ne']; nlinarith
  · rw [div_mul_eq_mul_div, one_mul, div_le_iff₀ hMr]; nlinarith


private lemma gauss_Icc (M : ℕ) : ∑ j ∈ Finset.Icc 1 M, (j : ℝ) = (M : ℝ) * (M + 1) / 2 := by
  induction M with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_Icc_succ_top (by omega), ih]
    push_cast; ring

theorem erdos_1094__h3__h3__h2 : ∀ (C : ℕ) (ε : ℝ),
  (0 : ℝ) < ε →
    ∃ (K₄ : ℕ),
      ∀ (n k : ℕ),
        K₄ < k →
          k * k ≤ C * (n * Nat.log (2 : ℕ) k) →
            n < k * k →
              |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
                    (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤
                ε * (↑k : ℝ) := by
  have h_theta : ∀ k : ℕ, ∑ p ∈ (Finset.range k).filter
      (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k), Real.log p ≤ 2 * k := by
    intro k
    have hsub : (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k) ⊆
        (Finset.Ioc 0 ⌊(k : ℝ)⌋₊).filter Nat.Prime := by
      intro p hp
      simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_Ioc, Nat.floor_natCast] at hp ⊢
      exact ⟨⟨hp.2.1.pos, hp.1.le⟩, hp.2.1⟩
    have hlog4 : Real.log 4 ≤ 2 := by
      rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
      push_cast
      linarith [Real.log_two_lt_d9]
    calc _ ≤ Chebyshev.theta k := by
          rw [Chebyshev.theta]
          exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun p _ _ => Real.log_natCast_nonneg p)
      _ ≤ Real.log 4 * k := Chebyshev.theta_le_log4_mul_x (by positivity)
      _ ≤ 2 * k := by gcongr
  have h_l51 : ∀ (C : ℕ) (δ : ℝ), 0 < δ → ∃ K₅ : ℕ, ∀ n k : ℕ, K₅ < k →
      k * k ≤ C * (n * Nat.log 2 k) → n < k * k → ∀ σ : ℝ, 0 ≤ σ → σ ≤ 1 →
      |∑ p ∈ (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k),
          (if Int.fract ((n : ℝ) / p) < σ then Real.log p else 0) -
        σ * ∑ p ∈ (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k),
          Real.log p| ≤ δ * k := by
    sorry
  intro C ε hε
  obtain ⟨K₅, hL5⟩ := h_l51 C (ε / 4) (by positivity)
  refine ⟨K₅, fun n k hk hlow hup => ?_⟩
  set S := (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k) with hS
  set L := ∑ p ∈ S, Real.log p with hLdef
  have hlog0 : ∀ p : ℕ, 0 ≤ Real.log p := fun p => Real.log_natCast_nonneg p
  have hL0 : 0 ≤ L := Finset.sum_nonneg (fun p _ => hlog0 p)
  have hL2 : L ≤ 2 * k := h_theta k
  have hk0 : (0 : ℝ) ≤ k := by positivity
  set M : ℕ := ⌈4 / ε⌉₊ + 1 with hMdef
  have hM : 0 < M := by omega
  have hMr : (0 : ℝ) < M := by exact_mod_cast hM
  have hM4 : 4 / ε ≤ M := by
    have := Nat.le_ceil (4 / ε)
    have h2 : ((⌈4 / ε⌉₊ : ℕ) : ℝ) ≤ M := by exact_mod_cast (Nat.le_succ _)
    linarith
  have hinvM : 1 / (M : ℝ) ≤ ε / 4 := by
    rw [div_le_iff₀ hMr]
    have := (div_le_iff₀ hε).1 hM4
    nlinarith
  set f : ℕ → ℝ := fun p => Int.fract ((n : ℝ) / p) with hf
  set A : ℕ → ℝ := fun p => (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M,
    (if (j : ℝ) / M ≤ f p then (1 : ℝ) else 0) with hAdef
  have hA : ∀ p, f p - 1 / M ≤ A p ∧ A p ≤ f p := fun p =>
    floor_count M hM (f p) (Int.fract_nonneg _) (Int.fract_lt_one _)
  -- the swap of the two sums
  have hswap : ∑ p ∈ S, A p * Real.log p = (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M,
      ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) := by
    rw [Finset.sum_comm, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro p _
    rw [hAdef]; simp only
    rw [mul_assoc, Finset.sum_mul]
    congr 1
    apply Finset.sum_congr rfl
    intro j _
    split_ifs <;> simp
  -- each inner sum is L minus the count below σ = j/M
  have hinner : ∀ j ∈ Finset.Icc 1 M,
      |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) - (L - ((j : ℝ) / M) * L)| ≤
        ε / 4 * k := by
    intro j hj
    rw [Finset.mem_Icc] at hj
    have hσ0 : (0 : ℝ) ≤ (j : ℝ) / M := by positivity
    have hσ1 : (j : ℝ) / M ≤ 1 := by
      rw [div_le_one hMr]; exact_mod_cast hj.2
    have h := hL5 n k hk hlow hup ((j : ℝ) / M) hσ0 hσ1
    have hsplit : ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) =
        L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) := by
      rw [hLdef, ← Finset.sum_sub_distrib]
      apply Finset.sum_congr rfl
      intro p _
      by_cases hc : (j : ℝ) / M ≤ f p
      · rw [if_pos hc, if_neg (not_lt.2 hc)]; ring
      · rw [if_neg hc, if_pos (not_le.1 hc)]; ring
    rw [hsplit]
    have : L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (L - (j : ℝ) / M * L) =
        -(∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (j : ℝ) / M * L) := by ring
    rw [this, abs_neg]
    exact h
  -- sum over j
  have hgsum : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) = L * ((M : ℝ) - 1) / 2 := by
    have : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
        (M : ℝ) * L - (L / M) * ∑ j ∈ Finset.Icc 1 M, (j : ℝ) := by
      rw [show ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
          ∑ j ∈ Finset.Icc 1 M, (L - L / M * (j : ℝ)) from
          Finset.sum_congr rfl (fun j _ => by ring)]
      rw [Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_const, Nat.card_Icc]
      simp only [nsmul_eq_mul, Nat.add_sub_cancel]
    rw [this, gauss_Icc]; field_simp; ring
  have hE : |∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
      L * ((M : ℝ) - 1) / 2| ≤ M * (ε / 4 * k) := by
    rw [← hgsum, ← Finset.sum_sub_distrib]
    calc _ ≤ ∑ j ∈ Finset.Icc 1 M, |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
          (L - ((j : ℝ) / M) * L)| := Finset.abs_sum_le_sum_abs _ _
      _ ≤ ∑ j ∈ Finset.Icc 1 M, ε / 4 * k := Finset.sum_le_sum hinner
      _ = M * (ε / 4 * k) := by rw [Finset.sum_const, Nat.card_Icc]; simp
  -- bracket Σ f log p between Σ A log p and Σ A log p + L/M
  have hlo : ∑ p ∈ S, A p * Real.log p ≤ ∑ p ∈ S, f p * Real.log p :=
    Finset.sum_le_sum (fun p _ => mul_le_mul_of_nonneg_right (hA p).2 (hlog0 p))
  have hhi : ∑ p ∈ S, f p * Real.log p ≤ ∑ p ∈ S, A p * Real.log p + L / M := by
    rw [hLdef, Finset.sum_div, ← Finset.sum_add_distrib]
    apply Finset.sum_le_sum; intro p _
    have := (hA p).1
    have hl := hlog0 p
    have : f p * Real.log p ≤ (A p + 1 / M) * Real.log p :=
      mul_le_mul_of_nonneg_right (by linarith) hl
    linarith [show (A p + 1 / M) * Real.log p = A p * Real.log p + Real.log p / M by ring]
  have htarget : ∑ p ∈ S, (Int.fract ((n : ℝ) / p) - 1 / 2) * Real.log p =
      ∑ p ∈ S, f p * Real.log p - L / 2 := by
    rw [hLdef, Finset.sum_div, ← Finset.sum_sub_distrib]
    apply Finset.sum_congr rfl; intro p _; simp only [hf]; ring
  rw [htarget]
  have hAval : ∑ p ∈ S, A p * Real.log p =
      (1 / (M : ℝ)) * (∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0)) :=
    hswap
  set T := ∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) with hT
  have hE' := abs_le.1 hE
  have hLM : L / M ≤ 2 * k * (ε / 4) := by
    rw [div_eq_mul_one_div]
    exact mul_le_mul hL2 hinvM (by positivity) (by positivity)
  have hTM1 : (1 / (M : ℝ)) * T ≤ L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k := by
    rw [one_div_mul_eq_div, div_le_iff₀ hMr]
    have : (L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 + M * (ε / 4 * k) := by
      field_simp
    rw [this]; linarith [hE'.2]
  have hTM2 : L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k ≤ (1 / (M : ℝ)) * T := by
    rw [one_div_mul_eq_div, le_div_iff₀ hMr]
    have : (L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 - M * (ε / 4 * k) := by
      field_simp
    rw [this]; linarith [hE'.1]
  have hmid : L * ((M : ℝ) - 1) / 2 / M = L / 2 - L / M / 2 := by field_simp
  rw [abs_le]
  constructor <;> nlinarith [hLM, hlo, hhi, hTM1, hTM2, hmid, hAval, div_nonneg hL0 hMr.le]

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--h2/attempts/20261015T145123Z-t1015c-a02-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--h2».Context

open scoped Nat

/-! Hole `h_sander` 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__h2 : ∀ (C : ℕ) (ε : ℝ),
  (0 : ℝ) < ε →
    ∃ (K₄ : ℕ),
      ∀ (n k : ℕ),
        K₄ < k →
          k * k ≤ C * (n * Nat.log (2 : ℕ) k) →
            n < k * k →
              |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
                    (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤
                ε * (↑k : ℝ) := by
  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 →

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 C\in\mathbb{N},\ \varepsilon>0\ \exists K_4\ \forall n,k\in\mathbb{N}:\quad K_4<k,\ \ k^2\le C\cdot n\cdot\lfloor\log_2 k\rfloor,\ \ n<k^2 \implies \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \Bigl(\Bigl\{\frac{n}{p}\Bigr\}-\frac12\Bigr)\log p\Bigr| \le \varepsilon k$

For every constant $C$ and every real $\varepsilon>0$ there is a threshold $K_4$ such that for all $k>K_4$ and all $n<k^2$ with $k^2\le C\,n\lfloor\log_2 k\rfloor$, the sum over primes $p$ with $k<2p$ and $20p<11k$ of $(\{n/p\}-\tfrac12)\log p$ has absolute value at most $\varepsilon k$. Here $\{n/p\}$ is Int.fract of the real quotient of the casts, $\log$ is Real.log, the sum runs over Finset.range k filtered by the three conditions, and the range hypotheses are in $\mathbb{N}$ where Nat.log 2 k is $\lfloor\log_2 k\rfloor$ (and $0$ for $k\le 1$), a natural number, so the right-hand side is a product of naturals.

Rendered from gloss/48538564f621….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/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--h2--h1: $\forall C\in\mathbb{N},\ \delta>0\ \exists K_5\ \forall n,k\in\mathbb{N},\ K_5<k,\ k^2\le C n\lfloor\log_2 k\rfloor,\ n<k^2,\ \forall \sigma\in[0,1]:\quad \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}}\ [\{n/p\}<\sigma]\,\log p \;-\; \sigma \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p\Bigr| \le \delta k$
Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000552.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--h2/Witness.lean, sha256 b0a73c3834b7.
import Mathlib

open scoped Nat

theorem witness : ∃ (C : ℕ) (ε : ℝ), (0 : ℝ) < ε := ⟨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 (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-a02; merged in 40aad8949bad under attestations/000552.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--h2/attempts/20261015T145123Z-t1015c-a02-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 20261015T145123Z-t1015c-a02-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.

  1. h_theta have ∀ (k : ℕ), ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) ≤ (2 : ℝ) * (↑k : ℝ)

    Leaves ∀ (C : ℕ) (ε : ℝ), (0 : ℝ) < ε → ∃ (K₄ : ℕ), ∀ (n k : ℕ), K₄ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with h_theta : ∀ (k : ℕ), ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) ≤ (2 : ℝ) * (↑k : ℝ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. .

    Lean, lines 51–67
      have h_theta : ∀ k : ℕ, ∑ p ∈ (Finset.range k).filter
      (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k), Real.log p ≤ 2 * k := by
    intro k
    have hsub : (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k) ⊆
        (Finset.Ioc 0 ⌊(k : ℝ)⌋₊).filter Nat.Prime := by
      intro p hp
      simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_Ioc, Nat.floor_natCast] at hp ⊢
      exact ⟨⟨hp.2.1.pos, hp.1.le⟩, hp.2.1⟩
    have hlog4 : Real.log 4 ≤ 2 := by
      rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
      push_cast
      linarith [Real.log_two_lt_d9]
    calc _ ≤ Chebyshev.theta k := by
          rw [Chebyshev.theta]
          exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun p _ _ => Real.log_natCast_nonneg p)
      _ ≤ Real.log 4 * k := Chebyshev.theta_le_log4_mul_x (by positivity)
      _ ≤ 2 * k := by gcongr

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 51–67 at 6ba7fea98468 ↗

    1. h_theta.hsub have {p ∈ Finset.range k | Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k} ⊆ Finset.filter Nat.Prime (Finset.Ioc (0 : ℕ) ⌊(↑k : ℝ)⌋₊)

      Leaves ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) ≤ (2 : ℝ) * (↑k : ℝ), with hsub : {p ∈ Finset.range k | Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k} ⊆ Finset.filter Nat.Prime (Finset.Ioc (0 : ℕ) ⌊(↑k : ℝ)⌋₊).

      Uses library Finset.range range n is the set of natural numbers less than n. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Finset.Ioc The finset $(a, b]$ of elements x such that a < x and x ≤ b. , Finset.mem_filter, Finset.mem_range, Finset.mem_Ioc, Nat.floor_natCast, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, lines 54–58
          have hsub : (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k) ⊆
        (Finset.Ioc 0 ⌊(k : ℝ)⌋₊).filter Nat.Prime := by
      intro p hp
      simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_Ioc, Nat.floor_natCast] at hp ⊢
      exact ⟨⟨hp.2.1.pos, hp.1.le⟩, hp.2.1⟩

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 54–58 at 6ba7fea98468 ↗

    2. h_theta.hlog4 have Real.log (4 : ℝ) ≤ (2 : ℝ)

      Leaves ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) ≤ (2 : ℝ) * (↑k : ℝ), with hlog4 : Real.log (4 : ℝ) ≤ (2 : ℝ).

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Real.log_pow, Real.log_two_lt_d9.

      Lean, lines 59–62
          have hlog4 : Real.log 4 ≤ 2 := by
      rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
      push_cast
      linarith [Real.log_two_lt_d9]

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 59–62 at 6ba7fea98468 ↗

    3. h_theta.s3 calc ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ) ≤ Chebyshev.theta (↑k : ℝ)

      Closes the goal.

      Uses library Chebyshev.theta The sum of log p over primes p ≤ x. , Finset.sum_le_sum_of_subset_of_nonneg, Real.log_natCast_nonneg.

      Lean, lines 63–65
          calc _ ≤ Chebyshev.theta k := by
          rw [Chebyshev.theta]
          exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun p _ _ => Real.log_natCast_nonneg p)

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 63–65 at 6ba7fea98468 ↗

    4. h_theta.s4 calc Chebyshev.theta (↑k : ℝ) ≤ Real.log (4 : ℝ) * (↑k : ℝ)

      Closes the goal.

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Chebyshev.theta_le_log4_mul_x Chebyshev's upper bound: θ x ≤ c x with the constant c = log 4. .

      Lean, line 66
            _ ≤ Real.log 4 * k := Chebyshev.theta_le_log4_mul_x (by positivity)

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 66 at 6ba7fea98468 ↗

    5. h_theta.s5 calc

      Closes the goal.

      Lean, line 67
            _ ≤ 2 * k := by gcongr

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 67 at 6ba7fea98468 ↗

  2. h_l51 hole ∀ (C : ℕ) (δ : ℝ), (0 : ℝ) < δ → ∃ (K₅ : ℕ), ∀ (n k : ℕ), K₅ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → ∀ (σ : ℝ), (0 : ℝ) ≤ σ → σ ≤ (1 : ℝ) → |(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < σ then Real.log (↑p : ℝ) else (0 : ℝ)) - σ * ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ)| ≤ δ * (↑k : ℝ) hole

    Leaves ∀ (C : ℕ) (ε : ℝ), (0 : ℝ) < ε → ∃ (K₄ : ℕ), ∀ (n k : ℕ), K₄ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with h_l51 : ∀ (C : ℕ) (δ : ℝ), (0 : ℝ) < δ → ∃ (K₅ : ℕ), ∀ (n k : ℕ), K₅ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → ∀ (σ : ℝ), (0 : ℝ) ≤ σ → σ ≤ (1 : ℝ) → |(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < σ then Real.log (↑p : ℝ) else (0 : ℝ)) - σ * ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ)| ≤ δ * (↑k : ℝ).

    Uses library Nat.log log b n, is the logarithm of natural number n in base b. , Finset.range range n is the set of natural numbers less than n. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Int.fract Int.fract a the fractional part of a, is a minus its floor. , Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. .

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

    Lean, lines 68–74
      have h_l51 : ∀ (C : ℕ) (δ : ℝ), 0 < δ → ∃ K₅ : ℕ, ∀ n k : ℕ, K₅ < k →
      k * k ≤ C * (n * Nat.log 2 k) → n < k * k → ∀ σ : ℝ, 0 ≤ σ → σ ≤ 1 →
      |∑ p ∈ (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k),
          (if Int.fract ((n : ℝ) / p) < σ then Real.log p else 0) -
        σ * ∑ p ∈ (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k),
          Real.log p| ≤ δ * k := by
    sorry

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 68–74 at 6ba7fea98468 ↗

  3. s3 obtain ∃ (K₅ : ℕ), ∀ (n k : ℕ), K₅ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → ∀ (σ : ℝ), (0 : ℝ) ≤ σ → σ ≤ (1 : ℝ) → |(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < σ then Real.log (↑p : ℝ) else (0 : ℝ)) - σ * ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ)| ≤ ε / (4 : ℝ) * (↑k : ℝ)

    Leaves ∃ (K₄ : ℕ), ∀ (n k : ℕ), K₄ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with K₅ : ℕ, hL5 : ∀ (n k : ℕ), K₅ < k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) → n < k * k → ∀ (σ : ℝ), (0 : ℝ) ≤ σ → σ ≤ (1 : ℝ) → |(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < σ then Real.log (↑p : ℝ) else (0 : ℝ)) - σ * ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ)| ≤ ε / (4 : ℝ) * (↑k : ℝ).

    Lean, line 76
      obtain ⟨K₅, hL5⟩ := h_l51 C (ε / 4) (by positivity)

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 76 at 6ba7fea98468 ↗

  4. hlog0 have ∀ (p : ℕ), (0 : ℝ) ≤ Real.log (↑p : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hlog0 : ∀ (p : ℕ), (0 : ℝ) ≤ Real.log (↑p : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Real.log_natCast_nonneg.

    Lean, line 80
      have hlog0 : ∀ p : ℕ, 0 ≤ Real.log p := fun p => Real.log_natCast_nonneg p

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 80 at 6ba7fea98468 ↗

  5. hL0 have (0 : ℝ) ≤ L

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hL0 : (0 : ℝ) ≤ L.

    Uses library Finset.sum_nonneg.

    Lean, line 81
      have hL0 : 0 ≤ L := Finset.sum_nonneg (fun p _ => hlog0 p)

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 81 at 6ba7fea98468 ↗

  6. hL2 have L ≤ (2 : ℝ) * (↑k : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hL2 : L ≤ (2 : ℝ) * (↑k : ℝ).

    Lean, line 82
      have hL2 : L ≤ 2 * k := h_theta k

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 82 at 6ba7fea98468 ↗

  7. hk0 have (0 : ℝ) ≤ (↑k : ℝ) routine: positivity

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hk0 : (0 : ℝ) ≤ (↑k : ℝ).

    Lean, line 83
      have hk0 : (0 : ℝ) ≤ k := by positivity

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 83 at 6ba7fea98468 ↗

  8. hM have (0 : ℕ) < M routine: omega

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hM : (0 : ℕ) < M.

    Lean, line 85
      have hM : 0 < M := by omega

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 85 at 6ba7fea98468 ↗

  9. hMr have (0 : ℝ) < (↑M : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hMr : (0 : ℝ) < (↑M : ℝ).

    Lean, line 86
      have hMr : (0 : ℝ) < M := by exact_mod_cast hM

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 86 at 6ba7fea98468 ↗

  10. hM4 have (4 : ℝ) / ε ≤ (↑M : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hM4 : (4 : ℝ) / ε ≤ (↑M : ℝ).

    Lean, lines 87–90
      have hM4 : 4 / ε ≤ M := by
    have := Nat.le_ceil (4 / ε)
    have h2 : ((⌈4 / ε⌉₊ : ℕ) : ℝ) ≤ M := by exact_mod_cast (Nat.le_succ _)
    linarith

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 87–90 at 6ba7fea98468 ↗

    1. hM4.this have (4 : ℝ) / ε ≤ (↑⌈(4 : ℝ) / ε⌉₊ : ℝ)

      Leaves (4 : ℝ) / ε ≤ (↑M : ℝ), with this : (4 : ℝ) / ε ≤ (↑⌈(4 : ℝ) / ε⌉₊ : ℝ).

      Uses library Nat.le_ceil.

      Lean, line 88
          have := Nat.le_ceil (4 / ε)

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 88 at 6ba7fea98468 ↗

    2. hM4.h2 have (↑⌈(4 : ℝ) / ε⌉₊ : ℝ) ≤ (↑M : ℝ)

      Leaves (4 : ℝ) / ε ≤ (↑M : ℝ), with h2 : (↑⌈(4 : ℝ) / ε⌉₊ : ℝ) ≤ (↑M : ℝ).

      Uses library Nat.le_succ.

      Lean, line 89
          have h2 : ((⌈4 / ε⌉₊ : ℕ) : ℝ) ≤ M := by exact_mod_cast (Nat.le_succ _)

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 89 at 6ba7fea98468 ↗

  11. hinvM have (1 : ℝ) / (↑M : ℝ) ≤ ε / (4 : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hinvM : (1 : ℝ) / (↑M : ℝ) ≤ ε / (4 : ℝ).

    Uses library div_le_iff₀ See div_le_iff₀' for a version with multiplication on the other side. .

    Lean, lines 91–94
      have hinvM : 1 / (M : ℝ) ≤ ε / 4 := by
    rw [div_le_iff₀ hMr]
    have := (div_le_iff₀ hε).1 hM4
    nlinarith

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 91–94 at 6ba7fea98468 ↗

    1. hinvM.this have (4 : ℝ) ≤ (↑M : ℝ) * ε

      Leaves (1 : ℝ) ≤ ε / (4 : ℝ) * (↑M : ℝ), with this : (4 : ℝ) ≤ (↑M : ℝ) * ε.

      Uses library div_le_iff₀ See div_le_iff₀' for a version with multiplication on the other side. .

      Lean, line 93
          have := (div_le_iff₀ hε).1 hM4

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 93 at 6ba7fea98468 ↗

  12. hA have ∀ (p : ℕ), f p - (1 : ℝ) / (↑M : ℝ) ≤ A p ∧ A p ≤ f p

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hA : ∀ (p : ℕ), f p - (1 : ℝ) / (↑M : ℝ) ≤ A p ∧ A p ≤ f p.

    Uses library Int.fract_nonneg, Int.fract_lt_one.

    Lean, lines 98–99
      have hA : ∀ p, f p - 1 / M ≤ A p ∧ A p ≤ f p := fun p =>
    floor_count M hM (f p) (Int.fract_nonneg _) (Int.fract_lt_one _)

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 98–99 at 6ba7fea98468 ↗

  13. hswap have ∑ p ∈ S, A p * Real.log (↑p : ℝ) = (1 : ℝ) / (↑M : ℝ) * ∑ j ∈ Finset.Icc (1 : ℕ) M, ∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hswap : ∑ p ∈ S, A p * Real.log (↑p : ℝ) = (1 : ℝ) / (↑M : ℝ) * ∑ j ∈ Finset.Icc (1 : ℕ) M, ∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.sum_comm, Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , mul_assoc, Finset.sum_mul.

    Lean, lines 101–111
      have hswap : ∑ p ∈ S, A p * Real.log p = (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M,
      ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) := by
    rw [Finset.sum_comm, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro p _
    rw [hAdef]; simp only
    rw [mul_assoc, Finset.sum_mul]
    congr 1
    apply Finset.sum_congr rfl
    intro j _
    split_ifs <;> simp

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 101–111 at 6ba7fea98468 ↗

  14. hinner have ∀ j ∈ Finset.Icc (1 : ℕ) M, |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hinner : ∀ j ∈ Finset.Icc (1 : ℕ) M, |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ).

    Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.mem_Icc, abs_neg.

    Lean, lines 113–134
      have hinner : ∀ j ∈ Finset.Icc 1 M,
      |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) - (L - ((j : ℝ) / M) * L)| ≤
        ε / 4 * k := by
    intro j hj
    rw [Finset.mem_Icc] at hj
    have hσ0 : (0 : ℝ) ≤ (j : ℝ) / M := by positivity
    have hσ1 : (j : ℝ) / M ≤ 1 := by
      rw [div_le_one hMr]; exact_mod_cast hj.2
    have h := hL5 n k hk hlow hup ((j : ℝ) / M) hσ0 hσ1
    have hsplit : ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) =
        L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) := by
      rw [hLdef, ← Finset.sum_sub_distrib]
      apply Finset.sum_congr rfl
      intro p _
      by_cases hc : (j : ℝ) / M ≤ f p
      · rw [if_pos hc, if_neg (not_lt.2 hc)]; ring
      · rw [if_neg hc, if_pos (not_le.1 hc)]; ring
    rw [hsplit]
    have : L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (L - (j : ℝ) / M * L) =
        -(∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (j : ℝ) / M * L) := by ring
    rw [this, abs_neg]
    exact h

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 113–134 at 6ba7fea98468 ↗

    1. hinner.h_x3c30 (hσ0) have (0 : ℝ) ≤ (↑j : ℝ) / (↑M : ℝ) routine: positivity

      Leaves |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ), with hσ0 : (0 : ℝ) ≤ (↑j : ℝ) / (↑M : ℝ).

      Lean, line 118
          have hσ0 : (0 : ℝ) ≤ (j : ℝ) / M := by positivity

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 118 at 6ba7fea98468 ↗

    2. hinner.h_x3c31 (hσ1) have (↑j : ℝ) / (↑M : ℝ) ≤ (1 : ℝ)

      Leaves |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ), with hσ1 : (↑j : ℝ) / (↑M : ℝ) ≤ (1 : ℝ).

      Uses library div_le_one.

      Lean, lines 119–120
          have hσ1 : (j : ℝ) / M ≤ 1 := by
      rw [div_le_one hMr]; exact_mod_cast hj.2

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 119–120 at 6ba7fea98468 ↗

    3. hinner.h have |(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (↑j : ℝ) / (↑M : ℝ) * ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ)| ≤ ε / (4 : ℝ) * (↑k : ℝ)

      Leaves |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ), with h : |(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (↑j : ℝ) / (↑M : ℝ) * ∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k, Real.log (↑p : ℝ)| ≤ ε / (4 : ℝ) * (↑k : ℝ).

      Lean, line 121
          have h := hL5 n k hk hlow hup ((j : ℝ) / M) hσ0 hσ1

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 121 at 6ba7fea98468 ↗

    4. hinner.hsplit have (∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) = L - ∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)

      Leaves |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ), with hsplit : (∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) = L - ∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ).

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.sum_sub_distrib, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 122–129
          have hsplit : ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) =
        L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) := by
      rw [hLdef, ← Finset.sum_sub_distrib]
      apply Finset.sum_congr rfl
      intro p _
      by_cases hc : (j : ℝ) / M ≤ f p
      · rw [if_pos hc, if_neg (not_lt.2 hc)]; ring
      · rw [if_neg hc, if_pos (not_le.1 hc)]; ring

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 122–129 at 6ba7fea98468 ↗

      1. hinner.hsplit.s1 case

        Leaves (if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) = Real.log (↑p : ℝ) - if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ), with hc : (↑j : ℝ) / (↑M : ℝ) ≤ f p.

        Uses library if_pos, if_neg, not_lt.

        Lean, line 128
              · rw [if_pos hc, if_neg (not_lt.2 hc)]; ring

        targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 128 at 6ba7fea98468 ↗

      2. hinner.hsplit.s2 case

        Leaves (if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) = Real.log (↑p : ℝ) - if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ), with hc : ¬(↑j : ℝ) / (↑M : ℝ) ≤ f p.

        Uses library if_neg, if_pos, not_le.

        Lean, line 129
              · rw [if_neg hc, if_pos (not_le.1 hc)]; ring

        targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 129 at 6ba7fea98468 ↗

    5. hinner.this have (L - ∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L) = -((∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (↑j : ℝ) / (↑M : ℝ) * L) routine: ring

      Leaves |(L - ∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ε / (4 : ℝ) * (↑k : ℝ), with this : (L - ∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L) = -((∑ p ∈ S, if f p < (↑j : ℝ) / (↑M : ℝ) then Real.log (↑p : ℝ) else (0 : ℝ)) - (↑j : ℝ) / (↑M : ℝ) * L).

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. .

      Lean, lines 131–132
          have : L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (L - (j : ℝ) / M * L) =
        -(∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (j : ℝ) / M * L) := by ring

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 131–132 at 6ba7fea98468 ↗

  15. hgsum have ∑ j ∈ Finset.Icc (1 : ℕ) M, (L - (↑j : ℝ) / (↑M : ℝ) * L) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hgsum : ∑ j ∈ Finset.Icc (1 : ℕ) M, (L - (↑j : ℝ) / (↑M : ℝ) * L) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ).

    Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. .

    Lean, lines 136–144
      have hgsum : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) = L * ((M : ℝ) - 1) / 2 := by
    have : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
        (M : ℝ) * L - (L / M) * ∑ j ∈ Finset.Icc 1 M, (j : ℝ) := by
      rw [show ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
          ∑ j ∈ Finset.Icc 1 M, (L - L / M * (j : ℝ)) from
          Finset.sum_congr rfl (fun j _ => by ring)]
      rw [Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_const, Nat.card_Icc]
      simp only [nsmul_eq_mul, Nat.add_sub_cancel]
    rw [this, gauss_Icc]; field_simp; ring

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 136–144 at 6ba7fea98468 ↗

    1. hgsum.this have ∑ j ∈ Finset.Icc (1 : ℕ) M, (L - (↑j : ℝ) / (↑M : ℝ) * L) = (↑M : ℝ) * L - L / (↑M : ℝ) * ∑ j ∈ Finset.Icc (1 : ℕ) M, (↑j : ℝ)

      Leaves ∑ j ∈ Finset.Icc (1 : ℕ) M, (L - (↑j : ℝ) / (↑M : ℝ) * L) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ), with this : ∑ j ∈ Finset.Icc (1 : ℕ) M, (L - (↑j : ℝ) / (↑M : ℝ) * L) = (↑M : ℝ) * L - L / (↑M : ℝ) * ∑ j ∈ Finset.Icc (1 : ℕ) M, (↑j : ℝ).

      Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , Finset.sum_sub_distrib, Finset.mul_sum, Finset.sum_const, Nat.card_Icc, nsmul_eq_mul, Nat.add_sub_cancel.

      Lean, lines 137–143
          have : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
        (M : ℝ) * L - (L / M) * ∑ j ∈ Finset.Icc 1 M, (j : ℝ) := by
      rw [show ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
          ∑ j ∈ Finset.Icc 1 M, (L - L / M * (j : ℝ)) from
          Finset.sum_congr rfl (fun j _ => by ring)]
      rw [Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_const, Nat.card_Icc]
      simp only [nsmul_eq_mul, Nat.add_sub_cancel]

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 137–143 at 6ba7fea98468 ↗

  16. hE have |(∑ j ∈ Finset.Icc (1 : ℕ) M, ∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ)| ≤ (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ))

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hE : |(∑ j ∈ Finset.Icc (1 : ℕ) M, ∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ)| ≤ (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ)).

    Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.sum_sub_distrib.

    Lean, lines 145–151
      have hE : |∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
      L * ((M : ℝ) - 1) / 2| ≤ M * (ε / 4 * k) := by
    rw [← hgsum, ← Finset.sum_sub_distrib]
    calc _ ≤ ∑ j ∈ Finset.Icc 1 M, |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
          (L - ((j : ℝ) / M) * L)| := Finset.abs_sum_le_sum_abs _ _
      _ ≤ ∑ j ∈ Finset.Icc 1 M, ε / 4 * k := Finset.sum_le_sum hinner
      _ = M * (ε / 4 * k) := by rw [Finset.sum_const, Nat.card_Icc]; simp

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 145–151 at 6ba7fea98468 ↗

    1. hE.s1 calc |∑ i ∈ Finset.Icc (1 : ℕ) M, ((∑ p ∈ S, if (↑i : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑i : ℝ) / (↑M : ℝ) * L))| ≤ ∑ j ∈ Finset.Icc (1 : ℕ) M, |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)|

      Closes the goal.

      Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.abs_sum_le_sum_abs.

      Lean, lines 148–149
          calc _ ≤ ∑ j ∈ Finset.Icc 1 M, |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
          (L - ((j : ℝ) / M) * L)| := Finset.abs_sum_le_sum_abs _ _

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 148–149 at 6ba7fea98468 ↗

    2. hE.s2 calc ∑ j ∈ Finset.Icc (1 : ℕ) M, |(∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)) - (L - (↑j : ℝ) / (↑M : ℝ) * L)| ≤ ∑ j ∈ Finset.Icc (1 : ℕ) M, ε / (4 : ℝ) * (↑k : ℝ)

      Closes the goal.

      Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.sum_le_sum In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i. .

      Lean, line 150
            _ ≤ ∑ j ∈ Finset.Icc 1 M, ε / 4 * k := Finset.sum_le_sum hinner

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 150 at 6ba7fea98468 ↗

    3. hE.s3 calc

      Closes the goal.

      Uses library Finset.sum_const, Nat.card_Icc.

      Lean, line 151
            _ = M * (ε / 4 * k) := by rw [Finset.sum_const, Nat.card_Icc]; simp

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 151 at 6ba7fea98468 ↗

  17. hlo have ∑ p ∈ S, A p * Real.log (↑p : ℝ) ≤ ∑ p ∈ S, f p * Real.log (↑p : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hlo : ∑ p ∈ S, A p * Real.log (↑p : ℝ) ≤ ∑ p ∈ S, f p * Real.log (↑p : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.sum_le_sum In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i. , mul_le_mul_of_nonneg_right.

    Lean, lines 153–154
      have hlo : ∑ p ∈ S, A p * Real.log p ≤ ∑ p ∈ S, f p * Real.log p :=
    Finset.sum_le_sum (fun p _ => mul_le_mul_of_nonneg_right (hA p).2 (hlog0 p))

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 153–154 at 6ba7fea98468 ↗

  18. hhi have ∑ p ∈ S, f p * Real.log (↑p : ℝ) ≤ ∑ p ∈ S, A p * Real.log (↑p : ℝ) + L / (↑M : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with hhi : ∑ p ∈ S, f p * Real.log (↑p : ℝ) ≤ ∑ p ∈ S, A p * Real.log (↑p : ℝ) + L / (↑M : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.sum_div, Finset.sum_add_distrib, Finset.sum_le_sum In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i. .

    Lean, lines 155–162
      have hhi : ∑ p ∈ S, f p * Real.log p ≤ ∑ p ∈ S, A p * Real.log p + L / M := by
    rw [hLdef, Finset.sum_div, ← Finset.sum_add_distrib]
    apply Finset.sum_le_sum; intro p _
    have := (hA p).1
    have hl := hlog0 p
    have : f p * Real.log p ≤ (A p + 1 / M) * Real.log p :=
      mul_le_mul_of_nonneg_right (by linarith) hl
    linarith [show (A p + 1 / M) * Real.log p = A p * Real.log p + Real.log p / M by ring]

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 155–162 at 6ba7fea98468 ↗

    1. hhi.s1 have f p - (1 : ℝ) / (↑M : ℝ) ≤ A p

      Leaves f p * Real.log (↑p : ℝ) ≤ A p * Real.log (↑p : ℝ) + Real.log (↑p : ℝ) / (↑M : ℝ), with this : f p - (1 : ℝ) / (↑M : ℝ) ≤ A p.

      Lean, line 158
          have := (hA p).1

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 158 at 6ba7fea98468 ↗

    2. hhi.hl have (0 : ℝ) ≤ Real.log (↑p : ℝ)

      Leaves f p * Real.log (↑p : ℝ) ≤ A p * Real.log (↑p : ℝ) + Real.log (↑p : ℝ) / (↑M : ℝ), with hl : (0 : ℝ) ≤ Real.log (↑p : ℝ).

      Lean, line 159
          have hl := hlog0 p

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 159 at 6ba7fea98468 ↗

    3. hhi.s3 have f p * Real.log (↑p : ℝ) ≤ (A p + (1 : ℝ) / (↑M : ℝ)) * Real.log (↑p : ℝ)

      Leaves f p * Real.log (↑p : ℝ) ≤ A p * Real.log (↑p : ℝ) + Real.log (↑p : ℝ) / (↑M : ℝ), with this : f p * Real.log (↑p : ℝ) ≤ (A p + (1 : ℝ) / (↑M : ℝ)) * Real.log (↑p : ℝ).

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , mul_le_mul_of_nonneg_right.

      Lean, lines 160–161
          have : f p * Real.log p ≤ (A p + 1 / M) * Real.log p :=
      mul_le_mul_of_nonneg_right (by linarith) hl

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 160–161 at 6ba7fea98468 ↗

  19. htarget have ∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ) = ∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)

    Leaves |∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤ ε * (↑k : ℝ), with htarget : ∑ p ∈ S, (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ) = ∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ).

    Uses library Int.fract Int.fract a the fractional part of a, is a minus its floor. , Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.sum_div, Finset.sum_sub_distrib, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 163–166
      have htarget : ∑ p ∈ S, (Int.fract ((n : ℝ) / p) - 1 / 2) * Real.log p =
      ∑ p ∈ S, f p * Real.log p - L / 2 := by
    rw [hLdef, Finset.sum_div, ← Finset.sum_sub_distrib]
    apply Finset.sum_congr rfl; intro p _; simp only [hf]; ring

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 163–166 at 6ba7fea98468 ↗

  20. hAval have ∑ p ∈ S, A p * Real.log (↑p : ℝ) = (1 : ℝ) / (↑M : ℝ) * ∑ j ∈ Finset.Icc (1 : ℕ) M, ∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ)

    Leaves |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ), with hAval : ∑ p ∈ S, A p * Real.log (↑p : ℝ) = (1 : ℝ) / (↑M : ℝ) * ∑ j ∈ Finset.Icc (1 : ℕ) M, ∑ p ∈ S, if (↑j : ℝ) / (↑M : ℝ) ≤ f p then Real.log (↑p : ℝ) else (0 : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. .

    Lean, lines 168–170
      have hAval : ∑ p ∈ S, A p * Real.log p =
      (1 / (M : ℝ)) * (∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0)) :=
    hswap

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 168–170 at 6ba7fea98468 ↗

  21. hE' have -((↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ))) ≤ T - L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) ∧ T - L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) ≤ (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ))

    Leaves |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ), with hE' : -((↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ))) ≤ T - L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) ∧ T - L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) ≤ (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ)).

    Uses library abs_le.

    Lean, line 172
      have hE' := abs_le.1 hE

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 172 at 6ba7fea98468 ↗

  22. hLM have L / (↑M : ℝ) ≤ (2 : ℝ) * (↑k : ℝ) * (ε / (4 : ℝ))

    Leaves |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ), with hLM : L / (↑M : ℝ) ≤ (2 : ℝ) * (↑k : ℝ) * (ε / (4 : ℝ)).

    Uses library div_eq_mul_one_div, mul_le_mul Alias of mul_le_mul_of_nonneg'. .

    Lean, lines 173–175
      have hLM : L / M ≤ 2 * k * (ε / 4) := by
    rw [div_eq_mul_one_div]
    exact mul_le_mul hL2 hinvM (by positivity) (by positivity)

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 173–175 at 6ba7fea98468 ↗

  23. hTM1 have (1 : ℝ) / (↑M : ℝ) * T ≤ L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) + ε / (4 : ℝ) * (↑k : ℝ)

    Leaves |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ), with hTM1 : (1 : ℝ) / (↑M : ℝ) * T ≤ L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) + ε / (4 : ℝ) * (↑k : ℝ).

    Uses library one_div_mul_eq_div, div_le_iff₀ See div_le_iff₀' for a version with multiplication on the other side. .

    Lean, lines 176–180
      have hTM1 : (1 / (M : ℝ)) * T ≤ L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k := by
    rw [one_div_mul_eq_div, div_le_iff₀ hMr]
    have : (L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 + M * (ε / 4 * k) := by
      field_simp
    rw [this]; linarith [hE'.2]

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 176–180 at 6ba7fea98468 ↗

    1. hTM1.this have (L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) + ε / (4 : ℝ) * (↑k : ℝ)) * (↑M : ℝ) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) + (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ)) routine: field_simp

      Leaves T ≤ (L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) + ε / (4 : ℝ) * (↑k : ℝ)) * (↑M : ℝ), with this : (L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) + ε / (4 : ℝ) * (↑k : ℝ)) * (↑M : ℝ) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) + (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ)).

      Lean, lines 178–179
          have : (L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 + M * (ε / 4 * k) := by
      field_simp

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 178–179 at 6ba7fea98468 ↗

  24. hTM2 have L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) - ε / (4 : ℝ) * (↑k : ℝ) ≤ (1 : ℝ) / (↑M : ℝ) * T

    Leaves |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ), with hTM2 : L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) - ε / (4 : ℝ) * (↑k : ℝ) ≤ (1 : ℝ) / (↑M : ℝ) * T.

    Uses library one_div_mul_eq_div, le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. .

    Lean, lines 181–185
      have hTM2 : L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k ≤ (1 / (M : ℝ)) * T := by
    rw [one_div_mul_eq_div, le_div_iff₀ hMr]
    have : (L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 - M * (ε / 4 * k) := by
      field_simp
    rw [this]; linarith [hE'.1]

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 181–185 at 6ba7fea98468 ↗

    1. hTM2.this have (L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) - ε / (4 : ℝ) * (↑k : ℝ)) * (↑M : ℝ) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) - (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ)) routine: field_simp

      Leaves (L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) - ε / (4 : ℝ) * (↑k : ℝ)) * (↑M : ℝ) ≤ T, with this : (L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) - ε / (4 : ℝ) * (↑k : ℝ)) * (↑M : ℝ) = L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) - (↑M : ℝ) * (ε / (4 : ℝ) * (↑k : ℝ)).

      Lean, lines 183–184
          have : (L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 - M * (ε / 4 * k) := by
      field_simp

      targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 183–184 at 6ba7fea98468 ↗

  25. hmid have L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) = L / (2 : ℝ) - L / (↑M : ℝ) / (2 : ℝ) routine: field_simp

    Leaves |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ), with hmid : L * ((↑M : ℝ) - (1 : ℝ)) / (2 : ℝ) / (↑M : ℝ) = L / (2 : ℝ) - L / (↑M : ℝ) / (2 : ℝ).

    Lean, line 186
      have hmid : L * ((M : ℝ) - 1) / 2 / M = L / 2 - L / M / 2 := by field_simp

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, line 186 at 6ba7fea98468 ↗

  26. close term |∑ p ∈ S, f p * Real.log (↑p : ℝ) - L / (2 : ℝ)| ≤ ε * (↑k : ℝ)

    Closes the goal.

    Uses library abs_le, div_nonneg.

    Lean, lines 187–188
      rw [abs_le]
  constructor <;> nlinarith [hLM, hlo, hhi, hTM1, hTM2, hmid, hAval, div_nonneg hL0 hMr.le]

    targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean, lines 187–188 at 6ba7fea98468 ↗

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

open scoped Nat

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

private lemma floor_count (M : ℕ) (hM : 0 < M) (f : ℝ) (h0 : 0 ≤ f) (h1 : f < 1) :
    f - 1 / M ≤ (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M, (if (j : ℝ) / M ≤ f then (1 : ℝ) else 0) ∧
    (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M, (if (j : ℝ) / M ≤ f then (1 : ℝ) else 0) ≤ f := by
  have hMr : (0 : ℝ) < M := by exact_mod_cast hM
  set m := ⌊(M : ℝ) * f⌋₊ with hm
  have hmf : (m : ℝ) ≤ M * f := Nat.floor_le (by positivity)
  have hfm : M * f < m + 1 := Nat.lt_floor_add_one _
  have hmM : m ≤ M := by
    have : (m : ℝ) < M := by nlinarith
    exact_mod_cast this.le
  have key : ∀ j : ℕ, ((j : ℝ) / M ≤ f ↔ j ≤ m) := by
    intro j
    rw [div_le_iff₀ hMr, hm, Nat.le_floor_iff (by positivity), mul_comm]
  have hsum : ∑ j ∈ Finset.Icc 1 M, (if (j : ℝ) / M ≤ f then (1 : ℝ) else 0) = m := by
    simp_rw [key]
    rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, mul_one]
    have : (Finset.Icc 1 M).filter (fun j => j ≤ m) = Finset.Icc 1 m := by
      ext j; simp only [Finset.mem_filter, Finset.mem_Icc]; omega
    rw [this, Nat.card_Icc]; simp
  rw [hsum]
  constructor
  · rw [div_mul_eq_mul_div, one_mul, le_div_iff₀ hMr, sub_mul, one_div, inv_mul_cancel₀ hMr.ne']; nlinarith
  · rw [div_mul_eq_mul_div, one_mul, div_le_iff₀ hMr]; nlinarith


private lemma gauss_Icc (M : ℕ) : ∑ j ∈ Finset.Icc 1 M, (j : ℝ) = (M : ℝ) * (M + 1) / 2 := by
  induction M with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_Icc_succ_top (by omega), ih]
    push_cast; ring

theorem erdos_1094__h3__h3__h2 : ∀ (C : ℕ) (ε : ℝ),
  (0 : ℝ) < ε →
    ∃ (K₄ : ℕ),
      ∀ (n k : ℕ),
        K₄ < k →
          k * k ≤ C * (n * Nat.log (2 : ℕ) k) →
            n < k * k →
              |∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
                    (Int.fract ((↑n : ℝ) / (↑p : ℝ)) - (1 / 2 : ℝ)) * Real.log (↑p : ℝ)| ≤
                ε * (↑k : ℝ) := by
  have h_theta : ∀ k : ℕ, ∑ p ∈ (Finset.range k).filter
      (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k), Real.log p ≤ 2 * k := by
    intro k
    have hsub : (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k) ⊆
        (Finset.Ioc 0 ⌊(k : ℝ)⌋₊).filter Nat.Prime := by
      intro p hp
      simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_Ioc, Nat.floor_natCast] at hp ⊢
      exact ⟨⟨hp.2.1.pos, hp.1.le⟩, hp.2.1⟩
    have hlog4 : Real.log 4 ≤ 2 := by
      rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
      push_cast
      linarith [Real.log_two_lt_d9]
    calc _ ≤ Chebyshev.theta k := by
          rw [Chebyshev.theta]
          exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun p _ _ => Real.log_natCast_nonneg p)
      _ ≤ Real.log 4 * k := Chebyshev.theta_le_log4_mul_x (by positivity)
      _ ≤ 2 * k := by gcongr
  have h_l51 : ∀ (C : ℕ) (δ : ℝ), 0 < δ → ∃ K₅ : ℕ, ∀ n k : ℕ, K₅ < k →
      k * k ≤ C * (n * Nat.log 2 k) → n < k * k → ∀ σ : ℝ, 0 ≤ σ → σ ≤ 1 →
      |∑ p ∈ (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k),
          (if Int.fract ((n : ℝ) / p) < σ then Real.log p else 0) -
        σ * ∑ p ∈ (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k),
          Real.log p| ≤ δ * k := by
    sorry
  intro C ε hε
  obtain ⟨K₅, hL5⟩ := h_l51 C (ε / 4) (by positivity)
  refine ⟨K₅, fun n k hk hlow hup => ?_⟩
  set S := (Finset.range k).filter (fun p => Nat.Prime p ∧ k < 2 * p ∧ 20 * p < 11 * k) with hS
  set L := ∑ p ∈ S, Real.log p with hLdef
  have hlog0 : ∀ p : ℕ, 0 ≤ Real.log p := fun p => Real.log_natCast_nonneg p
  have hL0 : 0 ≤ L := Finset.sum_nonneg (fun p _ => hlog0 p)
  have hL2 : L ≤ 2 * k := h_theta k
  have hk0 : (0 : ℝ) ≤ k := by positivity
  set M : ℕ := ⌈4 / ε⌉₊ + 1 with hMdef
  have hM : 0 < M := by omega
  have hMr : (0 : ℝ) < M := by exact_mod_cast hM
  have hM4 : 4 / ε ≤ M := by
    have := Nat.le_ceil (4 / ε)
    have h2 : ((⌈4 / ε⌉₊ : ℕ) : ℝ) ≤ M := by exact_mod_cast (Nat.le_succ _)
    linarith
  have hinvM : 1 / (M : ℝ) ≤ ε / 4 := by
    rw [div_le_iff₀ hMr]
    have := (div_le_iff₀ hε).1 hM4
    nlinarith
  set f : ℕ → ℝ := fun p => Int.fract ((n : ℝ) / p) with hf
  set A : ℕ → ℝ := fun p => (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M,
    (if (j : ℝ) / M ≤ f p then (1 : ℝ) else 0) with hAdef
  have hA : ∀ p, f p - 1 / M ≤ A p ∧ A p ≤ f p := fun p =>
    floor_count M hM (f p) (Int.fract_nonneg _) (Int.fract_lt_one _)
  -- the swap of the two sums
  have hswap : ∑ p ∈ S, A p * Real.log p = (1 / (M : ℝ)) * ∑ j ∈ Finset.Icc 1 M,
      ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) := by
    rw [Finset.sum_comm, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro p _
    rw [hAdef]; simp only
    rw [mul_assoc, Finset.sum_mul]
    congr 1
    apply Finset.sum_congr rfl
    intro j _
    split_ifs <;> simp
  -- each inner sum is L minus the count below σ = j/M
  have hinner : ∀ j ∈ Finset.Icc 1 M,
      |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) - (L - ((j : ℝ) / M) * L)| ≤
        ε / 4 * k := by
    intro j hj
    rw [Finset.mem_Icc] at hj
    have hσ0 : (0 : ℝ) ≤ (j : ℝ) / M := by positivity
    have hσ1 : (j : ℝ) / M ≤ 1 := by
      rw [div_le_one hMr]; exact_mod_cast hj.2
    have h := hL5 n k hk hlow hup ((j : ℝ) / M) hσ0 hσ1
    have hsplit : ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) =
        L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) := by
      rw [hLdef, ← Finset.sum_sub_distrib]
      apply Finset.sum_congr rfl
      intro p _
      by_cases hc : (j : ℝ) / M ≤ f p
      · rw [if_pos hc, if_neg (not_lt.2 hc)]; ring
      · rw [if_neg hc, if_pos (not_le.1 hc)]; ring
    rw [hsplit]
    have : L - ∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (L - (j : ℝ) / M * L) =
        -(∑ p ∈ S, (if f p < (j : ℝ) / M then Real.log p else 0) - (j : ℝ) / M * L) := by ring
    rw [this, abs_neg]
    exact h
  -- sum over j
  have hgsum : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) = L * ((M : ℝ) - 1) / 2 := by
    have : ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
        (M : ℝ) * L - (L / M) * ∑ j ∈ Finset.Icc 1 M, (j : ℝ) := by
      rw [show ∑ j ∈ Finset.Icc 1 M, (L - ((j : ℝ) / M) * L) =
          ∑ j ∈ Finset.Icc 1 M, (L - L / M * (j : ℝ)) from
          Finset.sum_congr rfl (fun j _ => by ring)]
      rw [Finset.sum_sub_distrib, ← Finset.mul_sum, Finset.sum_const, Nat.card_Icc]
      simp only [nsmul_eq_mul, Nat.add_sub_cancel]
    rw [this, gauss_Icc]; field_simp; ring
  have hE : |∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
      L * ((M : ℝ) - 1) / 2| ≤ M * (ε / 4 * k) := by
    rw [← hgsum, ← Finset.sum_sub_distrib]
    calc _ ≤ ∑ j ∈ Finset.Icc 1 M, |∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) -
          (L - ((j : ℝ) / M) * L)| := Finset.abs_sum_le_sum_abs _ _
      _ ≤ ∑ j ∈ Finset.Icc 1 M, ε / 4 * k := Finset.sum_le_sum hinner
      _ = M * (ε / 4 * k) := by rw [Finset.sum_const, Nat.card_Icc]; simp
  -- bracket Σ f log p between Σ A log p and Σ A log p + L/M
  have hlo : ∑ p ∈ S, A p * Real.log p ≤ ∑ p ∈ S, f p * Real.log p :=
    Finset.sum_le_sum (fun p _ => mul_le_mul_of_nonneg_right (hA p).2 (hlog0 p))
  have hhi : ∑ p ∈ S, f p * Real.log p ≤ ∑ p ∈ S, A p * Real.log p + L / M := by
    rw [hLdef, Finset.sum_div, ← Finset.sum_add_distrib]
    apply Finset.sum_le_sum; intro p _
    have := (hA p).1
    have hl := hlog0 p
    have : f p * Real.log p ≤ (A p + 1 / M) * Real.log p :=
      mul_le_mul_of_nonneg_right (by linarith) hl
    linarith [show (A p + 1 / M) * Real.log p = A p * Real.log p + Real.log p / M by ring]
  have htarget : ∑ p ∈ S, (Int.fract ((n : ℝ) / p) - 1 / 2) * Real.log p =
      ∑ p ∈ S, f p * Real.log p - L / 2 := by
    rw [hLdef, Finset.sum_div, ← Finset.sum_sub_distrib]
    apply Finset.sum_congr rfl; intro p _; simp only [hf]; ring
  rw [htarget]
  have hAval : ∑ p ∈ S, A p * Real.log p =
      (1 / (M : ℝ)) * (∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0)) :=
    hswap
  set T := ∑ j ∈ Finset.Icc 1 M, ∑ p ∈ S, (if (j : ℝ) / M ≤ f p then Real.log p else 0) with hT
  have hE' := abs_le.1 hE
  have hLM : L / M ≤ 2 * k * (ε / 4) := by
    rw [div_eq_mul_one_div]
    exact mul_le_mul hL2 hinvM (by positivity) (by positivity)
  have hTM1 : (1 / (M : ℝ)) * T ≤ L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k := by
    rw [one_div_mul_eq_div, div_le_iff₀ hMr]
    have : (L * ((M : ℝ) - 1) / 2 / M + ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 + M * (ε / 4 * k) := by
      field_simp
    rw [this]; linarith [hE'.2]
  have hTM2 : L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k ≤ (1 / (M : ℝ)) * T := by
    rw [one_div_mul_eq_div, le_div_iff₀ hMr]
    have : (L * ((M : ℝ) - 1) / 2 / M - ε / 4 * k) * M = L * ((M : ℝ) - 1) / 2 - M * (ε / 4 * k) := by
      field_simp
    rw [this]; linarith [hE'.1]
  have hmid : L * ((M : ℝ) - 1) / 2 / M = L / 2 - L / M / 2 := by field_simp
  rw [abs_le]
  constructor <;> nlinarith [hLM, hlo, hhi, hTM1, hTM2, hmid, hAval, div_nonneg hL0 hMr.le]
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 →