large range up to exp(log²k/(20 log log k))

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-q; merged in 442912b27e19 under attestations/000529.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--h4/attempts/20261015T023100Z-t1015-q-partial.lean.

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

open scoped Nat

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

/-- The product `(n-k)(n-k+1)⋯(n-1) = ∏_{i=1}^{k} (n - i)`. -/
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 ] ⟩

/-- The set of integers `m ∈ (k, k + k^θ)` such that `n/m` is within `1/k^{1-θ}`
of an integer. Its cardinality is exactly the quantity `K` bounded by
`konyagin_application`. -/
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 c₉ : ℝ := 256
private noncomputable def K_const : ℝ := max 4 c₉
private noncomputable def B_const : ℝ := 16 * K_const
private noncomputable def C₀_const : ℝ := 4 * B_const
private noncomputable def c₆ : ℝ := 4 * C₀_const

private noncomputable def KonHole : Prop :=
  ∀ (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

private lemma kon_of_hole (hK : KonHole)

    (lam th : ℝ) (hlam : 1 ≤ lam) (hth0 : 0 < th) (hth1 : th < 1) (hth : th = theta)
    (n : ℤ) (k r : ℕ) (hkn : (k : ℤ) < n) (hr2 : 2 ≤ r)
    (hr_le : (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - th)) :
    (((Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ th⌋ + 2)).filter
        (fun m : ℤ => (m : ℝ) < (k : ℝ) + (k : ℝ) ^ th ∧
          |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - th))).card : ℝ)
      < c₆ * (k : ℝ) ^ th *
          (((n : ℝ) * (r ! : ℝ) * lam ^ r / (k : ℝ) ^ (r + 1)) ^ ((2 * (r : ℝ) - 1)⁻¹) +
           ((k : ℝ) ^ ((r : ℝ) + th) / ((n : ℝ) * (r ! : ℝ) * lam ^ r)) ^ (((r : ℝ) - 1)⁻¹) +
           (((r : ℝ) + 1) * lam / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹)) +
        2 * (r : ℝ) * lam := by
  subst hth
  have h := hK lam hlam n k r hkn hr2 hr_le
  have e : c₆ = 65536 := by unfold c₆ C₀_const B_const K_const c₉; norm_num
  rw [e]
  have hf : ((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 : ℝ)))) =
      ((Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ (21 / 40 : ℝ)⌋ + 2)).filter
      (fun m : ℤ => (m : ℝ) < (k : ℝ) + (k : ℝ) ^ (21 / 40 : ℝ) ∧
        |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - (21 / 40 : ℝ)))) :=
    Finset.filter_congr (fun m hm => by simp [(Finset.mem_Ioo.1 hm).1])
  rw [hf] at h
  exact h

private noncomputable def BHP : Prop := ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
    C * (k : ℝ) ^ theta / Real.log k ≤ (primeCard (k : ℝ) ((k : ℝ) + (k : ℝ) ^ theta) : ℝ)


/-! ### Large case machinery (Konyagin with variable `r`) -/

/-- The exponent `E₁ = (1-θ)(2r-1)/(3r-2)`. -/
private noncomputable def E1exp (r : ℕ) : ℝ := (1 - theta) * (2 * (r : ℝ) - 1) / (3 * (r : ℝ) - 2)

/-- The Konyagin parameter `λ` for the large range. -/
private noncomputable def lamLarge (k : ℕ) (n : ℤ) (r : ℕ) : ℝ :=
  ((k : ℝ) ^ ((r : ℝ) + 1 - E1exp r) / ((n : ℝ) * (Nat.factorial r : ℝ))) ^ ((1 : ℝ) / (r : ℝ))

/-
`λ^r = k^{r+1-E₁}/(n r!)`.
-/
private lemma lamLarge_pow (k : ℕ) (n : ℤ) (r : ℕ) (hn0 : 0 < n) (hk0 : 0 < k) (hr1 : 1 ≤ r) :
    (lamLarge k n r) ^ r =
      (k : ℝ) ^ ((r : ℝ) + 1 - E1exp r) / ((n : ℝ) * (Nat.factorial r : ℝ)) := by
  unfold lamLarge; rw [ ← Real.rpow_natCast, ← Real.rpow_mul ( ?_ ) ] ; norm_num [ show r ≠ 0 by linarith ] ;
  positivity

/-
`λ ≥ 1` on the large range.
-/
private lemma lamLarge_ge_one (k : ℕ) (n : ℤ) (r : ℕ) (hn0 : 0 < n) (hk : 1 < k) (hr3 : 3 ≤ r)
    (hub : (n : ℝ) * (Nat.factorial r : ℝ) ≤ (k : ℝ) ^ ((r : ℝ) + theta)) :
    1 ≤ lamLarge k n r := by
  refine' Real.one_le_rpow _ _;
  · rw [ one_le_div ];
    · refine' le_trans hub ( Real.rpow_le_rpow_of_exponent_le ( mod_cast hk.le ) _ );
      unfold E1exp; rw [ le_sub_comm ] ; rw [ div_le_iff₀ ] <;> nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast, show ( theta : ℝ ) < 1 by exact_mod_cast theta_lt_one ] ;
    · positivity;
  · positivity

