medium-large range k²/log²k < n ≤ k^(2+21/40)/2

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 t1015-r; merged in 5039d3796f58 under attestations/000528.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--h2--h2--h2--h3/attempts/20261015T021346Z-t1015-r-partial.lean.

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

open scoped Nat

/-! Hole `h_mediumlarge` 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 noncomputable def Pprod (k : ℕ) (n : ℤ) : ℤ := ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ))

/-- The exponent `θ = 21/40`. -/
private noncomputable def theta : ℝ := 21 / 40

/-- The number of primes `p` (as positive integers) with `a < p < b`. -/
private noncomputable def primeCard (a b : ℝ) : ℕ :=
  ((Finset.Ioo ⌊a⌋ ⌈b⌉).filter
    (fun p : ℤ => 0 < p ∧ (p.natAbs).Prime ∧ a < (p : ℝ) ∧ (p : ℝ) < b)).card
private lemma theta_pos : (0 : ℝ) < theta := by unfold theta; norm_num
private lemma theta_lt_one : theta < 1 := by unfold theta; norm_num

/-- If a prime `p` divides one of the factors `n - i` with `1 ≤ i ≤ k`, then it
divides `P`. -/
private lemma dvd_Pprod_of_factor (k : ℕ) (n : ℤ) (p : ℤ) (i : ℕ)
    (hi : i ∈ Finset.Icc 1 k) (hp : p ∣ (n - (i : ℤ))) : p ∣ Pprod k n := by
  unfold Pprod
  exact hp.trans (Finset.dvd_prod_of_mem (fun i : ℕ => (n - (i : ℤ))) hi)

/-
If `p ∣ t` for some integer `t` strictly between `n - k` and `n`, then `p`
divides `P` (as `t` equals one of the factors `n - i`).
-/
private lemma dvd_Pprod_of_mem (k : ℕ) (n : ℤ) (p : ℤ) (t : ℤ)
    (h1 : n - (k : ℤ) < t) (h2 : t < n) (hpt : p ∣ t) : p ∣ Pprod k n := by
  convert dvd_Pprod_of_factor k n p ( Int.toNat ( n - t ) ) ?_ ?_ using 1 <;> norm_num [ Int.toNat_of_nonneg ( sub_nonneg.mpr h2.le ) ];
  · omega;
  · assumption

/-
If a prime `p ∈ (k, k + k^θ)` is such that `n/p` is far from any integer
(distance `≥ 1/k^{1-θ}`), then `p` divides `P`.
-/
private lemma dvd_from_far (k : ℕ) (n : ℤ) (p : ℕ) (hk1 : 1 ≤ k) (hp0 : 0 < p)
    (hkp : (k : ℝ) < p) (hpk : (p : ℝ) < (k : ℝ) + (k : ℝ) ^ theta)
    (hfar : 1 / (k : ℝ) ^ (1 - theta) ≤ |(n : ℝ) / (p : ℝ) - round ((n : ℝ) / (p : ℝ))|) :
    (p : ℤ) ∣ Pprod k n := by
  -- Set `i := n % (p : ℤ)` and `j := i.toNat`.
  set i := n % (p : ℤ)
  set j := i.toNat
  have hj : (j : ℤ) = i := by
    exact Int.toNat_of_nonneg <| Int.emod_nonneg _ <| by positivity;
  -- From `hfar`, we have `(p:ℝ)/(k:ℝ)^(1-theta) ≤ (min i (p-i) : ℝ)`.
  have h_frac : (p : ℝ) / (k : ℝ) ^ (1 - theta) ≤ min (i : ℝ) ((p : ℝ) - i) := by
    have h_frac : |(n : ℝ) / p - round ((n : ℝ) / p)| = min ((i : ℝ) / p) (1 - (i : ℝ) / p) := by
      have h_frac : Int.fract ((n : ℝ) / p) = (i : ℝ) / p := by
        rw [ Int.fract_eq_iff ];
        field_simp;
        norm_cast;
        exact ⟨ by norm_num; exact Int.emod_nonneg _ ( by positivity ), Int.emod_lt_of_pos _ ( by positivity ), n / p, by linarith [ Int.emod_add_mul_ediv n p ] ⟩;
      rw [ ← h_frac, abs_sub_round_eq_min ];
    have hp' : (0:ℝ) < p := by exact_mod_cast hp0
    have h1 := mul_le_mul_of_nonneg_left hfar hp'.le
    rw [h_frac, mul_min_of_nonneg _ _ hp'.le] at h1
    have e1 : (p:ℝ) * ((i:ℝ)/p) = i := by field_simp
    have e2 : (p:ℝ) * (1 - (i:ℝ)/p) = p - i := by field_simp
    rw [e1, e2] at h1
    calc (p:ℝ) / (k:ℝ)^(1-theta) = p * (1 / (k:ℝ)^(1-theta)) := by ring
      _ ≤ _ := h1
  -- So `1 ≤ i ≤ k`.
  have h_i_bounds : 1 ≤ i ∧ i ≤ k := by
    have h_i_bounds : (p : ℝ) / (k : ℝ) ^ (1 - theta) > (k : ℝ) ^ theta := by
      rw [ gt_iff_lt, lt_div_iff₀ ] <;> norm_num at *;
      · rw [ ← Real.rpow_add ] <;> norm_num ; linarith [ ( by norm_cast : ( k : ℝ ) + 1 ≤ p ) ];
        grind +extAll;
      · positivity;
    constructor <;> norm_num at *;
    · exact Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith [ show ( k : ℝ ) ^ theta ≥ 1 by exact Real.one_le_rpow ( mod_cast hk1 ) ( by exact div_nonneg ( by norm_num ) ( by norm_num ) ) ] );
    · exact Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith );
  convert dvd_Pprod_of_factor k n ( p : ℤ ) j _ _ using 1;
  · grind;
  · exact ⟨ n / p, by linarith [ Int.emod_add_mul_ediv n p ] ⟩

