Erdős problem 272 - szabo strong

/-
Erdos 272: the Szabo strong variant.

The final theorem is Bounty.target, with exactly the task's requested type.
All combinatorial reductions used in the proof are proved below.

Proof outline: private witnesses and progression matching give the bound for
common-point families and for families with a long common interval core.
Trace counts give a common point for the crooked members after a linear loss.
Straddling estimates and one-sided endpoint stability then give the required
long-core structure. The lower construction and upper bound yield the big-O
statement.

Pinned environment: Lean 4.33.1; FormalConjectures
8432eac998110a563e03df65a28c117e97c8c142; Mathlib
0df444a360eaa60ab8c11dca51a86af692955474.
-/


section
open Finset Filter Asymptotics

theorem arithInterSet_empty (N : ℕ) : Erdos272.IsArithInterSet N ∅ := by
  simp [Erdos272.IsArithInterSet]

theorem admissible_card_le_pow {N : ℕ} {A : Finset (Finset ℕ)}
    (hA : Erdos272.IsArithInterSet N A) : A.card ≤ 2 ^ N := by
  have h := Finset.card_le_card hA.1
  simpa using h

theorem admissible_cards_nonempty (N : ℕ) :
    {m : ℕ | ∃ A : Finset (Finset ℕ), ∃ (_ : Erdos272.IsArithInterSet N A), A.card = m}.Nonempty := by
  exact ⟨0, ∅, arithInterSet_empty N, rfl⟩

theorem admissible_cards_bddAbove (N : ℕ) :
    BddAbove {m : ℕ | ∃ A : Finset (Finset ℕ),
      ∃ (_ : Erdos272.IsArithInterSet N A), A.card = m} := by
  refine ⟨2 ^ N, ?_⟩
  rintro m ⟨A, hA, rfl⟩
  exact admissible_card_le_pow hA

theorem card_le_max {N : ℕ} {A : Finset (Finset ℕ)}
    (hA : Erdos272.IsArithInterSet N A) : A.card ≤ Erdos272.maxArithInterCard N := by
  exact le_csSup (admissible_cards_bddAbove N) ⟨A, hA, rfl⟩

theorem max_is_attained (N : ℕ) :
    ∃ A : Finset (Finset ℕ), Erdos272.IsArithInterSet N A ∧
      A.card = Erdos272.maxArithInterCard N := by
  obtain ⟨A, hA, heq⟩ := Nat.sSup_mem
    (admissible_cards_nonempty N) (admissible_cards_bddAbove N)
  exact ⟨A, hA, heq⟩

theorem nonempty_small_isAP {s : Finset ℕ} (hs : s.Nonempty) (hcard : s.card ≤ 2) :
    ∃ l > 0, (s : Set ℕ).IsAPOfLength l := by
  have hpos := Finset.card_pos.mpr hs
  by_cases h : s.card = 1
  · obtain ⟨a, rfl⟩ := Finset.card_eq_one.mp h
    exact ⟨1, by norm_num, Set.IsAPOfLength.one.mpr ⟨a, by simp⟩⟩
  · have htwo : s.card = 2 := by omega
    obtain ⟨a, b, hab, rfl⟩ := Finset.card_eq_two.mp htwo
    refine ⟨2, by norm_num, ?_⟩
    rw [Finset.coe_pair]
    rcases lt_or_gt_of_ne hab with hab | hba
    · exact Nat.isAPOfLength_pair hab
    · rw [Set.pair_comm]
      exact Nat.isAPOfLength_pair hba

theorem small_star_admissible {N c : ℕ} {A : Finset (Finset ℕ)}
    (hsub : A ⊆ (Finset.Icc 1 N).powerset)
    (hc : ∀ s ∈ A, c ∈ s)
    (hsize : ∀ s ∈ A, s.card ≤ 3) : Erdos272.IsArithInterSet N A := by
  refine ⟨hsub, ?_⟩
  intro s hs t ht hst
  apply nonempty_small_isAP ⟨c, Finset.mem_inter.mpr ⟨hc s hs, hc t ht⟩⟩
  by_contra h
  have hthree : 3 ≤ (s ∩ t).card := by omega
  have heqs : s ∩ t = s := Finset.eq_of_subset_of_card_le
    Finset.inter_subset_left ((hsize s hs).trans hthree)
  have heqt : s ∩ t = t := Finset.eq_of_subset_of_card_le
    Finset.inter_subset_right ((hsize t ht).trans hthree)
  exact hst (heqs.symm.trans heqt)

