medium range k^(2−21/40)/2 < n ≤ k²/log²k

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 20261014T181000Z-t1014-r-partial.lean, extracted by the gate at 15d1d4647b94 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_count hole ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑{m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ (21 / 40 : ℝ)⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ))}.card : ℝ) < (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * (21 / 40 : ℝ) - (1 : ℝ)) + (↑k : ℝ) ^ (21 / 40 : ℝ) * Real.log (↑k : ℝ) ^ (-2 : ℝ) hole

   Leaves (¬∃ (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 : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with h_count : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑{m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ (21 / 40 : ℝ)⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ))}.card : ℝ) < (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * (21 / 40 : ℝ) - (1 : ℝ)) + (↑k : ℝ) ^ (21 / 40 : ℝ) * Real.log (↑k : ℝ) ^ (-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. , Finset.Ioo The finset $(a, b)$ of elements x such that a < x and x < b. , round round x rounds x to the nearest integer, breaking ties towards positive infinity. .

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

   Lean, lines 31–38

     have h_count : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
         (1 / 2 : ℝ) * (k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (n : ℝ) →
         (n : ℝ) ≤ (k : ℝ) ^ 2 / (Real.log k) ^ 2 →
         (((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 : ℝ) <
           3 + 56 * (k : ℝ) ^ (2 * (21 / 40 : ℝ) - 1) + (k : ℝ) ^ (21 / 40 : ℝ) * (Real.log k) ^ (-(2 : ℝ)) := by
       sorry

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 31–38 at 6ba7fea98468 ↗

2. s2 case

   Leaves (¬∃ (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 : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with 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 : ℝ).

   Uses library Or.inl Or.inl is "left injection" into an Or. .

   Lean, line 51

     · exact Or.inl hB0

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 51 at 6ba7fea98468 ↗

3. theta_pos have (0 : ℝ) < theta

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with theta_pos : (0 : ℝ) < theta.

   Lean, lines 57–59

     have theta_pos : (0 : ℝ) < theta := by
       clear * - 
       simp only [theta]; norm_num

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 57–59 at 6ba7fea98468 ↗

4. theta_lt_one have theta < (1 : ℝ)

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with theta_lt_one : theta < (1 : ℝ).

   Lean, lines 60–62

     have theta_lt_one : theta < 1 := by
       clear * - 
       simp only [theta]; norm_num

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 60–62 at 6ba7fea98468 ↗

5. dvd_Pprod_of_factor have ∀ (k : ℕ) (n p : ℤ), ∀ i ∈ Finset.Icc (1 : ℕ) k, p ∣ n - (↑i : ℤ) → p ∣ Pprod k n

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with dvd_Pprod_of_factor : ∀ (k : ℕ) (n p : ℤ), ∀ i ∈ Finset.Icc (1 : ℕ) k, p ∣ n - (↑i : ℤ) → p ∣ Pprod k n.

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

   Lean, lines 63–67

     have dvd_Pprod_of_factor : ∀ (k : ℕ) (n : ℤ) (p : ℤ) (i : ℕ) (hi : i ∈ Finset.Icc 1 k) (hp : p ∣ (n - (i : ℤ))), p ∣ Pprod k n := by
       intro k n p i hi hp
       clear * - k n p i hi hp
       simp only [Pprod]
       exact hp.trans (Finset.dvd_prod_of_mem (fun i : ℕ => (n - (i : ℤ))) hi)

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 63–67 at 6ba7fea98468 ↗

6. dvd_from_far have ∀ (k : ℕ) (n : ℤ) (p : ℕ), (1 : ℕ) ≤ k → (0 : ℕ) < p → (↑k : ℝ) < (↑p : ℝ) → (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta → (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)| → (↑p : ℤ) ∣ Pprod k n

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with dvd_from_far : ∀ (k : ℕ) (n : ℤ) (p : ℕ), (1 : ℕ) ≤ k → (0 : ℕ) < p → (↑k : ℝ) < (↑p : ℝ) → (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta → (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)| → (↑p : ℤ) ∣ Pprod k n.

   Uses library round round x rounds x to the nearest integer, breaking ties towards positive infinity. .

   Lean, lines 68–105

     have 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
       intro k n p hk1 hp0 hkp hpk hfar
       clear * - dvd_Pprod_of_factor theta_pos theta_lt_one k n p hk1 hp0 hkp hpk hfar
       -- 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 ] ⟩

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 68–105 at 6ba7fea98468 ↗

   1. dvd_from_far.hj have (↑j : ℤ) = i

      Leaves (↑p : ℤ) ∣ Pprod k n, with hj : (↑j : ℤ) = i.

      Uses library Int.toNat_of_nonneg, Int.emod_nonneg.

      Lean, lines 74–75

          have hj : (j : ℤ) = i := by
            exact Int.toNat_of_nonneg <| Int.emod_nonneg _ <| by positivity;

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 74–75 at 6ba7fea98468 ↗

   2. dvd_from_far.h_frac have (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ))

      Leaves (↑p : ℤ) ∣ Pprod k n, with h_frac : (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ)).

      Uses library Min.min Returns the lesser of its two arguments. , mul_min_of_nonneg.

      Lean, lines 77–92

          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

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 77–92 at 6ba7fea98468 ↗

      1. dvd_from_far.h_frac.h_frac have |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)| = min ((↑i : ℝ) / (↑p : ℝ)) ((1 : ℝ) - (↑i : ℝ) / (↑p : ℝ))

         Leaves (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ)), with h_frac : |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)| = min ((↑i : ℝ) / (↑p : ℝ)) ((1 : ℝ) - (↑i : ℝ) / (↑p : ℝ)).

         Uses library round round x rounds x to the nearest integer, breaking ties towards positive infinity. , Min.min Returns the lesser of its two arguments. , abs_sub_round_eq_min.

         Lean, lines 78–84

               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 ];

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 78–84 at 6ba7fea98468 ↗

         1. dvd_from_far.h_frac.h_frac.h_frac have Int.fract ((↑n : ℝ) / (↑p : ℝ)) = (↑i : ℝ) / (↑p : ℝ)

            Leaves |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)| = min ((↑i : ℝ) / (↑p : ℝ)) ((1 : ℝ) - (↑i : ℝ) / (↑p : ℝ)), with h_frac : Int.fract ((↑n : ℝ) / (↑p : ℝ)) = (↑i : ℝ) / (↑p : ℝ).

            Uses library Int.fract Int.fract a the fractional part of a, is a minus its floor. , Int.fract_eq_iff, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , Int.emod_nonneg, Int.emod_lt_of_pos, Int.emod_add_mul_ediv.

            Lean, lines 79–83

                    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 ] ⟩;

            targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 79–83 at 6ba7fea98468 ↗

      2. dvd_from_far.h_frac.hp' have (0 : ℝ) < (↑p : ℝ)

         Leaves (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ)), with hp' : (0 : ℝ) < (↑p : ℝ).

         Lean, line 85

               have hp' : (0:ℝ) < p := by exact_mod_cast hp0

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 85 at 6ba7fea98468 ↗

      3. dvd_from_far.h_frac.h1 have (↑p : ℝ) * ((1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta)) ≤ (↑p : ℝ) * |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)|

         Leaves (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ)), with h1 : (↑p : ℝ) * ((1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta)) ≤ (↑p : ℝ) * |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)|.

         Uses library mul_le_mul_of_nonneg_left.

         Lean, line 86

               have h1 := mul_le_mul_of_nonneg_left hfar hp'.le

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 86 at 6ba7fea98468 ↗

      4. dvd_from_far.h_frac.e1 have (↑p : ℝ) * ((↑i : ℝ) / (↑p : ℝ)) = (↑i : ℝ) routine: field_simp

         Leaves (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ)), with e1 : (↑p : ℝ) * ((↑i : ℝ) / (↑p : ℝ)) = (↑i : ℝ).

         Lean, line 88

               have e1 : (p:ℝ) * ((i:ℝ)/p) = i := by field_simp

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 88 at 6ba7fea98468 ↗

      5. dvd_from_far.h_frac.e2 have (↑p : ℝ) * ((1 : ℝ) - (↑i : ℝ) / (↑p : ℝ)) = (↑p : ℝ) - (↑i : ℝ) routine: field_simp

         Leaves (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ)), with e2 : (↑p : ℝ) * ((1 : ℝ) - (↑i : ℝ) / (↑p : ℝ)) = (↑p : ℝ) - (↑i : ℝ).

         Lean, line 89

               have e2 : (p:ℝ) * (1 - (i:ℝ)/p) = p - i := by field_simp

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 89 at 6ba7fea98468 ↗

      6. dvd_from_far.h_frac.s6 calc (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) = (↑p : ℝ) * ((1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta)) routine: ring

         Closes the goal.

         Lean, line 91

               calc (p:ℝ) / (k:ℝ)^(1-theta) = p * (1 / (k:ℝ)^(1-theta)) := by ring

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 91 at 6ba7fea98468 ↗

      7. dvd_from_far.h_frac.s7 calc (↑p : ℝ) * ((1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta)) ≤ min (↑i : ℝ) ((↑p : ℝ) - (↑i : ℝ))

         Closes the goal.

         Lean, line 92

                 _ ≤ _ := h1

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 92 at 6ba7fea98468 ↗

   3. dvd_from_far.h_i_bounds have (1 : ℤ) ≤ i ∧ i ≤ (↑k : ℤ)

      Leaves (↑p : ℤ) ∣ Pprod k n, with h_i_bounds : (1 : ℤ) ≤ i ∧ i ≤ (↑k : ℤ).

      Lean, lines 94–102

          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 );

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 94–102 at 6ba7fea98468 ↗

      1. dvd_from_far.h_i_bounds.h_i_bounds have (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) > (↑k : ℝ) ^ theta

         Leaves (1 : ℤ) ≤ i ∧ i ≤ (↑k : ℤ), with h_i_bounds : (↑p : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta) > (↑k : ℝ) ^ theta.

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

         Lean, lines 95–99

               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;

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 95–99 at 6ba7fea98468 ↗

         1. dvd_from_far.h_i_bounds.h_i_bounds.s1 case

            Leaves (↑k : ℝ) ^ (21 / 40 : ℝ) * (↑k : ℝ) ^ (19 / 40 : ℝ) < (↑p : ℝ), with theta_pos : True, theta_lt_one : True, dvd_Pprod_of_factor : ∀ (k : ℕ) (n p : ℤ) (i : ℕ), (1 : ℕ) ≤ i → i ≤ k → p ∣ n - (↑i : ℤ) → p ∣ Pprod k n, hkp : k < p, hpk : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ), hfar : ((↑k : ℝ) ^ (19 / 40 : ℝ))⁻¹ ≤ |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)|, h_frac : (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑i : ℝ) ∧ (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑p : ℝ) - (↑i : ℝ).

            Uses library Real.rpow_add, Lean.Grind.Config.extAll If extAll is true, grind uses any extensionality theorems available in the environment. .

            Lean, lines 97–98

                    · rw [ ← Real.rpow_add ] <;> norm_num ; linarith [ ( by norm_cast : ( k : ℝ ) + 1 ≤ p ) ];
                      grind +extAll;

            targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 97–98 at 6ba7fea98468 ↗

         2. dvd_from_far.h_i_bounds.h_i_bounds.s2 case routine: positivity

            Leaves (0 : ℝ) < (↑k : ℝ) ^ (19 / 40 : ℝ), with theta_pos : True, theta_lt_one : True, dvd_Pprod_of_factor : ∀ (k : ℕ) (n p : ℤ) (i : ℕ), (1 : ℕ) ≤ i → i ≤ k → p ∣ n - (↑i : ℤ) → p ∣ Pprod k n, hkp : k < p, hpk : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ), hfar : ((↑k : ℝ) ^ (19 / 40 : ℝ))⁻¹ ≤ |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)|, h_frac : (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑i : ℝ) ∧ (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑p : ℝ) - (↑i : ℝ).

            Lean, line 99

                    · positivity;

            targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 99 at 6ba7fea98468 ↗

      2. dvd_from_far.h_i_bounds.s2 case

         Leaves (1 : ℤ) ≤ i, with theta_pos : True, theta_lt_one : True, dvd_Pprod_of_factor : ∀ (k : ℕ) (n p : ℤ) (i : ℕ), (1 : ℕ) ≤ i → i ≤ k → p ∣ n - (↑i : ℤ) → p ∣ Pprod k n, hkp : k < p, hpk : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ), hfar : ((↑k : ℝ) ^ (19 / 40 : ℝ))⁻¹ ≤ |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)|, h_frac : (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑i : ℝ) ∧ (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑p : ℝ) - (↑i : ℝ), h_i_bounds : (↑k : ℝ) ^ (21 / 40 : ℝ) < (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ).

         Uses library Int.le_of_lt_add_one, Int.cast_lt, Real.one_le_rpow, div_nonneg.

         Lean, line 101

               · 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 ) ) ] );

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 101 at 6ba7fea98468 ↗

      3. dvd_from_far.h_i_bounds.s3 case

         Leaves i ≤ (↑k : ℤ), with theta_pos : True, theta_lt_one : True, dvd_Pprod_of_factor : ∀ (k : ℕ) (n p : ℤ) (i : ℕ), (1 : ℕ) ≤ i → i ≤ k → p ∣ n - (↑i : ℤ) → p ∣ Pprod k n, hkp : k < p, hpk : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ), hfar : ((↑k : ℝ) ^ (19 / 40 : ℝ))⁻¹ ≤ |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)|, h_frac : (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑i : ℝ) ∧ (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ) ≤ (↑p : ℝ) - (↑i : ℝ), h_i_bounds : (↑k : ℝ) ^ (21 / 40 : ℝ) < (↑p : ℝ) / (↑k : ℝ) ^ (19 / 40 : ℝ).

         Uses library Int.le_of_lt_add_one, Int.cast_lt.

         Lean, line 102

               · exact Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith );

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 102 at 6ba7fea98468 ↗

   4. dvd_from_far.s4 case

      Leaves j ∈ Finset.Icc (1 : ℕ) k.

      Lean, line 104

          · grind;

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 104 at 6ba7fea98468 ↗

   5. dvd_from_far.s5 case

      Leaves (↑p : ℤ) ∣ n - (↑j : ℤ).

      Uses library Exists.intro Existential introduction. , Int.emod_add_mul_ediv.

      Lean, line 105

          · exact ⟨ n / p, by linarith [ Int.emod_add_mul_ediv n p ] ⟩

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 105 at 6ba7fea98468 ↗