private noncomputable def badSet (k : ℕ) (n : ℤ) : Finset ℤ :=
  (Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ theta⌋ + 2)).filter
    (fun m : ℤ => (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧
      |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - theta))
private lemma exists_far_prime (k : ℕ) (n : ℤ) (hk1 : 1 ≤ k)
    (hcount : ((badSet k n).card : ℝ) < (primeCard (k : ℝ) ((k : ℝ) + (k : ℝ) ^ theta) : ℝ)) :
    ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧
      (p : ℤ) ∣ Pprod k n := by
  norm_cast at *;
  contrapose! hcount;
  refine' le_trans ( Finset.card_le_card _ ) _;
  exact Finset.image ( fun m : ℤ => m ) ( Finset.filter ( fun m : ℤ => ( m : ℝ ) < ( k : ℝ ) + ( k : ℝ ) ^ theta ∧ |( n : ℝ ) / m - round ( ( n : ℝ ) / m )| < 1 / ( k : ℝ ) ^ ( 1 - theta ) ) ( Finset.Ioo ( k : ℤ ) ( ( k : ℤ ) + ⌊ ( k : ℝ ) ^ theta⌋ + 2 ) ) );
  · intro p hp; simp_all +decide ;
    refine' ⟨ _, _ ⟩;
    · linarith [ show ⌈ ( k : ℝ ) ^ theta⌉ ≤ ⌊ ( k : ℝ ) ^ theta⌋ + 1 by exact Int.ceil_le_floor_add_one _ ];
    · exact Classical.not_not.1 fun h => hcount ( Int.natAbs p ) hp.2.2.1 ( by linarith [ abs_of_pos hp.2.1 ] ) ( by simpa [ abs_of_pos hp.2.1 ] using hp.2.2.2.2 ) ( by simpa [ abs_of_pos hp.2.1 ] using dvd_from_far k n ( Int.natAbs p ) hk1 ( by linarith [ abs_of_pos hp.2.1 ] ) ( by simpa [ abs_of_pos hp.2.1 ] using hp.2.2.2.1 ) ( by simpa [ abs_of_pos hp.2.1 ] using hp.2.2.2.2 ) ( by simpa [ abs_of_pos hp.2.1 ] using h ) );
  · unfold badSet; aesop;

/-
Core asymptotic fact: `(log x)^b · x^{-c} → 0` for `c > 0`.
-/
private lemma tendsto_log_rpow_mul_rpow_neg (b c : ℝ) (hc : 0 < c) :
    Filter.Tendsto (fun x : ℝ => (Real.log x) ^ b * x ^ (-c)) Filter.atTop (nhds 0) := by
  -- Use the fact that `Real.log x ^ b` is little-o of `x ^ c` as `x` tends to infinity.
  have h_log : (fun x : ℝ => Real.log x ^ b) =o[Filter.atTop] (fun x : ℝ => x ^ c) :=
    isLittleO_log_rpow_rpow_atTop b hc
  convert h_log.tendsto_div_nhds_zero.congr' _ using 1;
  filter_upwards [ Filter.eventually_gt_atTop 0 ] with x hx using by rw [ div_eq_mul_inv, Real.rpow_neg hx.le ] ;