/-
`λ < k^{(2-θ)/r}` from minimality of `r`.
-/
private lemma lamLarge_lt (k : ℕ) (n : ℤ) (r : ℕ) (hn0 : 0 < n) (hk : 1 < k) (hr3 : 3 ≤ r)
    (hmin : (k : ℝ) ^ (((r : ℝ) - 1) + theta) < (n : ℝ) * (Nat.factorial (r - 1) : ℝ)) :
    lamLarge k n r < (k : ℝ) ^ ((2 - theta) / (r : ℝ)) := by
  refine' lt_of_lt_of_le ( Real.rpow_lt_rpow ( _ ) _ ( by positivity ) ) _;
  exact ( k : ℝ ) ^ ( 2 - E1exp r - theta );
  · positivity;
  · rw [ div_lt_iff₀ ( by positivity ) ];
    refine' lt_of_le_of_lt _ ( mul_lt_mul_of_pos_left ( show ( n : ℝ ) * r.factorial > k ^ ( r - 1 + theta ) * r from _ ) ( by positivity ) );
    · rw [ ← mul_assoc, ← Real.rpow_add ( by positivity ) ] ; ring_nf;
      exact le_mul_of_one_le_left ( by positivity ) ( by norm_cast; linarith );
    · rcases r <;> simp_all +decide [ Nat.factorial_succ ];
      nlinarith [ show ( k : ℝ ) ^ ( ( ↑‹ℕ› : ℝ ) + theta ) > 0 by positivity ];
  · rw [ ← Real.rpow_mul ( by positivity ) ] ; ring_nf;
    exact Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) ( by nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast, inv_pos.mpr ( by positivity : 0 < ( r : ℝ ) ), mul_inv_cancel₀ ( by positivity : ( r : ℝ ) ≠ 0 ), show ( E1exp r : ℝ ) ≥ 0 by exact div_nonneg ( mul_nonneg ( sub_nonneg.mpr <| by linarith [ show ( theta : ℝ ) ≤ 1 by exact le_of_lt <| by norm_num [ theta ] ] ) <| by linarith [ show ( r : ℝ ) ≥ 3 by norm_cast ] ) <| by linarith [ show ( r : ℝ ) ≥ 3 by norm_cast ] ] )

/-
Konyagin's theorem with the balanced choice of `λ` makes the first two terms
equal to `k^{(θ-1)/(3r-2)}`.
-/
private lemma large_card_raw (hK : KonHole) (k : ℕ) (n : ℤ) (r : ℕ) (hk : 1 < k) (hn0 : 0 < n) (hr3 : 3 ≤ r)
    (hrle : (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - theta)) (hkn : (k : ℤ) < n)
    (hub : (n : ℝ) * (Nat.factorial r : ℝ) ≤ (k : ℝ) ^ ((r : ℝ) + theta)) :
    ((badSet k n).card : ℝ) <
      c₆ * (k : ℝ) ^ theta *
        (2 * (k : ℝ) ^ ((theta - 1) / (3 * (r : ℝ) - 2)) +
          (((r : ℝ) + 1) * lamLarge k n r / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹)) +
      2 * (r : ℝ) * lamLarge k n r := by
  -- Let `l := lamLarge k n r`. By `hr3`, `lamLarge_ge_one` applies, so try `Let's choose `l := lamLarge k n r` and `Let's choose `l := lamLarge k n r`.
  set l := lamLarge k n r with hl;
  have hT1 : ((n : ℝ) * (Nat.factorial r : ℝ) * l ^ r / (k : ℝ) ^ (r + 1)) ^ ((2 * (r : ℝ) - 1)⁻¹) = (k : ℝ) ^ ((theta - 1) / (3 * (r : ℝ) - 2)) := by
    have hT1 : ((n : ℝ) * (Nat.factorial r : ℝ) * l ^ r / (k : ℝ) ^ (r + 1)) = (k : ℝ) ^ (-(E1exp r)) := by
      have hT1 : ((n : ℝ) * (Nat.factorial r : ℝ) * l ^ r) = (k : ℝ) ^ ((r : ℝ) + 1 - E1exp r) := by
        rw [ lamLarge_pow k n r hn0 ( by positivity ) ( by linarith ) ];
        rw [ mul_div_cancel₀ _ ( by positivity ) ];
      rw [ hT1, div_eq_iff ( by positivity ) ] ; rw [ ← Real.rpow_natCast, ← Real.rpow_add ( by positivity ) ] ; push_cast ; ring_nf;
    rw [ hT1, ← Real.rpow_mul ] <;> norm_num [ E1exp ];
    field_simp;
    exact congr_arg _ ( by rw [ neg_div', div_eq_div_iff ] <;> nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast, show ( k : ℝ ) ≥ 2 by norm_cast ] );
  have hT2 : ((k : ℝ) ^ ((r : ℝ) + theta) / ((n : ℝ) * (Nat.factorial r : ℝ) * l ^ r)) ^ (((r : ℝ) - 1)⁻¹) = (k : ℝ) ^ ((theta - 1) / (3 * (r : ℝ) - 2)) := by
    have hT2_base : ((k : ℝ) ^ ((r : ℝ) + theta) / ((n : ℝ) * (Nat.factorial r : ℝ) * l ^ r)) = (k : ℝ) ^ (theta - 1 + E1exp r) := by
      rw [ lamLarge_pow k n r hn0 ( by positivity ) ( by linarith ) ];
      rw [ mul_div_cancel₀ _ ( by positivity ) ];
      rw [ ← Real.rpow_sub ( by positivity ) ] ; ring_nf;
    rw [ hT2_base, ← Real.rpow_mul ( by positivity ) ];
    congr 1;
    unfold E1exp;
    rw [ ← div_eq_mul_inv, div_eq_div_iff ] <;> nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast, mul_div_cancel₀ ( ( 1 - theta ) * ( 2 * r - 1 ) ) ( by linarith [ show ( r : ℝ ) ≥ 3 by norm_cast ] : ( 3 * r - 2 : ℝ ) ≠ 0 ) ];
  have := kon_of_hole hK;
  convert this l theta ( lamLarge_ge_one k n r hn0 hk hr3 hub ) theta_pos theta_lt_one rfl n k r hkn ( by linarith ) hrle using 1 ; try (case e'_2 => rfl)
  all_goals first | rfl | (rw [hT1, hT2]; ring)

/-
Pointwise bound for the first Konyagin term in the large range.
-/
private lemma large_term1_le (k r : ℕ) (hk : 1 < k) (hr3 : 3 ≤ r) (hlog1 : 1 < Real.log k)
    (h3r2 : (3 * (r : ℝ) - 2) < 7 * (1 / 20) * Real.log k / Real.log (Real.log k)) :
    (k : ℝ) ^ ((theta - 1) / (3 * (r : ℝ) - 2)) ≤ (Real.log k) ^ (-(19 : ℝ) / 14) := by
  rw [ Real.rpow_def_of_pos, Real.rpow_def_of_pos ] <;> try positivity;
  -- By simplifying, we can see that the inequality holds.
  have h_simplified : (20 * Real.log (Real.log k) * (3 * (r : ℝ) - 2)) / 7 < Real.log k := by
    rw [ lt_div_iff₀ ] at h3r2 <;> nlinarith [ Real.log_pos hlog1 ];
  unfold theta; norm_num; rw [ mul_div, div_le_iff₀ ] <;> nlinarith [ ( by norm_cast : ( 3 :ℝ ) ≤ r ) ] ;

/-
Pointwise bound for the third Konyagin term in the large range.
-/
private lemma large_term3_le (k : ℕ) (n : ℤ) (r : ℕ) (hk : 1 < k) (hn0 : 0 < n) (hr3 : 3 ≤ r)
    (hlog1 : 1 < Real.log k)
    (hmin : (k : ℝ) ^ (((r : ℝ) - 1) + theta) < (n : ℝ) * (Nat.factorial (r - 1) : ℝ))
    (hrk : ((r : ℝ) + 1) ≤ (k : ℝ) ^ (theta / (r : ℝ)))
    (hrconv : (r : ℝ) ≤ 3 * (1 / 20) * Real.log k / Real.log (Real.log k)) :
    (((r : ℝ) + 1) * lamLarge k n r / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹) ≤
      (Real.log k) ^ (-(10 : ℝ) / 9) := by
  -- Step 1: the base `((r:ℝ)+1)*λ/(k:ℝ) < (k:ℝ)^(2/(r:ℝ) - 1)`.
  have h_base : ((r + 1 : ℝ) * lamLarge k n r / k) < (k : ℝ) ^ (2 / (r : ℝ) - 1) := by
    have h_base : ((r + 1 : ℝ) * lamLarge k n r) < (k : ℝ) ^ (2 / (r : ℝ)) := by
      refine' lt_of_le_of_lt ( mul_le_mul_of_nonneg_right hrk ( Real.rpow_nonneg ( by positivity ) _ ) ) _;
      convert mul_lt_mul_of_pos_left ( lamLarge_lt k n r hn0 hk hr3 hmin ) ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr hk.le ) _ ) using 1 ; ring_nf;
      rw [ ← Real.rpow_add ( by positivity ) ] ; ring_nf;
    convert div_lt_div_iff_of_pos_right ( by positivity : 0 < ( k : ℝ ) ) |>.2 h_base using 1 ; try (case e'_2 => rfl) ; rw [ Real.rpow_sub_one ( by positivity ) ];
  refine le_trans ( Real.rpow_le_rpow ( ?_ ) h_base.le ( ?_ ) ) ?_;
  · unfold lamLarge; positivity;
  · positivity;
  · rw [ ← Real.rpow_mul ( by positivity ), mul_comm ];
    rw [ Real.rpow_def_of_pos ( by positivity ), Real.rpow_def_of_pos ( by positivity ) ] ; ring_nf at * ; norm_num at *;
    field_simp at *;
    rw [ le_div_iff₀ ( Real.log_pos hlog1 ) ] at hrconv ; nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast ]