theorem insert_injective_fixed_card {α : Type*} [DecidableEq α]
    {c : α} {s t : Finset α} (hcard : s.card = t.card)
    (h : insert c s = insert c t) : s = t := by
  by_cases hs : c ∈ s
  · have ht : c ∈ t := by
      by_contra ht
      have hh := congrArg Finset.card h
      simp [Finset.insert_eq_of_mem hs, Finset.card_insert_of_notMem ht] at hh
      omega
    simpa [Finset.insert_eq_of_mem hs, Finset.insert_eq_of_mem ht] using h
  · have ht : c ∉ t := by
      intro ht
      have hh := congrArg Finset.card h
      simp [Finset.insert_eq_of_mem ht, Finset.card_insert_of_notMem hs] at hh
      omega
    apply Finset.ext
    intro x
    have hh := Finset.ext_iff.mp h x
    by_cases hx : x = c
    · subst x
      simp [hs, ht]
    · simpa [hx] using hh

/-- Pairs in `[1,N]`, enlarged to contain 1, together with the singleton `{1}`. -/
def lowerFamily (N : ℕ) : Finset (Finset ℕ) :=
  insert {1} (((Finset.Icc 1 N).powersetCard 2).image (insert 1))

theorem lowerFamily_admissible {N : ℕ} (hN : 1 ≤ N) :
    Erdos272.IsArithInterSet N (lowerFamily N) := by
  apply small_star_admissible (c := 1)
  · intro s hs
    rcases Finset.mem_insert.mp hs with rfl | hs
    · simp [hN]
    · obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hs
      exact Finset.mem_powerset.mpr (Finset.insert_subset
        (Finset.mem_Icc.mpr ⟨le_rfl, hN⟩) (Finset.mem_powersetCard.mp ht).1)
  · intro s hs
    rcases Finset.mem_insert.mp hs with rfl | hs
    · simp
    · obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hs
      simp
  · intro s hs
    rcases Finset.mem_insert.mp hs with rfl | hs
    · simp
    · obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hs
      have hh := Finset.card_insert_le 1 t
      rw [(Finset.mem_powersetCard.mp ht).2] at hh
      exact hh

theorem card_lowerFamily (N : ℕ) : (lowerFamily N).card = N.choose 2 + 1 := by
  have hinj : Set.InjOn (insert 1)
      (((Finset.Icc 1 N).powersetCard 2) : Set (Finset ℕ)) := by
    intro s hs t ht heq
    exact insert_injective_fixed_card
      ((Finset.mem_powersetCard.mp hs).2.trans (Finset.mem_powersetCard.mp ht).2.symm) heq
  have hnot : {1} ∉ (((Finset.Icc 1 N).powersetCard 2).image (insert 1)) := by
    intro h
    obtain ⟨s, hs, heq⟩ := Finset.mem_image.mp h
    have hh : s.card ≤ ({1} : Finset ℕ).card := by
      rw [← heq]
      exact Finset.card_le_card (Finset.subset_insert 1 s)
    simp [(Finset.mem_powersetCard.mp hs).2] at hh
  rw [lowerFamily, Finset.card_insert_of_notMem hnot,
    Finset.card_image_of_injOn hinj, Finset.card_powersetCard]
  simp

theorem lower_bound {N : ℕ} (hN : 1 ≤ N) :
    N.choose 2 + 1 ≤ Erdos272.maxArithInterCard N := by
  rw [← card_lowerFamily]
  exact card_le_max (lowerFamily_admissible hN)

theorem lower_bound_real {N : ℕ} (hN : 1 ≤ N) :
    (N : ℝ)^2 / 2 - (N : ℝ) / 2 + 1 ≤ (Erdos272.maxArithInterCard N : ℝ) := by
  have h : ((N.choose 2 + 1 : ℕ) : ℝ) ≤ (Erdos272.maxArithInterCard N : ℝ) :=
    Nat.cast_le.mpr (lower_bound hN)
  rw [Nat.cast_add, Nat.cast_one, Nat.cast_choose_two] at h
  nlinarith