7. exists_far_prime have ∀ (k : ℕ) (n : ℤ), (1 : ℕ) ≤ k → (↑(badSet k n).card : ℝ) < (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with exists_far_prime : ∀ (k : ℕ) (n : ℤ), (1 : ℕ) ≤ k → (↑(badSet k n).card : ℝ) < (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n.

   Lean, lines 109–135

     have 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
       intro k n hk1 hcount
       clear * - dvd_from_far k n hk1 hcount
       by_contra hne
       push_neg at hne
       have hsub : ((Finset.Ioo ⌊(k:ℝ)⌋ ⌈(k:ℝ) + (k:ℝ)^theta⌉).filter (fun p : ℤ => 0 < p ∧ (p.natAbs).Prime ∧ (k:ℝ) < (p : ℝ) ∧ (p : ℝ) < (k:ℝ) + (k:ℝ)^theta)) ⊆ badSet k n := by
         intro p hp
         rw [Finset.mem_filter] at hp
         obtain ⟨hpI, hp0, hpr, hkp, hpb⟩ := hp
         have hq : ((p.natAbs : ℕ) : ℤ) = p := Int.natAbs_of_nonneg hp0.le
         have hqR : ((p.natAbs : ℕ) : ℝ) = (p : ℝ) := by rw [← Int.cast_natCast, hq]
         simp only [badSet, Finset.mem_filter, Finset.mem_Ioo]
         refine ⟨⟨?_, ?_⟩, hpb, ?_⟩
         · exact_mod_cast hkp
         · have h1 : p < ⌈(k:ℝ) + (k:ℝ)^theta⌉ := (Finset.mem_Ioo.mp hpI).2
           have h2 : ⌈(k:ℝ) + (k:ℝ)^theta⌉ ≤ (k:ℤ) + ⌊(k:ℝ)^theta⌋ + 1 := by
             rw [Int.ceil_le]; push_cast
             linarith [Int.lt_floor_add_one ((k:ℝ)^theta)]
           omega
         · by_contra hfar
           push_neg at hfar
           apply hne p.natAbs hpr (by rw [hqR]; exact hkp) (by rw [hqR]; exact hpb)
           exact dvd_from_far k n p.natAbs hk1 (by omega) (by rw [hqR]; exact hkp) (by rw [hqR]; exact hpb) (by rw [hqR]; exact hfar)
       have hc := Finset.card_le_card hsub
       have hc2 : primeCard (k:ℝ) ((k:ℝ) + (k:ℝ)^theta) ≤ (badSet k n).card := hc
       have hc' : (primeCard (k:ℝ) ((k:ℝ) + (k:ℝ)^theta) : ℝ) ≤ ((badSet k n).card : ℝ) := by exact_mod_cast hc2
       linarith

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 109–135 at 6ba7fea98468 ↗

   1. exists_far_prime.hsub have {p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta} ⊆ badSet k n

      Leaves False, with hsub : {p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta} ⊆ badSet k n.

      Uses library Finset.Ioo The finset $(a, b)$ of elements x such that a < x and x < b. , Finset.mem_filter, Finset.mem_Ioo, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, lines 114–131

          have hsub : ((Finset.Ioo ⌊(k:ℝ)⌋ ⌈(k:ℝ) + (k:ℝ)^theta⌉).filter (fun p : ℤ => 0 < p ∧ (p.natAbs).Prime ∧ (k:ℝ) < (p : ℝ) ∧ (p : ℝ) < (k:ℝ) + (k:ℝ)^theta)) ⊆ badSet k n := by
            intro p hp
            rw [Finset.mem_filter] at hp
            obtain ⟨hpI, hp0, hpr, hkp, hpb⟩ := hp
            have hq : ((p.natAbs : ℕ) : ℤ) = p := Int.natAbs_of_nonneg hp0.le
            have hqR : ((p.natAbs : ℕ) : ℝ) = (p : ℝ) := by rw [← Int.cast_natCast, hq]
            simp only [badSet, Finset.mem_filter, Finset.mem_Ioo]
            refine ⟨⟨?_, ?_⟩, hpb, ?_⟩
            · exact_mod_cast hkp
            · have h1 : p < ⌈(k:ℝ) + (k:ℝ)^theta⌉ := (Finset.mem_Ioo.mp hpI).2
              have h2 : ⌈(k:ℝ) + (k:ℝ)^theta⌉ ≤ (k:ℤ) + ⌊(k:ℝ)^theta⌋ + 1 := by
                rw [Int.ceil_le]; push_cast
                linarith [Int.lt_floor_add_one ((k:ℝ)^theta)]
              omega
            · by_contra hfar
              push_neg at hfar
              apply hne p.natAbs hpr (by rw [hqR]; exact hkp) (by rw [hqR]; exact hpb)
              exact dvd_from_far k n p.natAbs hk1 (by omega) (by rw [hqR]; exact hkp) (by rw [hqR]; exact hpb) (by rw [hqR]; exact hfar)

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 114–131 at 6ba7fea98468 ↗

      1. exists_far_prime.hsub.s1 obtain p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ ∧ (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta

         Leaves p ∈ badSet k n, with hpI : p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉, hp0 : (0 : ℤ) < p, hpr : Nat.Prime p.natAbs, hkp : (↑k : ℝ) < (↑p : ℝ), hpb : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta.

         Lean, line 117

               obtain ⟨hpI, hp0, hpr, hkp, hpb⟩ := hp

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 117 at 6ba7fea98468 ↗

      2. exists_far_prime.hsub.hq have (↑p.natAbs : ℤ) = p

         Leaves p ∈ badSet k n, with hq : (↑p.natAbs : ℤ) = p.

         Uses library Int.natAbs_of_nonneg.

         Lean, line 118

               have hq : ((p.natAbs : ℕ) : ℤ) = p := Int.natAbs_of_nonneg hp0.le

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 118 at 6ba7fea98468 ↗

      3. exists_far_prime.hsub.hqR have (↑p.natAbs : ℝ) = (↑p : ℝ)

         Leaves p ∈ badSet k n, with hqR : (↑p.natAbs : ℝ) = (↑p : ℝ).

         Uses library Int.cast_natCast.

         Lean, line 119

               have hqR : ((p.natAbs : ℕ) : ℝ) = (p : ℝ) := by rw [← Int.cast_natCast, hq]

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 119 at 6ba7fea98468 ↗

      4. exists_far_prime.hsub.s4 case

         Leaves (↑k : ℤ) < p.

         Lean, line 122

               · exact_mod_cast hkp

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 122 at 6ba7fea98468 ↗

      5. exists_far_prime.hsub.s5 case

         Leaves p < (↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (2 : ℤ).

         Lean, lines 123–127

               · have h1 : p < ⌈(k:ℝ) + (k:ℝ)^theta⌉ := (Finset.mem_Ioo.mp hpI).2
                 have h2 : ⌈(k:ℝ) + (k:ℝ)^theta⌉ ≤ (k:ℤ) + ⌊(k:ℝ)^theta⌋ + 1 := by
                   rw [Int.ceil_le]; push_cast
                   linarith [Int.lt_floor_add_one ((k:ℝ)^theta)]
                 omega

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 123–127 at 6ba7fea98468 ↗

         1. exists_far_prime.hsub.s5.h1 have p < ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉

            Leaves p < (↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (2 : ℤ), with h1 : p < ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉.

            Uses library Finset.mem_Ioo.

            Lean, line 123

                  · have h1 : p < ⌈(k:ℝ) + (k:ℝ)^theta⌉ := (Finset.mem_Ioo.mp hpI).2

            targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 123 at 6ba7fea98468 ↗

         2. exists_far_prime.hsub.s5.h2 have ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ ≤ (↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (1 : ℤ)

            Leaves p < (↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (2 : ℤ), with h2 : ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ ≤ (↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (1 : ℤ).

            Uses library Int.ceil_le, Int.lt_floor_add_one.

            Lean, lines 124–126

                    have h2 : ⌈(k:ℝ) + (k:ℝ)^theta⌉ ≤ (k:ℤ) + ⌊(k:ℝ)^theta⌋ + 1 := by
                      rw [Int.ceil_le]; push_cast
                      linarith [Int.lt_floor_add_one ((k:ℝ)^theta)]

            targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 124–126 at 6ba7fea98468 ↗

      6. exists_far_prime.hsub.s6 case

         Leaves |(↑n : ℝ) / (↑p : ℝ) - (↑(round ((↑n : ℝ) / (↑p : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta).

         Lean, lines 128–131

               · by_contra hfar
                 push_neg at hfar
                 apply hne p.natAbs hpr (by rw [hqR]; exact hkp) (by rw [hqR]; exact hpb)
                 exact dvd_from_far k n p.natAbs hk1 (by omega) (by rw [hqR]; exact hkp) (by rw [hqR]; exact hpb) (by rw [hqR]; exact hfar)

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 128–131 at 6ba7fea98468 ↗

   2. exists_far_prime.hc have {p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta}.card ≤ (badSet k n).card

      Leaves False, with hc : {p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ theta⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta}.card ≤ (badSet k n).card.

      Uses library Finset.card_le_card.

      Lean, line 132

          have hc := Finset.card_le_card hsub

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 132 at 6ba7fea98468 ↗

   3. exists_far_prime.hc2 have primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta) ≤ (badSet k n).card

      Leaves False, with hc2 : primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta) ≤ (badSet k n).card.

      Lean, line 133

          have hc2 : primeCard (k:ℝ) ((k:ℝ) + (k:ℝ)^theta) ≤ (badSet k n).card := hc

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 133 at 6ba7fea98468 ↗

   4. exists_far_prime.hc' have (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ) ≤ (↑(badSet k n).card : ℝ)

      Leaves False, with hc' : (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ) ≤ (↑(badSet k n).card : ℝ).

      Lean, line 134

          have hc' : (primeCard (k:ℝ) ((k:ℝ) + (k:ℝ)^theta) : ℝ) ≤ ((badSet k n).card : ℝ) := by exact_mod_cast hc2

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 134 at 6ba7fea98468 ↗

8. tendsto_log_rpow_mul_rpow_neg have ∀ (b c : ℝ), (0 : ℝ) < c → Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b * x ^ (-c)) Filter.atTop (nhds (0 : ℝ))

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with tendsto_log_rpow_mul_rpow_neg : ∀ (b c : ℝ), (0 : ℝ) < c → Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b * x ^ (-c)) Filter.atTop (nhds (0 : ℝ)).

   Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , 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. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , Filter.eventually_gt_atTop, div_eq_mul_inv Dividing by an element is the same as multiplying by its inverse. , Real.rpow_neg See also rpow_neg_eq_inv_rpow for a version with x⁻¹ ^ y in the RHS. .

   Lean, lines 136–143

     have 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
       intro b c hc
       clear * - b c hc
       -- 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 ] ;

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 136–143 at 6ba7fea98468 ↗

   1. tendsto_log_rpow_mul_rpow_neg.h_log have (fun (x : ℝ) => Real.log x ^ b) =o[Filter.atTop] fun (x : ℝ) => x ^ c

      Leaves Filter.Tendsto (fun (x : ℝ) => Real.log x ^ b * x ^ (-c)) Filter.atTop (nhds (0 : ℝ)), with h_log : (fun (x : ℝ) => Real.log x ^ b) =o[Filter.atTop] fun (x : ℝ) => x ^ c.

      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. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , isLittleO_log_rpow_rpow_atTop.

      Lean, lines 140–141

          have h_log : (fun x : ℝ => Real.log x ^ b) =o[Filter.atTop] (fun x : ℝ => x ^ c) :=
            isLittleO_log_rpow_rpow_atTop b hc

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 140–141 at 6ba7fea98468 ↗

9. poly_log_lt have ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ)

   Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with poly_log_lt : ∀ (A α β tt : ℝ), α < tt → ∀ (C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ).

   Uses library Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , 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. , gt_mem_nhds, Filter.eventually_gt_atTop, div_lt_iff₀ See div_lt_iff₀' for a version with multiplication on the other side. , div_pos, Real.rpow_pos_of_pos, Nat.cast_pos Specialisation of Nat.cast_pos', which seems to be easier for Lean to use. , Real.log_pos, Nat.one_lt_cast.

   Lean, lines 144–159

     have 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
       intro A α β tt hα C hC
       clear * - tendsto_log_rpow_mul_rpow_neg A α β tt hα C hC
       -- 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

   targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 144–159 at 6ba7fea98468 ↗

   1. poly_log_lt.h_lim have Filter.Tendsto (fun (k : ℕ) => A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β / ((↑k : ℝ) ^ tt / Real.log (↑k : ℝ))) Filter.atTop (nhds (0 : ℝ))

      Leaves ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), with h_lim : Filter.Tendsto (fun (k : ℕ) => A * (↑k : ℝ) ^ α * Real.log (↑k : ℝ) ^ β / ((↑k : ℝ) ^ tt / Real.log (↑k : ℝ))) Filter.atTop (nhds (0 : ℝ)).

      Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , 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. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. .

      Lean, lines 149–157

          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;

      targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 149–157 at 6ba7fea98468 ↗

      1. poly_log_lt.h_lim.h_simp suffices Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ))

         Leaves Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ)).

         Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , 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. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , Filter.eventually_gt_atTop, Real.rpow_sub, Real.rpow_add, Real.log_pos, Nat.one_lt_cast, Real.rpow_one.

         Lean, lines 151–154

               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;

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 151–154 at 6ba7fea98468 ↗

      2. poly_log_lt.h_lim.this have Filter.Tendsto (fun (x : ℝ) => Real.log x ^ (β + (1 : ℝ)) * x ^ (-(tt - α))) Filter.atTop (nhds (0 : ℝ))

         Leaves Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ)), with this : Filter.Tendsto (fun (x : ℝ) => Real.log x ^ (β + (1 : ℝ)) * x ^ (-(tt - α))) Filter.atTop (nhds (0 : ℝ)).

         Lean, line 155

               have := @tendsto_log_rpow_mul_rpow_neg ( β + 1 ) ( tt - α ) ?_;

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 155 at 6ba7fea98468 ↗

      3. poly_log_lt.h_lim.s3 case

         Leaves Filter.Tendsto (fun (k : ℕ) => A * Real.log (↑k : ℝ) ^ (β + (1 : ℝ)) * (↑k : ℝ) ^ (α - tt)) Filter.atTop (nhds (0 : ℝ)), with this : Filter.Tendsto (fun (x : ℝ) => Real.log x ^ (β + (1 : ℝ)) * x ^ (-(tt - α))) Filter.atTop (nhds (0 : ℝ)).

         Uses library Filter.Tendsto.comp, tendsto_natCast_atTop_atTop.

         Lean, line 156

               · convert this.const_mul A |> Filter.Tendsto.comp <| tendsto_natCast_atTop_atTop using 2 <;> norm_num ; ring;

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 156 at 6ba7fea98468 ↗

      4. poly_log_lt.h_lim.s4 case routine: linarith

         Leaves (0 : ℝ) < tt - α.

         Lean, line 157

               · linarith;

         targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 157 at 6ba7fea98468 ↗