/-
The Konyagin estimate on the large range is eventually dominated by
`C · k^θ / log k`.
-/
private lemma large_asym (C : ℝ) (hC : 0 < C) : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ, ∀ r : ℕ,
    3 ≤ r → 0 < n →
    (k : ℝ) ^ (((r : ℝ) - 1) + theta) < (n : ℝ) * (Nat.factorial (r - 1) : ℝ) →
    (3 * (r : ℝ) - 2) < 7 * (1 / 20) * Real.log k / Real.log (Real.log k) →
    ((r : ℝ) + 1) ≤ (k : ℝ) ^ (theta / (r : ℝ)) →
    (r : ℝ) ≤ 3 * (1 / 20) * Real.log k / Real.log (Real.log k) →
    (r : ℝ) ≤ Real.log k →
    c₆ * (k : ℝ) ^ theta *
        (2 * (k : ℝ) ^ ((theta - 1) / (3 * (r : ℝ) - 2)) +
          (((r : ℝ) + 1) * lamLarge k n r / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹)) +
      2 * (r : ℝ) * lamLarge k n r ≤ C * (k : ℝ) ^ theta / Real.log k := by
  revert hC;
  intro hC_pos
  obtain ⟨k₀, hk₀⟩ : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
    2 * c₆ * (k : ℝ) ^ theta * (Real.log k) ^ (-(19 : ℝ) / 14) +
    c₆ * (k : ℝ) ^ theta * (Real.log k) ^ (-(10 : ℝ) / 9) +
    2 * (k : ℝ) ^ ((2 - theta) / 3) * (Real.log k) ^ (1 : ℝ) ≤ C * (k : ℝ) ^ theta / Real.log k := by
      obtain ⟨k₀₁, hk₀₁⟩ : ∃ k₀₁ : ℕ, ∀ k : ℕ, k₀₁ ≤ k →
          2 * c₆ * (k : ℝ) ^ theta * (Real.log k) ^ (-(19 : ℝ) / 14) ≤ C / 3 * (k : ℝ) ^ theta / Real.log k := by
            have := poly_log_lt_logpow ( 2 * c₆ ) theta ( -19 / 14 ) ( by norm_num ) ( C / 3 ) ( by linarith ) ; aesop;
      obtain ⟨k₀₂, hk₀₂⟩ : ∃ k₀₂ : ℕ, ∀ k : ℕ, k₀₂ ≤ k →
          c₆ * (k : ℝ) ^ theta * (Real.log k) ^ (-(10 : ℝ) / 9) ≤ C / 3 * (k : ℝ) ^ theta / Real.log k := by
            have := poly_log_lt_logpow ( c₆ ) theta ( - ( 10 : ℝ ) / 9 ) ( by norm_num ) ( C / 3 ) ( by linarith ) ; aesop;
      obtain ⟨k₀₃, hk₀₃⟩ : ∃ k₀₃ : ℕ, ∀ k : ℕ, k₀₃ ≤ k →
          2 * (k : ℝ) ^ ((2 - theta) / 3) * (Real.log k) ^ (1 : ℝ) ≤ C / 3 * (k : ℝ) ^ theta / Real.log k := by
            have := poly_log_lt ( 2 : ℝ ) ( ( 2 - theta ) / 3 ) 1 theta ( by linarith [ show theta > 1 / 2 by norm_num [ theta ] ] ) ( C / 3 ) ( by linarith ) ; aesop;
      exact ⟨ Max.max k₀₁ ( Max.max k₀₂ k₀₃ ), fun k hk => by convert add_le_add_three ( hk₀₁ k ( le_trans ( le_max_left _ _ ) hk ) ) ( hk₀₂ k ( le_trans ( le_max_of_le_right ( le_max_left _ _ ) ) hk ) ) ( hk₀₃ k ( le_trans ( le_max_of_le_right ( le_max_right _ _ ) ) hk ) ) using 1 ; try (case e'_2 => rfl) ; ring ⟩;
  refine' ⟨ k₀ + 2, fun k hk n r hr hn hmin h3r2 hrk hrconv hrlog => le_trans _ ( hk₀ k ( by linarith ) ) ⟩;
  refine' add_le_add _ _;
  · refine' le_trans ( mul_le_mul_of_nonneg_left ( add_le_add ( mul_le_mul_of_nonneg_left ( large_term1_le k r ( by linarith ) ( by linarith ) ( by
      linarith [ show ( r : ℝ ) ≥ 3 by norm_cast ] ) ( by
      exact h3r2 ) ) zero_le_two ) ( large_term3_le k n r ( by linarith ) ( by linarith ) ( by linarith ) ( by
      linarith [ show ( r : ℝ ) ≥ 3 by norm_cast ] ) ( by
      convert hmin using 1 ) ( by
      exact_mod_cast hrk ) ( by
      exact hrconv ) ) ) ( by
      exact mul_nonneg ( by unfold c₆; norm_num [ B_const, K_const, C₀_const ] ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) ) ) _;
    linarith;
  · have h_lamLarge_lt : lamLarge k n r < (k : ℝ) ^ ((2 - theta) / 3) := by
      refine' lt_of_lt_of_le ( lamLarge_lt k n r hn ( by linarith ) hr hmin ) _;
      exact Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) ( by rw [ div_le_div_iff₀ ] <;> nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast, show ( theta : ℝ ) > 0 by exact_mod_cast theta_pos, show ( theta : ℝ ) < 1 by exact_mod_cast theta_lt_one ] );
    norm_num at *;
    nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast, show ( k : ℝ ) ^ ( ( 2 - theta ) / 3 : ℝ ) ≥ 0 by positivity ]