/-- The finite upper bound still required to finish the proposed proof. -/
def FiniteUpperBound : Prop :=
  ∃ C : ℝ, ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N →
    ∀ A : Finset (Finset ℕ), Erdos272.IsArithInterSet N A →
      (A.card : ℝ) ≤ (N : ℝ)^2 / 2 + C * (N : ℝ)

/-- A conditional reduction, not a proof of the requested unconditional theorem. -/
theorem target_of_finite_upper_bound (hupper : FiniteUpperBound) :
    fcTypeOfName% "Erdos272.erdos_272.variants.szabo_strong" := by
  rcases hupper with ⟨C, N₀, hupper⟩
  refine Asymptotics.IsBigO.of_bound (max |C| 1) ?_
  filter_upwards [Filter.eventually_ge_atTop (max N₀ 1)] with N hN
  have hN₀ : N₀ ≤ N := (le_max_left _ _).trans hN
  have hN₁ : 1 ≤ N := (le_max_right _ _).trans hN
  obtain ⟨A, hA, hcard⟩ := max_is_attained N
  have hupperN := hupper N hN₀ A hA
  rw [hcard] at hupperN
  have hlowerN := lower_bound_real hN₁
  have hC : C ≤ max |C| 1 := (le_abs_self C).trans (le_max_left _ _)
  have hone : (1 : ℝ) ≤ max |C| 1 := le_max_right _ _
  have hNnonneg : (0 : ℝ) ≤ N := Nat.cast_nonneg N
  simp only [Real.norm_eq_abs, abs_of_nonneg hNnonneg]
  refine abs_le.mpr ⟨?_, ?_⟩
  · nlinarith [mul_le_mul_of_nonneg_right hone hNnonneg]
  · nlinarith [mul_le_mul_of_nonneg_right hC hNnonneg]

theorem finite_upper_bound_of_target
    (h : fcTypeOfName% "Erdos272.erdos_272.variants.szabo_strong") :
    FiniteUpperBound := by
  obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp h
  obtain ⟨N₀, hC⟩ := Filter.eventually_atTop.mp hC
  refine ⟨C, N₀, ?_⟩
  intro N hN A hA
  have hbound := hC N hN
  have hNnonneg : (0 : ℝ) ≤ N := Nat.cast_nonneg N
  simp only [Real.norm_eq_abs, abs_of_nonneg hNnonneg] at hbound
  have hu := (abs_le.mp hbound).2
  have hcard : (A.card : ℝ) ≤ (Erdos272.maxArithInterCard N : ℝ) :=
    Nat.cast_le.mpr (card_le_max hA)
  linarith

theorem target_iff_finite_upper_bound :
    (fcTypeOfName% "Erdos272.erdos_272.variants.szabo_strong") ↔ FiniteUpperBound :=
  ⟨finite_upper_bound_of_target, target_of_finite_upper_bound⟩

end
section
open Finset

theorem range_image_isAP (a d k : ℕ) (hd : 0 < d) :
    (((Finset.range k).image (fun i => a + i * d) : Finset ℕ) : Set ℕ).IsAPOfLength k := by
  refine ⟨a, d, ?_, ?_⟩
  · have hinj : Function.Injective (fun i : ℕ => a + i * d) := by
      intro i j hij
      nlinarith
    simp [Finset.card_image_of_injective _ hinj]
  · ext x
    simp

theorem multiples_isAP {d M : ℕ} (hd : 0 < d) :
    (((Finset.Icc 0 M).filter (fun x => d ∣ x) : Finset ℕ) : Set ℕ).IsAPOfLength
      (↑(M / d + 1 : ℕ)) := by
  have heq : (Finset.Icc 0 M).filter (fun x => d ∣ x) =
      (Finset.range (M / d + 1)).image (fun i => 0 + i * d) := by
    ext x
    simp only [Finset.mem_filter, Finset.mem_Icc, Nat.zero_le, true_and,
      Finset.mem_image, Finset.mem_range, zero_add]
    constructor
    · rintro ⟨hx, hdvd⟩
      refine ⟨x / d, ?_, Nat.div_mul_cancel hdvd⟩
      exact Nat.lt_succ_of_le ((Nat.le_div_iff_mul_le hd).mpr
        (by simpa [Nat.div_mul_cancel hdvd] using hx))
    · rintro ⟨i, hi, rfl⟩
      exact ⟨(Nat.le_div_iff_mul_le hd).mp (Nat.le_of_lt_succ hi), dvd_mul_left d i⟩
  rw [heq]
  exact range_image_isAP 0 d (M / d + 1) hd

