medium range: few m with n/m near an integer

Checked by the kernel — these bytes are the ones its attestation names: attestations/000527.json, merge commit 14c4ddbade6f.

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

open scoped Nat

/-! Hole `h_count` 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 theta : ℝ := 21 / 40

private lemma theta_pos : (0 : ℝ) < theta := by unfold theta; norm_num
private lemma theta_lt_one : theta < 1 := by unfold theta; norm_num

/-- The set of integers `m ∈ (k, k + k^θ)` such that `n/m` is within `1/k^{1-θ}`
of an integer. Its cardinality is exactly the quantity `K` bounded by
`konyagin_application`. -/
private noncomputable def badSet (k : ℕ) (n : ℤ) : Finset ℤ :=
  (Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ theta⌋ + 2)).filter
    (fun m : ℤ => (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧
      |(n : ℝ) / (m : ℝ) - round ((n : ℝ) / (m : ℝ))| < 1 / (k : ℝ) ^ (1 - theta))

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

private noncomputable def medWindow (k : ℕ) : Finset ℤ :=
  (Finset.Ioo (k : ℤ) ((k : ℤ) + ⌊(k : ℝ) ^ theta⌋ + 2)).filter
    (fun m : ℤ => (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta)

/-- The `h`-fiber: window integers `m` with `n/m` within `1/k^{1-θ}` of `h`. -/
private noncomputable def medFiber (k : ℕ) (n : ℤ) (h : ℤ) : Finset ℤ :=
  (medWindow k).filter (fun m : ℤ => |(n : ℝ) / (m : ℝ) - (h : ℝ)| < 1 / (k : ℝ) ^ (1 - theta))

/-- The set of integers `h` between `⌊n/(k+k^θ)⌋` and `⌈n/k⌉`. -/
private noncomputable def medJ (k : ℕ) (n : ℤ) : Finset ℤ :=
  Finset.Icc ⌊(n : ℝ) / ((k : ℝ) + (k : ℝ) ^ theta)⌋ ⌈(n : ℝ) / (k : ℝ)⌉

/-
At most `2L+1` integers `m` (within any finset) satisfy `|m - x| < L`.
-/
private lemma card_int_abs_sub_lt_le (x L : ℝ) (hL : 0 ≤ L) (S : Finset ℤ) :
    ((S.filter (fun m : ℤ => |(m : ℝ) - x| < L)).card : ℝ) ≤ 2 * L + 1 := by
  -- Every integer `m` with `|(m:ℝ) - x| < L` satisfies `x - L < m < x + L`.
  have h_filter_subset : S.filter (fun m : ℤ => |(m : ℝ) - x| < L) ⊆ Finset.Ioo (⌊x - L⌋) (⌈x + L⌉) := by
    intro m hm; simp_all +decide [ abs_lt ] ;
    exact ⟨ Int.floor_lt.2 ( by linarith ), Int.lt_ceil.2 ( by linarith ) ⟩;
  refine' le_trans _ ( show 2 * L + 1 ≥ ↑ ( Int.toNat ( ⌈x + L⌉ - ⌊x - L⌋ - 1 ) ) from _ );
  · refine' mod_cast le_trans ( Finset.card_le_card h_filter_subset ) _ ; simp +decide [ Int.card_Ioo ];
  · rcases n : ⌈x + L⌉ - ⌊x - L⌋ - 1 with ( _ | _ | n ) <;> simp_all +decide [ Int.toNat ];
    · rw [ ← @Int.cast_inj ℝ ] at * ; norm_num at * ; linarith [ Int.floor_le ( x - L ), Int.lt_floor_add_one ( x - L ), Int.le_ceil ( x + L ), Int.ceil_lt_add_one ( x + L ) ];
    · linarith;
    · linarith

/-
Every bad integer lies in some fiber indexed by `h ∈ medJ`.
-/
private lemma badSet_subset_biUnion (k : ℕ) (n : ℤ) (hk1 : 1 ≤ k) (hn : 0 < n) :
    badSet k n ⊆ (medJ k n).biUnion (medFiber k n) := by
  intro m hm; simp_all +decide ;
  refine' ⟨ round ( ( n : ℝ ) / m ), _, _ ⟩ <;> simp_all +decide [ medJ, medFiber ];
  · -- From `hmW` (unfold `medWindow`, `Finset.mem_filter`, `Finset.mem_Ioo`): `(k:ℤ) < m` and `(m:ℝ) < (k:ℝ)+(k:ℝ)^theta`. So `(k:ℝ) < (m:ℝ)` and `(m:ℝ) > 0`.
    have hm_bounds : (k : ℝ) < m ∧ m < (k : ℝ) + (k : ℝ) ^ theta := by
      exact ⟨ mod_cast Finset.mem_Ioo.mp ( Finset.mem_filter.mp hm |>.1 ) |>.1, Finset.mem_filter.mp hm |>.2.1 ⟩;
    constructor <;> rw [ round_eq ] <;> norm_num [ Int.floor_le, Int.le_ceil ] at *;
    · exact Int.floor_mono <| le_add_of_le_of_nonneg ( div_le_div_of_nonneg_left ( by positivity ) ( by linarith [ show ( k : ℝ ) ≥ 1 by norm_cast ] ) <| by linarith ) <| by positivity;
    · refine' Int.le_of_lt_add_one ( Int.floor_lt.mpr _ );
      norm_num +zetaDelta at *;
      linarith [ show ( n : ℝ ) / m < ( n : ℝ ) / k by gcongr ; linarith, Int.le_ceil ( ( n : ℝ ) / k ) ];
  · unfold badSet at hm; unfold medWindow at *; aesop;

/-
`|medJ| ≤ 3 + n / k^{2-θ}`.
-/
private lemma medJ_card_le (k : ℕ) (n : ℤ) (hk1 : 1 ≤ k) (hn : 0 < n) :
    ((medJ k n).card : ℝ) ≤ 3 + (n : ℝ) / (k : ℝ) ^ (2 - theta) := by
  -- By definition of медJ, we have
  have cei : (medJ k n).card ≤ (⌈(n : ℝ) / k⌉ - ⌊(n : ℝ) / (k + (k : ℝ) ^ theta)⌋ + 1) := by
    simp +decide [ medJ ];
    constructor <;> linarith [ show ⌊ ( n : ℝ ) / ( k + k ^ theta ) ⌋ ≤ ⌈ ( n : ℝ ) / k ⌉ from Int.floor_le_ceil _ |> le_trans <| Int.ceil_mono <| by gcongr ; linarith [ Real.rpow_nonneg ( Nat.cast_nonneg k ) theta ] ];
  -- By definition of ceiling and floor functions, we have:
  have h_ceil_floor : (⌈(n : ℝ) / k⌉ : ℝ) < (n : ℝ) / k + 1 ∧ (⌊(n : ℝ) / (k + (k : ℝ) ^ theta)⌋ : ℝ) > (n : ℝ) / (k + (k : ℝ) ^ theta) - 1 := by
    exact ⟨ Int.ceil_lt_add_one _, Int.sub_one_lt_floor _ ⟩;
  -- Now bound the difference:
  have h_diff : (n : ℝ) / k - (n : ℝ) / (k + (k : ℝ) ^ theta) ≤ (n : ℝ) / (k : ℝ) ^ (2 - theta) := by
    rw [ Real.rpow_sub ] <;> norm_num;
    · field_simp;
      nlinarith only [ show ( k : ℝ ) ≥ 1 by norm_cast, show ( k : ℝ ) ^ theta ≥ 0 by positivity ];
    · linarith;
  push_cast [ ← @Int.cast_le ℝ ] at * ; linarith

/-
Each fiber has at most `1 + 8 k^{1+θ}/n` elements.
-/
private lemma medFiber_card_le : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
    (1 / 2) * (k : ℝ) ^ (2 - theta) < (n : ℝ) → ∀ h : ℤ,
    ((medFiber k n h).card : ℝ) ≤ 1 + 8 * (k : ℝ) ^ (1 + theta) / (n : ℝ) := by
  obtain ⟨k₀, hk₀⟩ : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → 8 ≤ (k : ℝ) ^ (1 - theta) := by
    convert Filter.eventually_atTop.mp ( eventually_le_rpow ( 1 - theta ) 8 ( by linarith [ theta_lt_one ] ) ) using 1;
  refine' ⟨ k₀ + 2, fun k hk n hn h => _ ⟩ ; norm_num at *;
  by_cases h_empty : medFiber k n h = ∅;
  · norm_num [ h_empty ];
    exact add_nonneg zero_le_one ( div_nonneg ( by positivity ) ( by exact_mod_cast ( by linarith [ show ( 0 :ℝ ) ≤ k ^ ( 2 - theta ) by positivity ] : ( 0 :ℝ ) ≤ n ) ) );
  · -- Since `medFiber k n h` is nonempty, we can pick any `m₀ ∈ medFiber k n h`.
    obtain ⟨m₀, hm₀⟩ : ∃ m₀ ∈ medFiber k n h, (k : ℝ) < m₀ ∧ (m₀ : ℝ) < (k : ℝ) + (k : ℝ) ^ theta ∧ |(n : ℝ) / m₀ - (h : ℝ)| < 1 / (k : ℝ) ^ (1 - theta) := by
      obtain ⟨ m₀, hm₀ ⟩ := Finset.nonempty_of_ne_empty h_empty; use m₀; simp_all +decide [ medFiber, medWindow ] ;
      exact_mod_cast hm₀.1.1.1;
    -- We'll use that $h \geq \frac{n}{2k}$ to bound $m/h$.
    have h_h_ge : (h : ℝ) ≥ (n : ℝ) / (2 * (k : ℝ)) := by
      have h_h_ge : (h : ℝ) > (n : ℝ) / ((k : ℝ) + (k : ℝ) ^ theta) - 1 := by
        have h_h_ge : (n : ℝ) / m₀ > (n : ℝ) / ((k : ℝ) + (k : ℝ) ^ theta) := by
          gcongr <;> norm_cast at *;
          · exact_mod_cast hn.trans_le' ( mul_nonneg ( by norm_num ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) );
          · linarith;
          · exact_mod_cast hm₀.2.2.1;
        linarith [ abs_lt.mp hm₀.2.2.2, show ( 1 : ℝ ) / k ^ ( 1 - theta ) ≤ 1 by exact div_le_self zero_le_one <| Real.one_le_rpow ( by norm_cast; linarith ) <| by linarith [ show theta < 1 by exact theta_lt_one ] ];
      have h_h_ge : (n : ℝ) / ((k : ℝ) + (k : ℝ) ^ theta) - (n : ℝ) / (2 * (k : ℝ)) ≥ 1 := by
        rw [ div_sub_div, ge_iff_le, le_div_iff₀ ];
        · have h_h_ge : (k : ℝ) ^ (2 - theta) ≥ 8 * (k : ℝ) := by
            have := hk₀ k ( by linarith );
            exact le_trans ( mul_le_mul_of_nonneg_right this ( Nat.cast_nonneg _ ) ) ( by rw [ ← Real.rpow_add_one ( by norm_cast; linarith ) ] ; ring_nf; norm_num );
          rw [ Real.rpow_sub ] at * <;> norm_num at *;
          · nlinarith [ show ( k : ℝ ) ^ theta > 0 by exact Real.rpow_pos_of_pos ( Nat.cast_pos.mpr ( by linarith ) ) _, show ( k : ℝ ) ^ theta ≤ k by exact le_trans ( Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) ( show theta ≤ 1 by exact le_of_lt ( by norm_num [ theta ] ) ) ) ( by norm_num ), mul_div_cancel₀ ( ( k : ℝ ) ^ 2 ) ( show ( k : ℝ ) ^ theta ≠ 0 by exact ne_of_gt ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr ( by linarith ) ) _ ) ) ];
          · linarith;
          · lia;
          · linarith;
        · exact mul_pos ( add_pos_of_pos_of_nonneg ( Nat.cast_pos.mpr ( by linarith ) ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) ) ( mul_pos zero_lt_two ( Nat.cast_pos.mpr ( by linarith ) ) );
        · exact ne_of_gt ( add_pos_of_pos_of_nonneg ( Nat.cast_pos.mpr ( by linarith ) ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) );
        · norm_cast ; linarith;
      linarith;
    -- Using the bound on $m/h$, we can show that $|m - n/h| < 4k^{1+\theta}/n$.
    have h_abs_lt : ∀ m ∈ medFiber k n h, |(m : ℝ) - (n : ℝ) / (h : ℝ)| < 4 * (k : ℝ) ^ (1 + theta) / (n : ℝ) := by
      intro m hm
      have h_abs_lt_step : |(m : ℝ) - (n : ℝ) / (h : ℝ)| ≤ (m : ℝ) / (h : ℝ) * |(n : ℝ) / (m : ℝ) - (h : ℝ)| := by
        by_cases hm_pos : 0 < m <;> by_cases hh_pos : 0 < h <;> simp_all +decide [div_mul_eq_mul_div];
        · field_simp;
          rw [ abs_div, abs_div, abs_of_pos ( by positivity : 0 < ( h : ℝ ) ), abs_of_pos ( by positivity : 0 < ( m : ℝ ) ) ];
          rw [ mul_div_cancel₀ _ ( by positivity ), mul_div_cancel₀ _ ( by positivity ), abs_sub_comm ];
        · contrapose! h_h_ge;
          exact lt_of_le_of_lt ( Int.cast_nonpos.mpr hh_pos ) ( div_pos ( by exact lt_of_le_of_lt ( by positivity ) hn ) ( by norm_cast; linarith ) );
        · grind +locals;
        · contrapose! hn;
          exact le_trans ( show ( n : ℝ ) ≤ 0 by exact_mod_cast le_of_not_gt fun hn => by { exact absurd h_h_ge ( by { exact not_le_of_gt <| lt_of_le_of_lt ( by norm_cast ) <| div_pos ( by positivity ) <| by norm_cast; linarith } ) } ) <| by positivity;
      -- Using the bound on $m/h$, we can show that $m/h \leq 4k^2/n$.
      have h_m_div_h_le : (m : ℝ) / (h : ℝ) ≤ 4 * (k : ℝ) ^ 2 / (n : ℝ) := by
        have h_m_div_h_le : (m : ℝ) ≤ 2 * (k : ℝ) := by
          have h_m_le : (m : ℝ) < (k : ℝ) + (k : ℝ) ^ theta := by
            exact Finset.mem_filter.mp ( Finset.mem_filter.mp hm |>.1 ) |>.2;
          exact_mod_cast Int.le_of_lt_add_one ( by rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith [ show ( k : ℝ ) ^ theta ≤ k by exact le_trans ( Real.rpow_le_rpow_of_exponent_le ( by norm_cast; linarith ) ( show theta ≤ 1 by exact le_of_lt theta_lt_one ) ) ( by norm_num ) ] );
        rw [ div_le_div_iff₀ ] <;> norm_num at *;
        · rw [ div_le_iff₀ ] at h_h_ge <;> nlinarith [ show ( k : ℝ ) ≥ 2 by norm_cast; linarith, show ( n : ℝ ) > 0 by exact lt_of_le_of_lt ( by positivity ) hn ];
        · exact_mod_cast h_h_ge.trans_lt' ( div_pos ( show ( 0 : ℝ ) < n by exact lt_of_le_of_lt ( by positivity ) hn ) ( by norm_cast; linarith ) );
        · exact_mod_cast hn.trans_le' ( mul_nonneg ( by norm_num ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) );
      -- Using the bound on $|n/m - h|$, we can show that $|n/m - h| < 1/k^{1-\theta}$.
      have h_abs_lt_step2 : |(n : ℝ) / (m : ℝ) - (h : ℝ)| < 1 / (k : ℝ) ^ (1 - theta) := by
        exact Finset.mem_filter.mp hm |>.2;
      refine lt_of_le_of_lt h_abs_lt_step <| lt_of_le_of_lt ( mul_le_mul_of_nonneg_right h_m_div_h_le <| abs_nonneg _ ) ?_;
      convert mul_lt_mul_of_pos_left h_abs_lt_step2 ( show ( 0 : ℝ ) < 4 * k ^ 2 / n by exact div_pos ( by norm_cast; nlinarith ) ( by exact_mod_cast ( by linarith [ show ( 0 :ℝ ) < n by exact lt_of_le_of_lt ( by positivity ) hn ] : ( 0 :ℝ ) < n ) ) ) using 1 ; ring_nf;
      rw [ show ( 1 + theta : ℝ ) = 2 - ( 1 - theta ) by ring, Real.rpow_sub ] <;> norm_num ; ring ; linarith;
    have h_card_le : ((medFiber k n h).card : ℝ) ≤ 2 * (4 * (k : ℝ) ^ (1 + theta) / (n : ℝ)) + 1 := by
      have := card_int_abs_sub_lt_le ( ( n : ℝ ) / h ) ( 4 * ( k : ℝ ) ^ ( 1 + theta ) / n ) ?_ ( medFiber k n h );
      · convert this using 2 ; rw [ Finset.filter_true_of_mem h_abs_lt ];
      · exact div_nonneg ( mul_nonneg zero_le_four ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) ) ( by linarith [ show ( 0 : ℝ ) ≤ n by exact_mod_cast Int.le_of_lt_add_one ( by { rw [ ← @Int.cast_lt ℝ ] ; push_cast; linarith [ show ( 0 : ℝ ) ≤ k ^ ( 2 - theta ) by positivity ] } ) ] );
    exact h_card_le.trans_eq ( by ring )