/-
`log k / log log k → ∞`.
-/
private lemma tendsto_log_div_loglog_atTop :
    Filter.Tendsto (fun k : ℕ => Real.log k / Real.log (Real.log k)) Filter.atTop Filter.atTop := by
  -- We'll use the change of variables $u = \log k$.
  suffices h_log : Filter.Tendsto (fun u : ℝ => u / Real.log u) Filter.atTop Filter.atTop by
    exact h_log.comp ( Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop );
  -- We can use the change of variables $v = \log u$ to transform the limit expression.
  suffices h_log : Filter.Tendsto (fun v : ℝ => Real.exp v / v) Filter.atTop Filter.atTop by
    have := h_log.comp Real.tendsto_log_atTop;
    exact this.congr' ( by filter_upwards [ Filter.eventually_gt_atTop 0 ] with x hx using by rw [ Function.comp_apply, Real.exp_log hx ] );
  simpa using Real.tendsto_exp_div_pow_atTop 1

/-- The reference exponent `r₀ = ⌈log k / (10 log log k)⌉`. -/
private noncomputable def r0L (k : ℕ) : ℕ := ⌈Real.log k / (10 * Real.log (Real.log k))⌉₊

/-
Bounds on the reference exponent `r₀`.
-/
private lemma large_r0_bounds : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
    1 ≤ r0L k ∧
    3 * (r0L k : ℝ) - 2 < 7 * (1 / 20) * Real.log k / Real.log (Real.log k) ∧
    (r0L k : ℝ) ≤ 3 * (1 / 20) * Real.log k / Real.log (Real.log k) ∧
    (r0L k : ℝ) ≤ Real.log k ∧
    (r0L k : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - theta) ∧
    (r0L k : ℝ) + 1 ≤ (k : ℝ) ^ (theta / (r0L k : ℝ)) := by
  -- By combining the results from the provided solution, we can choose a sufficiently large $k₀$ such that all conditions hold.
  obtain ⟨k₀, hk₀⟩ : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
    100 ≤ Real.log k ∧ 200 ≤ Real.log k / Real.log (Real.log k) ∧ Real.log k ≤ (1/2) * (k:ℝ)^(1-theta) := by
      obtain ⟨k₁, hk₁⟩ : ∃ k₁ : ℕ, ∀ k : ℕ, k₁ ≤ k → 100 ≤ Real.log k := by
        exact ⟨ Nat.ceil ( Real.exp 100 ), fun k hk => by simpa using Real.log_le_log ( by positivity ) ( Nat.ceil_le.mp hk ) ⟩
      obtain ⟨k₂, hk₂⟩ : ∃ k₂ : ℕ, ∀ k : ℕ, k₂ ≤ k → 200 ≤ Real.log k / Real.log (Real.log k) := by
        have := tendsto_log_div_loglog_atTop.eventually_ge_atTop 200; aesop;
      obtain ⟨k₃, hk₃⟩ : ∃ k₃ : ℕ, ∀ k : ℕ, k₃ ≤ k → Real.log k ≤ (1/2) * (k:ℝ)^(1-theta) := by
        have := isLittleO_log_rpow_atTop ( show ( 0 : ℝ ) < 1 - theta by norm_num [ theta ] );
        rw [ Asymptotics.isLittleO_iff ] at this;
        obtain ⟨ k₃, hk₃ ⟩ := Filter.eventually_atTop.mp ( this ( show 0 < ( 1 / 2 : ℝ ) by norm_num ) ) ; use ⌈k₃⌉₊ + 1; intros k hk; specialize hk₃ k ( Nat.le_of_ceil_le ( by linarith ) ) ; rw [ Real.norm_of_nonneg ( Real.log_nonneg <| Nat.one_le_cast.mpr <| by linarith ), Real.norm_of_nonneg ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) ] at hk₃; linarith;
      use max k₁ (max k₂ k₃);
      grind;
  refine' ⟨ k₀ + 3, fun k hk => _ ⟩ ; specialize hk₀ k ( by linarith ) ; norm_num [ r0L ] at *;
  refine' ⟨ _, _, _, _, _, _ ⟩;
  any_goals ring_nf at *; nlinarith [ Nat.ceil_lt_add_one ( show 0 ≤ Real.log k / ( 10 * Real.log ( Real.log k ) ) by exact div_nonneg ( by linarith ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith ) ) ) ) ];
  · ring_nf at *;
    linarith [ Nat.ceil_lt_add_one ( show 0 ≤ Real.log k * ( Real.log ( Real.log k ) ) ⁻¹ * ( 1 / 10 ) by exact mul_nonneg ( mul_nonneg ( Real.log_nonneg ( by norm_cast; linarith ) ) ( inv_nonneg.mpr ( Real.log_nonneg ( by linarith ) ) ) ) ( by norm_num ) ) ];
  · rw [ le_div_iff₀ ( Real.log_pos <| show 1 < Real.log k from by linarith ) ] at *;
    nlinarith [ Nat.ceil_lt_add_one ( show 0 ≤ Real.log k / ( 10 * Real.log ( Real.log k ) ) by exact div_nonneg ( Real.log_nonneg ( by norm_cast; linarith ) ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith ) ) ) ), Real.log_pos ( show 1 < Real.log k from by linarith ), mul_div_cancel₀ ( Real.log k ) ( show ( 10 * Real.log ( Real.log k ) ) ≠ 0 by linarith [ Real.log_pos ( show 1 < Real.log k from by linarith ) ] ) ];
  · refine' le_trans ( Nat.ceil_lt_add_one _ |> le_of_lt ) _;
    · exact div_nonneg ( Real.log_nonneg ( by norm_cast; linarith ) ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith ) ) );
    · rw [ div_add_one, div_le_iff₀ ] <;> nlinarith [ show 1 ≤ Real.log ( Real.log k ) from by rw [ Real.le_log_iff_exp_le ( by linarith ) ] ; exact Real.exp_one_lt_d9.le.trans ( by norm_num; linarith ) ];
  · refine' le_trans ( Nat.ceil_lt_add_one ( by exact div_nonneg ( by linarith ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith ) ) ) ) |> le_of_lt ) _;
    rw [ div_add_one, div_le_iff₀ ] <;> nlinarith [ show 1 ≤ Real.log ( Real.log k ) from by rw [ Real.le_log_iff_exp_le ( by linarith ) ] ; exact Real.exp_one_lt_d9.le.trans ( by norm_num; linarith ) ];
  · -- We'll use that $Real.exp M \leq Real.exp (theta * L / (r0L k))$ since $M \leq theta * L / (r0L k)$.
    have h_exp : Real.exp (Real.log (Real.log k)) ≤ Real.exp (theta * Real.log k / (Nat.ceil (Real.log k / (10 * Real.log (Real.log k)))) ) := by
      refine' Real.exp_le_exp.mpr _;
      rw [ le_div_iff₀ ];
      · have hM_le : (Nat.ceil (Real.log k / (10 * Real.log (Real.log k)))) * Real.log (Real.log k) < theta * Real.log k := by
          have hM_le : (Real.log k / (10 * Real.log (Real.log k)) + 1) * Real.log (Real.log k) < theta * Real.log k := by
            rw [ div_add_one, div_mul_eq_mul_div, div_lt_iff₀ ] <;> norm_num [ theta ];
            · rw [ le_div_iff₀ ] at hk₀ <;> nlinarith [ Real.log_pos ( show 1 < Real.log k from by linarith ) ];
            · exact Real.log_pos ( by linarith );
            · exact ⟨ ⟨ by linarith, by linarith, by linarith ⟩, by linarith, by linarith ⟩;
          exact lt_of_le_of_lt ( mul_le_mul_of_nonneg_right ( Nat.ceil_lt_add_one ( by exact div_nonneg ( by linarith ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith ) ) ) ) |> le_of_lt ) ( Real.log_nonneg ( by linarith ) ) ) hM_le;
        linarith;
      · exact Nat.cast_pos.mpr ( Nat.ceil_pos.mpr ( div_pos ( by linarith ) ( mul_pos ( by norm_num ) ( Real.log_pos ( by linarith ) ) ) ) );
    rw [ Real.exp_log ( Real.log_pos <| by norm_cast; linarith ) ] at h_exp;
    -- Since $\lceil x \rceil + 1 \leq L$, we have $\lceil x \rceil + 1 \leq \exp(\theta \cdot L / \lceil x \rceil)$.
    have h_ceil : (⌈Real.log k / (10 * Real.log (Real.log k))⌉₊ : ℝ) + 1 ≤ Real.log k := by
      have := Nat.ceil_lt_add_one ( show 0 ≤ Real.log k / ( 10 * Real.log ( Real.log k ) ) by exact div_nonneg ( by linarith ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith ) ) ) );
      rw [ div_add_one, lt_div_iff₀ ] at this <;> nlinarith [ show 1 ≤ Real.log ( Real.log k ) from by rw [ Real.le_log_iff_exp_le ( by linarith ) ] ; exact Real.exp_one_lt_d9.le.trans ( by norm_num; linarith ) ];
    convert h_ceil.trans h_exp using 1 ; try (case e'_2 => rfl) ;
    rw [ Real.rpow_def_of_pos ( Nat.cast_pos.mpr ( by linarith ) ) ] ; ring_nf

/-
The reference exponent `r₀` satisfies the Konyagin admissibility `n r₀! ≤ k^{r₀+θ}`.
-/
private lemma large_r0_P : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ, 0 < n →
    (n : ℝ) ≤ Real.exp ((Real.log k) ^ 2 / (20 * Real.log (Real.log k))) →
    (n : ℝ) * (Nat.factorial (r0L k) : ℝ) ≤ (k : ℝ) ^ ((r0L k : ℝ) + theta) := by
  -- For sufficiently large $k$, we have $L \geq 6M$.
  obtain ⟨k₀₁, hk₀₁⟩ : ∃ k₀₁ : ℕ, ∀ k : ℕ, k₀₁ ≤ k → Real.log k ≥ 10 ∧ Real.log (Real.log k) ≥ 1 ∧ Real.log k ≥ 6 * Real.log (Real.log k) := by
    have h_log_log : Filter.Tendsto (fun k : ℕ => Real.log k / Real.log (Real.log k)) Filter.atTop Filter.atTop :=
      tendsto_log_div_loglog_atTop
    have h_log_log : ∃ k₀₁ : ℕ, ∀ k : ℕ, k₀₁ ≤ k → Real.log k ≥ 10 ∧ Real.log (Real.log k) ≥ 1 := by
      have h_log_log : Filter.Tendsto (fun k : ℕ => Real.log k) Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun k : ℕ => Real.log (Real.log k)) Filter.atTop Filter.atTop := by
        exact ⟨ Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop, Real.tendsto_log_atTop.comp <| Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop ⟩;
      exact Filter.eventually_atTop.mp ( h_log_log.1.eventually_ge_atTop 10 |> Filter.Eventually.and <| h_log_log.2.eventually_ge_atTop 1 );
    have := ‹Filter.Tendsto ( fun k : ℕ => Real.log k / Real.log ( Real.log k ) ) Filter.atTop Filter.atTop›.eventually_gt_atTop 6;
    obtain ⟨ k₀₁, hk₀₁ ⟩ := Filter.eventually_atTop.mp this; obtain ⟨ k₀₂, hk₀₂ ⟩ := h_log_log; exact ⟨ Max.max k₀₁ k₀₂, fun k hk => ⟨ hk₀₂ k ( le_trans ( le_max_right _ _ ) hk ) |>.1, hk₀₂ k ( le_trans ( le_max_right _ _ ) hk ) |>.2, by have := hk₀₂ k ( le_trans ( le_max_right _ _ ) hk ) |>.1; have := hk₀₂ k ( le_trans ( le_max_right _ _ ) hk ) |>.2; have := hk₀₁ k ( le_trans ( le_max_left _ _ ) hk ) ; rw [ lt_div_iff₀ ] at this <;> linarith ⟩ ⟩ ;
  use k₀₁ + 2;
  intros k hk n hn h_exp
  have h_log_bound : (Real.log k) ^ 2 / (20 * Real.log (Real.log k)) + (r0L k : ℝ) * Real.log (Real.log k) ≤ (r0L k : ℝ) * Real.log k := by
    have h_log_bound : (r0L k : ℝ) ≥ Real.log k / (10 * Real.log (Real.log k)) := by
      exact Nat.le_ceil _;
    rw [ ge_iff_le, div_le_iff₀ ] at h_log_bound <;> nlinarith [ hk₀₁ k ( by linarith ), Real.log_pos ( show ( k : ℝ ) > 1 by norm_cast; linarith ), Real.log_pos ( show ( Real.log k : ℝ ) > 1 by linarith [ hk₀₁ k ( by linarith ) ] ), mul_div_cancel₀ ( Real.log k ^ 2 ) ( by linarith [ hk₀₁ k ( by linarith ) ] : ( 20 * Real.log ( Real.log k ) ) ≠ 0 ) ];
  have h_log_bound : Real.log (n : ℝ) + Real.log (Nat.factorial (r0L k) : ℝ) ≤ (r0L k : ℝ) * Real.log k + theta * Real.log k := by
    have h_log_bound : Real.log (Nat.factorial (r0L k) : ℝ) ≤ (r0L k : ℝ) * Real.log (r0L k) := by
      rw [ ← Real.log_pow ] ; gcongr ; norm_cast ; exact Nat.recOn ( r0L k ) ( by norm_num ) fun n ihn => by rw [ Nat.factorial_succ, pow_succ' ] ; exact le_trans ( Nat.mul_le_mul_left _ ihn ) ( by gcongr ; linarith ) ;
    have h_log_bound : Real.log (n : ℝ) ≤ (Real.log k) ^ 2 / (20 * Real.log (Real.log k)) := by
      exact Real.log_le_iff_le_exp ( by positivity ) |>.2 h_exp;
    have h_log_bound : Real.log (r0L k : ℝ) ≤ Real.log (Real.log k) := by
      gcongr;
      · exact Nat.cast_pos.mpr ( Nat.ceil_pos.mpr ( div_pos ( Real.log_pos ( by norm_cast; linarith ) ) ( mul_pos ( by norm_num ) ( Real.log_pos ( show 1 < Real.log k from by linarith [ hk₀₁ k ( by linarith ) ] ) ) ) ) );
      · have := Nat.ceil_lt_add_one ( show 0 ≤ Real.log k / ( 10 * Real.log ( Real.log k ) ) by exact div_nonneg ( Real.log_nonneg ( by norm_cast; linarith ) ) ( mul_nonneg ( by norm_num ) ( Real.log_nonneg ( by linarith [ hk₀₁ k ( by linarith ) ] ) ) ) );
        exact le_trans this.le ( by rw [ div_add_one, div_le_iff₀ ] <;> nlinarith [ hk₀₁ k ( by linarith ) ] );
    nlinarith [ show 0 ≤ theta * Real.log k from mul_nonneg ( by norm_num [ theta ] ) ( Real.log_nonneg ( by norm_cast; linarith ) ) ];
  rw [ ← Real.log_le_log_iff ( by positivity ) ( by exact Real.rpow_pos_of_pos ( Nat.cast_pos.mpr <| by linarith ) _ ), Real.log_mul ( by positivity ) ( by positivity ), Real.log_rpow ( Nat.cast_pos.mpr <| by linarith ) ] ; linarith

/-
Existence of the minimal `r` with `n r! ≤ k^{r+θ}` and all its bounds.
-/
private lemma large_r_data : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
    (1 / 2) * (k : ℝ) ^ (2 + theta) < (n : ℝ) →
    (n : ℝ) ≤ Real.exp ((Real.log k) ^ 2 / (20 * Real.log (Real.log k))) →
    ∃ r : ℕ, 3 ≤ r ∧ (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - theta) ∧
      (n : ℝ) * (Nat.factorial r : ℝ) ≤ (k : ℝ) ^ ((r : ℝ) + theta) ∧
      (k : ℝ) ^ (((r : ℝ) - 1) + theta) < (n : ℝ) * (Nat.factorial (r - 1) : ℝ) ∧
      (3 * (r : ℝ) - 2) < 7 * (1 / 20) * Real.log k / Real.log (Real.log k) ∧
      ((r : ℝ) + 1) ≤ (k : ℝ) ^ (theta / (r : ℝ)) ∧
      (r : ℝ) ≤ 3 * (1 / 20) * Real.log k / Real.log (Real.log k) ∧
      (r : ℝ) ≤ Real.log k := by
  obtain ⟨kb, hb⟩ := large_r0_bounds
  obtain ⟨kp, hp⟩ := large_r0_P
  use max (max kb kp) 2;
  intro k hk n hn hn'; rcases lt_trichotomy n 0 with hn0 | rfl | hn0 <;> norm_num at *;
  · linarith [ show ( n : ℝ ) < 0 by exact_mod_cast hn0, show ( 0 : ℝ ) ≤ k ^ ( 2 + theta ) by positivity ];
  · exact False.elim <| hn.not_ge <| by positivity;
  · refine' ⟨ Nat.find ( show ∃ r : ℕ, ( n : ℝ ) * r.factorial ≤ k ^ ( r + theta ) from ⟨ r0L k, hp k hk.2.1 n hn0 hn' ⟩ ), _, _, _, _, _ ⟩ <;> norm_num at *;
    · intro m hm; interval_cases m <;> norm_num at * <;> try linarith;
      · refine' lt_of_le_of_lt _ hn;
        rw [ show ( 2 + theta : ℝ ) = theta + 2 by ring, Real.rpow_add ] <;> norm_num <;> try linarith;
        nlinarith [ show ( k : ℝ ) ^ theta > 0 by exact Real.rpow_pos_of_pos ( Nat.cast_pos.mpr ( by linarith ) ) _, show ( k : ℝ ) ^ 2 ≥ 4 by norm_cast; nlinarith ];
      · rw [ show ( 2 + theta : ℝ ) = 1 + theta + 1 by ring, Real.rpow_add ] at hn <;> norm_num at * <;> try linarith;
        nlinarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith, show ( k : ℝ ) ^ ( 1 + theta ) > 0 by exact Real.rpow_pos_of_pos ( by norm_cast; linarith ) _ ];
    · exact le_trans ( Nat.cast_le.mpr <| Nat.find_min' _ <| hp k hk.2.1 n hn0 hn' ) <| hb k hk.1 |>.2.2.2.2.1;
    · exact Nat.find_spec ( ⟨ r0L k, hp k hk.2.1 n hn0 hn' ⟩ : ∃ r : ℕ, ( n : ℝ ) * r.factorial ≤ k ^ ( r + theta ) );
    · have := Nat.find_min ( show ∃ r : ℕ, ( n : ℝ ) * r.factorial ≤ k ^ ( r + theta ) from ⟨ r0L k, hp k hk.2.1 n hn0 hn' ⟩ ) ( show Nat.find ( show ∃ r : ℕ, ( n : ℝ ) * r.factorial ≤ k ^ ( r + theta ) from ⟨ r0L k, hp k hk.2.1 n hn0 hn' ⟩ ) - 1 < Nat.find ( show ∃ r : ℕ, ( n : ℝ ) * r.factorial ≤ k ^ ( r + theta ) from ⟨ r0L k, hp k hk.2.1 n hn0 hn' ⟩ ) from Nat.sub_lt ( Nat.pos_of_ne_zero ( by
                                                                                                                                                                                                                                                                      norm_num [ Nat.find_eq_zero ];
                                                                                                                                                                                                                                                                      refine' lt_of_le_of_lt _ hn;
                                                                                                                                                                                                                                                                      rw [ Real.rpow_add ] <;> norm_num <;> try linarith;
                                                                                                                                                                                                                                                                      nlinarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith, show ( k : ℝ ) ^ theta > 0 by exact Real.rpow_pos_of_pos ( by norm_cast; linarith ) _, show ( k : ℝ ) ^ 2 ≥ 4 by norm_cast; nlinarith ] ) ) zero_lt_one ) ; norm_num at *;
      convert this using 2 ; try (case e'_2 => rfl) ; rw [ Nat.cast_sub ] <;> norm_num;
      refine' lt_of_le_of_lt _ hn;
      rw [ show ( 2 + theta : ℝ ) = theta + 2 by ring, Real.rpow_add ] <;> norm_num <;> try linarith;
      nlinarith [ show ( k : ℝ ) ^ theta > 0 by exact Real.rpow_pos_of_pos ( by norm_cast; linarith ) _, show ( k : ℝ ) ^ 2 ≥ 4 by norm_cast; nlinarith ];
    · refine' ⟨ _, _, _, _ ⟩;
      · refine' lt_of_le_of_lt _ ( hb k hk.1 |>.2.1 );
        gcongr;
        exact Nat.find_min' _ ( hp k hk.2.1 n hn0 hn' );
      · refine' le_trans _ ( Real.rpow_le_rpow_of_exponent_le _ <| div_le_div_of_nonneg_left _ _ <| Nat.cast_le.mpr <| Nat.find_le _ ) <;> norm_num [ hb k hk.1 ];
        any_goals exact r0L k;
        · refine' le_trans _ ( hb k hk.1 |>.2.2.2.2.2 );
          gcongr;
          exact Nat.find_min' _ ( hp k hk.2.1 n hn0 hn' );
        · linarith;
        · exact le_of_lt ( by norm_num : ( 0 : ℝ ) < 21 / 40 );
        · refine' lt_of_le_of_lt _ hn;
          rw [ show ( 2 + theta : ℝ ) = theta + 2 by ring, Real.rpow_add ] <;> norm_num <;> try linarith;
          nlinarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith, show ( k : ℝ ) ^ theta > 0 by exact Real.rpow_pos_of_pos ( by norm_cast; linarith ) _, show ( k : ℝ ) ^ 2 ≥ 4 by norm_cast; nlinarith ];
        · exact hp k hk.2.1 n hn0 hn';
      · exact le_trans ( Nat.cast_le.mpr ( Nat.find_min' _ ( hp k hk.2.1 n hn0 hn' ) ) ) ( hb k hk.1 |>.2.2.1 );
      · exact le_trans ( Nat.cast_le.mpr ( Nat.find_min' _ ( hp k hk.2.1 n hn0 hn' ) ) ) ( hb k hk.1 |>.2.2.2.1 )