/-- The arithmetic hull of `0,a,b`, expressed by divisibility and an interval. -/
def hullZero (a b : ℕ) : Finset ℕ :=
  (Finset.Icc 0 (max a b)).filter (fun x => a.gcd b ∣ x)

theorem gcd_mem_hullZero {a : ℕ} (b : ℕ) (ha : 0 < a) : a.gcd b ∈ hullZero a b := by
  exact Finset.mem_filter.mpr ⟨Finset.mem_Icc.mpr
    ⟨Nat.zero_le _, (Nat.gcd_le_left b ha).trans (le_max_left _ _)⟩, dvd_rfl⟩

/-- Closure under the hulls from a closest positive point forces a progression. -/
theorem hullZero_closed_isAP {s : Finset ℕ} {a : ℕ}
    (ha : a ∈ s) (hapos : 0 < a)
    (hmin : ∀ b ∈ s, 0 < b → a ≤ b)
    (hclosed : ∀ b ∈ s, hullZero a b ⊆ s) :
    ∃ l > 0, (s : Set ℕ).IsAPOfLength l := by
  have hne : s.Nonempty := ⟨a, ha⟩
  have hdvd : ∀ b ∈ s, a ∣ b := by
    intro b hb
    have hgmem : a.gcd b ∈ s := hclosed b hb (gcd_mem_hullZero b hapos)
    have hgpos : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b hapos
    have heq : a.gcd b = a := le_antisymm (Nat.gcd_le_left b hapos)
      (hmin _ hgmem hgpos)
    rw [← heq]
    exact Nat.gcd_dvd_right a b
  let M := s.max' hne
  have hMmem : M ∈ s := Finset.max'_mem s hne
  have hgcd : a.gcd M = a := Nat.gcd_eq_left_iff_dvd.mpr (hdvd M hMmem)
  have heq : s = (Finset.Icc 0 M).filter (fun x => a ∣ x) := by
    apply Finset.Subset.antisymm
    · intro x hx
      exact Finset.mem_filter.mpr ⟨Finset.mem_Icc.mpr
        ⟨Nat.zero_le _, Finset.le_max' s x hx⟩, hdvd x hx⟩
    · intro x hx
      apply hclosed M hMmem
      have haM : a ≤ M := Finset.le_max' s a ha
      simpa [hullZero, max_eq_right haM, hgcd] using hx
  refine ⟨(M / a + 1 : ℕ), by positivity, ?_⟩
  rw [heq]
  exact multiples_isAP hapos

/-- A non-progression has a failed gcd hull from every closest positive point. -/
theorem closest_positive_witness {s : Finset ℕ} {a : ℕ}
    (ha : a ∈ s) (hapos : 0 < a)
    (hmin : ∀ b ∈ s, 0 < b → a ≤ b)
    (hcrooked : ¬ ∃ l > 0, (s : Set ℕ).IsAPOfLength l) :
    ∃ b ∈ s, ¬ hullZero a b ⊆ s := by
  by_contra h
  push Not at h
  exact hcrooked (hullZero_closed_isAP ha hapos hmin h)

theorem finset_ap_representation {s : Finset ℕ} {l : ℕ∞}
    (h : (s : Set ℕ).IsAPOfLength l) :
    ∃ a d : ℕ, ∀ x : ℕ, x ∈ s ↔ ∃ i < s.card, a + i * d = x := by
  have hl : (s.card : ℕ∞) = l := by simpa using h.card
  obtain ⟨a, d, heq⟩ := h.eq
  refine ⟨a, d, ?_⟩
  intro x
  change x ∈ (s : Set ℕ) ↔ _
  rw [heq]
  simp [← hl]