/-
A sub-`tt` power times any log-power is eventually dominated by
`C · k^tt / log k`, for `C > 0` and `α < tt`.
-/
private lemma poly_log_lt (A α β tt : ℝ) (hα : α < tt) (C : ℝ) (hC : 0 < C) :
    ∀ᶠ k : ℕ in Filter.atTop,
      A * (k : ℝ) ^ α * (Real.log k) ^ β ≤ C * (k : ℝ) ^ tt / Real.log k := by
  -- Let's choose any $C > 0$ and derive a contradiction.
  have h_lim : Filter.Tendsto (fun k : ℕ => (A * (k : ℝ) ^ α * (Real.log k) ^ β) / ((k : ℝ) ^ tt / (Real.log k))) Filter.atTop (nhds 0) := by
    -- Simplify the expression inside the limit.
    suffices h_simp : Filter.Tendsto (fun k : ℕ => A * (Real.log k) ^ (β + 1) * (k : ℝ) ^ (α - tt)) Filter.atTop (nhds 0) by
      refine h_simp.congr' ?_;
      filter_upwards [ Filter.eventually_gt_atTop 1 ] with k hk ; rw [ Real.rpow_sub ( by positivity ) ] ; ring_nf;
      rw [ Real.rpow_add ( Real.log_pos ( Nat.one_lt_cast.mpr hk ) ), Real.rpow_one ] ; norm_num ; ring;
    have := @tendsto_log_rpow_mul_rpow_neg ( β + 1 ) ( tt - α ) ?_;
    · convert this.const_mul A |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop using 2 <;> norm_num ; ring;
    · linarith;
  filter_upwards [ h_lim.eventually ( gt_mem_nhds hC ), Filter.eventually_gt_atTop 1 ] with k hk₁ hk₂;
  rw [ div_lt_iff₀ ( div_pos ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr hk₂.le ) _ ) ( Real.log_pos ( Nat.one_lt_cast.mpr hk₂ ) ) ) ] at hk₁ ; ring_nf at hk₁ ⊢ ; linarith

