Konyagin's bound on m with n/m near an integer

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1015-r; merged in d64a3b864afa under attestations/000530.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1/attempts/20261015T023339Z-t1015-r-partial.lean.

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

open scoped Nat

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

private noncomputable def intIcc (M : ℝ) : Finset ℤ := Finset.Icc 0 ⌊M⌋

/-- A point `u` is `(f, W, δ)`-good if there exist `v ∈ ℤ` and `w ∈ ℕ` with
    `w > 0`, `w ≤ W`, and `|f(u) - v/w| < δ`. -/
private noncomputable def IsGood (f : ℝ → ℝ) (W δ : ℝ) (u : ℤ) : Prop :=
  ∃ (v : ℤ) (w : ℕ), 0 < w ∧ (w : ℝ) ≤ W ∧ |f (u : ℝ) - (v : ℝ) / (w : ℝ)| < δ


private noncomputable def smoothDenom (k x : ℝ) : ℝ :=
  k / 2 + (x + k / 2) * Real.smoothTransition ((4 * x + 2 * k) / k)

/-- The globally smooth modification of `f(x) = (-1)^r n / (k + x)`. -/
private noncomputable def fK (n k : ℝ) (r : ℕ) (x : ℝ) : ℝ := ((-1 : ℝ) ^ r * n) / smoothDenom k x