/-- A progression containing the three points contains their gcd hull. -/
theorem hullZero_subset_of_isAP {s : Finset ℕ} {l : ℕ∞} {u v : ℕ}
    (hAP : (s : Set ℕ).IsAPOfLength l)
    (hzero : 0 ∈ s) (hu : u ∈ s) (hv : v ∈ s) (hupos : 0 < u) :
    hullZero u v ⊆ s := by
  obtain ⟨a, d, hrep⟩ := finset_ap_representation hAP
  obtain ⟨i₀, hi₀, h₀⟩ := (hrep 0).mp hzero
  have ha : a = 0 := by omega
  subst a
  obtain ⟨i, hi, hui⟩ := (hrep u).mp hu
  obtain ⟨j, hj, hvj⟩ := (hrep v).mp hv
  simp only [zero_add] at hui hvj hrep
  have hd : 0 < d := by nlinarith
  have hdu : d ∣ u := by rw [← hui]; exact dvd_mul_left d i
  have hdv : d ∣ v := by rw [← hvj]; exact dvd_mul_left d j
  intro x hx
  obtain ⟨hxrange, hxdiv⟩ := Finset.mem_filter.mp hx
  have hxmax : x ≤ max u v := (Finset.mem_Icc.mp hxrange).2
  have hdx : d ∣ x := (Nat.dvd_gcd hdu hdv).trans hxdiv
  have hdivmul : x / d * d = x := Nat.div_mul_cancel hdx
  have humax : u ≤ max i j * d := by nlinarith [le_max_left i j]
  have hvmax : v ≤ max i j * d := by nlinarith [le_max_right i j]
  have hxbound : x ≤ max i j * d := hxmax.trans (max_le humax hvmax)
  have hindex : x / d ≤ max i j :=
    Nat.le_of_mul_le_mul_right (by simpa [hdivmul] using hxbound) hd
  exact (hrep x).mpr ⟨x / d, hindex.trans_lt (max_lt_iff.mpr ⟨hi, hj⟩), hdivmul⟩

/-- A failed hull is private among progression-intersecting sets containing zero. -/
theorem hullZero_witness_private {F : Finset (Finset ℕ)}
    (hF : (F : Set (Finset ℕ)).Pairwise fun s t =>
      ∃ l > 0, ((s ∩ t : Finset ℕ) : Set ℕ).IsAPOfLength l)
    (hzero : ∀ s ∈ F, 0 ∈ s)
    {s t : Finset ℕ} (hs : s ∈ F) (ht : t ∈ F) {a b : ℕ}
    (ha : a ∈ s) (hb : b ∈ s) (hapos : 0 < a)
    (hfail : ¬ hullZero a b ⊆ s) (hat : a ∈ t) (hbt : b ∈ t) : t = s := by
  by_contra hne
  obtain ⟨l, hl, hAP⟩ := hF hs ht (fun hst => hne hst.symm)
  have hh := hullZero_subset_of_isAP hAP
    (Finset.mem_inter.mpr ⟨hzero s hs, hzero t ht⟩)
    (Finset.mem_inter.mpr ⟨ha, hat⟩) (Finset.mem_inter.mpr ⟨hb, hbt⟩) hapos
  exact hfail (hh.trans Finset.inter_subset_left)

end
section
open Finset