/-
The `θ`-power times `(log k)^{-2}` is eventually dominated by `C · k^tt / log k`.
-/
private lemma poly_log_lt_eq (A tt : ℝ) (C : ℝ) (hC : 0 < C) :
    ∀ᶠ k : ℕ in Filter.atTop,
      A * (k : ℝ) ^ tt * (Real.log k) ^ (-(2 : ℝ)) ≤ C * (k : ℝ) ^ tt / Real.log k := by
  -- We'll use that $A \leq C \cdot \log k$ for sufficiently large $k$.
  have h_log_bound : ∀ᶠ k : ℕ in Filter.atTop, A ≤ C * Real.log k := by
    exact Filter.eventually_atTop.mpr ⟨ ⌈Real.exp ( A / C ) ⌉₊ + 1, fun k hk => by nlinarith [ Nat.le_ceil ( Real.exp ( A / C ) ), Real.log_exp ( A / C ), Real.log_le_log ( by positivity ) ( show ( k :ℝ ) ≥ Real.exp ( A / C ) by exact le_of_lt ( Nat.lt_of_ceil_lt hk ) ), mul_div_cancel₀ A hC.ne' ] ⟩;
  filter_upwards [ h_log_bound, Filter.eventually_gt_atTop 1 ] with k hk₁ hk₂;
  have hl : 0 < Real.log k := Real.log_pos (by exact_mod_cast hk₂)
  have hp : 0 ≤ (k:ℝ)^tt := Real.rpow_nonneg (Nat.cast_nonneg _) _
  rw [Real.rpow_neg hl.le, Real.rpow_two]
  have e : A * (k:ℝ)^tt * (Real.log k ^ 2)⁻¹ = A * (k:ℝ)^tt / Real.log k / Real.log k := by
    field_simp
  rw [e, div_le_div_iff_of_pos_right hl, div_le_iff₀ hl]
  nlinarith [mul_le_mul_of_nonneg_right hk₁ hp]

/-
The `tt`-power times `(log k)^β` with `β < -1` is eventually dominated by
`C · k^tt / log k`.
-/
private lemma poly_log_lt_logpow (A tt β : ℝ) (hβ : β < -1) (C : ℝ) (hC : 0 < C) :
    ∀ᶠ k : ℕ in Filter.atTop,
      A * (k : ℝ) ^ tt * (Real.log k) ^ β ≤ C * (k : ℝ) ^ tt / Real.log k := by
  have h_log_pow : Filter.Tendsto (fun k : ℕ => A * (Real.log k) ^ (β + 1)) Filter.atTop (nhds 0) := by
    simpa using tendsto_const_nhds.mul ( tendsto_rpow_neg_atTop ( by linarith : 0 < - ( β + 1 ) ) |> Filter.Tendsto.comp <| Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop );
  filter_upwards [ h_log_pow.eventually ( gt_mem_nhds hC ), Filter.eventually_gt_atTop 1 ] with k hk₁ hk₂ ; rw [ le_div_iff₀ ( Real.log_pos <| Nat.one_lt_cast.mpr hk₂ ) ] ; ring_nf at *;
  convert mul_le_mul_of_nonneg_left hk₁.le ( Real.rpow_nonneg ( Nat.cast_nonneg k ) tt ) using 1 ; rw [ show ( 1 + β ) = β + 1 by ring, Real.rpow_add ( Real.log_pos <| Nat.one_lt_cast.mpr hk₂ ), Real.rpow_one ] ; ring

/-
If the count of primes in `(a, b)` is positive, there is a prime in `(a, b)`.
-/
private lemma konyagin_finish (k : ℕ) (n : ℤ) (hk1 : 1 ≤ k) (C : ℝ)
    (hbhp : C * (k : ℝ) ^ theta / Real.log k ≤
      (primeCard (k : ℝ) ((k : ℝ) + (k : ℝ) ^ theta) : ℝ))
    (hcard : ((badSet k n).card : ℝ) < C * (k : ℝ) ^ theta / Real.log k) :
    ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + 3 * (k : ℝ) ^ theta ∧
      (p : ℤ) ∣ Pprod k n := by
  obtain ⟨p, hp, hpk, hpb, hdvd⟩ := exists_far_prime k n hk1 (lt_of_lt_of_le hcard hbhp)
  refine ⟨p, hp, hpk, ?_, hdvd⟩
  have : (0 : ℝ) ≤ (k : ℝ) ^ theta := Real.rpow_nonneg (by positivity) _
  linarith

private lemma eventually_le_rpow (p A : ℝ) (hp : 0 < p) :
    ∀ᶠ k : ℕ in Filter.atTop, A ≤ (k : ℝ) ^ p := by
  exact Filter.Tendsto.eventually_ge_atTop ( tendsto_rpow_atTop hp |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop ) A

private noncomputable def lamML (k : ℕ) (n : ℤ) : ℝ := Real.sqrt ((k : ℝ) ^ (2 + theta) / (2 * (n : ℝ))) * Real.log k

/-- An `n`-free upper bound for `lamML` on the medium-large range. -/
private noncomputable def lamUB (k : ℕ) : ℝ := (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2

private noncomputable def g_ml (k : ℕ) : ℝ :=
  (65536 : ℝ) * (k : ℝ) ^ theta * (
    ((k : ℝ) ^ (theta - 1) * (Real.log k) ^ 2) ^ ((1 : ℝ) / 3) +
    (Real.log k) ^ (-(2 : ℝ)) +
    (3 * lamUB k / (k : ℝ)) ^ ((1 : ℝ) / 4)) + 4 * lamUB k

private lemma log_sq_lt_self : ∀ᶠ k : ℕ in Filter.atTop, (Real.log k) ^ 2 < (k : ℝ) := by
  have h_log_sq_lt_k : Filter.Tendsto (fun k : ℕ => (Real.log k) ^ 2 / (k : ℝ)) Filter.atTop (nhds 0) := by
    have h_log_sq_lt_k : Filter.Tendsto (fun x : ℝ => (Real.log x) ^ 2 / x) Filter.atTop (nhds 0) := by
      convert tendsto_log_rpow_mul_rpow_neg 2 1 ( by norm_num ) using 2 ; norm_num;
      rw [ Real.rpow_neg_one, div_eq_mul_inv ];
    exact h_log_sq_lt_k.comp tendsto_natCast_atTop_atTop;
  filter_upwards [ h_log_sq_lt_k.eventually ( gt_mem_nhds zero_lt_one ), Filter.eventually_gt_atTop 0 ] with k hk₁ hk₂ using by rw [ div_lt_one ( by positivity ) ] at hk₁; exact hk₁;

/-
On the medium-large range, `lamML ≥ 1`.
-/
private lemma lamML_ge_one (k : ℕ) (n : ℤ) (hk : 3 ≤ k) (hnpos : 0 < n)
    (hn : (n : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (2 + theta)) : 1 ≤ lamML k n := by
  refine' one_le_mul_of_one_le_of_one_le ( Real.le_sqrt_of_sq_le _ ) ( Real.le_log_iff_exp_le _ |>.2 _ );
  · rw [ le_div_iff₀ ] <;> first | positivity | linarith;
  · positivity;
  · exact le_trans ( Real.exp_one_lt_d9.le ) ( by norm_num; linarith [ show ( k : ℝ ) ≥ 3 by norm_cast ] )

/-
On the medium-large range, `lamML ≤ lamUB`.
-/
private lemma lamML_le_lamUB (k : ℕ) (n : ℤ) (hk : 2 ≤ k)
    (hn : (k : ℝ) ^ 2 / (Real.log k) ^ 2 < (n : ℝ)) : lamML k n ≤ lamUB k := by
  have h_lamML : Real.sqrt ((k : ℝ) ^ (2 + theta) / (2 * (n : ℝ))) ≤ (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * Real.log k := by
    have h_sqrt : (k : ℝ) ^ (2 + theta) / (2 * (n : ℝ)) ≤ (k : ℝ) ^ theta * (Real.log k) ^ 2 / 2 := by
      rw [ div_le_iff₀ ] <;> norm_num [ Real.rpow_add ( by positivity : 0 < ( k : ℝ ) ) ] at *;
      · rw [ div_lt_iff₀ ] at hn <;> nlinarith [ show 0 < ( k : ℝ ) ^ theta by positivity, show 0 < ( Real.log k ) ^ 2 by exact sq_pos_of_pos <| Real.log_pos <| Nat.one_lt_cast.mpr hk ];
      · exact_mod_cast hn.trans_le' ( div_nonneg ( sq_nonneg _ ) ( sq_nonneg _ ) );
    convert Real.sqrt_le_sqrt h_sqrt using 1 ; norm_num [ Real.sqrt_div_self ] ; ring_nf;
    rw [ Real.sqrt_mul ( by positivity ), Real.sqrt_sq ( by positivity ), Real.sqrt_eq_rpow, Real.sqrt_eq_rpow, ← Real.rpow_mul ( by positivity ) ] ; ring;
  unfold lamML lamUB
  have hl := mul_le_mul_of_nonneg_right h_lamML ( Real.log_nonneg <| Nat.one_le_cast.mpr <| by linarith )
  calc _ ≤ _ := hl
    _ = _ := by ring

/-
`lamML^2 = k^{2+θ}/(2n) · (log k)^2`.
-/
private lemma lamML_sq (k : ℕ) (n : ℤ) (hn0 : 0 < n) :
    (lamML k n) ^ 2 = (k : ℝ) ^ (2 + theta) / (2 * (n : ℝ)) * (Real.log k) ^ 2 := by
  unfold lamML
  rw [mul_pow, Real.sq_sqrt (by positivity)]

private lemma ml_card_bound (hK : ∀ (lam : ℝ), 1 ≤ lam → ∀ (n : ℤ) (k r : ℕ), (k : ℤ) < n → 2 ≤ r →
      (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - theta) →
      (((Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ theta⌋ + 2)).filter
        (fun m : ℤ => (k : ℤ) < m ∧ (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧
          |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - theta))).card : ℝ)
      < (65536 : ℝ) * (k : ℝ) ^ theta *
          (((n : ℝ) * (Nat.factorial r : ℝ) * lam ^ r / (k : ℝ) ^ (r + 1)) ^ ((2 * (r : ℝ) - 1)⁻¹) +
           ((k : ℝ) ^ ((r : ℝ) + theta) / ((n : ℝ) * (Nat.factorial r : ℝ) * lam ^ r)) ^ (((r : ℝ) - 1)⁻¹) +
           (((r : ℝ) + 1) * lam / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹)) +
        2 * (r : ℝ) * lam) : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
    (k : ℝ) ^ 2 / (Real.log k) ^ 2 < (n : ℝ) →
    (n : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (2 + theta) →
    ((badSet k n).card : ℝ) < g_ml k := by
      obtain ⟨k₀, hk₀⟩ : ∃ k₀ : ℕ, ∀ k ≥ k₀, 2 ≤ (1 / 2) * (k : ℝ) ^ (1 - theta) ∧ (Real.log k) ^ 2 < k ∧ 3 ≤ k := by
        obtain ⟨k₁, hk₁⟩ : ∃ k₁ : ℕ, ∀ k ≥ k₁, 2 ≤ (1 / 2) * (k : ℝ) ^ (1 - theta) := by
          have := @eventually_le_rpow ( 1 - theta ) 4 ( by norm_num [ theta ] );
          exact Filter.eventually_atTop.mp ( this.mono fun k hk => by linarith )
        obtain ⟨k₂, hk₂⟩ : ∃ k₂ : ℕ, ∀ k ≥ k₂, (Real.log k) ^ 2 < k := by
          exact Filter.eventually_atTop.mp ( log_sq_lt_self )
        use max k₁ (max k₂ 3);
        exact fun k hk => ⟨ hk₁ k ( le_trans ( le_max_left _ _ ) hk ), hk₂ k ( le_trans ( le_max_of_le_right ( le_max_left _ _ ) ) hk ), le_trans ( le_max_of_le_right ( le_max_right _ _ ) ) hk ⟩;
      refine' ⟨ k₀ + 3, fun k hk n hn₁ hn₂ => _ ⟩;
      have hKon : ((badSet k n).card : ℝ) < (65536 : ℝ) * (k : ℝ) ^ theta * (((n : ℝ) * ((2 : ℕ)!) * (lamML k n) ^ 2 / (k : ℝ) ^ (2 + 1)) ^ ((1 : ℝ) / 3) + ((k : ℝ) ^ ((2 : ℝ) + theta) / ((n : ℝ) * ((2 : ℕ)!) * (lamML k n) ^ 2)) ^ 1 + ((3 * lamML k n) / (k : ℝ)) ^ ((1 : ℝ) / 4)) + 2 * (2 : ℝ) * (lamML k n) := by
        have hbS : badSet k n = (Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ theta⌋ + 2)).filter
            (fun m : ℤ => (k : ℤ) < m ∧ (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧
              |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - theta)) := by
          simp only [badSet]
          apply Finset.filter_congr
          intro x hx
          rw [Finset.mem_Ioo] at hx
          exact ⟨fun h => ⟨hx.1, h⟩, fun h => h.2⟩
        rw [hbS]
        convert hK ( lamML k n ) ( lamML_ge_one k n ( by linarith [ hk₀ k ( by linarith ) ] ) ( by
          exact_mod_cast hn₁.trans_le' ( div_nonneg ( sq_nonneg _ ) ( sq_nonneg _ ) ) ) ( by
          exact hn₂ ) ) n k 2 ( by
          rw [ div_lt_iff₀ ] at hn₁;
          · exact_mod_cast ( by nlinarith [ hk₀ k ( by linarith ), show ( k : ℝ ) ≥ 3 by norm_cast; linarith ] : ( k : ℝ ) < n );
          · exact sq_pos_of_pos <| Real.log_pos <| Nat.one_lt_cast.mpr <| by linarith [ hk₀ k <| by linarith ] ; ) ( by norm_num ) ( by
          exact hk₀ k ( by linarith ) |>.1 ) using 1 ; norm_num [ Nat.factorial ];
      have hT1 : ((n : ℝ) * ((2 : ℕ)!) * (lamML k n) ^ 2 / (k : ℝ) ^ (2 + 1)) ^ ((1 : ℝ) / 3) = ((k : ℝ) ^ (theta - 1) * (Real.log k) ^ 2) ^ ((1 : ℝ) / 3) := by
        have hT1 : (n : ℝ) * ((2 : ℕ)!) * (lamML k n) ^ 2 = (k : ℝ) ^ (2 + theta) * (Real.log k) ^ 2 := by
          rw [ lamML_sq ] ; ring_nf;
          · simp +decide [ mul_comm, show n ≠ 0 by rintro rfl; exact absurd hn₁ ( by norm_num; positivity ) ];
          · exact_mod_cast hn₁.trans_le' ( div_nonneg ( sq_nonneg _ ) ( sq_nonneg _ ) );
        rw [ hT1, mul_div_right_comm ];
        rw [ ← Real.rpow_natCast, ← Real.rpow_sub ( by norm_cast; linarith ) ] ; ring_nf
      have hT2 : ((k : ℝ) ^ ((2 : ℝ) + theta) / ((n : ℝ) * ((2 : ℕ)!) * (lamML k n) ^ 2)) ^ 1 = (Real.log k) ^ (-(2 : ℝ)) := by
        rw [ show ( n : ℝ ) * 2! * lamML k n ^ 2 = ( k : ℝ ) ^ ( 2 + theta ) * ( Real.log k ) ^ 2 by
              rw [ lamML_sq ] ; ring_nf;
              · by_cases hn : n = 0 <;> simp_all +decide [ mul_comm ];
                exact absurd hT1 ( ne_of_lt ( Real.rpow_pos_of_pos ( mul_pos ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr ( by linarith ) ) _ ) ( sq_pos_of_pos ( Real.log_pos ( Nat.one_lt_cast.mpr ( by linarith [ hk₀ k ( by linarith ) ] ) ) ) ) ) _ ) );
              · exact_mod_cast hn₁.trans_le' ( div_nonneg ( sq_nonneg _ ) ( sq_nonneg _ ) ) ] ; norm_cast ; norm_num;
        rw [ ← div_div, div_self ( by exact ne_of_gt ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr ( by linarith ) ) _ ) ), one_div ]
      have hT3 : ((3 * lamML k n) / (k : ℝ)) ^ ((1 : ℝ) / 4) ≤ (3 * lamUB k / (k : ℝ)) ^ ((1 : ℝ) / 4) := by
        gcongr;
        · exact div_nonneg ( mul_nonneg zero_le_three ( show 0 ≤ lamML k n from mul_nonneg ( Real.sqrt_nonneg _ ) ( Real.log_natCast_nonneg _ ) ) ) ( Nat.cast_nonneg _ );
        · have h := lamML_le_lamUB k n ( by linarith ) hn₁; gcongr
      have hLast : 2 * (2 : ℝ) * (lamML k n) ≤ 4 * (lamUB k) := by
        have := lamML_le_lamUB k n ( by linarith ) hn₁; norm_num at *; linarith;
      unfold g_ml; nlinarith [ show 0 < (65536 : ℝ) * ( k : ℝ ) ^ theta by exact mul_pos ( by exact lt_of_lt_of_le ( by norm_num ) ( show ( 256 : ℝ ) ≤ (65536 : ℝ) by norm_num ) ) ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr <| by linarith ) _ ) ] ;