/-
`smoothDenom k` is positive everywhere when `k > 0`.
-/
private lemma smoothDenom_pos (k : ℝ) (hk : 0 < k) (x : ℝ) : 0 < smoothDenom k x := by
  unfold smoothDenom;
  by_cases h : x + k / 2 ≥ 0 <;> simp_all +decide;
  · exact add_pos_of_pos_of_nonneg ( half_pos hk ) ( mul_nonneg h ( Real.smoothTransition.nonneg _ ) );
  · rw [ Real.smoothTransition.zero_of_nonpos ] <;> nlinarith [ mul_div_cancel₀ ( 4 * x + 2 * k ) hk.ne' ]

/-
`smoothDenom k x = k + x` for `x ≥ -k/4`.
-/
private lemma smoothDenom_eq (k : ℝ) (hk : 0 < k) (x : ℝ) (hx : -k / 4 ≤ x) :
    smoothDenom k x = k + x := by
  unfold smoothDenom; rw [ Real.smoothTransition.one_of_one_le ( by rw [ le_div_iff₀ hk ] ; linarith ) ] ; ring;

/-
`smoothDenom k` is smooth.
-/
private lemma smoothDenom_contDiff (k : ℝ) (m : ℕ∞) :
    ContDiff ℝ (m : WithTop ℕ∞) (smoothDenom k) := by
  refine' ContDiff.add contDiff_const _;
  refine' ContDiff.mul ( contDiff_id.add contDiff_const ) _;
  exact ContDiff.comp ( Real.smoothTransition.contDiff ) ( by exact ContDiff.div_const ( by exact ContDiff.add ( contDiff_const.mul contDiff_id ) contDiff_const ) _ )

/-
`fK n k r` is smooth, given `k > 0`.
-/
private lemma fK_contDiff (n k : ℝ) (hk : 0 < k) (r : ℕ) (m : ℕ∞) :
    ContDiff ℝ (m : WithTop ℕ∞) (fK n k r) := by
  exact ContDiff.div ( contDiff_const ) ( smoothDenom_contDiff k m ) fun x => ne_of_gt ( smoothDenom_pos k hk x )

/-
The iterated derivatives of `fK` on `[0, ∞)` are given by the explicit formula
for `(-1)^r n / (k + x)`.
-/
private lemma iteratedDeriv_fK (n k : ℝ) (hk : 0 < k) (r j : ℕ) (x : ℝ) (hx : 0 ≤ x) :
    iteratedDeriv j (fK n k r) x
      = ((-1 : ℝ) ^ r * n) * ((-1) ^ j * (j ! : ℝ) * (k + x) ^ (-1 - (j : ℤ))) := by
  -- Apply the equality we've shown in the neighborhood to the specific point x.
  have h_eq_at_x : iteratedDeriv j (fK n k r) x = iteratedDeriv j (fun y => (-1 : ℝ) ^ r * n / (k + y)) x := by
    apply Filter.EventuallyEq.iteratedDeriv_eq
    generalize_proofs at *; (
    filter_upwards [ lt_mem_nhds ( show x > -k / 4 by linarith ) ] with y hy using by unfold fK; rw [ smoothDenom_eq k hk y ( by linarith ) ] ;)
  generalize_proofs at *; (
  -- Apply the chain rule to compute the derivative.
  have h_chain : iteratedDeriv j (fun y => (-1 : ℝ) ^ r * n / (k + y)) x = (-1 : ℝ) ^ r * n * iteratedDeriv j (fun y => 1 / (k + y)) x := by
    convert iteratedDeriv_const_mul ( ( -1 ) ^ r * n ) _ using 1 ; norm_num [ div_eq_mul_inv ];
    have hc : ContDiffAt ℝ (↑j) (fun y : ℝ => k + y) x := contDiffAt_const.add contDiffAt_id
    have h2 := hc.inv (by show k + x ≠ 0; intro h; linarith)
    have e : (fun y : ℝ => 1 / (k + y)) = (fun y => k + y)⁻¹ := by
      funext y; simp [one_div]
    rw [e]; exact h2
  generalize_proofs at *; (
  convert h_eq_at_x.trans h_chain using 1
  generalize_proofs at *; (
  -- By definition of $fK$, we know that its $j$-th derivative is given by the formula.
  have h_deriv : iteratedDeriv j (fun y => 1 / (k + y)) x = (-1 : ℝ) ^ j * (Nat.factorial j) * (k + x) ^ (-1 - j : ℤ) := by
    have hs : IsOpen {y : ℝ | (0:ℝ) < y} := isOpen_lt continuous_const continuous_id
    have hmem : k + x ∈ {y : ℝ | (0:ℝ) < y} := by simp; linarith
    have heq := iteratedDerivWithin_of_isOpen (n := j) (f := fun y : ℝ => 1/y) hs hmem
    rw [show (fun y : ℝ => 1 / (k + y)) = (fun z : ℝ => (fun y : ℝ => 1/y) (k + z)) from rfl,
        iteratedDeriv_comp_const_add]
    simp only []
    rw [← heq]
    exact iteratedDerivWithin_one_div j hs hmem
  generalize_proofs at *; (
  grind +splitIndPred))))

/-
Absolute value of the `r`-th derivative of `fK` on `[0, ∞)`.
-/
private lemma abs_iteratedDeriv_r (n k : ℝ) (hk : 0 < k) (hn : 0 < n) (r : ℕ) (x : ℝ)
    (hx : 0 ≤ x) :
    |iteratedDeriv r (fK n k r) x| = (n * (r ! : ℝ)) / (k + x) ^ (r + 1) := by
  rw [ iteratedDeriv_fK n k hk r r x hx ] ; norm_num [ abs_mul, abs_div, abs_pow, abs_of_pos hn, abs_of_pos ( add_pos_of_pos_of_nonneg hk hx ) ] ; ring_nf;
  rw [ show ( -1 - r : ℤ ) = - ( r + 1 ) by ring, zpow_neg ] ; norm_cast ; ring;

/-
Absolute value of the `(r+1)`-th derivative of `fK` on `[0, ∞)`.
-/
private lemma abs_iteratedDeriv_r1 (n k : ℝ) (hk : 0 < k) (hn : 0 < n) (r : ℕ) (x : ℝ)
    (hx : 0 ≤ x) :
    |iteratedDeriv (r + 1) (fK n k r) x| = (n * ((r + 1)! : ℝ)) / (k + x) ^ (r + 2) := by
  convert abs_iteratedDeriv_r n k hk hn ( r + 1 ) x hx using 1;
  unfold fK;
  norm_num [ pow_succ', div_eq_mul_inv ]

/-
The key ratio inequality: `(1 + u)^{r+1} ≤ 2` when `2 r u ≤ 1`.
-/
private lemma key_ratio (r : ℕ) (hr : 2 ≤ r) (u : ℝ) (hu : 0 ≤ u) (hru : 2 * (r : ℝ) * u ≤ 1) :
    (1 + u) ^ (r + 1) ≤ 2 := by
  -- For r ≥ 3, we have u ≤ 1/(2*r) ≤ 1/6, and (1+u)^4 ≤ 2.
  by_cases hr_ge_3 : r ≥ 3;
  · -- Using the exponential bound, we have $(1 + u)^{r+1} \leq \exp(u(r+1))$.
    have h_exp_bound : (1 + u) ^ (r + 1) ≤ Real.exp (u * (r + 1)) := by
      rw [ ← Real.rpow_natCast, Real.rpow_def_of_pos ( by positivity ) ];
      exact Real.exp_le_exp.mpr ( by push_cast; nlinarith [ Real.log_le_sub_one_of_pos ( by linarith : 0 < 1 + u ) ] );
    refine le_trans h_exp_bound ?_;
    rw [ ← Real.log_le_log_iff ( by positivity ) ( by positivity ), Real.log_exp ];
    exact le_trans ( by nlinarith [ show ( r : ℝ ) ≥ 3 by norm_cast ] ) ( Real.log_two_gt_d9.le );
  · interval_cases r ; norm_num at * ; nlinarith [ sq_nonneg u ]

/-
A good-point witness: if `n/(k+u)` is close to an integer, then `u` is
`(fK, 1, δ)`-good.
-/
private lemma isGood_fK (n k δ : ℝ) (hk : 0 < k) (r : ℕ) (u : ℤ) (hu : 0 ≤ u)
    (hdist : |(n : ℝ) / (k + (u : ℝ)) - round ((n : ℝ) / (k + (u : ℝ)))| < δ) :
    IsGood (fK n k r) 1 δ u := by
  refine' ⟨ _, _ ⟩;
  exact ( -1 ) ^ r * round ( n / ( k + u ) );
  refine' ⟨ 1, _, _, _ ⟩ <;> norm_num [ fK, smoothDenom_eq _ hk _ _ ];
  convert hdist using 1 ; rw [ smoothDenom_eq _ hk _ ( by linarith [ show ( u : ℝ ) ≥ 0 by positivity ] ) ] ; ring_nf;
  norm_num [ ← sub_mul, abs_mul ]

/-
The bound `(k + k^θ)^{r+1} ≤ 2 k^{r+1}`, which makes the lower and upper bounds
on `|f^{(r)}|` differ by a factor of at most 2.
-/
private lemma KplusN_pow_le (k : ℝ) (hk : 0 < k) (theta : ℝ) (r : ℕ) (hr : 2 ≤ r)
    (hr_le : (r : ℝ) ≤ (1 / 2) * k ^ (1 - theta)) :
    (k + k ^ theta) ^ (r + 1) ≤ 2 * k ^ (r + 1) := by
  -- Note that $k + k^\theta = k * (1 + k^{\theta-1})$.
  have h_factor : k + k ^ theta = k * (1 + k ^ (theta - 1)) := by
    rw [ Real.rpow_sub hk, Real.rpow_one ] ; ring_nf ; norm_num [ hk.ne' ];
    rw [ mul_right_comm, mul_inv_cancel₀ hk.ne', one_mul ];
  rw [ h_factor, mul_pow ];
  rw [ mul_comm ];
  exact mul_le_mul_of_nonneg_right ( key_ratio r hr _ ( Real.rpow_nonneg hk.le _ ) ( by rw [ show ( 1 - theta : ℝ ) = - ( theta - 1 ) by ring, Real.rpow_neg hk.le ] at hr_le; nlinarith [ Real.rpow_pos_of_pos hk ( theta - 1 ), mul_inv_cancel₀ ( ne_of_gt ( Real.rpow_pos_of_pos hk ( theta - 1 ) ) ) ] ) ) ( by positivity )

private lemma nat_k_ge_one (theta : ℝ) (htheta1 : theta < 1) (k r : ℕ) (hr2 : 2 ≤ r)
    (hr_le : (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - theta)) : 1 ≤ k := by
  rcases Nat.eq_zero_or_pos k with hk | hk
  · subst hk
    simp only [Nat.cast_zero] at hr_le
    rw [Real.zero_rpow (by linarith)] at hr_le
    have : (2 : ℝ) ≤ r := by exact_mod_cast hr2
    linarith
  · exact hk

/-
We apply `konyagin_thm` to the function `f(x) = (-1)^r n / (k + x)` on the
interval `[0, k^θ]` with `W = 1`.

The number of integers `m ∈ (k, k + k^θ)` with `‖n/m‖ < 1/k^{1-θ}` is bounded by
`(65536 : ℝ)·k^θ·((n·r!·λ^r/k^{r+1})^{1/(2r-1)} + (k^{r+θ}/(n·r!·λ^r))^{1/(r-1)}
  + ((r+1)·λ/k)^{1/(2r)}) + 2·r·λ`.
-/
private theorem konyagin_application (hK : ∀ (r : ℕ), 2 ≤ r → ∀ (N : ℝ), 0 < N → ∀ (W : ℝ), 1 ≤ W → ∀ (δ : ℝ), 0 < δ →
      ∀ (lam : ℝ), 1 ≤ lam → ∀ (D_r : ℝ), 0 < D_r → ∀ (D_r1 : ℝ), 0 < D_r1 →
      ∀ (f : ℝ → ℝ), ContDiff ℝ (↑(r + 1) : ℕ∞) f →
      (∀ x ∈ Set.Icc (0 : ℝ) N, D_r / 2 ≤ |iteratedDeriv r f x|) →
      (∀ x ∈ Set.Icc (0 : ℝ) N, |iteratedDeriv r f x| ≤ D_r) →
      (∀ x ∈ Set.Icc (0 : ℝ) N, |iteratedDeriv (r + 1) f x| ≤ D_r1) →
      ∀ (S : Finset ℤ), (∀ u ∈ S, (0 : ℤ) ≤ u ∧ u ≤ ⌊N⌋) →
      (∀ u ∈ S, ∃ (v : ℤ) (w : ℕ), 0 < w ∧ (w : ℝ) ≤ W ∧ |f (u : ℝ) - (v : ℝ) / (w : ℝ)| < δ) →
      (S.card : ℝ) < (65536 : ℝ) * N *
      ((D_r * lam ^ (r : ℕ) * W ^ 2) ^ ((2 * (r : ℝ) - 1)⁻¹) +
       (δ * W ^ 2 / (D_r * lam ^ (r : ℕ))) ^ (((r : ℝ) - 1)⁻¹) +
       (D_r1 * lam * W ^ 2 / D_r) ^ ((2 * (r : ℝ))⁻¹)) +
      2 * (r : ℝ) * lam)
    (lam theta : ℝ) (hlam : 1 ≤ lam) (htheta0 : 0 < theta) (htheta1 : theta < 1)
    (n : ℤ) (k r : ℕ) (hkn : (k : ℤ) < n) (hr2 : 2 ≤ r)
    (hr_le : (r : ℝ) ≤ (1 / 2) * (k : ℝ) ^ (1 - theta)) :
    (((Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ theta⌋ + 2)).filter
        (fun m : ℤ => (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧
          |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - theta))).card : ℝ)
      < (65536 : ℝ) * (k : ℝ) ^ theta *
          (((n : ℝ) * (r ! : ℝ) * lam ^ r / (k : ℝ) ^ (r + 1)) ^ ((2 * (r : ℝ) - 1)⁻¹) +
           ((k : ℝ) ^ ((r : ℝ) + theta) / ((n : ℝ) * (r ! : ℝ) * lam ^ r)) ^ (((r : ℝ) - 1)⁻¹) +
           (((r : ℝ) + 1) * lam / (k : ℝ)) ^ ((2 * (r : ℝ))⁻¹)) +
        2 * (r : ℝ) * lam := by
  have hk : (1 : ℤ) ≤ (k : ℤ) := by
    exact_mod_cast nat_k_ge_one theta htheta1 k r hr2 hr_le
  have hr_leK : (r : ℝ) ≤ (1 / 2) * ((k : ℤ) : ℝ) ^ (1 - theta) := by
    push_cast; exact hr_le
  rw [show (k : ℝ) = ((k : ℤ) : ℝ) from by norm_cast]
  set K : ℤ := (k : ℤ) with hKdef
  clear_value K
  clear hKdef
  -- Apply the Konyagin theorem with the given parameters.
  have hh := hK r hr2 (K ^ theta) (by
  positivity) 1 (by
  norm_num) (1 / K ^ (1 - theta)) (by
  positivity) lam hlam (n * (r ! : ℝ) / K ^ (r + 1)) (by
  exact div_pos ( mul_pos ( by norm_cast; linarith ) ( by positivity ) ) ( by positivity )) (n * ((r + 1)! : ℝ) / K ^ (r + 2)) (by
  exact div_pos ( mul_pos ( by norm_cast; linarith ) ( by positivity ) ) ( by positivity )) (fK n K r) (by
  exact fK_contDiff _ _ ( by positivity ) _ _) (by
  intro x hx
  have h_abs : |iteratedDeriv r (fK n K r) x| = (n * (r ! : ℝ)) / (K + x) ^ (r + 1) := by
    convert abs_iteratedDeriv_r n K ( by positivity ) ( by norm_cast; linarith ) r x hx.1 using 1
  rw [h_abs];
  rw [ div_div, div_le_div_iff₀ ] <;> try positivity;
  · have := KplusN_pow_le K (by positivity) theta r hr2 hr_leK; simp_all +decide [ mul_assoc, mul_comm ] ;
    exact mul_le_mul_of_nonneg_left ( mul_le_mul_of_nonneg_left ( le_trans ( pow_le_pow_left₀ ( by linarith [ show ( K : ℝ ) ≥ 1 by norm_cast ] ) ( by linarith ) _ ) this ) ( by positivity ) ) ( by norm_cast; linarith );
  · exact pow_pos ( by linarith [ hx.1, show ( K : ℝ ) ≥ 1 by norm_cast ] ) _) (by
  intro x hx
  have h_abs : |iteratedDeriv r (fK n K r) x| = (n * (r ! : ℝ)) / (K + x) ^ (r + 1) := by
    convert abs_iteratedDeriv_r n K ( by positivity ) ( by norm_cast; linarith ) r x hx.1 using 1;
  exact h_abs.symm ▸ div_le_div_of_nonneg_left ( by exact mul_nonneg ( by norm_cast; linarith ) ( by positivity ) ) ( by positivity ) ( by exact pow_le_pow_left₀ ( by positivity ) ( by linarith [ hx.1 ] ) _ )) (by
  intro x hx
  have h_abs : |iteratedDeriv (r + 1) (fK n K r) x| = n * ((r + 1)! : ℝ) / (K + x) ^ (r + 2) := by
    convert abs_iteratedDeriv_r1 n K ( by positivity ) ( by norm_cast; linarith ) r x hx.1 using 1;
  exact h_abs.symm ▸ div_le_div_of_nonneg_left ( by exact mul_nonneg ( by norm_cast; linarith ) ( by positivity ) ) ( by positivity ) ( by exact pow_le_pow_left₀ ( by positivity ) ( by linarith [ hx.1 ] ) _ ));
  convert hh ( Finset.image ( fun m : ℤ => m - K ) ( Finset.filter ( fun m : ℤ => ( m : ℝ ) < K + K ^ theta ∧ |( n : ℝ ) / m - round ( n / m : ℝ )| < 1 / K ^ ( 1 - theta ) ) ( Finset.Ioo K ( K + ⌊ ( K : ℝ ) ^ theta⌋ + 2 ) ) ) ) _ _ using 1 <;> norm_num [ Finset.card_image_of_injOn ];
  · field_simp;
    refine Or.inl <| congr_arg₂ _ ( congr_arg₂ _ rfl ?_ ) ?_ <;> norm_num [ Nat.factorial_succ ] ; ring_nf;
    · norm_num [ Real.rpow_add ( by positivity : 0 < ( K : ℝ ) ), Real.rpow_sub ( by positivity : 0 < ( K : ℝ ) ) ] ; ring_nf;
      simp +decide [ mul_assoc, mul_comm, mul_left_comm, ne_of_gt ( zero_lt_one.trans_le hk ) ];
    · congr 1 ; rw [ div_eq_div_iff ] <;> ring_nf <;> norm_cast <;> norm_num [ Nat.factorial_ne_zero, show K ≠ 0 by linarith, show n ≠ 0 by linarith ];
  · rintro x y hy₁ hy₂ hy₃ hy₄ rfl; exact ⟨ by linarith, by exact Int.le_of_lt_add_one <| by rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith [ Int.floor_le ( ( K : ℝ ) ^ theta ), Int.lt_floor_add_one ( ( K : ℝ ) ^ theta ) ] ⟩ ;
  · rintro u x hx₁ hx₂ hx₃ hx₄ rfl
    obtain ⟨v, w, h1, h2, h3⟩ := isGood_fK n K ( ( K ^ ( 1 - theta ) ) ⁻¹ ) ( by positivity ) r ( x - K ) ( by linarith ) ( by simpa using hx₄ )
    exact ⟨v, w, h1, by exact_mod_cast h2, h3⟩

/-
**Pigeonhole.** If the number of "bad" integers in `(k, k + k^θ)` is strictly
less than the number of primes in `(k, k + k^θ)`, then there is a prime
`p ∈ (k, k + k^θ)` dividing `P`.
-/

theorem erdos_1094__h2__h2__h2__h3__h1 : ∀ (lam : ℝ),
  (1 : ℝ) ≤ lam →
    ∀ (n : ℤ) (k r : ℕ),
      (↑k : ℤ) < n →
        (2 : ℕ) ≤ r →
          (↑r : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((1 : ℝ) - (21 / 40 : ℝ)) →
            (↑{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 :
                ℝ) <
              (65536 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) *
                  (((↑n : ℝ) * (↑r.factorial : ℝ) * lam ^ r / (↑k : ℝ) ^ (r + (1 : ℕ))) ^
                        ((2 : ℝ) * (↑r : ℝ) - (1 : ℝ))⁻¹ +
                      ((↑k : ℝ) ^ ((↑r : ℝ) + (21 / 40 : ℝ)) / ((↑n : ℝ) * (↑r.factorial : ℝ) * lam ^ r)) ^
                        ((↑r : ℝ) - (1 : ℝ))⁻¹ +
                    (((↑r : ℝ) + (1 : ℝ)) * lam / (↑k : ℝ)) ^ ((2 : ℝ) * (↑r : ℝ))⁻¹) +
                (2 : ℝ) * (↑r : ℝ) * lam := by
  have h_thm : ∀ (r : ℕ), 2 ≤ r → ∀ (N : ℝ), 0 < N → ∀ (W : ℝ), 1 ≤ W → ∀ (δ : ℝ), 0 < δ →
      ∀ (lam : ℝ), 1 ≤ lam → ∀ (D_r : ℝ), 0 < D_r → ∀ (D_r1 : ℝ), 0 < D_r1 →
      ∀ (f : ℝ → ℝ), ContDiff ℝ (↑(r + 1) : ℕ∞) f →
      (∀ x ∈ Set.Icc (0 : ℝ) N, D_r / 2 ≤ |iteratedDeriv r f x|) →
      (∀ x ∈ Set.Icc (0 : ℝ) N, |iteratedDeriv r f x| ≤ D_r) →
      (∀ x ∈ Set.Icc (0 : ℝ) N, |iteratedDeriv (r + 1) f x| ≤ D_r1) →
      ∀ (S : Finset ℤ), (∀ u ∈ S, (0 : ℤ) ≤ u ∧ u ≤ ⌊N⌋) →
      (∀ u ∈ S, ∃ (v : ℤ) (w : ℕ), 0 < w ∧ (w : ℝ) ≤ W ∧ |f (u : ℝ) - (v : ℝ) / (w : ℝ)| < δ) →
      (S.card : ℝ) < (65536 : ℝ) * N *
      ((D_r * lam ^ (r : ℕ) * W ^ 2) ^ ((2 * (r : ℝ) - 1)⁻¹) +
       (δ * W ^ 2 / (D_r * lam ^ (r : ℕ))) ^ (((r : ℝ) - 1)⁻¹) +
       (D_r1 * lam * W ^ 2 / D_r) ^ ((2 * (r : ℝ))⁻¹)) +
      2 * (r : ℝ) * lam := by
    sorry
  intro lam hlam n k r hkn hr2 hr_le
  have e : ((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 : ℝ)))) := by
    apply Finset.filter_congr
    intro x hx
    rw [Finset.mem_Ioo] at hx
    exact ⟨fun h => h.2, fun h => ⟨hx.1, h⟩⟩
  rw [e]
  exact konyagin_application h_thm lam (21 / 40 : ℝ) hlam (by norm_num) (by norm_num) n k r hkn hr2 hr_le