theorem prod_le_card_succ_mul_prod_pred (s : Finset ℕ) (hs : ∀ p ∈ s, 2 ≤ p) :
    (∏ p ∈ s, p) ≤ (s.card + 1) * ∏ p ∈ s, (p - 1) := by
  induction s using Finset.induction_on_max with
  | empty => simp
  | insert a s hmax ih =>
    have hnot : a ∉ s := by
      intro ha
      exact (lt_irrefl a) (hmax a ha)
    have ha : 2 ≤ a := hs a (Finset.mem_insert_self _ _)
    have hs' : ∀ p ∈ s, 2 ≤ p := fun p hp => hs p (Finset.mem_insert_of_mem hp)
    have hsub : s ⊆ Finset.Icc 2 (a - 1) := by
      intro p hp
      exact Finset.mem_Icc.mpr ⟨hs' p hp, by have := hmax p hp; omega⟩
    have hcard := Finset.card_le_card hsub
    simp only [Nat.card_Icc] at hcard
    have hca : s.card + 2 ≤ a := by omega
    have hprod := Nat.mul_le_mul_left a (ih hs')
    have hcoef : a * (s.card + 1) ≤ (s.card + 2) * (a - 1) := by
      have hapred : a - 1 + 1 = a := by omega
      nlinarith
    have hprod' := Nat.mul_le_mul_right (∏ p ∈ s, (p - 1)) hcoef
    rw [Finset.prod_insert hnot, Finset.prod_insert hnot, Finset.card_insert_of_notMem hnot]
    nlinarith

theorem le_primeFactors_card_succ_mul_totient (n : ℕ) :
    n ≤ (n.primeFactors.card + 1) * n.totient := by
  have hprime : ∀ p ∈ n.primeFactors, 2 ≤ p :=
    fun p hp => (Nat.prime_of_mem_primeFactors hp).two_le
  have hprod := prod_le_card_succ_mul_prod_pred n.primeFactors hprime
  have hmult := Nat.mul_le_mul_left n.totient hprod
  have hidentity := Nat.totient_mul_prod_primeFactors n
  have hpos : 0 < ∏ p ∈ n.primeFactors, (p - 1) :=
    Finset.prod_pos (fun p hp => by have := hprime p hp; omega)
  have hineq : n * (∏ p ∈ n.primeFactors, (p - 1)) ≤
      ((n.primeFactors.card + 1) * n.totient) * (∏ p ∈ n.primeFactors, (p - 1)) := by
    nlinarith
  exact (mul_le_mul_iff_left₀ hpos).mp hineq

theorem primeFactors_card_le_log_two {n : ℕ} (hn : n ≠ 0) :
    n.primeFactors.card ≤ Nat.log 2 n := by
  apply (Nat.le_log_iff_pow_le (by decide) hn).mpr
  calc
    2 ^ n.primeFactors.card ≤ ∏ p ∈ n.primeFactors, p :=
      Finset.pow_card_le_prod _ _ _
        (fun p hp => (Nat.prime_of_mem_primeFactors hp).two_le)
    _ ≤ n := Nat.le_of_dvd (Nat.pos_of_ne_zero hn) (Nat.prod_primeFactors_dvd n)

theorem le_log_succ_mul_totient (n : ℕ) :
    n ≤ (Nat.log 2 n + 1) * n.totient := by
  by_cases hn : n = 0
  · simp [hn]
  · exact (le_primeFactors_card_succ_mul_totient n).trans
      (Nat.mul_le_mul_right _ (Nat.add_le_add_right (primeFactors_card_le_log_two hn) 1))

theorem totient_ratio_le_log_succ {n : ℕ} (hn : 0 < n) :
    (n : ℝ) / (n.totient : ℝ) ≤ (Nat.log 2 n : ℝ) + 1 := by
  have hp : (0 : ℝ) < n.totient := Nat.cast_pos.mpr (Nat.totient_pos.mpr hn)
  apply (div_le_iff₀ hp).mpr
  exact_mod_cast le_log_succ_mul_totient n

end
section
open Finset

theorem odd_reciprocal_sq_step {x : ℝ} (hx : 0 ≤ x) :
    1 / (2 * x + 5) ^ 2 ≤ 1 / (4 * x + 8) - 1 / (4 * x + 12) := by
  have h4 : 0 < 2 * x + 4 := by positivity
  have h6 : 0 < 2 * x + 6 := by positivity
  calc
    1 / (2 * x + 5) ^ 2 ≤ 1 / ((2 * x + 4) * (2 * x + 6)) :=
      one_div_le_one_div_of_le (mul_pos h4 h6) (by nlinarith)
    _ = 1 / (4 * x + 8) - 1 / (4 * x + 12) := by
      have h8 : 4 * x + 8 ≠ 0 := by positivity
      have h12 : 4 * x + 12 ≠ 0 := by positivity
      field_simp
      ring

theorem odd_reciprocal_sq_tail (N : ℕ) :
    (∑ k ∈ Finset.range N, 1 / (2 * (k : ℝ) + 5) ^ 2) ≤
      1 / 8 - 1 / (4 * (N : ℝ) + 8) := by
  induction N with
  | zero => norm_num
  | succ N ih =>
    rw [Finset.sum_range_succ]
    have hs := odd_reciprocal_sq_step (Nat.cast_nonneg N)
    calc
      _ ≤ (1 / 8 - 1 / (4 * (N : ℝ) + 8)) +
          (1 / (4 * (N : ℝ) + 8) - 1 / (4 * (N : ℝ) + 12)) := add_le_add ih hs
      _ = _ := by push_cast; ring

theorem odd_reciprocal_sq_sum (N : ℕ) :
    (∑ k ∈ Finset.range N, 1 / (2 * (k : ℝ) + 3) ^ 2) ≤ 17 / 72 := by
  cases N with
  | zero => norm_num
  | succ N =>
    rw [Finset.sum_range_succ']
    have heq : (∑ k ∈ Finset.range N, 1 / (2 * ((k + 1 : ℕ) : ℝ) + 3) ^ 2) =
        ∑ k ∈ Finset.range N, 1 / (2 * (k : ℝ) + 5) ^ 2 := by
      apply Finset.sum_congr rfl
      intro k hk
      push_cast
      congr 2; ring
    rw [heq]
    norm_num only [Nat.cast_zero, mul_zero, zero_add]
    have ht := odd_reciprocal_sq_tail N
    have hp : 0 ≤ 1 / (4 * (N : ℝ) + 8) := by positivity
    linarith

def positiveMultiples (N d : ℕ) : Finset ℕ :=
  (Finset.Icc 1 N).filter (fun a => d ∣ a)

def divisorBlock (N d : ℕ) : Finset (ℕ × ℕ) :=
  positiveMultiples N d ×ˢ positiveMultiples N d

def coprimeSquare (N : ℕ) : Finset (ℕ × ℕ) :=
  ((Finset.Icc 1 N) ×ˢ (Finset.Icc 1 N)).filter (fun p => p.1.Coprime p.2)

def noncoprimeSquare (N : ℕ) : Finset (ℕ × ℕ) :=
  ((Finset.Icc 1 N) ×ˢ (Finset.Icc 1 N)).filter (fun p => ¬p.1.Coprime p.2)

theorem card_positiveMultiples_le (N : ℕ) {d : ℕ} (hd : 0 < d) :
    (positiveMultiples N d).card ≤ N / d := by
  have hmaps : Set.MapsTo (fun a : ℕ => a / d)
      (positiveMultiples N d : Set ℕ) (Finset.Icc 1 (N / d) : Set ℕ) := by
    intro a ha
    obtain ⟨haI, had⟩ := Finset.mem_filter.mp ha
    obtain ⟨ha1, haN⟩ := Finset.mem_Icc.mp haI
    exact Finset.mem_Icc.mpr
      ⟨Nat.div_pos (Nat.le_of_dvd ha1 had) hd, Nat.div_le_div_right haN⟩
  have hinj : Set.InjOn (fun a : ℕ => a / d) (positiveMultiples N d : Set ℕ) := by
    intro a ha b hb hab
    have hda := (Finset.mem_filter.mp ha).2
    have hdb := (Finset.mem_filter.mp hb).2
    calc
      a = a / d * d := (Nat.div_mul_cancel hda).symm
      _ = b / d * d := congrArg (fun k => k * d) hab
      _ = b := Nat.div_mul_cancel hdb
  simpa using Finset.card_le_card_of_injOn (fun a : ℕ => a / d) hmaps hinj

theorem card_divisorBlock_le (N : ℕ) {d : ℕ} (hd : 0 < d) :
    (divisorBlock N d).card ≤ (N / d) ^ 2 := by
  have hh := card_positiveMultiples_le N hd
  simp only [divisorBlock, Finset.card_product]
  nlinarith

theorem card_divisorBlock_real_le (N : ℕ) {d : ℕ} (hd : 0 < d) :
    ((divisorBlock N d).card : ℝ) ≤ (N : ℝ) ^ 2 / (d : ℝ) ^ 2 := by
  have hdR : (0 : ℝ) < d := Nat.cast_pos.mpr hd
  have hquot : ((N / d : ℕ) : ℝ) ≤ (N : ℝ) / (d : ℝ) := by
    apply (le_div_iff₀ hdR).mpr
    exact_mod_cast Nat.div_mul_le_self N d
  have hsq := (sq_le_sq₀ (Nat.cast_nonneg (N / d))
    (div_nonneg (Nat.cast_nonneg N) hdR.le)).mpr hquot
  have hc : ((divisorBlock N d).card : ℝ) ≤ ((N / d : ℕ) : ℝ) ^ 2 :=
    by exact_mod_cast card_divisorBlock_le N hd
  exact hc.trans (by simpa [div_pow] using hsq)