/-
The medium-large bound `g_ml` is eventually dominated by `C · k^θ / log k`.
-/
private lemma ml_rhs_le (C : ℝ) (hC : 0 < C) :
    ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → g_ml k ≤ C * (k : ℝ) ^ theta / Real.log k := by
  obtain ⟨k₁, hk₁⟩ : ∃ k₁ : ℕ, ∀ k : ℕ, k₁ ≤ k → ((65536 : ℝ) * (k : ℝ) ^ theta * ((k : ℝ) ^ (theta - 1) * (Real.log k) ^ 2) ^ ((1 : ℝ) / 3)) ≤ C / 4 * (k : ℝ) ^ theta / Real.log k := by
    have h_poly_log : ∀ᶠ k : ℕ in Filter.atTop, (65536 : ℝ) * (k : ℝ) ^ ((4 * theta - 1) / 3 : ℝ) * (Real.log k) ^ (2 / 3 : ℝ) ≤ C / 4 * (k : ℝ) ^ theta / Real.log k := by
      have := poly_log_lt (65536 : ℝ) ( ( 4 * theta - 1 ) / 3 ) ( 2 / 3 ) theta ?_ ( C / 4 ) ( by linarith ) <;> norm_num at *;
      · exact this;
      · unfold theta; norm_num;
    obtain ⟨ k₁, hk₁ ⟩ := Filter.eventually_atTop.mp h_poly_log;
    refine' ⟨ k₁ + 2, fun k hk => le_trans _ ( hk₁ k ( by linarith ) ) ⟩ ; norm_num [ Real.rpow_def_of_pos, show k > 0 by linarith ] ; ring_nf ; norm_num;
    rw [ Real.mul_rpow ( by positivity ) ( by positivity ), ← Real.exp_mul ] ; ring_nf ; norm_num [ Real.exp_add, Real.exp_neg, Real.exp_mul, Real.exp_log ( show 0 < ( k : ℝ ) by norm_cast; linarith ) ] ; ring_nf ; norm_num;
    rw [ ← Real.rpow_natCast, ← Real.rpow_mul ( by positivity ) ] ; ring_nf ; norm_num [ ← Real.rpow_mul ( Nat.cast_nonneg _ ), ← Real.rpow_neg ( Nat.cast_nonneg _ ) ] ; ring_nf ; norm_num;
    rw [ show ( theta * ( 4 / 3 ) : ℝ ) = theta + theta * ( 1 / 3 ) by ring, Real.rpow_add ( by norm_cast; linarith ) ] ; ring_nf ; norm_num;
  -- Apply the asymptotic lemmas to get the bounds for E2, E3, and E4.
  obtain ⟨k₂, hk₂⟩ : ∃ k₂ : ℕ, ∀ k : ℕ, k₂ ≤ k → (65536 : ℝ) * (k : ℝ) ^ theta * (Real.log k) ^ (-(2 : ℝ)) ≤ C / 4 * (k : ℝ) ^ theta / Real.log k := by
    have := poly_log_lt_eq (65536 : ℝ) theta ( C / 4 ) ( by linarith );
    exact Filter.eventually_atTop.mp this;
  obtain ⟨k₃, hk₃⟩ : ∃ k₃ : ℕ, ∀ k : ℕ, k₃ ≤ k → (65536 : ℝ) * (k : ℝ) ^ theta * (3 * (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2 / (k : ℝ)) ^ (1 / 4 : ℝ) ≤ C / 4 * (k : ℝ) ^ theta / Real.log k := by
    have := poly_log_lt ( (65536 : ℝ) * ( 3 * ( 1 / Real.sqrt 2 ) ) ^ ( 1 / 4 : ℝ ) ) ( ( 9 * theta - 2 ) / 8 ) ( 1 / 2 ) theta ?_ ( C / 4 ) ( by linarith ) <;> norm_num at *;
    · obtain ⟨ k₃, hk₃ ⟩ := this; use k₃ + 2; intros k hk; convert hk₃ k ( by linarith ) using 1; rw [ Real.div_rpow ( by positivity ) ( by positivity ), Real.mul_rpow ( by positivity ) ( by positivity ), Real.mul_rpow ( by positivity ) ( by positivity ) ] ; ring_nf;
      rw [ ← Real.rpow_mul ( by positivity ), ← Real.rpow_natCast, ← Real.rpow_mul ( by positivity ) ] ; ring_nf;
      rw [ show ( -1 / 4 + theta * ( 9 / 8 ) : ℝ ) = theta + theta * ( 1 / 8 ) - 1 / 4 by ring ] ; norm_num [ Real.rpow_add ( by norm_cast; linarith : 0 < ( k : ℝ ) ), Real.rpow_sub ( by norm_cast; linarith : 0 < ( k : ℝ ) ) ] ; ring;
    · unfold theta; norm_num;
  obtain ⟨k₄, hk₄⟩ : ∃ k₄ : ℕ, ∀ k : ℕ, k₄ ≤ k → 4 * (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2 ≤ C / 4 * (k : ℝ) ^ theta / Real.log k := by
    have := poly_log_lt ( 4 * ( 1 / Real.sqrt 2 ) ) ( theta / 2 ) 2 theta ?_ ( C / 4 ) ?_ <;> norm_num at *;
    · exact this;
    · linarith [theta_pos];
    · positivity;
  refine ⟨max k₁ (max k₂ (max k₃ k₄)), fun k hk => ?_⟩
  have a1 := hk₁ k (le_trans (le_max_left _ _) hk)
  have a2 := hk₂ k (le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk)
  have a3 := hk₃ k (le_trans (le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) (le_max_right _ _)) hk)
  have a4 := hk₄ k (le_trans (le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) (le_max_right _ _)) hk)
  have e3 : (3 * lamUB k / (k:ℝ)) = 3 * (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2 / (k : ℝ) := by
    unfold lamUB; ring
  have e4 : 4 * lamUB k = 4 * (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2 := by
    unfold lamUB; ring
  unfold g_ml
  rw [e3, e4]
  have e : C * (k:ℝ)^theta / Real.log k = 4 * (C/4 * (k:ℝ)^theta / Real.log k) := by ring
  have ex : (65536 : ℝ) * (k : ℝ) ^ theta * (((k : ℝ) ^ (theta - 1) * (Real.log k) ^ 2) ^ ((1 : ℝ) / 3) +
      (Real.log k) ^ (-(2 : ℝ)) + (3 * (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2 / (k : ℝ)) ^ ((1 : ℝ) / 4))
      = (65536 : ℝ) * (k : ℝ) ^ theta * ((k : ℝ) ^ (theta - 1) * (Real.log k) ^ 2) ^ ((1 : ℝ) / 3) +
        (65536 : ℝ) * (k : ℝ) ^ theta * (Real.log k) ^ (-(2 : ℝ)) +
        (65536 : ℝ) * (k : ℝ) ^ theta * (3 * (1 / Real.sqrt 2) * (k : ℝ) ^ (theta / 2) * (Real.log k) ^ 2 / (k : ℝ)) ^ ((1 : ℝ) / 4) := by ring
  linarith

theorem erdos_1094__h2__h2__h2__h3 : (¬∃ (C : ℝ),
      (0 : ℝ) < C ∧
        ∃ (k₀ : ℕ),
          ∀ (k : ℕ),
            k₀ ≤ k →
              C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
                (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                        (0 : ℤ) < p ∧
                          Nat.Prime p.natAbs ∧
                            (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
                  ℝ)) ∨
  ∃ (k₀ : ℕ),
    ∀ (k : ℕ),
      k₀ ≤ k →
        ∀ (n : ℤ),
          (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) →
            (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) →
              ∃ (p : ℕ),
                Nat.Prime p ∧
                  (↑k : ℝ) < (↑p : ℝ) ∧
                    (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
                      (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
  have h_kon : ∀ (lam : ℝ), 1 ≤ lam → ∀ (n : ℤ) (k r : ℕ), (k : ℤ) < n → 2 ≤ r →
      (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - (21 / 40 : ℝ)) →
      (((Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ (21 / 40 : ℝ)⌋ + 2)).filter
        (fun m : ℤ => (k : ℤ) < m ∧ (m : ℝ) < (k : ℝ) + (k : ℝ) ^ (21 / 40 : ℝ) ∧
          |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - (21 / 40 : ℝ)))).card : ℝ)
      < (65536 : ℝ) * (k : ℝ) ^ (21 / 40 : ℝ) *
          (((n : ℝ) * (Nat.factorial r : ℝ) * lam ^ r / (k : ℝ) ^ (r + 1)) ^ ((2 * (r : ℝ) - 1)⁻¹) +
           ((k : ℝ) ^ ((r : ℝ) + (21 / 40 : ℝ)) / ((n : ℝ) * (Nat.factorial r : ℝ) * lam ^ r)) ^ (((r : ℝ) - 1)⁻¹) +
           (((r : ℝ) + 1) * lam / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹)) +
        2 * (r : ℝ) * lam := by
    sorry
  by_cases hB0 : ∃ (C : ℝ),
      (0 : ℝ) < C ∧
        ∃ (k₀ : ℕ),
          ∀ (k : ℕ),
            k₀ ≤ k →
              C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
                (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                        (0 : ℤ) < p ∧
                          Nat.Prime p.natAbs ∧
                            (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
                  ℝ)
  swap
  · exact Or.inl hB0
  refine Or.inr ?_
  obtain ⟨C, hC, kb, hb⟩ := hB0
  obtain ⟨k1, hk1card⟩ := ml_card_bound h_kon
  obtain ⟨k2, hk2rhs⟩ := ml_rhs_le C hC
  refine ⟨max (max kb k1) (max k2 2), ?_⟩
  intro k hk n hlow hhigh
  have hkb : kb ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk
  have hki1 : k1 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk
  have hki2 : k2 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk2le : 2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk
  have hk1 : 1 ≤ k := by omega
  have hbhp : C * (k : ℝ) ^ theta / Real.log k ≤
      (primeCard (k : ℝ) ((k : ℝ) + (k : ℝ) ^ theta) : ℝ) := hb k hkb
  have hcard : ((badSet k n).card : ℝ) < C * (k : ℝ) ^ theta / Real.log k :=
    lt_of_lt_of_le (hk1card k hki1 n hlow hhigh) (hk2rhs k hki2)
  exact konyagin_finish k n hk1 C hbhp hcard