/-- The `n`-free upper bound for the bad count on the medium range. -/
private noncomputable def g_med (k : ℕ) : ℝ :=
  3 + 56 * (k : ℝ) ^ (2 * theta - 1) + (k : ℝ) ^ theta * (Real.log k) ^ (-(2 : ℝ))

/-
The elementary counting bound for the bad count on the medium range.
-/
private lemma 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
  -- By definition of $g_{\text{med}}$, we know that for sufficiently large $k$, $g_{\text{med}}(k)$ is greater than the bound given by the lemma.
  have h_bound : ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ,
    (1 / 2) * (k : ℝ) ^ (2 - theta) < (n : ℝ) →
    (n : ℝ) ≤ (k : ℝ) ^ 2 / (Real.log k) ^ 2 →
    ((badSet k n).card : ℝ) ≤ (3 + (n : ℝ) / (k : ℝ) ^ (2 - theta)) * (1 + 8 * (k : ℝ) ^ (1 + theta) / (n : ℝ)) := by
      have := @medFiber_card_le;
      obtain ⟨k₀, hk₀⟩ := this
      use max k₀ 2
      intro k hk n hn hhigh
      have hk0 : k₀ ≤ k := by
        exact le_trans ( le_max_left _ _ ) hk
      have hk1 : 1 ≤ k := by
        linarith [ le_max_right k₀ 2 ]
      have hn0 : 0 < n := by
        exact_mod_cast hn.trans_le' ( mul_nonneg ( by norm_num ) ( Real.rpow_nonneg ( Nat.cast_nonneg _ ) _ ) )
      have h_card : ((badSet k n).card : ℝ) ≤ ∑ h ∈ medJ k n, ((medFiber k n h).card : ℝ) := by
        exact_mod_cast Finset.card_le_card ( badSet_subset_biUnion k n hk1 hn0 ) |> le_trans <| Finset.card_biUnion_le;
      refine le_trans h_card <| le_trans ( Finset.sum_le_sum fun x hx => hk₀ k hk0 n hn x ) ?_;
      have := medJ_card_le k n hk1 hn0; norm_num at *; nlinarith [ show ( 0 :ℝ ) ≤ 8 * k ^ ( 1 + theta ) / n by positivity ] ;
  obtain ⟨ k₀, hk₀ ⟩ := h_bound; use Max.max k₀ 2; intros k hk n hn hn'; refine lt_of_le_of_lt ( hk₀ k ( le_trans ( le_max_left _ _ ) hk ) n hn hn' ) ?_ ; unfold g_med; ring_nf; norm_num;
  -- Simplify the expression by cancelling out common terms.
  have h_simp : (n : ℝ) * (k : ℝ) ^ (1 + theta) / (k : ℝ) ^ (2 - theta) = (n : ℝ) * (k : ℝ) ^ (2 * theta - 1) ∧ (k : ℝ) ^ (1 + theta) / (n : ℝ) < 2 * (k : ℝ) ^ (2 * theta - 1) ∧ (n : ℝ) / (k : ℝ) ^ (2 - theta) ≤ (k : ℝ) ^ theta * (Real.log k) ^ (-2 : ℝ) := by
    refine' ⟨ _, _, _ ⟩;
    · rw [ mul_div_assoc, ← Real.rpow_sub ( by norm_cast; linarith [ le_max_right k₀ 2 ] ) ] ; ring_nf;
    · rw [ div_lt_iff₀ ];
      · refine' lt_of_le_of_lt _ ( mul_lt_mul_of_pos_left hn ( by exact mul_pos zero_lt_two ( Real.rpow_pos_of_pos ( Nat.cast_pos.mpr ( by linarith [ le_max_right k₀ 2 ] ) ) _ ) ) ) ; ring_nf ; norm_num [ theta ];
        rw [ ← Real.rpow_add' ] <;> norm_num;
      · exact lt_of_le_of_lt ( by positivity ) hn;
    · convert div_le_div_of_nonneg_right hn' ( Real.rpow_nonneg ( Nat.cast_nonneg k ) _ ) using 1 ; norm_cast ; norm_num ; ring_nf;
      rw [ show ( k : ℝ ) ^ theta = ( k : ℝ ) ^ ( 2 - ( 2 - theta ) ) by ring_nf, Real.rpow_sub ] <;> norm_num ; ring ; linarith [ le_max_right k₀ 2 ];
  ring_nf at *;
  by_cases hn : n = 0 <;> simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ];
  · exact absurd ‹_› ( not_lt_of_ge ( by positivity ) );
  · linarith

theorem erdos_1094__h2__h2__h2__h2__h1 : ∃ (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 : ℝ) := by
  obtain ⟨k₀, hk₀⟩ := med_card_bound
  refine ⟨k₀, fun k hk n hlo hhi => ?_⟩
  have h := hk₀ k hk n (by simpa [theta] using hlo) hhi
  have hset : {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 : ℝ))} = badSet k n := by
    unfold badSet theta
    refine Finset.filter_congr (fun m hm => ?_)
    have := (Finset.mem_Ioo.mp hm).1
    simp [this]
  rw [hset]
  simpa [g_med, theta] using h