10. poly_log_lt_eq have ∀ (A tt C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ tt * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ)

    Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with poly_log_lt_eq : ∀ (A tt C : ℝ), (0 : ℝ) < C → ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ tt * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ).

    Uses library Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , 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. , Filter.eventually_gt_atTop, Real.rpow_neg See also rpow_neg_eq_inv_rpow for a version with x⁻¹ ^ y in the RHS. , Real.rpow_two, div_le_div_iff_of_pos_right, div_le_iff₀ See div_le_iff₀' for a version with multiplication on the other side. , mul_le_mul_of_nonneg_right.

    Lean, lines 160–174

      have 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
        intro A tt C hC
        clear * - A tt C hC
        -- 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]

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 160–174 at 6ba7fea98468 ↗

    1. poly_log_lt_eq.h_log_bound have ∀ᶠ (k : ℕ) in Filter.atTop, A ≤ C * Real.log (↑k : ℝ)

       Leaves ∀ᶠ (k : ℕ) in Filter.atTop, A * (↑k : ℝ) ^ tt * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), with h_log_bound : ∀ᶠ (k : ℕ) in Filter.atTop, A ≤ C * Real.log (↑k : ℝ).

       Uses library Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , 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. , Filter.eventually_atTop, Exists.intro Existential introduction. , Real.exp The real exponential function, defined as the real part of the complex exponential , Nat.le_ceil, Real.log_exp, Real.log_le_log, le_of_lt, Nat.lt_of_ceil_lt, mul_div_cancel₀.

       Lean, lines 165–166

           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' ] ⟩;

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 165–166 at 6ba7fea98468 ↗

    2. poly_log_lt_eq.hl have (0 : ℝ) < Real.log (↑k : ℝ)

       Leaves A * (↑k : ℝ) ^ tt * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), with hl : (0 : ℝ) < Real.log (↑k : ℝ).

       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_pos.

       Lean, line 168

           have hl : 0 < Real.log k := Real.log_pos (by exact_mod_cast hk₂)

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 168 at 6ba7fea98468 ↗

    3. poly_log_lt_eq.hp have (0 : ℝ) ≤ (↑k : ℝ) ^ tt

       Leaves A * (↑k : ℝ) ^ tt * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), with hp : (0 : ℝ) ≤ (↑k : ℝ) ^ tt.

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

       Lean, line 169

           have hp : 0 ≤ (k:ℝ)^tt := Real.rpow_nonneg (Nat.cast_nonneg _) _

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 169 at 6ba7fea98468 ↗

    4. poly_log_lt_eq.e have A * (↑k : ℝ) ^ tt * (Real.log (↑k : ℝ) ^ (2 : ℕ))⁻¹ = A * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ) / Real.log (↑k : ℝ) routine: field_simp

       Leaves A * (↑k : ℝ) ^ tt * (Real.log (↑k : ℝ) ^ (2 : ℕ))⁻¹ ≤ C * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ), with e : A * (↑k : ℝ) ^ tt * (Real.log (↑k : ℝ) ^ (2 : ℕ))⁻¹ = A * (↑k : ℝ) ^ tt / Real.log (↑k : ℝ) / Real.log (↑k : ℝ).

       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 171–172

           have e : A * (k:ℝ)^tt * (Real.log k ^ 2)⁻¹ = A * (k:ℝ)^tt / Real.log k / Real.log k := by
             field_simp

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 171–172 at 6ba7fea98468 ↗