/-- **Large `n`:** `½ k^{2+θ} < n ≤ exp(log²k / (20 log log k))`. -/
private lemma case_large (hK : KonHole) (hB : BHP) : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
    (1 / 2) * (k : ℝ) ^ (2 + theta) < (n : ℝ) →
    (n : ℝ) ≤ Real.exp ((Real.log k) ^ 2 / (20 * Real.log (Real.log k))) →
    ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + 3 * (k : ℝ) ^ theta ∧
      (p : ℤ) ∣ Pprod k n := by
  obtain ⟨C, hC, kb, hb⟩ := hB
  obtain ⟨k1, hasym⟩ := large_asym C hC
  obtain ⟨k2, hrdata⟩ := large_r_data
  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 hk1' : 1 < k := by omega
  have hkR : (1 : ℝ) < (k : ℝ) := by exact_mod_cast hk1'
  -- `n > 0` and `(k:ℤ) < n`
  have hk2R : (2 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk2le
  have hkpow : (k : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (2 + theta) := by
    have h1 : (k : ℝ) ^ (2 + theta) = (k : ℝ) ^ 2 * (k : ℝ) ^ theta := by
      rw [show (2 + theta : ℝ) = (2 : ℕ) + theta by norm_num,
        Real.rpow_add (by linarith), Real.rpow_natCast]
    have h2 : (1 : ℝ) ≤ (k : ℝ) ^ theta :=
      Real.one_le_rpow (le_of_lt hkR) (le_of_lt theta_pos)
    rw [h1]
    nlinarith [mul_nonneg (sq_nonneg (k : ℝ)) (by linarith : (0:ℝ) ≤ (k : ℝ) ^ theta - 1)]
  have hknR : (k : ℝ) < (n : ℝ) := lt_of_le_of_lt hkpow hlow
  have hkn : (k : ℤ) < n := by exact_mod_cast hknR
  have hn0 : 0 < n := lt_trans (by exact_mod_cast hk1) hkn
  obtain ⟨r, hr3, hrle, hub, hmin, h3r2, hrk, hrconv, hrlog⟩ :=
    hrdata k hki2 n hlow hhigh
  have hraw := large_card_raw hK k n r hk1' hn0 hr3 hrle hkn hub
  have hbnd := hasym k hki1 n r hr3 hn0 hmin h3r2 hrk hrconv hrlog
  have hbhp : C * (k : ℝ) ^ theta / Real.log k ≤
      (primeCard (k : ℝ) ((k : ℝ) + (k : ℝ) ^ theta) : ℝ) := by
    exact hb k hkb
  exact konyagin_finish k n hk1 C hbhp (lt_of_lt_of_le hraw hbnd)

theorem erdos_1094__h2__h2__h2__h4 : (¬∃ (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 : ℤ),
          (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) →
            (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) →
              ∃ (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 hB : BHP
  · exact Or.inr (case_large h_kon hB)
  · exact Or.inl hB