11. konyagin_finish have ∀ (k : ℕ) (n : ℤ), (1 : ℕ) ≤ k → ∀ (C : ℝ), C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) ≤ (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ) → (↑(badSet k n).card : ℝ) < C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n

    Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with konyagin_finish : ∀ (k : ℕ) (n : ℤ), (1 : ℕ) ≤ k → ∀ (C : ℝ), C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) ≤ (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ) → (↑(badSet k n).card : ℝ) < C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n.

    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. , Exists.intro Existential introduction. .

    Lean, lines 175–183

      have 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
        intro k n hk1 C hbhp hcard
        clear * - exists_far_prime k n hk1 C hbhp hcard
        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

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 175–183 at 6ba7fea98468 ↗

    1. konyagin_finish.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with p : ℕ, hp : Nat.Prime p, hpk : (↑k : ℝ) < (↑p : ℝ), hpb : (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta, hdvd : (↑p : ℤ) ∣ Pprod k n.

       Uses library lt_of_lt_of_le.

       Lean, line 180

           obtain ⟨p, hp, hpk, hpb, hdvd⟩ := exists_far_prime k n hk1 (lt_of_lt_of_le hcard hbhp)

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 180 at 6ba7fea98468 ↗

    2. konyagin_finish.this have (0 : ℝ) ≤ (↑k : ℝ) ^ theta

       Leaves (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta, with this : (0 : ℝ) ≤ (↑k : ℝ) ^ theta.

       Uses library Real.rpow_nonneg.

       Lean, line 182

           have : (0 : ℝ) ≤ (k : ℝ) ^ theta := Real.rpow_nonneg (by positivity) _

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 182 at 6ba7fea98468 ↗

12. med_rhs_le have ∀ (C : ℝ), (0 : ℝ) < C → ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

    Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with med_rhs_le : ∀ (C : ℝ), (0 : ℝ) < C → ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

    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. , Exists.intro Existential introduction. , Max.max Returns the greater of its two arguments. .

    Lean, lines 185–206

      have med_rhs_le : ∀ (C : ℝ) (hC : 0 < C), ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → g_med k ≤ C * (k : ℝ) ^ theta / Real.log k := by
        intro C hC
        clear * - poly_log_lt poly_log_lt_eq theta_pos theta_lt_one C hC
        -- Apply `poly_log_lt` three times to get each term's bound, then combine them.
        have h1 : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → 3 ≤ (C / 3) * (k : ℝ) ^ theta / Real.log k := by
          have := poly_log_lt 3 0 0 theta theta_pos ( C / 3 ) ( by linarith ) ; aesop;
        have h2 : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → 56 * (k : ℝ) ^ (2 * theta - 1) ≤ (C / 3) * (k : ℝ) ^ theta / Real.log k := by
          convert poly_log_lt 56 ( 2 * theta - 1 ) 0 theta ( by linarith [ theta_pos, theta_lt_one ] ) ( C / 3 ) ( by linarith ) using 1;
          norm_num [ Filter.eventually_atTop ]
        have h3 : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → (k : ℝ) ^ theta * (Real.log k) ^ (-(2 : ℝ)) ≤ (C / 3) * (k : ℝ) ^ theta / Real.log k := by
          convert poly_log_lt_eq 1 theta ( C / 3 ) ( by linarith ) using 1;
          norm_num [ Filter.eventually_atTop ];
        obtain ⟨a1, h1'⟩ := h1
        obtain ⟨a2, h2'⟩ := h2
        obtain ⟨a3, h3'⟩ := h3
        refine ⟨max a1 (max a2 a3), fun k hk => ?_⟩
        have x1 := h1' k (le_trans (le_max_left _ _) hk)
        have x2 := h2' k (le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk)
        have x3 := h3' k (le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk)
        simp only [g_med]
        have e : C * (k:ℝ) ^ theta / Real.log k = 3 * (C / 3 * (k:ℝ) ^ theta / Real.log k) := by ring
        linarith

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 185–206 at 6ba7fea98468 ↗

    1. med_rhs_le.h1 have ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with h1 : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       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 189–190

           have h1 : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → 3 ≤ (C / 3) * (k : ℝ) ^ theta / Real.log k := by
             have := poly_log_lt 3 0 0 theta theta_pos ( C / 3 ) ( by linarith ) ; aesop;

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 189–190 at 6ba7fea98468 ↗

       1. med_rhs_le.h1.this have ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) * (↑k : ℝ) ^ (0 : ℝ) * Real.log (↑k : ℝ) ^ (0 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

          Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with this : ∀ᶠ (k : ℕ) in Filter.atTop, (3 : ℝ) * (↑k : ℝ) ^ (0 : ℝ) * Real.log (↑k : ℝ) ^ (0 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

          Lean, line 190

                have := poly_log_lt 3 0 0 theta theta_pos ( C / 3 ) ( by linarith ) ; aesop;

          targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 190 at 6ba7fea98468 ↗

    2. med_rhs_le.h2 have ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with h2 : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       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. , Filter.eventually_atTop.

       Lean, lines 191–193

           have h2 : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → 56 * (k : ℝ) ^ (2 * theta - 1) ≤ (C / 3) * (k : ℝ) ^ theta / Real.log k := by
             convert poly_log_lt 56 ( 2 * theta - 1 ) 0 theta ( by linarith [ theta_pos, theta_lt_one ] ) ( C / 3 ) ( by linarith ) using 1;
             norm_num [ Filter.eventually_atTop ]

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 191–193 at 6ba7fea98468 ↗

    3. med_rhs_le.h3 have ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with h3 : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       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. , Filter.eventually_atTop.

       Lean, lines 194–196

           have h3 : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → (k : ℝ) ^ theta * (Real.log k) ^ (-(2 : ℝ)) ≤ (C / 3) * (k : ℝ) ^ theta / Real.log k := by
             convert poly_log_lt_eq 1 theta ( C / 3 ) ( by linarith ) using 1;
             norm_num [ Filter.eventually_atTop ];

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 194–196 at 6ba7fea98468 ↗

    4. med_rhs_le.s4 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with a1 : ℕ, h1' : ∀ (k : ℕ), a1 ≤ k → (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Lean, line 197

           obtain ⟨a1, h1'⟩ := h1

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 197 at 6ba7fea98468 ↗

    5. med_rhs_le.s5 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with a2 : ℕ, h2' : ∀ (k : ℕ), a2 ≤ k → (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Lean, line 198

           obtain ⟨a2, h2'⟩ := h2

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 198 at 6ba7fea98468 ↗

    6. med_rhs_le.s6 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with a3 : ℕ, h3' : ∀ (k : ℕ), a3 ≤ k → (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Lean, line 199

           obtain ⟨a3, h3'⟩ := h3

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 199 at 6ba7fea98468 ↗

    7. med_rhs_le.x1 have (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with x1 : (3 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_left.

       Lean, line 201

           have x1 := h1' k (le_trans (le_max_left _ _) hk)

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 201 at 6ba7fea98468 ↗

    8. med_rhs_le.x2 have (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with x2 : (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_left, le_max_right.

       Lean, line 202

           have x2 := h2' k (le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk)

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 202 at 6ba7fea98468 ↗

    9. med_rhs_le.x3 have (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with x3 : (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_right.

       Lean, line 203

           have x3 := h3' k (le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk)

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 203 at 6ba7fea98468 ↗

    10. med_rhs_le.e have C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) = (3 : ℝ) * (C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)) routine: ring

        Leaves (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * theta - (1 : ℝ)) + (↑k : ℝ) ^ theta * Real.log (↑k : ℝ) ^ (-2 : ℝ) ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ), with e : C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) = (3 : ℝ) * (C / (3 : ℝ) * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)).

        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, line 205

            have e : C * (k:ℝ) ^ theta / Real.log k = 3 * (C / 3 * (k:ℝ) ^ theta / Real.log k) := by ring

        targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 205 at 6ba7fea98468 ↗

13. med_card_bound have ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑(badSet k n).card : ℝ) < g_med k

    Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with med_card_bound : ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑(badSet k n).card : ℝ) < g_med k.

    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. , Exists.intro Existential introduction. .

    Lean, lines 209–222

      have med_card_bound : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ, (1 / 2) * (k : ℝ) ^ (2 - theta) < (n : ℝ) → (n : ℝ) ≤ (k : ℝ) ^ 2 / (Real.log k) ^ 2 → ((badSet k n).card : ℝ) < g_med k := by
        obtain ⟨k₀, hk₀⟩ := h_count
        refine ⟨k₀, fun k hk n h1 h2 => ?_⟩
        have hc := hk₀ k hk n h1 h2
        have e : 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 [e]
        exact hc

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 209–222 at 6ba7fea98468 ↗

    1. med_card_bound.s1 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑{m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ (21 / 40 : ℝ)⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ))}.card : ℝ) < (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * (21 / 40 : ℝ) - (1 : ℝ)) + (↑k : ℝ) ^ (21 / 40 : ℝ) * Real.log (↑k : ℝ) ^ (-2 : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑(badSet k n).card : ℝ) < g_med k, with k₀ : ℕ, hk₀ : ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑{m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ (21 / 40 : ℝ)⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ))}.card : ℝ) < (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * (21 / 40 : ℝ) - (1 : ℝ)) + (↑k : ℝ) ^ (21 / 40 : ℝ) * Real.log (↑k : ℝ) ^ (-2 : ℝ).

       Lean, line 210

           obtain ⟨k₀, hk₀⟩ := h_count

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 210 at 6ba7fea98468 ↗

    2. med_card_bound.hc have (↑{m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ (21 / 40 : ℝ)⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ))}.card : ℝ) < (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * (21 / 40 : ℝ) - (1 : ℝ)) + (↑k : ℝ) ^ (21 / 40 : ℝ) * Real.log (↑k : ℝ) ^ (-2 : ℝ)

       Leaves (↑(badSet k n).card : ℝ) < g_med k, with hc : (↑{m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ (21 / 40 : ℝ)⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ))}.card : ℝ) < (3 : ℝ) + (56 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) * (21 / 40 : ℝ) - (1 : ℝ)) + (↑k : ℝ) ^ (21 / 40 : ℝ) * Real.log (↑k : ℝ) ^ (-2 : ℝ).

       Lean, line 212

           have hc := hk₀ k hk n h1 h2

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 212 at 6ba7fea98468 ↗

    3. med_card_bound.e have badSet k n = {m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta)}

       Leaves (↑(badSet k n).card : ℝ) < g_med k, with e : badSet k n = {m ∈ Finset.Ioo (↑k : ℤ) ((↑k : ℤ) + ⌊(↑k : ℝ) ^ theta⌋ + (2 : ℤ)) | (↑k : ℤ) < m ∧ (↑m : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ theta ∧ |(↑n : ℝ) / (↑m : ℝ) - (↑(round ((↑n : ℝ) / (↑m : ℝ))) : ℝ)| < (1 : ℝ) / (↑k : ℝ) ^ ((1 : ℝ) - theta)}.

       Uses library Finset.Ioo The finset $(a, b)$ of elements x such that a < x and x < b. , round round x rounds x to the nearest integer, breaking ties towards positive infinity. , Finset.filter_congr, Finset.mem_Ioo, Iff.intro If a → b and b → a then a and b are equivalent. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

       Lean, lines 213–220

           have e : 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⟩

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 213–220 at 6ba7fea98468 ↗

14. case_medium have BHP → ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n

    Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with case_medium : BHP → ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n.

    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. , Exists.intro Existential introduction. , Max.max Returns the greater of its two arguments. .

    Lean, lines 223–245

      have case_medium : ∀ (hB : BHP), ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
        (1 / 2) * (k : ℝ) ^ (2 - theta) < (n : ℝ) →
        (n : ℝ) ≤ (k : ℝ) ^ 2 / (Real.log k) ^ 2 →
        ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + 3 * (k : ℝ) ^ theta ∧
          (p : ℤ) ∣ Pprod k n := by
        intro hB
        clear * - med_card_bound med_rhs_le konyagin_finish hB
        obtain ⟨C, hC, kb, hb⟩ := hB
        obtain ⟨k1, hk1card⟩ := med_card_bound
        obtain ⟨k2, hk2rhs⟩ := med_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) : ℝ) := by
          exact 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

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 223–245 at 6ba7fea98468 ↗

    1. case_medium.s1 obtain BHP

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with C : ℝ, hC : (0 : ℝ) < C, kb : ℕ, hb : ∀ (k : ℕ), kb ≤ k → C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) ≤ (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ).

       Lean, line 230

           obtain ⟨C, hC, kb, hb⟩ := hB

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 230 at 6ba7fea98468 ↗

    2. case_medium.s2 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑(badSet k n).card : ℝ) < g_med k

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with k1 : ℕ, hk1card : ∀ (k : ℕ), k1 ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → (↑(badSet k n).card : ℝ) < g_med k.

       Lean, line 231

           obtain ⟨k1, hk1card⟩ := med_card_bound

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 231 at 6ba7fea98468 ↗

    3. case_medium.s3 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

       Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with k2 : ℕ, hk2rhs : ∀ (k : ℕ), k2 ≤ k → g_med k ≤ C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

       Lean, line 232

           obtain ⟨k2, hk2rhs⟩ := med_rhs_le C hC

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 232 at 6ba7fea98468 ↗

    4. case_medium.hkb have kb ≤ k

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hkb : kb ≤ k.

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_left.

       Lean, line 235

           have hkb : kb ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 235 at 6ba7fea98468 ↗

    5. case_medium.hki1 have k1 ≤ k

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hki1 : k1 ≤ k.

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_right, le_max_left.

       Lean, line 236

           have hki1 : k1 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 236 at 6ba7fea98468 ↗

    6. case_medium.hki2 have k2 ≤ k

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hki2 : k2 ≤ k.

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_left, le_max_right.

       Lean, line 237

           have hki2 : k2 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 237 at 6ba7fea98468 ↗

    7. case_medium.hk2le have (2 : ℕ) ≤ k

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hk2le : (2 : ℕ) ≤ k.

       Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_right.

       Lean, line 238

           have hk2le : 2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 238 at 6ba7fea98468 ↗

    8. case_medium.hk1 have (1 : ℕ) ≤ k routine: omega

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hk1 : (1 : ℕ) ≤ k.

       Lean, line 239

           have hk1 : 1 ≤ k := by omega

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 239 at 6ba7fea98468 ↗

    9. case_medium.hbhp have C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) ≤ (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ)

       Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hbhp : C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ) ≤ (↑(primeCard (↑k : ℝ) ((↑k : ℝ) + (↑k : ℝ) ^ theta)) : ℝ).

       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 240–242

           have hbhp : C * (k : ℝ) ^ theta / Real.log k ≤
               (primeCard (k : ℝ) ((k : ℝ) + (k : ℝ) ^ theta) : ℝ) := by
             exact hb k hkb

       targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 240–242 at 6ba7fea98468 ↗

    10. case_medium.hcard have (↑(badSet k n).card : ℝ) < C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ)

        Leaves ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n, with hcard : (↑(badSet k n).card : ℝ) < C * (↑k : ℝ) ^ theta / Real.log (↑k : ℝ).

        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. , lt_of_lt_of_le.

        Lean, lines 243–244

            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)

        targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, lines 243–244 at 6ba7fea98468 ↗

15. s15 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n

    Leaves ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), with k₀ : ℕ, hk₀ : ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - theta) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ theta ∧ (↑p : ℤ) ∣ Pprod k n.

    Lean, line 247

      obtain ⟨k₀, hk₀⟩ := case_medium hB0

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 247 at 6ba7fea98468 ↗

16. close term ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))

    Closes the goal.

    Uses library Exists.intro Existential introduction. .

    Lean, line 248

      exact ⟨k₀, hk₀⟩

    targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean, line 248 at 6ba7fea98468 ↗