diff --git a/LeanPool/RunsOfMultiples.lean b/LeanPool/RunsOfMultiples.lean new file mode 100644 index 0000000000..0f37f92ee5 --- /dev/null +++ b/LeanPool/RunsOfMultiples.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ + +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Main +public import LeanPool.RunsOfMultiples.Alt.Main +public import LeanPool.RunsOfMultiples.Examples + +/-! +# Sharp asymptotic bounds for runs of multiples in finite sets + +Source: url:https://github.com/jas-ho/runs-of-multiples-lean/blob/8b7e5f23534c321722725f78b6e64981557f0ef5/docs/runs-of-multiples.pdf +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 (Lean proofs) +Status: verified +Main declarations: `RunsOfMultiples.main_theorem`, `RunsOfMultiples.main_theorem_alt` +Tags: extremal-number-theory, smooth-numbers, entropy, compression +MSC: 11N25, 11B75, 05D05 +-/ + +/-! +# Runs of multiples in finite sets + +The two proofs and their supporting entropy, prime-counting, smooth-number and chain-compression +lemmas were produced with AI under Jason Hoelscher-Obermaier's direction. The original source is +https://github.com/jas-ho/runs-of-multiples-lean/tree/8b7e5f23534c321722725f78b6e64981557f0ef5. +The Lean proofs were written by Claude Opus 5.5. The compression argument was written informally +by GPT-6-Astra; its write-up is `docs/first-missing-multiple.pdf` at the same upstream commit. +Lean Pool ports the project to its pinned toolchain, factors out shared block padding, and +preserves the entropy and compression routes and both lower-bound constructions. +-/ diff --git a/LeanPool/RunsOfMultiples/Alt/Chains.lean b/LeanPool/RunsOfMultiples/Alt/Chains.lean new file mode 100644 index 0000000000..2473f34f53 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Chains.lean @@ -0,0 +1,429 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Alt.Compression +public import Mathlib.Data.Nat.Factorization.Basic +public import Mathlib.Data.Nat.Log +public import Mathlib.Tactic.Ring + +/-! +# The two compressions of Lemma 2, and the closure theorem + +* `pChain p`: chains `b, b p, b p², …` with `p ∤ b`; +* `pqChain p q` (`p < q`): chains `b p^D, b p^(D-1) q, …, b q^D` with `p, q ∤ b`. + +Both satisfy the window condition `Cons`, so compression keeps every `|A S t|` from decreasing. +Taking a compression-stable set of minimal element sum gives `exists_closed`, the content of +Lemma 2 of the second proof. +-/ + +open Finset + +@[expose] public section + +namespace RunsOfMultiples + +section pChain + +variable {p : ℕ} (hp : p.Prime) + +/-- Chains along a single prime `p`. -/ +noncomputable def pChain : ChainSys ℕ where + key n := n / p ^ n.factorization p + pos n := n.factorization p + elt b u := b * p ^ u + vld b _ := 0 < b ∧ ¬ p ∣ b + elt_key_pos n hn := Nat.div_mul_cancel (Nat.ordProj_dvd n p) + vld_key_pos n hn := ⟨Nat.ordCompl_pos p hn.ne', Nat.not_dvd_ordCompl hp hn.ne'⟩ + key_elt b u h := by + have hfac : (b * p ^ u).factorization p = u := by + rw [Nat.factorization_mul h.1.ne' (pow_ne_zero _ hp.ne_zero), Nat.factorization_pow, + Finsupp.add_apply, Finsupp.smul_apply, Nat.factorization_eq_zero_of_not_dvd h.2, + hp.factorization_self] + simp + change b * p ^ u / p ^ (b * p ^ u).factorization p = b + rw [hfac, Nat.mul_div_cancel _ (pow_pos hp.pos u)] + pos_elt b u h := by + rw [Nat.factorization_mul h.1.ne' (pow_ne_zero _ hp.ne_zero), Nat.factorization_pow, + Finsupp.add_apply, Finsupp.smul_apply, Nat.factorization_eq_zero_of_not_dvd h.2, + hp.factorization_self] + simp + elt_pos b u h := Nat.mul_pos h.1 (pow_pos hp.pos u) + vld_mono _ _ _ h _ := h + elt_lt b u v h huv := Nat.mul_lt_mul_of_pos_left (Nat.pow_lt_pow_right hp.one_lt huv) h.1 + +lemma pChain_cons (t : ℕ) (b : ℕ) : (pChain hp).Cons t b := by + classical + by_cases hb : 0 < b ∧ ¬ p ∣ b + swap + · exact ⟨PUnit, ∅, fun _ => b, fun _ => 0, fun e he => absurd he hb, + fun S _ e he => absurd he hb⟩ + refine ⟨ℕ, (Icc 1 t).filter (fun c => ¬ p ∣ c), fun c => b * c, fun c => Nat.log p (t / c), + ?_, ?_⟩ + · intro e _ c hc h _ + rw [mem_filter, mem_Icc] at hc + exact ⟨Nat.mul_pos hb.1 (by omega), fun hdvd => + ((Nat.Prime.dvd_mul hp).1 hdvd).elim hb.2 hc.2⟩ + · intro S hS e he + change b * p ^ e ∈ A S t ↔ b * p ^ e ∈ S ∧ ∀ c ∈ (Icc 1 t).filter (fun c => ¬ p ∣ c), + ∀ h ≤ Nat.log p (t / c), b * c * p ^ (e + h) ∈ S + rw [A, mem_filter] + refine and_congr_right fun _ => ?_ + constructor + · intro hall c hc h hh + rw [mem_filter, mem_Icc] at hc + have hct : c * p ^ h ≤ t := by + have h1 : p ^ h ≤ t / c := by + have hpos : t / c ≠ 0 := (Nat.div_pos hc.1.2 hc.1.1).ne' + exact le_trans (Nat.pow_le_pow_right hp.pos hh) (Nat.pow_log_le_self p hpos) + calc c * p ^ h ≤ c * (t / c) := Nat.mul_le_mul_left c h1 + _ ≤ t := Nat.mul_div_le t c + have := hall (c * p ^ h) (mem_Icc.2 ⟨Nat.mul_pos hc.1.1 (pow_pos hp.pos h) , hct⟩) + rw [show c * p ^ h * (b * p ^ e) = b * c * p ^ (e + h) by ring] at this + exact this + · intro hcons j hj + rw [mem_Icc] at hj + have hj0 : 0 < j := by omega + set c := (pChain hp).key j with hc + set h := (pChain hp).pos j with hh + have hvj := (pChain hp).vld_key_pos j hj0 + have hjeq : c * p ^ h = j := (pChain hp).elt_key_pos j hj0 + have hcle : c ≤ j := by + calc c = c * 1 := (mul_one c).symm + _ ≤ c * p ^ h := Nat.mul_le_mul_left c (Nat.one_le_pow _ _ hp.pos) + _ = j := hjeq + have hcI : c ∈ (Icc 1 t).filter (fun c => ¬ p ∣ c) := + mem_filter.2 ⟨mem_Icc.2 ⟨hvj.1, hcle.trans hj.2⟩, hvj.2⟩ + have hhle : h ≤ Nat.log p (t / c) := by + apply Nat.le_log_of_pow_le hp.one_lt + rw [Nat.le_div_iff_mul_le hvj.1, mul_comm, hjeq] + exact hj.2 + have := hcons c hcI h hhle + rw [show b * c * p ^ (e + h) = c * p ^ h * (b * p ^ e) by ring, hjeq] at this + exact this + +/-- `x / p` sits one position below `x` on the `p`-chain of `x`. -/ +lemma pChain_div {x : ℕ} (hx : 0 < x) (hpx : p ∣ x) : + (pChain hp).vld ((pChain hp).key x) ((pChain hp).pos x - 1) ∧ + (pChain hp).pos x - 1 < (pChain hp).pos x ∧ + (pChain hp).elt ((pChain hp).key x) ((pChain hp).pos x - 1) = x / p := by + have hv := (pChain hp).vld_key_pos x hx + have hx' := (pChain hp).elt_key_pos x hx + have hpos : 0 < (pChain hp).pos x := by + change 0 < x.factorization p + exact hp.factorization_pos_of_dvd hx.ne' hpx + refine ⟨hv, by omega, ?_⟩ + change (pChain hp).key x * p ^ ((pChain hp).pos x - 1) = x / p + conv_rhs => rw [← hx'] + change _ = (pChain hp).key x * p ^ (pChain hp).pos x / p + rw [show (pChain hp).pos x = (pChain hp).pos x - 1 + 1 by omega, pow_succ, ← mul_assoc, + Nat.mul_div_cancel _ hp.pos] + simp + +end pChain + +section pqChain + +variable {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (hpq : p < q) + +lemma pow_mul_pow_mono {a b : ℕ} (hab : a ≤ b) {d u v : ℕ} (huv : u ≤ v) (hvd : v ≤ d) : + a ^ (d - u) * b ^ u ≤ a ^ (d - v) * b ^ v := by + have e1 : d - u = (d - v) + (v - u) := by omega + have e2 : v = u + (v - u) := by omega + rw [e1, pow_add, show b ^ v = b ^ u * b ^ (v - u) by rw [← pow_add, Nat.add_sub_cancel' huv]] + have : a ^ (v - u) ≤ b ^ (v - u) := Nat.pow_le_pow_left hab _ + calc a ^ (d - v) * a ^ (v - u) * b ^ u = a ^ (d - v) * b ^ u * a ^ (v - u) := by ring + _ ≤ a ^ (d - v) * b ^ u * b ^ (v - u) := Nat.mul_le_mul_left _ this + _ = a ^ (d - v) * (b ^ u * b ^ (v - u)) := by ring + +include hp hq hpq in +lemma pq_factorization {b D u : ℕ} (hb : 0 < b) (hbp : ¬ p ∣ b) (hbq : ¬ q ∣ b) : + (b * p ^ (D - u) * q ^ u).factorization p = D - u ∧ + (b * p ^ (D - u) * q ^ u).factorization q = u := by + have hpq' : p ≠ q := hpq.ne + have h1 : b * p ^ (D - u) ≠ 0 := Nat.mul_ne_zero hb.ne' (pow_ne_zero _ hp.ne_zero) + rw [Nat.factorization_mul h1 (pow_ne_zero _ hq.ne_zero), + Nat.factorization_mul hb.ne' (pow_ne_zero _ hp.ne_zero), Nat.factorization_pow, + Nat.factorization_pow] + simp only [Finsupp.add_apply, Finsupp.smul_apply, + Nat.factorization_eq_zero_of_not_dvd hbp, Nat.factorization_eq_zero_of_not_dvd hbq, + hp.factorization, hq.factorization, Finsupp.single_apply, smul_eq_mul] + refine ⟨?_, ?_⟩ + · simp [hpq'.symm] + · simp [hpq'] + +/-- Chains along a pair of primes `p < q` (fixed total exponent). -/ +noncomputable def pqChain : ChainSys (ℕ × ℕ) where + key n := (n / (p ^ n.factorization p * q ^ n.factorization q), + n.factorization p + n.factorization q) + pos n := n.factorization q + elt k u := k.1 * p ^ (k.2 - u) * q ^ u + vld k u := 0 < k.1 ∧ ¬ p ∣ k.1 ∧ ¬ q ∣ k.1 ∧ u ≤ k.2 + elt_key_pos n hn := by + have hcop : Nat.Coprime (p ^ n.factorization p) (q ^ n.factorization q) := + Nat.Coprime.pow _ _ ((Nat.coprime_primes hp hq).2 hpq.ne) + have hdvd : p ^ n.factorization p * q ^ n.factorization q ∣ n := + hcop.mul_dvd_of_dvd_of_dvd (Nat.ordProj_dvd n p) (Nat.ordProj_dvd n q) + simp only [Nat.add_sub_cancel] + rw [mul_assoc, Nat.div_mul_cancel hdvd] + vld_key_pos n hn := by + have hcop : Nat.Coprime (p ^ n.factorization p) (q ^ n.factorization q) := + Nat.Coprime.pow _ _ ((Nat.coprime_primes hp hq).2 hpq.ne) + have hdvd : p ^ n.factorization p * q ^ n.factorization q ∣ n := + hcop.mul_dvd_of_dvd_of_dvd (Nat.ordProj_dvd n p) (Nat.ordProj_dvd n q) + set b := n / (p ^ n.factorization p * q ^ n.factorization q) with hbdef + have hbn : b * (p ^ n.factorization p * q ^ n.factorization q) = n := Nat.div_mul_cancel hdvd + have hb0 : 0 < b := by + rcases Nat.eq_zero_or_pos b with h | h + · rw [h, zero_mul] at hbn; omega + · exact h + have hfac : b.factorization p = 0 ∧ b.factorization q = 0 := by + have := congrArg (fun m => m.factorization) hbn + rw [Nat.factorization_mul hb0.ne' (Nat.mul_ne_zero (pow_ne_zero _ hp.ne_zero) + (pow_ne_zero _ hq.ne_zero)), + Nat.factorization_mul (pow_ne_zero _ hp.ne_zero) (pow_ne_zero _ hq.ne_zero), + Nat.factorization_pow, Nat.factorization_pow] at this + have hpv := DFunLike.congr_fun this p + have hqv := DFunLike.congr_fun this q + simp only [Finsupp.add_apply, Finsupp.smul_apply, hp.factorization, hq.factorization, + Finsupp.single_apply, smul_eq_mul] at hpv hqv + simp only [hpq.ne, hpq.ne.symm, ite_true, ite_false] at hpv hqv + constructor <;> omega + refine ⟨hb0, fun h => ?_, fun h => ?_, by omega⟩ + · have := hp.factorization_pos_of_dvd hb0.ne' h; omega + · have := hq.factorization_pos_of_dvd hb0.ne' h; omega + key_elt k u h := by + obtain ⟨hb, hbp, hbq, hu⟩ := h + obtain ⟨h1, h2⟩ := pq_factorization (D := k.2) (u := u) hp hq hpq hb hbp hbq + simp only [h1, h2] + ext + · simp only + rw [mul_assoc, Nat.mul_div_cancel _ (Nat.mul_pos (pow_pos hp.pos _) (pow_pos hq.pos _))] + · simp only + omega + pos_elt k u h := (pq_factorization hp hq hpq h.1 h.2.1 h.2.2.1).2 + elt_pos k u h := Nat.mul_pos (Nat.mul_pos h.1 (pow_pos hp.pos _)) (pow_pos hq.pos _) + vld_mono k u v h hvu := ⟨h.1, h.2.1, h.2.2.1, le_trans hvu h.2.2.2⟩ + elt_lt k u v h huv := by + obtain ⟨hb, -, -, hv⟩ := h + have e1 : k.2 - u = (k.2 - v) + (v - u) := by omega + have e2 : v = u + (v - u) := by omega + have hlt : p ^ (v - u) < q ^ (v - u) := Nat.pow_lt_pow_left hpq (by omega) + change k.1 * p ^ (k.2 - u) * q ^ u < k.1 * p ^ (k.2 - v) * q ^ v + rw [e1, pow_add, show q ^ v = q ^ u * q ^ (v - u) by rw [← pow_add, Nat.add_sub_cancel' huv.le]] + have hpos : 0 < k.1 * p ^ (k.2 - v) * q ^ u := + Nat.mul_pos (Nat.mul_pos hb (pow_pos hp.pos _)) (pow_pos hq.pos _) + calc k.1 * (p ^ (k.2 - v) * p ^ (v - u)) * q ^ u + = k.1 * p ^ (k.2 - v) * q ^ u * p ^ (v - u) := by ring + _ < k.1 * p ^ (k.2 - v) * q ^ u * q ^ (v - u) := Nat.mul_lt_mul_of_pos_left hlt hpos + _ = k.1 * p ^ (k.2 - v) * (q ^ u * q ^ (v - u)) := by ring + +lemma pqChain_cons (t : ℕ) (k : ℕ × ℕ) : (pqChain hp hq hpq).Cons t k := by + classical + by_cases hk : 0 < k.1 ∧ ¬ p ∣ k.1 ∧ ¬ q ∣ k.1 + swap + · exact ⟨PUnit, ∅, fun _ => k, fun _ => 0, fun e he => absurd ⟨he.1, he.2.1, he.2.2.1⟩ hk, + fun S _ e he => absurd ⟨he.1, he.2.1, he.2.2.1⟩ hk⟩ + obtain ⟨b, D⟩ := k + obtain ⟨hb, hbp, hbq⟩ := hk + set P : ℕ → ℕ → ℕ → Prop := fun c d h => c * p ^ (d - h) * q ^ h ≤ t with hP + set I : Finset (ℕ × ℕ) := + (((Icc 1 t).filter (fun c => ¬ p ∣ c ∧ ¬ q ∣ c)) ×ˢ range (t + 1)).filter + (fun cd => cd.1 * p ^ cd.2 ≤ t) with hI + refine ⟨ℕ × ℕ, I, fun cd => (b * cd.1, D + cd.2), + fun cd => Nat.findGreatest (P cd.1 cd.2) cd.2, ?_, ?_⟩ + · intro e he cd hcd h hh + simp only [hI, mem_filter, mem_product, mem_Icc] at hcd + have hle : Nat.findGreatest (P cd.1 cd.2) cd.2 ≤ cd.2 := Nat.findGreatest_le _ + refine ⟨Nat.mul_pos hb (by omega), fun hdvd => ?_, fun hdvd => ?_, ?_⟩ + · exact ((Nat.Prime.dvd_mul hp).1 hdvd).elim hbp hcd.1.1.2.1 + · exact ((Nat.Prime.dvd_mul hq).1 hdvd).elim hbq hcd.1.1.2.2 + · change e + h ≤ D + cd.2 + have heD : e ≤ D := he.2.2.2 + have hh' : h ≤ Nat.findGreatest (P cd.1 cd.2) cd.2 := hh + omega + · intro S hS e he + have heD : e ≤ D := he.2.2.2 + change b * p ^ (D - e) * q ^ e ∈ A S t ↔ b * p ^ (D - e) * q ^ e ∈ S ∧ ∀ cd ∈ I, + ∀ h ≤ Nat.findGreatest (P cd.1 cd.2) cd.2, + b * cd.1 * p ^ (D + cd.2 - (e + h)) * q ^ (e + h) ∈ S + rw [A, mem_filter] + refine and_congr_right fun _ => ?_ + constructor + · intro hall cd hcd h hh + simp only [hI, mem_filter, mem_product, mem_Icc, mem_range] at hcd + obtain ⟨⟨⟨⟨hc1, hct⟩, -⟩, -⟩, hcpd⟩ := hcd + have hd : Nat.findGreatest (P cd.1 cd.2) cd.2 ≤ cd.2 := Nat.findGreatest_le _ + -- `P cd.1 cd.2 h` holds since `P` holds at the greatest index and is antitone + have hPG : P cd.1 cd.2 (Nat.findGreatest (P cd.1 cd.2) cd.2) := + Nat.findGreatest_spec (m := 0) (Nat.zero_le _) (by simpa [hP] using hcpd) + have hPh : P cd.1 cd.2 h := by + simp only [hP] at hPG ⊢ + calc cd.1 * p ^ (cd.2 - h) * q ^ h + = cd.1 * (p ^ (cd.2 - h) * q ^ h) := by ring + _ ≤ cd.1 * (p ^ (cd.2 - Nat.findGreatest (P cd.1 cd.2) cd.2) * + q ^ Nat.findGreatest (P cd.1 cd.2) cd.2) := + Nat.mul_le_mul_left _ (pow_mul_pow_mono hpq.le hh hd) + _ = _ := by ring + _ ≤ t := hPG + have hj := hall (cd.1 * p ^ (cd.2 - h) * q ^ h) + (mem_Icc.2 ⟨Nat.mul_pos (Nat.mul_pos hc1 (pow_pos hp.pos _)) (pow_pos hq.pos _), hPh⟩) + have hexp : D + cd.2 - (e + h) = (D - e) + (cd.2 - h) := by omega + rw [hexp, pow_add, pow_add] + rw [show cd.1 * p ^ (cd.2 - h) * q ^ h * (b * p ^ (D - e) * q ^ e) = + b * cd.1 * (p ^ (D - e) * p ^ (cd.2 - h)) * (q ^ e * q ^ h) by ring] at hj + exact hj + · intro hcons j hj + rw [mem_Icc] at hj + have hj0 : 0 < j := by omega + set C := pqChain hp hq hpq + have hvj := C.vld_key_pos j hj0 + have hjeq := C.elt_key_pos j hj0 + set c := (C.key j).1 + set d := (C.key j).2 + set h := C.pos j + have hhd : h ≤ d := hvj.2.2.2 + change c * p ^ (d - h) * q ^ h = j at hjeq + have hcpd : c * p ^ d ≤ j := by + have := Nat.mul_le_mul_left c (pow_mul_pow_mono hpq.le (Nat.zero_le h) hhd) + simp only [Nat.sub_zero, pow_zero, mul_one] at this + calc c * p ^ d ≤ c * (p ^ (d - h) * q ^ h) := this + _ = j := by rw [← hjeq]; ring + have hc1 : 1 ≤ c := hvj.1 + have hdt : d < t + 1 := by + have : d < p ^ d := Nat.lt_pow_self hp.one_lt + have : p ^ d ≤ c * p ^ d := Nat.le_mul_of_pos_left _ hc1 + omega + have hcI : (c, d) ∈ I := by + simp only [hI, mem_filter, mem_product, mem_Icc, mem_range] + refine ⟨⟨⟨⟨hc1, ?_⟩, hvj.2.1, hvj.2.2.1⟩, hdt⟩, by omega⟩ + have : c ≤ c * p ^ d := Nat.le_mul_of_pos_right _ (pow_pos hp.pos _) + omega + have hhG : h ≤ Nat.findGreatest (P c d) d := + Nat.le_findGreatest hhd (by simp only [hP]; omega) + have := hcons (c, d) hcI h hhG + have hexp : D + d - (e + h) = (D - e) + (d - h) := by omega + simp only at this + rw [hexp, pow_add, pow_add] at this + rw [show j * (b * p ^ (D - e) * q ^ e) = b * c * (p ^ (D - e) * p ^ (d - h)) * + (q ^ e * q ^ h) by rw [← hjeq]; ring] + exact this + +/-- `a / q * p` sits one position below `a` on the `(p, q)`-chain of `a`. -/ +lemma pqChain_shift {a : ℕ} (ha : 0 < a) (hqa : q ∣ a) : + (pqChain hp hq hpq).vld ((pqChain hp hq hpq).key a) ((pqChain hp hq hpq).pos a - 1) ∧ + (pqChain hp hq hpq).pos a - 1 < (pqChain hp hq hpq).pos a ∧ + (pqChain hp hq hpq).elt ((pqChain hp hq hpq).key a) ((pqChain hp hq hpq).pos a - 1) = + a / q * p := by + set C := pqChain hp hq hpq + have hv := C.vld_key_pos a ha + have ha' := C.elt_key_pos a ha + have hpos : 0 < C.pos a := by + change 0 < a.factorization q + exact hq.factorization_pos_of_dvd ha.ne' hqa + refine ⟨C.vld_mono _ _ _ hv (by omega), by omega, ?_⟩ + set b := (C.key a).1 + set D := (C.key a).2 + set u := C.pos a + have huD : u ≤ D := hv.2.2.2 + change b * p ^ (D - u) * q ^ u = a at ha' + change b * p ^ (D - (u - 1)) * q ^ (u - 1) = a / q * p + have e1 : D - (u - 1) = (D - u) + 1 := by omega + have hqu : q ^ u = q ^ (u - 1) * q := by rw [← pow_succ, Nat.sub_add_cancel hpos] + have ha2 : a = b * p ^ (D - u) * q ^ (u - 1) * q := by rw [← ha', hqu]; ring + have hdiv : a / q = b * p ^ (D - u) * q ^ (u - 1) := by + rw [ha2, Nat.mul_div_cancel _ hq.pos] + rw [hdiv, e1, pow_succ] + ring + +end pqChain + +/-- If a chain has an occupied position `pos n` and an empty valid position below it, the +chain's occupied set is not an initial segment. -/ +lemma ChainSys.gap {κ : Type} [DecidableEq κ] {C : ChainSys κ} {T : Finset ℕ} + (hT : ∀ n ∈ T, 0 < n) {n u : ℕ} (hn : n ∈ T) (hu : u < C.pos n) + (hout : C.elt (C.key n) u ∉ T) : + C.occ T (C.key n) ≠ range (C.occ T (C.key n)).card := by + intro h + have hn0 := hT n hn + have hmem : C.pos n ∈ C.occ T (C.key n) := + (ChainSys.mem_occ_iff hT).2 ⟨C.vld_key_pos n hn0, by rw [C.elt_key_pos n hn0]; exact hn⟩ + rw [h, mem_range] at hmem + have : u ∈ C.occ T (C.key n) := by rw [h, mem_range]; omega + exact hout ((ChainSys.mem_occ_iff hT).1 this).2 + +/-- One-step divisor closure implies divisor closure. -/ +lemma divClosed_of_step {T : Finset ℕ} (hT : ∀ n ∈ T, 0 < n) + (hstep : ∀ x ∈ T, ∀ p : ℕ, p.Prime → p ∣ x → x / p ∈ T) : DivClosed T := by + intro a + induction a using Nat.strong_induction_on with + | _ a ih => + intro ha d hd + by_cases hda : d = a + · rw [hda]; exact ha + have ha0 := hT a ha + obtain ⟨m, rfl⟩ := hd + have hm1 : m ≠ 1 := by intro h; apply hda; rw [h, mul_one] + have hm0 : m ≠ 0 := by intro h; rw [h, mul_zero] at ha0; omega + have hd0 : 0 < d := Nat.pos_of_ne_zero (by rintro rfl; simp at ha0) + obtain ⟨r, hr, m', rfl⟩ : ∃ r, r.Prime ∧ ∃ m', m = r * m' := + ⟨m.minFac, Nat.minFac_prime hm1, Nat.minFac_dvd m⟩ + have hm'0 : 0 < m' := Nat.pos_of_ne_zero (by rintro rfl; simp at hm0) + have hmem := hstep (d * (r * m')) ha r hr ⟨d * m', by ring⟩ + have hdiv : d * (r * m') / r = d * m' := by + rw [show d * (r * m') = r * (d * m') by ring, Nat.mul_div_cancel_left _ hr.pos] + rw [hdiv] at hmem + have hlt : d * m' < d * (r * m') := by + apply Nat.mul_lt_mul_of_pos_left _ hd0 + have := hr.two_le + calc m' < 2 * m' := by omega + _ ≤ r * m' := Nat.mul_le_mul_right _ this + exact ih _ hlt hmem d (Dvd.intro _ rfl) + +/-- **Lemma 2**: every finite set of positive integers can be replaced by a set of the same size, +closed under divisors and under replacing a prime factor by a smaller prime, without decreasing +any run count `|A S t|`. -/ +theorem exists_closed (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : + ∃ T : Finset ℕ, (∀ a ∈ T, 0 < a) ∧ T.card = S.card ∧ DivClosed T ∧ ShiftClosed T ∧ + ∀ t, (A S t).card ≤ (A T t).card := by + classical + let good : Finset ℕ → Prop := fun T => + (∀ a ∈ T, 0 < a) ∧ T.card = S.card ∧ ∀ t, (A S t).card ≤ (A T t).card + have hex : ∃ s, ∃ T, good T ∧ ∑ n ∈ T, n = s := ⟨_, S, ⟨hS, rfl, fun _ => le_rfl⟩, rfl⟩ + obtain ⟨T, hT, hTs⟩ := Nat.find_spec hex + have hmin : ∀ T', good T' → ∑ n ∈ T, n ≤ ∑ n ∈ T', n := fun T' hT' => by + rw [hTs]; exact Nat.find_min' hex ⟨T', hT', rfl⟩ + -- compressing a good set gives a good set + have hcomp : ∀ {κ : Type} [DecidableEq κ] (C : ChainSys κ), (∀ t k, C.Cons t k) → + good (C.comp T) := by + intro κ _ C hC + exact ⟨ChainSys.comp_pos hT.1, by rw [ChainSys.card_comp hT.1, hT.2.1], + fun t => (hT.2.2 t).trans (ChainSys.card_A_le_comp hT.1 t (hC t))⟩ + -- no chain of a minimal good set has a gap + have hnogap : ∀ {κ : Type} [DecidableEq κ] (C : ChainSys κ), (∀ t k, C.Cons t k) → + ∀ k, C.occ T k = range (C.occ T k).card := by + intro κ _ C hC k + by_contra hk + have h1 := (ChainSys.sum_comp_le (C := C) hT.1).2 ⟨k, hk⟩ + have h2 := hmin _ (hcomp C hC) + omega + refine ⟨T, hT.1, hT.2.1, ?_, ?_, hT.2.2⟩ + · apply divClosed_of_step hT.1 + intro x hx p hp hpx + by_contra hout + obtain ⟨hv, hlt, heq⟩ := pChain_div hp (hT.1 x hx) hpx + exact ChainSys.gap hT.1 hx hlt (by rw [heq]; exact hout) + (hnogap (pChain hp) (fun t b => pChain_cons hp t b) _) + · intro a ha p q hp hq hpq hqa + by_contra hout + obtain ⟨hv, hlt, heq⟩ := pqChain_shift hp hq hpq (hT.1 a ha) hqa + exact ChainSys.gap hT.1 ha hlt (by rw [heq]; exact hout) + (hnogap (pqChain hp hq hpq) (fun t k => pqChain_cons hp hq hpq t k) _) + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Alt/Compression.lean b/LeanPool/RunsOfMultiples/Alt/Compression.lean new file mode 100644 index 0000000000..de551106b7 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Compression.lean @@ -0,0 +1,360 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Alt.Defs +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Tactic.Linarith + +/-! +# Chain compression (Lemma 1 and the abstract part of Lemma 2) + +A *chain system* splits the positive integers into chains: every `n > 0` sits at position +`pos n` of the chain `key n`, and `elt k u` is the element at position `u` of chain `k` +(valid positions form an initial segment, elements increase along a chain). + +`comp S` replaces the occupied positions of every chain by an initial segment of the same size. +We show `|comp S| = |S|`, that `comp` does not decrease any `|A S t|` provided the multiples +`j * elt k e` (`j ≤ t`) can be described by "shifted windows" in target chains (`Cons`), and +that `comp` strictly decreases the sum of the elements as soon as some chain has a gap. +-/ + +open Finset + +@[expose] public section + +namespace RunsOfMultiples + +/-- A partition of the positive integers into increasing chains. -/ +structure ChainSys (κ : Type) where + /-- The chain containing a positive integer. -/ + key : ℕ → κ + /-- The position of a positive integer in its chain. -/ + pos : ℕ → ℕ + /-- The integer at a given chain and position. -/ + elt : κ → ℕ → ℕ + /-- The positions belonging to a chain, forming an initial segment. -/ + vld : κ → ℕ → Prop + elt_key_pos : ∀ n, 0 < n → elt (key n) (pos n) = n + vld_key_pos : ∀ n, 0 < n → vld (key n) (pos n) + key_elt : ∀ k u, vld k u → key (elt k u) = k + pos_elt : ∀ k u, vld k u → pos (elt k u) = u + elt_pos : ∀ k u, vld k u → 0 < elt k u + vld_mono : ∀ k u v, vld k u → v ≤ u → vld k v + elt_lt : ∀ k u v, vld k v → u < v → elt k u < elt k v + +namespace ChainSys + +variable {κ : Type} [DecidableEq κ] (C : ChainSys κ) + +/-- Occupied positions of chain `k`. -/ +def occ (S : Finset ℕ) (k : κ) : Finset ℕ := (S.filter (fun n => C.key n = k)).image C.pos + +/-- Compression: every chain's occupied positions become an initial segment. -/ +def comp (S : Finset ℕ) : Finset ℕ := + (S.image C.key).biUnion (fun k => (range (C.occ S k).card).image (C.elt k)) + +/-- The window condition describing `A S t` along chain `k`. -/ +def Cons (t : ℕ) (k : κ) : Prop := + ∃ (ι : Type) (I : Finset ι) (tgt : ι → κ) (Lc : ι → ℕ), + (∀ e, C.vld k e → ∀ i ∈ I, ∀ h ≤ Lc i, C.vld (tgt i) (e + h)) ∧ + ∀ S : Finset ℕ, (∀ n ∈ S, 0 < n) → ∀ e, C.vld k e → + (C.elt k e ∈ A S t ↔ C.elt k e ∈ S ∧ ∀ i ∈ I, ∀ h ≤ Lc i, C.elt (tgt i) (e + h) ∈ S) + +variable {C} + +section basic + +variable {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) +include hS + +lemma mem_occ_iff {k : κ} {u : ℕ} : u ∈ C.occ S k ↔ C.vld k u ∧ C.elt k u ∈ S := by + unfold occ + rw [mem_image] + constructor + · rintro ⟨n, hn, rfl⟩ + rw [mem_filter] at hn + obtain ⟨hnS, rfl⟩ := hn + exact ⟨C.vld_key_pos n (hS n hnS), by rw [C.elt_key_pos n (hS n hnS)]; exact hnS⟩ + · rintro ⟨hv, hmem⟩ + exact ⟨C.elt k u, mem_filter.2 ⟨hmem, C.key_elt k u hv⟩, C.pos_elt k u hv⟩ + +lemma vld_of_lt_card {k : κ} {u : ℕ} (hu : u < (C.occ S k).card) : C.vld k u := by + have hne : (C.occ S k).Nonempty := card_pos.1 (by omega) + have hM : (C.occ S k).max' hne ∈ C.occ S k := max'_mem _ _ + have hsub : C.occ S k ⊆ range ((C.occ S k).max' hne + 1) := fun x hx => + mem_range.2 (Nat.lt_succ_of_le (le_max' _ _ hx)) + have := card_le_card hsub + rw [card_range] at this + exact C.vld_mono k _ u ((mem_occ_iff hS).1 hM).1 (by omega) + +lemma mem_comp_iff {n : ℕ} (hn : 0 < n) : n ∈ C.comp S ↔ C.pos n < (C.occ S (C.key n)).card := by + unfold comp + rw [mem_biUnion] + constructor + · rintro ⟨k, -, hk⟩ + rw [mem_image] at hk + obtain ⟨u, hu, rfl⟩ := hk + rw [mem_range] at hu + have hv := vld_of_lt_card hS hu + rw [C.key_elt k u hv, C.pos_elt k u hv] + exact hu + · intro h + obtain ⟨u, hu⟩ : (C.occ S (C.key n)).Nonempty := card_pos.1 (by omega) + unfold occ at hu + rw [mem_image] at hu + obtain ⟨m, hm, -⟩ := hu + rw [mem_filter] at hm + exact ⟨C.key n, mem_image.2 ⟨m, hm.1, hm.2⟩, + mem_image.2 ⟨C.pos n, mem_range.2 h, C.elt_key_pos n hn⟩⟩ + +lemma comp_pos : ∀ n ∈ C.comp S, 0 < n := by + intro n hn + unfold comp at hn + rw [mem_biUnion] at hn + obtain ⟨k, -, hk⟩ := hn + rw [mem_image] at hk + obtain ⟨u, hu, rfl⟩ := hk + exact C.elt_pos k u (vld_of_lt_card hS (mem_range.1 hu)) + +lemma occ_comp (k : κ) : C.occ (C.comp S) k = range (C.occ S k).card := by + ext u + rw [mem_occ_iff (comp_pos hS), mem_range] + constructor + · rintro ⟨hv, hmem⟩ + have := (mem_comp_iff hS (C.elt_pos k u hv)).1 hmem + rwa [C.key_elt k u hv, C.pos_elt k u hv] at this + · intro hu + have hv := vld_of_lt_card hS hu + refine ⟨hv, (mem_comp_iff hS (C.elt_pos k u hv)).2 ?_⟩ + rwa [C.key_elt k u hv, C.pos_elt k u hv] + +/-- On a chain, `pos` is injective. -/ +lemma pos_injOn (k : κ) : Set.InjOn C.pos ↑(S.filter (fun n => C.key n = k)) := by + intro x hx y hy hxy + simp only [coe_filter, Set.mem_ofPred_eq] at hx hy + rw [← C.elt_key_pos x (hS x hx.1), ← C.elt_key_pos y (hS y hy.1), hx.2, hy.2, hxy] + +lemma card_fibre (k : κ) : (S.filter (fun n => C.key n = k)).card = (C.occ S k).card := + (card_image_of_injOn (pos_injOn hS k)).symm + +lemma key_mem_of_mem_comp {n : ℕ} (hn : n ∈ C.comp S) : C.key n ∈ S.image C.key := by + have hn0 := comp_pos hS n hn + have h := (mem_comp_iff hS hn0).1 hn + obtain ⟨u, hu⟩ : (C.occ S (C.key n)).Nonempty := card_pos.1 (by omega) + unfold occ at hu + rw [mem_image] at hu + obtain ⟨m, hm, -⟩ := hu + rw [mem_filter] at hm + exact mem_image.2 ⟨m, hm.1, hm.2⟩ + +/-- Compression preserves cardinality. -/ +theorem card_comp : (C.comp S).card = S.card := by + rw [card_eq_sum_card_fiberwise (f := C.key) (t := S.image C.key) + (fun n hn => key_mem_of_mem_comp hS hn), + card_eq_sum_card_fiberwise (f := C.key) (t := S.image C.key) + (fun n hn => mem_image_of_mem _ hn)] + refine sum_congr rfl fun k _ => ?_ + rw [card_fibre (comp_pos hS), card_fibre hS, occ_comp hS, card_range] + +/-- The sum of a set, chain by chain. -/ +lemma sum_eq_sum_occ : ∑ n ∈ S, n = ∑ k ∈ S.image C.key, ∑ u ∈ C.occ S k, C.elt k u := by + rw [← sum_fiberwise_of_maps_to (g := C.key) (t := S.image C.key) + (fun n hn => mem_image_of_mem _ hn)] + refine sum_congr rfl fun k _ => ?_ + unfold occ + rw [sum_image (pos_injOn hS k)] + refine sum_congr rfl fun n hn => ?_ + rw [mem_filter] at hn + rw [← hn.2, C.elt_key_pos n (hS n hn.1)] + +end basic + +/-- Sum over an initial segment is at most the sum over any set of the same size, for a +function increasing on an initial segment containing the set; strictly if the set is not the +initial segment. -/ +lemma sum_range_le_sum (f : ℕ → ℕ) (P : ℕ → Prop) + (hf : ∀ u v, P v → u < v → f u < f v) : + ∀ (s : ℕ) (E : Finset ℕ), E.card = s → (∀ u ∈ E, P u) → + ∑ u ∈ range s, f u ≤ ∑ u ∈ E, f u ∧ (E ≠ range s → ∑ u ∈ range s, f u < ∑ u ∈ E, f u) := by + intro s + induction s with + | zero => + intro E hE _ + rw [card_eq_zero] at hE + subst hE + simp + | succ s ih => + intro E hE hP' + have hne : E.Nonempty := card_pos.1 (by omega) + set M := E.max' hne with hMdef + have hME : M ∈ E := max'_mem _ _ + have hcard : (E.erase M).card = s := by rw [card_erase_of_mem hME, hE]; rfl + obtain ⟨ih1, ih2⟩ := ih (E.erase M) hcard (fun u hu => hP' u (mem_of_mem_erase hu)) + -- the maximum is at least `s` + have hsM : s ≤ M := by + have hsub : E ⊆ range (M + 1) := fun x hx => + mem_range.2 (Nat.lt_succ_of_le (le_max' _ _ hx)) + have := card_le_card hsub + rw [card_range] at this + omega + have hfs : f s ≤ f M := by + rcases Nat.lt_or_eq_of_le hsM with h | h + · exact (hf s M (hP' M hME) h).le + · rw [h] + rw [sum_range_succ, ← add_sum_erase E f hME] + refine ⟨by linarith, fun hneq => ?_⟩ + rcases Nat.lt_or_eq_of_le hsM with h | h + · have := hf s M (hP' M hME) h + linarith + · -- `M = s`, so the rest must differ from `range s` + have hrest : E.erase M ≠ range s := by + intro hcontra + apply hneq + ext x + rw [mem_range] + constructor + · intro hx + by_cases hxM : x = M + · omega + · have : x ∈ E.erase M := mem_erase.2 ⟨hxM, hx⟩ + rw [hcontra, mem_range] at this + omega + · intro hx + by_cases hxs : x = s + · rw [hxs, h]; exact hME + · have : x ∈ range s := mem_range.2 (by omega) + rw [← hcontra] at this + exact mem_of_mem_erase this + have := ih2 hrest + have hfsM : f s = f M := by rw [h] + linarith + +/-- Compression does not increase the sum, and strictly decreases it if some chain has a gap. -/ +theorem sum_comp_le {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) : + ∑ n ∈ C.comp S, n ≤ ∑ n ∈ S, n ∧ + ((∃ k, C.occ S k ≠ range (C.occ S k).card) → ∑ n ∈ C.comp S, n < ∑ n ∈ S, n) := by + have hkeys : (C.comp S).image C.key ⊆ S.image C.key := by + intro k hk + rw [mem_image] at hk + obtain ⟨n, hn, rfl⟩ := hk + exact key_mem_of_mem_comp hS hn + have hcompsum : ∑ n ∈ C.comp S, n = + ∑ k ∈ S.image C.key, ∑ u ∈ range (C.occ S k).card, C.elt k u := by + rw [← sum_fiberwise_of_maps_to (g := C.key) (t := S.image C.key) + (fun n hn => key_mem_of_mem_comp hS hn)] + refine sum_congr rfl fun k _ => ?_ + rw [← occ_comp hS k] + unfold occ + rw [sum_image (pos_injOn (comp_pos hS) k)] + refine sum_congr rfl fun n hn => ?_ + rw [mem_filter] at hn + rw [← hn.2, C.elt_key_pos n (comp_pos hS n hn.1)] + have hchain : ∀ k, ∑ u ∈ range (C.occ S k).card, C.elt k u ≤ ∑ u ∈ C.occ S k, C.elt k u ∧ + (C.occ S k ≠ range (C.occ S k).card → + ∑ u ∈ range (C.occ S k).card, C.elt k u < ∑ u ∈ C.occ S k, C.elt k u) := fun k => + sum_range_le_sum (C.elt k) (C.vld k) + (fun u v hv huv => C.elt_lt k u v hv huv) _ _ rfl + (fun u hu => ((mem_occ_iff hS).1 hu).1) + rw [hcompsum, sum_eq_sum_occ (C := C) hS] + refine ⟨sum_le_sum fun k _ => (hchain k).1, ?_⟩ + rintro ⟨k, hk⟩ + have hkS : k ∈ S.image C.key := by + by_contra hk' + apply hk + have : C.occ S k = ∅ := by + unfold occ + rw [image_eq_empty, filter_eq_empty_iff] + intro n hn hnk + exact hk' (mem_image.2 ⟨n, hn, hnk⟩) + rw [this] + rfl + exact sum_lt_sum (fun k _ => (hchain k).1) ⟨k, hkS, (hchain k).2 hk⟩ + +/-- **Lemma 1 + compression**: if every chain satisfies the window condition for `t`, +compression does not decrease `|A S t|`. -/ +theorem card_A_le_comp {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) (t : ℕ) (hC : ∀ k, C.Cons t k) : + (A S t).card ≤ (A (C.comp S) t).card := by + have hS' := comp_pos (C := C) hS + rw [card_eq_sum_card_fiberwise (f := C.key) (t := S.image C.key) + (fun n hn => mem_image_of_mem _ (A_subset S t hn)), + card_eq_sum_card_fiberwise (f := C.key) (t := S.image C.key) + (fun n hn => key_mem_of_mem_comp hS (A_subset _ t hn))] + refine sum_le_sum fun k _ => ?_ + obtain ⟨ι, I, tgt, Lc, hvld, hiff⟩ := hC k + classical + -- the valid starting positions along chain `k` + let V : Finset ℕ → Finset ℕ := fun T => (C.occ T k).filter + (fun e => ∀ i ∈ I, ∀ h ∈ range (Lc i + 1), e + h ∈ C.occ T (tgt i)) + -- the fibre of `A T t` over `k` is in bijection with `V T` + have hfib : ∀ T : Finset ℕ, (∀ n ∈ T, 0 < n) → + ((A T t).filter (fun n => C.key n = k)).card = (V T).card := by + intro T hT + have hsub : (A T t).filter (fun n => C.key n = k) ⊆ T.filter (fun n => C.key n = k) := + filter_subset_filter _ (A_subset T t) + rw [← card_image_of_injOn (Set.InjOn.mono (by exact_mod_cast hsub) (pos_injOn hT k))] + congr 1 + ext e + simp only [mem_image, mem_filter, V, mem_range] + constructor + · rintro ⟨n, ⟨hnA, hnk⟩, rfl⟩ + have hn0 := hT n (A_subset T t hnA) + have hv : C.vld k (C.pos n) := by rw [← hnk]; exact C.vld_key_pos n hn0 + have helt : C.elt k (C.pos n) = n := by rw [← hnk]; exact C.elt_key_pos n hn0 + have := (hiff T hT (C.pos n) hv).1 (by rw [helt]; exact hnA) + refine ⟨(mem_occ_iff hT).2 ⟨hv, this.1⟩, fun i hi h hh => ?_⟩ + exact (mem_occ_iff hT).2 ⟨hvld _ hv i hi h (by omega), this.2 i hi h (by omega)⟩ + · rintro ⟨he, hcons⟩ + obtain ⟨hv, hmem⟩ := (mem_occ_iff hT).1 he + refine ⟨C.elt k e, ⟨(hiff T hT e hv).2 ⟨hmem, fun i hi h hh => ?_⟩, + C.key_elt k e hv⟩, C.pos_elt k e hv⟩ + exact ((mem_occ_iff hT).1 (hcons i hi h (by omega))).2 + rw [hfib S hS, hfib _ hS'] + -- Lemma 1: `|V S| + Lc i ≤ |occ S (tgt i)|` + have hwin : ∀ i ∈ I, (V S).Nonempty → (V S).card + Lc i ≤ (C.occ S (tgt i)).card := by + intro i hi hne + set e₀ := (V S).max' hne + have he₀ : e₀ ∈ V S := max'_mem _ _ + have hdisj : Disjoint (V S) ((Icc 1 (Lc i)).image (fun h => e₀ + h)) := by + rw [disjoint_left] + intro x hx hx' + rw [mem_image] at hx' + obtain ⟨h, hh, rfl⟩ := hx' + rw [mem_Icc] at hh + have := le_max' (V S) _ hx + omega + have hsub : V S ∪ (Icc 1 (Lc i)).image (fun h => e₀ + h) ⊆ C.occ S (tgt i) := by + intro x hx + rw [mem_union] at hx + rcases hx with hx | hx + · have := (mem_filter.1 hx).2 i hi 0 (mem_range.2 (Nat.succ_pos _)) + simpa using this + · rw [mem_image] at hx + obtain ⟨h, hh, rfl⟩ := hx + rw [mem_Icc] at hh + exact (mem_filter.1 he₀).2 i hi h (mem_range.2 (by omega)) + have := card_le_card hsub + rw [card_union_of_disjoint hdisj, card_image_of_injective _ (add_right_injective e₀), + Nat.card_Icc] at this + omega + -- after compression, the first `|V S|` positions are valid starts + have hrange : range (V S).card ⊆ V (C.comp S) := by + intro e he + rw [mem_range] at he + have hne : (V S).Nonempty := card_pos.1 (by omega) + have hVocc : (V S).card ≤ (C.occ S k).card := card_le_card (filter_subset _ _) + simp only [V, mem_filter, occ_comp hS, mem_range] + refine ⟨by omega, fun i hi h hh => ?_⟩ + have := hwin i hi hne + omega + have := card_le_card hrange + rwa [card_range] at this + +end ChainSys + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Alt/Defs.lean b/LeanPool/RunsOfMultiples/Alt/Defs.lean new file mode 100644 index 0000000000..b352e78ace --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Defs.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Defs +public import Mathlib.Data.Nat.Prime.Defs + +/-! +# The compression proof: shared definitions + +The compression proof (`docs/first-missing-multiple.pdf`) compresses `S` to a set `T` with the +same cardinality and no fewer runs (`|A S t| ≤ |A T t|` for all `t`) that is +* (i) closed under divisors (`DivClosed`), and +* (ii) closed under replacing a prime factor `q` by a smaller prime `p` (`ShiftClosed`). +-/ + +@[expose] public section + +namespace RunsOfMultiples + +/-- (i): every divisor of an element of `T` belongs to `T`. -/ +def DivClosed (T : Finset ℕ) : Prop := ∀ a ∈ T, ∀ d, d ∣ a → d ∈ T + +/-- (ii): if `a ∈ T`, `q ∣ a` and `p < q` are primes, then `a / q * p ∈ T`. -/ +def ShiftClosed (T : Finset ℕ) : Prop := + ∀ a ∈ T, ∀ p q : ℕ, p.Prime → q.Prime → p < q → q ∣ a → a / q * p ∈ T + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Alt/Lower.lean b/LeanPool/RunsOfMultiples/Alt/Lower.lean new file mode 100644 index 0000000000..fbbc982235 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Lower.lean @@ -0,0 +1,526 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.BlockLower +public import LeanPool.RunsOfMultiples.LowerEstimates +public import Mathlib.Algebra.Order.Antidiag.FinsuppEquiv +public import Mathlib.Data.Finset.Finsupp +public import Mathlib.Data.Nat.Factorization.Basic + +/-! +# Runs of multiples: the lower bound via the "matching construction" + +This file formalises §3 ("A matching construction") of `docs/first-missing-multiple.pdf`. + +For `y ≥ 2` let +* `small y` = primes `p ≤ √y` (encoded as `p * p ≤ y`), `q = #small y`; +* `large y` = primes in `(√y, y]` (encoded as `y < p * p`, `p ≤ y`), `m = #large y`; +* `L = ⌊log₂ y⌋ = Nat.log 2 y`, `H = 2 q L`. + +`S_y` is the set of integers `∏_{p ≤ √y} p ^ u_p * ∏_{√y < p ≤ y} p ^ v_p` with +`0 ≤ u_p ≤ H` and `∑ v_p ≤ m`. We represent exponent vectors as finsupps `ℕ →₀ ℕ` and +the number as `f.prod (· ^ ·)`. The small-prime part ranges over `smallExp y H` +(`Finset.finsupp`), the large-prime part over `largeExp y m`: finsupps supported on +`insert 1 (large y)` with total sum exactly `m`, the coordinate at `1` being a slack +variable (`1 ^ v = 1`), so that these give exactly the products with `∑ v_p ≤ m` +(stars and bars with a slack variable; `Finset.card_finsuppAntidiag_nat_eq_choose`). + +The good elements (`u_p ≤ H - L`, `∑ v_p ≤ m - 1`) have all first `y` multiples in `S_y`, +at least a quarter of `S_y` is good, and `|S_y| ≤ (H + 1) ^ q * C(2m, m) ≤ exp (C y / log y)`. +The padding step is the same as in `RunsOfMultiples.Replication` (`replicate`). +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +namespace Alt + +/-- Primes `p` with `p ≤ √y`, i.e. `p * p ≤ y`. -/ +def small (y : ℕ) : Finset ℕ := (y + 1).primesBelow.filter (fun p => p * p ≤ y) + +/-- Primes `p` with `√y < p ≤ y`. -/ +def large (y : ℕ) : Finset ℕ := (y + 1).primesBelow.filter (fun p => y < p * p) + +/-- `q = π(√y)`. -/ +def qq (y : ℕ) : ℕ := (small y).card + +/-- `m = π(y) - π(√y)`. -/ +def mm (y : ℕ) : ℕ := (large y).card + +/-- `L = ⌊log₂ y⌋`. -/ +def LL (y : ℕ) : ℕ := Nat.log 2 y + +/-- `H = 2 q L`. -/ +def HH (y : ℕ) : ℕ := 2 * qq y * LL y + +/-- Index set for the large-prime exponents, with a slack coordinate at `1`. -/ +def slack (y : ℕ) : Finset ℕ := insert 1 (large y) + +/-- The number with exponent vector `f`. -/ +noncomputable def pw (f : ℕ →₀ ℕ) : ℕ := f.prod (· ^ ·) + +/-- Small-prime exponent vectors with all entries `≤ e`. -/ +noncomputable def smallExp (y e : ℕ) : Finset (ℕ →₀ ℕ) := + (small y).finsupp (fun _ => range (e + 1)) + +/-- Large-prime exponent vectors (plus slack at `1`) with total sum `k`. -/ +noncomputable def largeExp (y k : ℕ) : Finset (ℕ →₀ ℕ) := (slack y).finsuppAntidiag k + +/-- Small parts `∏_{p ≤ √y} p ^ u_p`, `u_p ≤ e`. -/ +noncomputable def smallPart (y e : ℕ) : Finset ℕ := (smallExp y e).image pw + +/-- Large parts `∏_{√y < p ≤ y} p ^ v_p`, `∑ v_p ≤ k`. -/ +noncomputable def largePart (y k : ℕ) : Finset ℕ := (largeExp y k).image pw + +/-- The block `S_y`. -/ +noncomputable def Sy (y : ℕ) : Finset ℕ := + (smallPart y (HH y) ×ˢ largePart y (mm y)).image (fun x => x.1 * x.2) + +/-- The good elements of `S_y`: `u_p ≤ H - L`, `∑ v_p ≤ m - 1`. -/ +noncomputable def Gy (y : ℕ) : Finset ℕ := + (smallPart y (HH y - LL y) ×ˢ largePart y (mm y - 1)).image (fun x => x.1 * x.2) + +/-! ### Basic facts -/ + +lemma pw_add (f g : ℕ →₀ ℕ) : pw (f + g) = pw f * pw g := + Finsupp.prod_add_index' (fun a => pow_zero a) (fun a b c => pow_add a b c) + +lemma pw_single (a k : ℕ) : pw (Finsupp.single a k) = a ^ k := + Finsupp.prod_single_index (pow_zero a) + +lemma pw_pos (f : ℕ →₀ ℕ) (hf : ∀ p ∈ f.support, 0 < p) : 0 < pw f := + Finset.prod_pos fun p hp => pow_pos (hf p hp) _ + +lemma mem_small {y p : ℕ} : p ∈ small y ↔ p.Prime ∧ p ≤ y ∧ p * p ≤ y := by + simp only [small, mem_filter, Nat.mem_primesBelow] + constructor + · rintro ⟨⟨h1, h2⟩, h3⟩; exact ⟨h2, by omega, h3⟩ + · rintro ⟨h1, h2, h3⟩; exact ⟨⟨by omega, h1⟩, h3⟩ + +lemma mem_large {y p : ℕ} : p ∈ large y ↔ p.Prime ∧ p ≤ y ∧ y < p * p := by + simp only [large, mem_filter, Nat.mem_primesBelow] + constructor + · rintro ⟨⟨h1, h2⟩, h3⟩; exact ⟨h2, by omega, h3⟩ + · rintro ⟨h1, h2, h3⟩; exact ⟨⟨by omega, h1⟩, h3⟩ + +lemma one_notMem_large (y : ℕ) : 1 ∉ large y := fun h => Nat.not_prime_one (mem_large.1 h).1 + +lemma card_largeExp (y k : ℕ) : (largeExp y k).card = (mm y + k).choose k := by + rw [largeExp, card_finsuppAntidiag_nat_eq_choose, slack, + card_insert_of_notMem (one_notMem_large y)] + rw [show (large y).card + 1 + k - 1 = mm y + k by unfold mm; omega] + +lemma card_smallExp (y e : ℕ) : (smallExp y e).card = (e + 1) ^ qq y := by + rw [smallExp, card_finsupp] + simp [qq] + +lemma pw_injOn_smallExp (y e : ℕ) : Set.InjOn pw (smallExp y e : Set (ℕ →₀ ℕ)) := by + intro f hf g hg h + have hpr : ∀ f ∈ (smallExp y e : Set (ℕ →₀ ℕ)), ∀ p ∈ f.support, p.Prime := by + intro f hf p hp + rw [mem_coe, smallExp, mem_finsupp_iff] at hf + exact (mem_small.1 (hf.1 hp)).1 + rw [← Nat.prod_pow_factorization_eq_self (hpr f hf), + ← Nat.prod_pow_factorization_eq_self (hpr g hg)] + exact congrArg Nat.factorization h + +lemma pw_erase_one (f : ℕ →₀ ℕ) : pw f = pw (f.erase 1) := by + conv_lhs => rw [← Finsupp.single_add_erase 1 f] + rw [pw_add, pw_single, one_pow, one_mul] + +lemma pw_injOn_largeExp (y k : ℕ) : Set.InjOn pw (largeExp y k : Set (ℕ →₀ ℕ)) := by + intro f hf g hg h + rw [mem_coe, largeExp, mem_finsuppAntidiag] at hf hg + have hpr : ∀ f : ℕ →₀ ℕ, f.support ⊆ slack y → ∀ p ∈ (f.erase 1).support, p.Prime := by + intro f hf p hp + rw [Finsupp.support_erase, mem_erase] at hp + have := hf hp.2 + rw [slack, mem_insert] at this + rcases this with h1 | h1 + · exact absurd h1 hp.1 + · exact (mem_large.1 h1).1 + have he : f.erase 1 = g.erase 1 := by + rw [← Nat.prod_pow_factorization_eq_self (hpr f hf.2), + ← Nat.prod_pow_factorization_eq_self (hpr g hg.2)] + have := h + rw [pw_erase_one f, pw_erase_one g] at this + exact congrArg Nat.factorization this + have hsum : ∀ f : ℕ →₀ ℕ, (slack y).sum f = f 1 + ∑ p ∈ large y, (f.erase 1) p := by + intro f + rw [slack, sum_insert (one_notMem_large y)] + congr 1 + refine sum_congr rfl fun p hp => ?_ + rw [Finsupp.erase_ne (fun h : p = 1 => one_notMem_large y (h ▸ hp))] + have h1 : f 1 = g 1 := by + have h2 := hsum f + have h3 := hsum g + rw [hf.1, he] at h2 + rw [hg.1] at h3 + omega + ext p + by_cases hp : p = 1 + · rw [hp, h1] + · rw [← Finsupp.erase_ne hp, he, Finsupp.erase_ne hp] + +/-! ### Unique factorisation: the parts and their product are injective -/ + +lemma prime_dvd_pw {f : ℕ →₀ ℕ} {p : ℕ} (hp : p.Prime) (h : p ∣ pw f) : + ∃ r ∈ f.support, p ∣ r := by + unfold pw Finsupp.prod at h + obtain ⟨r, hr, hpr⟩ := (Prime.dvd_finsetProd_iff hp.prime _).1 h + exact ⟨r, hr, hp.dvd_of_dvd_pow hpr⟩ + +lemma prime_dvd_smallPart {y e a p : ℕ} (ha : a ∈ smallPart y e) (hp : p.Prime) (h : p ∣ a) : + p ∈ small y := by + obtain ⟨f, hf, rfl⟩ := mem_image.1 ha + obtain ⟨r, hr, hpr⟩ := prime_dvd_pw hp h + rw [smallExp, mem_finsupp_iff] at hf + have hrs := hf.1 hr + rwa [(Nat.prime_dvd_prime_iff_eq hp (mem_small.1 hrs).1).1 hpr] + +lemma prime_dvd_largePart {y k a p : ℕ} (ha : a ∈ largePart y k) (hp : p.Prime) (h : p ∣ a) : + p ∈ large y := by + obtain ⟨f, hf, rfl⟩ := mem_image.1 ha + obtain ⟨r, hr, hpr⟩ := prime_dvd_pw hp h + rw [largeExp, mem_finsuppAntidiag] at hf + have hrs := hf.2 hr + rw [slack, mem_insert] at hrs + rcases hrs with rfl | hrs + · exact absurd (Nat.eq_one_of_dvd_one hpr) hp.one_lt.ne' + · rwa [(Nat.prime_dvd_prime_iff_eq hp (mem_large.1 hrs).1).1 hpr] + +lemma coprime_parts {y e k a b : ℕ} (ha : a ∈ smallPart y e) (hb : b ∈ largePart y k) : + Nat.Coprime a b := + Nat.coprime_of_dvd fun p hp hpa hpb => by + have h1 := (mem_small.1 (prime_dvd_smallPart ha hp hpa)).2.2 + have h2 := (mem_large.1 (prime_dvd_largePart hb hp hpb)).2.2 + omega + +lemma smallPart_pos {y e a : ℕ} (ha : a ∈ smallPart y e) : 0 < a := by + obtain ⟨f, hf, rfl⟩ := mem_image.1 ha + refine pw_pos f fun p hp => ?_ + rw [smallExp, mem_finsupp_iff] at hf + exact (mem_small.1 (hf.1 hp)).1.pos + +lemma largePart_pos {y k b : ℕ} (hb : b ∈ largePart y k) : 0 < b := by + obtain ⟨f, hf, rfl⟩ := mem_image.1 hb + refine pw_pos f fun p hp => ?_ + rw [largeExp, mem_finsuppAntidiag] at hf + have := hf.2 hp + rw [slack, mem_insert] at this + rcases this with rfl | h + · exact one_pos + · exact (mem_large.1 h).1.pos + +lemma mul_injOn_parts (y e k : ℕ) : Set.InjOn (fun x : ℕ × ℕ => x.1 * x.2) + (↑(smallPart y e ×ˢ largePart y k) : Set (ℕ × ℕ)) := by + rintro ⟨a, b⟩ hab ⟨a', b'⟩ hab' h + simp only [coe_product, Set.mem_prod, mem_coe] at hab hab' h + have h1 : a ∣ a' := (coprime_parts hab.1 hab'.2).dvd_of_dvd_mul_right ⟨b, h.symm⟩ + have h2 : a' ∣ a := (coprime_parts hab'.1 hab.2).dvd_of_dvd_mul_right ⟨b', h⟩ + have h3 : a = a' := Nat.dvd_antisymm h1 h2 + subst h3 + have h4 : b = b' := Nat.eq_of_mul_eq_mul_left (smallPart_pos hab.1) h + rw [h4] + +lemma card_smallPart (y e : ℕ) : (smallPart y e).card = (e + 1) ^ qq y := by + rw [smallPart, card_image_of_injOn (pw_injOn_smallExp y e), card_smallExp] + +lemma card_largePart (y k : ℕ) : (largePart y k).card = (mm y + k).choose k := by + rw [largePart, card_image_of_injOn (pw_injOn_largeExp y k), card_largeExp] + +/-- `|S_y| = (H + 1) ^ q * C(2m, m)` (equation (9)). -/ +lemma card_Sy (y : ℕ) : (Sy y).card = (HH y + 1) ^ qq y * (mm y + mm y).choose (mm y) := by + rw [Sy, card_image_of_injOn (mul_injOn_parts _ _ _), card_product, card_smallPart, + card_largePart] + +lemma card_Gy (y : ℕ) : + (Gy y).card = (HH y - LL y + 1) ^ qq y * (mm y + (mm y - 1)).choose (mm y - 1) := by + rw [Gy, card_image_of_injOn (mul_injOn_parts _ _ _), card_product, card_smallPart, + card_largePart] + +/-! ### At least a quarter of `S_y` is good -/ + +/-- Bernoulli: `(H + 1) ^ q ≤ 2 (H - L + 1) ^ q` for `H = 2 q L`. -/ +lemma bernoulli_aux (q L : ℕ) : (2 * q * L + 1) ^ q ≤ 2 * (2 * q * L - L + 1) ^ q := by + rcases Nat.eq_zero_or_pos q with rfl | hq + · simp + have hLe : L ≤ 2 * q * L := by nlinarith + set N : ℝ := ((2 * q * L + 1 : ℕ) : ℝ) with hNdef + have hN : 0 < N := by positivity + have hLN : (L : ℝ) ≤ N := by rw [hNdef]; exact_mod_cast (by omega : L ≤ 2 * q * L + 1) + have hx : (-2 : ℝ) ≤ -(L / N) := by + have : (L : ℝ) / N ≤ 1 := (div_le_one hN).2 hLN + linarith + have hb := one_add_mul_le_pow hx q + have hcast : ((2 * q * L - L + 1 : ℕ) : ℝ) = N * (1 + -(L / N)) := by + rw [hNdef, Nat.cast_add, Nat.cast_sub hLe]; push_cast; field_simp; ring + have h2 : (1 : ℝ) / 2 ≤ 1 + q * -(L / N) := by + have h3 : (q : ℝ) * L / N ≤ 1 / 2 := by + rw [div_le_iff₀ hN, hNdef]; push_cast; linarith + have h4 : (q : ℝ) * -(L / N) = -((q : ℝ) * L / N) := by ring + linarith + have key : N ^ q ≤ 2 * (N * (1 + -(L / N))) ^ q := by + rw [mul_pow] + have hNq : 0 < N ^ q := pow_pos hN q + have := mul_le_mul_of_nonneg_left (h2.trans hb) hNq.le + linarith + rw [← hcast, hNdef] at key + exact_mod_cast key + +/-- `C(2m, m) = 2 C(2m - 1, m - 1)` (for `m ≥ 1`; for `m = 0` both sides are `1`). -/ +lemma choose_le_two_mul (m : ℕ) : (m + m).choose m ≤ 2 * (m + (m - 1)).choose (m - 1) := by + rcases m with _ | m + · simp + · rw [Nat.add_sub_cancel, show m + 1 + (m + 1) = 2 * m + 1 + 1 by ring, + show m + 1 + m = 2 * m + 1 by ring, Nat.choose_succ_succ, Nat.choose_symm_half] + omega + +/-- At least a quarter of `S_y` is good. -/ +lemma card_Sy_le (y : ℕ) : (Sy y).card ≤ 4 * (Gy y).card := by + rw [card_Sy, card_Gy] + have h1 := bernoulli_aux (qq y) (LL y) + have h2 := choose_le_two_mul (mm y) + rw [show HH y = 2 * qq y * LL y from rfl] + calc (2 * qq y * LL y + 1) ^ qq y * (mm y + mm y).choose (mm y) + ≤ (2 * (2 * qq y * LL y - LL y + 1) ^ qq y) * + (2 * (mm y + (mm y - 1)).choose (mm y - 1)) := Nat.mul_le_mul h1 h2 + _ = _ := by ring + +/-! ### Good elements have their first `y` multiples in `S_y` -/ + +/-- If `1 ≤ j ≤ y` has no prime factor `> √y`, its exponent vector lies in `smallExp y L`: +each small-prime exponent of `j` is at most `L = ⌊log₂ y⌋`. -/ +lemma factorization_mem_smallExp {y j : ℕ} (hj1 : 1 ≤ j) (hjy : j ≤ y) + (h : ∀ p, p.Prime → p ∣ j → p * p ≤ y) : j.factorization ∈ smallExp y (LL y) := by + rw [smallExp, mem_finsupp_iff] + have hj0 : j ≠ 0 := by omega + refine ⟨fun p hp => ?_, fun p hp => ?_⟩ + · rw [Nat.support_factorization, Nat.mem_primeFactors] at hp + exact mem_small.2 ⟨hp.1, (Nat.le_of_dvd (by omega) hp.2.1).trans hjy, h p hp.1 hp.2.1⟩ + · rw [mem_range, Nat.lt_succ_iff] + have hp2 : 1 < p := (mem_small.1 hp).1.one_lt + have h1 : p ^ j.factorization p ≤ j := Nat.ordProj_le p hj0 + have h2 : y < 2 ^ (LL y).succ := Nat.lt_pow_succ_log_self (by norm_num) y + have h3 : 2 ^ (LL y).succ ≤ p ^ (LL y).succ := + Nat.pow_le_pow_left (mem_small.1 hp).1.two_le _ + have h4 : p ^ j.factorization p < p ^ (LL y).succ := by omega + have := (Nat.pow_lt_pow_iff_right (by omega)).1 h4 + omega + +/-- Every `1 ≤ j ≤ y` is `js * jl` with `js` having small-prime exponents `≤ L` and +`jl ∈ {1} ∪ (√y, y]` (at most one prime factor `> √y`, counted with multiplicity). -/ +lemma decomp {y j : ℕ} (hj1 : 1 ≤ j) (hjy : j ≤ y) : + ∃ js jl, j = js * jl ∧ js.factorization ∈ smallExp y (LL y) ∧ 1 ≤ js ∧ jl ∈ slack y := by + by_cases h : ∃ p, p.Prime ∧ p ∣ j ∧ y < p * p + · obtain ⟨p, hp, ⟨j', rfl⟩, hpy⟩ := h + have hj' : 1 ≤ j' := by + rcases Nat.eq_zero_or_pos j' with h0 | h0 + · rw [h0, mul_zero] at hj1; omega + · exact h0 + have hpj' : p ≤ p * j' := Nat.le_mul_of_pos_right p hj' + have hj'y : j' ≤ y := (Nat.le_mul_of_pos_left j' hp.pos).trans hjy + refine ⟨j', p, by ring, factorization_mem_smallExp hj' hj'y ?_, hj', ?_⟩ + · intro r hr hrj + by_contra hry + push Not at hry + have h5 : p * r ≤ y := + (Nat.le_of_dvd (by omega) (Nat.mul_dvd_mul_left p hrj)).trans hjy + have h6 : y * y < p * p * (r * r) := Nat.mul_lt_mul'' hpy hry + have h7 : p * r * (p * r) ≤ y * y := Nat.mul_le_mul h5 h5 + have h8 : p * p * (r * r) = p * r * (p * r) := by ring + omega + · rw [slack, mem_insert]; exact Or.inr (mem_large.2 ⟨hp, hpj'.trans hjy, hpy⟩) + · push Not at h + exact ⟨j, 1, by ring, factorization_mem_smallExp hj1 hjy fun p hp hpj => h p hp hpj, hj1, + mem_insert_self _ _⟩ + +lemma add_mem_smallExp {y : ℕ} {g e : ℕ →₀ ℕ} (hg : g ∈ smallExp y (LL y)) + (he : e ∈ smallExp y (HH y - LL y)) : g + e ∈ smallExp y (HH y) := by + rw [smallExp, mem_finsupp_iff] at hg he ⊢ + refine ⟨Finsupp.support_add.trans (union_subset hg.1 he.1), fun i hi => ?_⟩ + have h1 := hg.2 i hi + have h2 := he.2 i hi + rw [mem_range] at h1 h2 ⊢ + have hq : 0 < qq y := card_pos.2 ⟨i, hi⟩ + have hLH : LL y ≤ HH y := Nat.le_mul_of_pos_left (LL y) (by omega) + rw [Finsupp.add_apply] + omega + +lemma add_single_mem_largeExp {y k x c : ℕ} {f : ℕ →₀ ℕ} (hf : f ∈ largeExp y k) + (hx : x ∈ slack y) : f + Finsupp.single x c ∈ largeExp y (k + c) := by + rw [largeExp, mem_finsuppAntidiag] at hf ⊢ + refine ⟨?_, Finsupp.support_add.trans + (union_subset hf.2 (Finsupp.support_single_subset.trans (singleton_subset_iff.2 hx)))⟩ + change ∑ i ∈ slack y, (f + Finsupp.single x c) i = k + c + simp only [Finsupp.add_apply, sum_add_distrib, Finsupp.single_apply, sum_ite_eq, hx, ↓reduceIte] + rw [← hf.1] + +/-- Sanity check of the slack encoding: `largePart y k` is exactly the set of +`∏_{√y < p ≤ y} p ^ v_p` with `∑ v_p ≤ k`, as in (8). -/ +lemma mem_largePart_iff {y k b : ℕ} : b ∈ largePart y k ↔ + ∃ v : ℕ →₀ ℕ, v.support ⊆ large y ∧ ∑ p ∈ large y, v p ≤ k ∧ pw v = b := by + constructor + · rintro hb + obtain ⟨f, hf, rfl⟩ := mem_image.1 hb + rw [largeExp, mem_finsuppAntidiag] at hf + refine ⟨f.erase 1, fun p hp => ?_, ?_, (pw_erase_one f).symm⟩ + · rw [Finsupp.support_erase, mem_erase] at hp + have := hf.2 hp.2 + rw [slack, mem_insert] at this + exact this.resolve_left hp.1 + · have h1 : (slack y).sum f = f 1 + ∑ p ∈ large y, (f.erase 1) p := by + rw [slack, sum_insert (one_notMem_large y)] + congr 1 + refine sum_congr rfl fun p hp => ?_ + rw [Finsupp.erase_ne (fun h : p = 1 => one_notMem_large y (h ▸ hp))] + omega + · rintro ⟨v, hv, hsum, rfl⟩ + have hv1 : v 1 = 0 := Finsupp.notMem_support_iff.1 fun h => one_notMem_large y (hv h) + have hvL : v ∈ largeExp y (∑ p ∈ large y, v p) := by + rw [largeExp, mem_finsuppAntidiag, slack, sum_insert (one_notMem_large y), hv1, zero_add] + exact ⟨rfl, hv.trans (subset_insert _ _)⟩ + have h := add_single_mem_largeExp (c := k - ∑ p ∈ large y, v p) hvL (mem_insert_self 1 _) + rw [show ∑ p ∈ large y, v p + (k - ∑ p ∈ large y, v p) = k by omega] at h + refine mem_image.2 ⟨_, h, ?_⟩ + rw [pw_add, pw_single, one_pow, mul_one] + +/-- If `a` is good and `1 ≤ j ≤ y`, then `j a ∈ S_y`. -/ +lemma mul_mem_Sy {y a j : ℕ} (ha : a ∈ Gy y) (hj1 : 1 ≤ j) (hjy : j ≤ y) : j * a ∈ Sy y := by + obtain ⟨⟨α, β⟩, hab, rfl⟩ := mem_image.1 ha + rw [mem_product] at hab + obtain ⟨e, he, rfl⟩ := mem_image.1 hab.1 + obtain ⟨f, hf, rfl⟩ := mem_image.1 hab.2 + obtain ⟨js, jl, rfl, hjs, hjs1, hjl⟩ := decomp hj1 hjy + have hjs' : pw js.factorization = js := Nat.prod_factorization_pow_eq_self (by omega) + have hsm := add_mem_smallExp hjs he + have hjl' := hjl + rw [slack, mem_insert] at hjl' + rcases hjl' with rfl | hjl' + · have hl := add_single_mem_largeExp (c := mm y - (mm y - 1)) hf hjl + rw [show mm y - 1 + (mm y - (mm y - 1)) = mm y by omega] at hl + refine mem_image.2 ⟨(pw (js.factorization + e), pw (f + Finsupp.single 1 (mm y - (mm y - 1)))), + mem_product.2 ⟨mem_image_of_mem _ hsm, mem_image_of_mem _ hl⟩, ?_⟩ + simp only [pw_add, pw_single, one_pow, hjs'] + ring + · have hm : 0 < mm y := card_pos.2 ⟨jl, hjl'⟩ + have hl := add_single_mem_largeExp (c := 1) hf hjl + rw [show mm y - 1 + 1 = mm y by omega] at hl + refine mem_image.2 ⟨(pw (js.factorization + e), pw (f + Finsupp.single jl 1)), + mem_product.2 ⟨mem_image_of_mem _ hsm, mem_image_of_mem _ hl⟩, ?_⟩ + simp only [pw_add, pw_single, pow_one, hjs'] + ring + +lemma Gy_subset_Sy {y : ℕ} (hy : 1 ≤ y) : Gy y ⊆ Sy y := fun a ha => by + simpa using mul_mem_Sy ha le_rfl hy + +lemma pos_of_mem_Sy {y a : ℕ} (ha : a ∈ Sy y) : 0 < a := by + obtain ⟨⟨α, β⟩, hab, rfl⟩ := mem_image.1 ha + rw [mem_product] at hab + exact Nat.mul_pos (smallPart_pos hab.1) (largePart_pos hab.2) + +lemma card_Sy_pos (y : ℕ) : 0 < (Sy y).card := by + rw [card_Sy] + exact Nat.mul_pos (pow_pos (by omega) _) (Nat.choose_pos (by omega)) + +/-! ### Size of `S_y`: `log |S_y| = O(y / log y)` (upper half of (12)) -/ + +lemma qq_le_sqrt (y : ℕ) : qq y ≤ Nat.sqrt y := by + calc qq y ≤ (Icc 1 (Nat.sqrt y)).card := by + refine card_le_card fun p hp => ?_ + have hp' := mem_small.1 hp + exact mem_Icc.2 ⟨hp'.1.one_lt.le, Nat.le_sqrt.2 hp'.2.2⟩ + _ = Nat.sqrt y := by simp + +lemma mm_le (y : ℕ) : mm y ≤ (y + 1).primesBelow.card := card_le_card (filter_subset _ _) + +lemma HH_add_one_le {y : ℕ} (hy : 2 ≤ y) : HH y + 1 ≤ y ^ 4 := by + have hq : qq y ≤ y := (qq_le_sqrt y).trans (Nat.sqrt_le_self y) + have hL : LL y ≤ y := Nat.log_le_self 2 y + have h1 : HH y ≤ 2 * (y * y) := by + unfold HH + calc 2 * qq y * LL y ≤ 2 * y * y := Nat.mul_le_mul (Nat.mul_le_mul_left 2 hq) hL + _ = 2 * (y * y) := by ring + have h2 : 2 * 2 ≤ y * y := Nat.mul_le_mul hy hy + have h3 : 2 * 2 * (y * y) ≤ y * y * (y * y) := Nat.mul_le_mul_right _ h2 + have h4 : y ^ 4 = y * y * (y * y) := by ring + omega + +/-- The constant in `|S_y| ≤ exp (C₃ y / log y)`. -/ +noncomputable def C₃ : ℝ := 64 + log 4 * (2 * log 4 + 2) + +lemma C₃_pos : 0 < C₃ := by + have : 0 < log (4 : ℝ) := log_pos (by norm_num) + unfold C₃; positivity + +/-- `|S_y| ≤ (H + 1) ^ q * 4 ^ m ≤ exp (C₃ y / log y)`, using `q ≤ √y`, `H + 1 ≤ y ^ 4` +and Chebyshev's bound for `m ≤ π(y)`. -/ +lemma card_Sy_le_exp {y : ℕ} (hy : 2 ≤ y) : ((Sy y).card : ℝ) ≤ exp (C₃ * (y / log y)) := by + have hy1 : (1 : ℝ) < y := by exact_mod_cast (show 1 < y by omega) + have hy0 : (0 : ℝ) < y := by linarith + have hly : 0 < log (y : ℝ) := log_pos hy1 + have hl4 : 0 < log (4 : ℝ) := log_pos (by norm_num) + have hN : (Sy y).card ≤ (y ^ 4) ^ qq y * 4 ^ mm y := by + rw [card_Sy] + refine Nat.mul_le_mul (Nat.pow_le_pow_left (HH_add_one_le hy) _) ?_ + calc (mm y + mm y).choose (mm y) ≤ 2 ^ (mm y + mm y) := Nat.choose_le_two_pow _ _ + _ = 4 ^ mm y := by rw [← two_mul, pow_mul]; norm_num + have hR : ((Sy y).card : ℝ) ≤ ((y : ℝ) ^ 4) ^ qq y * 4 ^ mm y := by exact_mod_cast hN + have e1 : ((y : ℝ) ^ 4) ^ qq y = exp (((4 * qq y : ℕ) : ℝ) * log y) := by + rw [exp_nat_mul, exp_log hy0, ← pow_mul] + have e2 : (4 : ℝ) ^ mm y = exp ((mm y : ℝ) * log 4) := by + rw [exp_nat_mul, exp_log (by norm_num)] + rw [e1, e2, ← exp_add] at hR + refine hR.trans (exp_le_exp.2 ?_) + have hq : (qq y : ℝ) ≤ √(y : ℝ) := + (Nat.cast_le.2 (qq_le_sqrt y)).trans Real.nat_sqrt_le_real_sqrt + have hm : (mm y : ℝ) ≤ (2 * log 4 + 2) * (y / log y) := + (Nat.cast_le.2 (mm_le y)).trans (card_primesBelow_le y hy) + have hs := sqrt_mul_log_le hy1 + have h1 : ((4 * qq y : ℕ) : ℝ) * log y ≤ 64 * (y / log y) := by + push_cast + have := mul_le_mul_of_nonneg_right hq hly.le + linarith + have h2 : (mm y : ℝ) * log 4 ≤ log 4 * (2 * log 4 + 2) * (y / log y) := by + have := mul_le_mul_of_nonneg_right hm hl4.le + linarith + unfold C₃ + linarith + +/-- The block of §3: `B = S_y`, `G` = good elements, `|G| ≥ |B| / 4`, +`|B| ≤ exp (C₃ y / log y)`. Same shape as `RunsOfMultiples.block`. -/ +theorem block_alt : ∃ δ : ℝ, 0 < δ ∧ ∃ C₂ : ℝ, 0 < C₂ ∧ ∀ y : ℕ, 2 ≤ y → ∃ B G : Finset ℕ, + (∀ a ∈ B, 0 < a) ∧ G ⊆ B ∧ (∀ a ∈ G, ∀ j, 1 ≤ j → j ≤ y → j * a ∈ B) ∧ 0 < B.card ∧ + δ * B.card ≤ G.card ∧ (B.card : ℝ) ≤ exp (C₂ * (y / log y)) := by + refine ⟨1 / 4, by norm_num, C₃, C₃_pos, fun y hy => ⟨Sy y, Gy y, fun a ha => pos_of_mem_Sy ha, + Gy_subset_Sy (by omega), fun a ha j hj1 hjy => mul_mem_Sy ha hj1 hjy, card_Sy_pos y, ?_, + card_Sy_le_exp hy⟩⟩ + have : ((Sy y).card : ℝ) ≤ 4 * (Gy y).card := by exact_mod_cast card_Sy_le y + linarith + +end Alt + +/-! ### Padding to every `n` (end of §3) + +`y = ⌊ε log n log log n⌋` with `ε = 1 / (2 C₂)`, so `|S_y| ≤ exp (L / 2) ≤ n / 2`; take +`⌊n / |S_y|⌋` disjoint dilates `M ^ i • S_y` and pad (`replicate` from +`RunsOfMultiples.Replication`). The argument below is the one of `lower_bound`, applied to the +block `block_alt` of §3. -/ + +/-- **Lower bound (alternative construction, §3).** -/ +theorem lower_bound_alt : ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ S : Finset ℕ, + (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ + c * n * Real.log n * Real.log (Real.log n) ≤ ((∑ a ∈ S, kVal S a : ℕ) : ℝ) := by + obtain ⟨δ, hδ, C₂, hC₂, hblock⟩ := Alt.block_alt + exact lower_bound_of_block hδ hC₂ hblock + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Alt/Main.lean b/LeanPool/RunsOfMultiples/Alt/Main.lean new file mode 100644 index 0000000000..4abcf1eddb --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Main.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Alt.Upper +public import LeanPool.RunsOfMultiples.Alt.Lower + +/-! +# Main theorem, compression proof + +Same statement as `main_theorem`, proved along the route of `docs/first-missing-multiple.pdf` +(lemma and equation numbers in `Alt/` refer to that document): +* upper bound: `exists_closed` (Lemma 2, chain compressions) + `sum_L_le_of_closed` + (Lemma 3, radical bound and double counting) in `upper_bound_alt`; +* lower bound: the box × simplex construction in `lower_bound_alt`. +-/ + +@[expose] public section + +namespace RunsOfMultiples + +theorem main_theorem_alt : + (∃ C : ℝ, ∃ N : ℕ, ∀ S : Finset ℕ, (∀ a ∈ S, 0 < a) → N ≤ S.card → + ((∑ a ∈ S, kVal S a : ℕ) : ℝ) ≤ + C * S.card * Real.log S.card * Real.log (Real.log S.card)) ∧ + (∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ S : Finset ℕ, (∀ a ∈ S, 0 < a) ∧ + S.card = n ∧ c * n * Real.log n * Real.log (Real.log n) ≤ ((∑ a ∈ S, kVal S a : ℕ) : ℝ)) := + ⟨upper_bound_alt, lower_bound_alt⟩ + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Alt/Radical.lean b/LeanPool/RunsOfMultiples/Alt/Radical.lean new file mode 100644 index 0000000000..e1afd4be8d --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Radical.lean @@ -0,0 +1,336 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Alt.Defs +public import LeanPool.RunsOfMultiples.PrimeEstimates +public import Mathlib.Data.Nat.Squarefree + +/-! +# Radical bound and double counting (Lemma 3 and equation (7)) + +For a finite set `T` of positive integers that is closed under divisors (`DivClosed`) and under +replacing a prime factor by a smaller prime (`ShiftClosed`), we show + + `∑_{a ∈ T} L T a = O(n log n log log n)`, `n = |T|`. + +* Lemma 3: for `b ∈ T` with `m` distinct prime factors, `2 ^ m ≤ n`, and every product + `∏_{p ∣ b} g p` with `g p ≤ p` prime lies in `T`. Each such product has at most `m ^ m` + preimages `g`, so `∏_{p ∣ b} π(p) ≤ n m ^ m`. With `log p ≤ 2 log π(p) + C` this gives + `∑_{p ∣ b} log p = O(log n log log n)`. (`docs/first-missing-multiple.pdf` uses `m!` preimages; + `m ^ m` suffices.) +* Equation (7): `∑_{a ∈ T} θ(L T a) ≤ ∑_{b ∈ T} ∑_{p ∣ b} log p`, via `(a, p) ↦ (p a, p)`. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +/-- Replacing the prime factors `p ∈ s` of `c * ∏ s` by smaller primes `g p` stays inside a +shift-closed set. -/ +lemma box_mem {T : Finset ℕ} (hshift : ShiftClosed T) (g : ℕ → ℕ) (s : Finset ℕ) + (hs : ∀ p ∈ s, p.Prime ∧ (g p).Prime ∧ g p ≤ p) : + ∀ c, c * ∏ p ∈ s, p ∈ T → c * ∏ p ∈ s, g p ∈ T := by + induction s using Finset.induction_on with + | empty => intro c hc; simpa using hc + | insert q s hq ih => + intro c hc + have hs' : ∀ p ∈ s, p.Prime ∧ (g p).Prime ∧ g p ≤ p := fun p hp => hs p (mem_insert_of_mem hp) + obtain ⟨hqp, hgq, hgqle⟩ := hs q (mem_insert_self q s) + rw [prod_insert hq] at hc ⊢ + have h1 : (c * q) * ∏ p ∈ s, g p ∈ T := ih hs' (c * q) (by rw [mul_assoc]; exact hc) + rcases hgqle.lt_or_eq with hlt | heq + · have h2 := hshift _ h1 (g q) q hgq hqp hlt ⟨c * ∏ p ∈ s, g p, by ring⟩ + have h3 : (c * q * ∏ p ∈ s, g p) / q = c * ∏ p ∈ s, g p := + Nat.div_eq_of_eq_mul_left hqp.pos (by ring) + rw [h3] at h2 + convert h2 using 1 + ring + · rw [heq] + convert h1 using 1 + ring + +/-- Products of prime factors of `b ∈ T` lie in a divisor-closed `T`. -/ +lemma prod_primeFactors_mem {T : Finset ℕ} (hdiv : DivClosed T) {b : ℕ} (hb : b ∈ T) + {s : Finset ℕ} (hs : s ⊆ b.primeFactors) : ∏ p ∈ s, p ∈ T := + hdiv b hb _ ((prod_dvd_prod_of_subset s b.primeFactors id hs).trans (Nat.prod_primeFactors_dvd b)) + +/-- (5): the squarefree divisors of `b` are distinct elements of `T`, so `2 ^ m ≤ |T|`. -/ +lemma two_pow_card_primeFactors_le {T : Finset ℕ} (hdiv : DivClosed T) {b : ℕ} (hb : b ∈ T) : + 2 ^ b.primeFactors.card ≤ T.card := by + rw [← card_powerset] + refine card_le_card_of_injOn (fun s => ∏ p ∈ s, p) + (fun s hs => prod_primeFactors_mem hdiv hb (mem_powerset.1 hs)) ?_ + intro s hs t ht hst + have hs' : ∀ p ∈ s, p.Prime := fun p hp => + Nat.prime_of_mem_primeFactors (mem_powerset.1 (mem_coe.1 hs) hp) + have ht' : ∀ p ∈ t, p.Prime := fun p hp => + Nat.prime_of_mem_primeFactors (mem_powerset.1 (mem_coe.1 ht) hp) + rw [← Nat.primeFactors_prod hs', ← Nat.primeFactors_prod ht'] + exact congrArg _ hst + +/-- (6), with `m ^ m` in place of `m!`: the box of index tuples has at most `|T| m ^ m` +elements. -/ +lemma prod_card_primesUpTo_le {T : Finset ℕ} (hdiv : DivClosed T) (hshift : ShiftClosed T) + {b : ℕ} (hb : b ∈ T) : + ∏ p ∈ b.primeFactors, (primesUpTo p).card ≤ + T.card * b.primeFactors.card ^ b.primeFactors.card := by + classical + set P := b.primeFactors with hP + let G : Finset (P → ℕ) := Fintype.piFinset (fun p : P => primesUpTo p.1) + let Φ : (P → ℕ) → ℕ := fun g => ∏ p : P, g p + have hG : G.card = ∏ p ∈ P, (primesUpTo p).card := by + simp only [G, Fintype.card_piFinset] + exact prod_coe_sort P (fun p => (primesUpTo p).card) + have hmem : ∀ g ∈ G, ∀ p : P, (g p).Prime ∧ g p ≤ p := by + intro g hg p + have := Fintype.mem_piFinset.1 hg p + simp only [primesUpTo, mem_filter, mem_range] at this + exact ⟨this.2, by omega⟩ + have hmaps : ∀ g ∈ G, Φ g ∈ T := by + intro g hg + let g' : ℕ → ℕ := fun x => if h : x ∈ P then g ⟨x, h⟩ else x + have hΦ : Φ g = 1 * ∏ p ∈ P, g' p := by + rw [one_mul, ← prod_coe_sort P g'] + refine prod_congr rfl fun p _ => ?_ + simp [g', p.2] + rw [hΦ] + refine box_mem hshift g' P (fun p hp => ?_) 1 + (by rw [one_mul]; exact prod_primeFactors_mem hdiv hb subset_rfl) + have := hmem g hg ⟨p, hp⟩ + simp only [g', hp, ↓reduceDIte] + exact ⟨Nat.prime_of_mem_primeFactors hp, this⟩ + have hfib : ∀ x ∈ T, (G.filter (fun g => Φ g = x)).card ≤ P.card ^ P.card := by + intro x _ + rcases (G.filter (fun g => Φ g = x)).eq_empty_or_nonempty with he | ⟨g₀, hg₀⟩ + · rw [he, card_empty]; exact Nat.zero_le _ + rw [mem_filter] at hg₀ + have hsub : G.filter (fun g => Φ g = x) ⊆ Fintype.piFinset (fun _ : P => x.primeFactors) := by + intro g hg + rw [mem_filter] at hg + rw [Fintype.mem_piFinset] + intro p + have hp := (hmem g hg.1 p).1 + rw [Nat.mem_primeFactors] + refine ⟨hp, ?_, ?_⟩ + · rw [← hg.2]; exact dvd_prod_of_mem _ (mem_univ p) + · rw [← hg.2]; exact (prod_pos fun q _ => (hmem g hg.1 q).1.pos).ne' + have hx : x.primeFactors.card ≤ P.card := by + have : x.primeFactors ⊆ univ.image g₀ := by + intro q hq + rw [Nat.mem_primeFactors] at hq + rw [← hg₀.2] at hq + obtain ⟨p, _, hqp⟩ := (Nat.Prime.prime hq.1).dvd_finsetProd_iff _ |>.1 hq.2.1 + rw [mem_image] + exact ⟨p, mem_univ p, ((Nat.prime_dvd_prime_iff_eq hq.1 (hmem g₀ hg₀.1 p).1).1 hqp).symm⟩ + refine (card_le_card this).trans (card_image_le.trans ?_) + simp + refine (card_le_card hsub).trans ?_ + rw [Fintype.card_piFinset, prod_const, card_univ, Fintype.card_coe] + exact Nat.pow_le_pow_left hx _ + have := card_le_mul_card_image_of_maps_to hmaps (P.card ^ P.card) hfib + rw [← hG, mul_comm] + exact this + +/-- `log p ≤ 2 log π(p) + C` for all primes `p`, from `π(4q) - π(q) ≥ q^(3/4)` for large `q` +(this is `π(x) ≥ √x` for large `x`, up to constants). -/ +lemma log_le_two_log_card_primesUpTo : ∃ C : ℝ, 0 ≤ C ∧ ∀ p : ℕ, p.Prime → + log (p : ℝ) ≤ 2 * log ((primesUpTo p).card : ℝ) + C := by + obtain ⟨q₀, hq₀⟩ := many_primes + set P₀ : ℕ := 8 * (q₀ + 1) with hP₀ + have hP₀1 : (1 : ℝ) ≤ P₀ := by norm_cast; omega + have hl8 : 0 ≤ log (8 : ℝ) := log_nonneg (by norm_num) + refine ⟨log P₀ + log 8, add_nonneg (log_nonneg hP₀1) hl8, fun p hp => ?_⟩ + have hcard1 : 1 ≤ (primesUpTo p).card := + card_pos.2 ⟨p, by simp [primesUpTo, hp]⟩ + have hlogc : 0 ≤ log ((primesUpTo p).card : ℝ) := log_nonneg (by exact_mod_cast hcard1) + by_cases hpP : p < P₀ + · have : log (p : ℝ) ≤ log P₀ := + log_le_log (by exact_mod_cast hp.pos) (by exact_mod_cast hpP.le) + linarith + push Not at hpP + set q := p / 4 with hq + have hqq₀ : q₀ ≤ q := by omega + have hq0 : 0 < q := by omega + have h8q : p ≤ 8 * q := by omega + have hsub : (Ioc q (4 * q)).filter Nat.Prime ⊆ primesUpTo p := by + intro x hx + simp only [mem_filter, mem_Ioc, primesUpTo, mem_range] at hx ⊢ + exact ⟨by omega, hx.2⟩ + have h1 : (q : ℝ) ^ ((3 : ℝ) / 4) ≤ (primesUpTo p).card := + (hq₀ q hqq₀).trans (by exact_mod_cast card_le_card hsub) + have hqpos : (0 : ℝ) < q := by exact_mod_cast hq0 + have h2 : (3 / 4 : ℝ) * log q ≤ log (primesUpTo p).card := by + rw [← log_rpow hqpos] + exact log_le_log (rpow_pos_of_pos hqpos _) h1 + have h3 : log (p : ℝ) ≤ log 8 + log q := by + rw [← log_mul (by norm_num) hqpos.ne'] + exact log_le_log (by exact_mod_cast hp.pos) (by exact_mod_cast h8q) + have := log_nonneg hP₀1 + have hlq : 0 ≤ log (q : ℝ) := log_nonneg (by exact_mod_cast hq0) + linarith + +/-- Lemma 3, explicit form: `∑_{p ∣ b} log p ≤ 2 log n + 2 m log m + C m`. -/ +lemma sum_log_primeFactors_le {C : ℝ} + (hC : ∀ p : ℕ, p.Prime → log (p : ℝ) ≤ 2 * log ((primesUpTo p).card : ℝ) + C) + {T : Finset ℕ} (hdiv : DivClosed T) (hshift : ShiftClosed T) {b : ℕ} (hb : b ∈ T) : + ∑ p ∈ b.primeFactors, log (p : ℝ) ≤ 2 * log (T.card : ℝ) + + 2 * ((b.primeFactors.card : ℝ) * log (b.primeFactors.card : ℝ)) + + C * b.primeFactors.card := by + set P := b.primeFactors with hP + set m := P.card with hm + have hn : (0 : ℝ) < T.card := by exact_mod_cast card_pos.2 ⟨b, hb⟩ + have h1 : ∑ p ∈ P, log (p : ℝ) ≤ ∑ p ∈ P, (2 * log ((primesUpTo p).card : ℝ) + C) := + sum_le_sum fun p hp => hC p (Nat.prime_of_mem_primeFactors hp) + rw [sum_add_distrib, ← mul_sum, sum_const, nsmul_eq_mul] at h1 + have hpos : ∀ p ∈ P, ((primesUpTo p).card : ℝ) ≠ 0 := fun p hp => by + have : 0 < (primesUpTo p).card := + card_pos.2 ⟨p, by simp [primesUpTo, Nat.prime_of_mem_primeFactors hp]⟩ + positivity + have h2 : ∑ p ∈ P, log ((primesUpTo p).card : ℝ) ≤ log (T.card : ℝ) + m * log m := by + rw [← log_prod hpos] + have hcast : (∏ p ∈ P, ((primesUpTo p).card : ℝ)) ≤ (T.card : ℝ) * (m : ℝ) ^ m := by + exact_mod_cast prod_card_primesUpTo_le hdiv hshift hb + have hprod : 0 < ∏ p ∈ P, ((primesUpTo p).card : ℝ) := + prod_pos fun p hp => lt_of_le_of_ne (Nat.cast_nonneg _) (hpos p hp).symm + rcases Nat.eq_zero_or_pos m with hm0 | hm0 + · rw [hm0] at hcast ⊢ + simp only [pow_zero, mul_one, CharP.cast_eq_zero, zero_mul, add_zero] at hcast ⊢ + exact log_le_log hprod hcast + · have hmr : (0 : ℝ) < m := by exact_mod_cast hm0 + refine (log_le_log hprod hcast).trans_eq ?_ + rw [log_mul hn.ne' (by positivity), log_pow] + linarith + +/-- **Lemma 3.** `∑_{p ∣ b} log p = O(log n log log n)` for `b ∈ T`, once `log log n ≥ 1`. -/ +theorem radical_bound : ∃ K : ℝ, 0 ≤ K ∧ ∀ T : Finset ℕ, DivClosed T → ShiftClosed T → + 1 ≤ log (log (T.card : ℝ)) → ∀ b ∈ T, + ∑ p ∈ b.primeFactors, log (p : ℝ) ≤ K * log (T.card : ℝ) * log (log (T.card : ℝ)) := by + obtain ⟨C, hC0, hC⟩ := log_le_two_log_card_primesUpTo + have hl2 : 0 < log (2 : ℝ) := log_pos one_lt_two + set c₂ : ℝ := (log 2)⁻¹ with hc₂ + have hc₂0 : 0 ≤ c₂ := by positivity + refine ⟨2 + 2 * (c₂ * (c₂ + 1)) + C * c₂, by positivity, fun T hdiv hshift hℓℓ b hb => ?_⟩ + set m := b.primeFactors.card with hm + have hn1 : (1 : ℝ) ≤ T.card := by exact_mod_cast card_pos.2 ⟨b, hb⟩ + set ℓ := log (T.card : ℝ) with hℓdef + have hℓ0 : 0 ≤ ℓ := log_nonneg hn1 + have hℓ1 : 1 ≤ ℓ := by + by_contra h + push Not at h + linarith [log_nonpos hℓ0 h.le] + set ℓℓ := log ℓ with hℓℓdef + -- m ≤ c₂ ℓ + have hmℓ : (m : ℝ) ≤ c₂ * ℓ := by + have h2m : ((2 ^ m : ℕ) : ℝ) ≤ T.card := by exact_mod_cast two_pow_card_primeFactors_le hdiv hb + have : (m : ℝ) * log 2 ≤ ℓ := by + rw [← log_pow] + push_cast at h2m + exact log_le_log (by positivity) h2m + rw [hc₂, inv_mul_eq_div, le_div_iff₀ hl2] + exact this + -- m log m ≤ c₂ (c₂ + 1) ℓ ℓℓ + have hmlog : (m : ℝ) * log m ≤ c₂ * (c₂ + 1) * (ℓ * ℓℓ) := by + have hrhs : 0 ≤ c₂ * (c₂ + 1) * (ℓ * ℓℓ) := by + have : 0 ≤ ℓℓ := by linarith + positivity + rcases Nat.eq_zero_or_pos m with hm0 | hm0 + · rw [hm0]; simpa using hrhs + have hmr : (1 : ℝ) ≤ m := by exact_mod_cast hm0 + have hlogm : log (m : ℝ) ≤ (c₂ + 1) * ℓℓ := by + have h1 : log (m : ℝ) ≤ log (c₂ * ℓ) := log_le_log (by linarith) hmℓ + have hc₂pos : 0 < c₂ := by positivity + rw [log_mul hc₂pos.ne' (by linarith)] at h1 + have h2 : log c₂ ≤ c₂ := by linarith [log_le_sub_one_of_pos hc₂pos] + have h3 : c₂ ≤ c₂ * ℓℓ := le_mul_of_one_le_right hc₂0 hℓℓ + linarith + have hlogm0 : 0 ≤ log (m : ℝ) := log_nonneg hmr + calc (m : ℝ) * log m ≤ (c₂ * ℓ) * ((c₂ + 1) * ℓℓ) := + mul_le_mul hmℓ hlogm hlogm0 (by positivity) + _ = c₂ * (c₂ + 1) * (ℓ * ℓℓ) := by ring + have hmain := sum_log_primeFactors_le hC hdiv hshift hb + rw [← hm, ← hℓdef] at hmain + have hℓℓ' : ℓ ≤ ℓ * ℓℓ := le_mul_of_one_le_right hℓ0 hℓℓ + have hCm : C * m ≤ C * c₂ * (ℓ * ℓℓ) := by + have : C * m ≤ C * (c₂ * ℓ) := mul_le_mul_of_nonneg_left hmℓ hC0 + have h' : C * (c₂ * ℓ) ≤ C * (c₂ * (ℓ * ℓℓ)) := + mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left hℓℓ' hc₂0) hC0 + linarith + calc ∑ p ∈ b.primeFactors, log (p : ℝ) ≤ 2 * ℓ + 2 * (m * log m) + C * m := hmain + _ ≤ 2 * (ℓ * ℓℓ) + 2 * (c₂ * (c₂ + 1) * (ℓ * ℓℓ)) + C * c₂ * (ℓ * ℓℓ) := by linarith + _ = (2 + 2 * (c₂ * (c₂ + 1)) + C * c₂) * ℓ * ℓℓ := by ring + +/-- **Double counting (7).** `∑_{a ∈ T} θ(L T a) ≤ ∑_{b ∈ T} ∑_{p ∣ b} log p`, via the injection +`(a, p) ↦ (p a, p)`: if `p ≤ L T a` then `p a ∈ T`. -/ +theorem sum_theta_L_le (T : Finset ℕ) (hpos : ∀ a ∈ T, 0 < a) : + ∑ a ∈ T, ∑ p ∈ primesUpTo (L T a), log (p : ℝ) ≤ + ∑ b ∈ T, ∑ p ∈ b.primeFactors, log (p : ℝ) := by + classical + rw [sum_sigma', sum_sigma'] + refine sum_le_sum_of_injOn (fun x => (⟨x.2 * x.1, x.2⟩ : Σ _ : ℕ, ℕ)) ?_ ?_ + (fun _ _ => le_rfl) (fun y _ _ => log_natCast_nonneg _) + · rintro ⟨a, p⟩ ha ⟨a', p'⟩ ha' h + simp only [Sigma.mk.inj_iff, heq_eq_eq] at h + obtain ⟨h1, rfl⟩ := h + have hp : 0 < p := by + have := (mem_sigma.1 (mem_coe.1 ha)).2 + simp only [primesUpTo, mem_filter] at this + exact this.2.pos + rw [Nat.eq_of_mul_eq_mul_left hp h1] + · intro y hy + rw [mem_image] at hy + obtain ⟨⟨a, p⟩, hx, rfl⟩ := hy + rw [mem_sigma] at hx ⊢ + obtain ⟨haT, hpa⟩ := hx + simp only [primesUpTo, mem_filter, mem_range] at hpa + have hA : a ∈ A T (L T a) := (mem_A_iff T hpos).2 ⟨haT, le_rfl⟩ + have hmem : p * a ∈ T := mul_mem_of_mem_A hA hpa.2.one_lt.le (by omega) + refine ⟨hmem, ?_⟩ + rw [Nat.mem_primeFactors] + exact ⟨hpa.2, dvd_mul_right p a, (Nat.mul_pos hpa.2.pos (hpos a haT)).ne'⟩ + +/-- **Upper bound for closed sets.** If `T` is closed under divisors and prime shifts, then +`∑_{a ∈ T} L T a = O(n log n log log n)` with `n = |T|`. -/ +theorem sum_L_le_of_closed : ∃ C : ℝ, ∃ N : ℕ, ∀ T : Finset ℕ, (∀ a ∈ T, 0 < a) → + DivClosed T → ShiftClosed T → N ≤ T.card → + (∑ a ∈ T, (L T a : ℝ)) ≤ C * T.card * Real.log T.card * Real.log (Real.log T.card) := by + obtain ⟨K, hK0, hK⟩ := radical_bound + obtain ⟨C₀, hC₀, hθ⟩ := theta_lower + set c : ℝ := log 2 / 2 with hcdef + have hc : 0 < c := by have := log_pos (one_lt_two : (1 : ℝ) < 2); positivity + refine ⟨(K + C₀) / c, ⌈exp (exp 1)⌉₊, fun T hpos hdiv hshift hN => ?_⟩ + set n : ℝ := (T.card : ℝ) with hndef + have hnexp : exp (exp 1) ≤ n := (Nat.le_ceil _).trans (by rw [hndef]; exact_mod_cast hN) + have hn0 : 0 < n := (exp_pos _).trans_le hnexp + have hℓ : exp 1 ≤ log n := (le_log_iff_exp_le hn0).2 hnexp + have hℓ0 : 0 < log n := (exp_pos 1).trans_le hℓ + have hℓℓ : 1 ≤ log (log n) := (le_log_iff_exp_le hℓ0).2 hℓ + have hℓ1 : 1 ≤ log n := by linarith [add_one_le_exp (1 : ℝ)] + -- θ(L a) ≥ c L a - C₀ + have h1 : ∀ a ∈ T, c * (L T a : ℝ) - C₀ ≤ ∑ p ∈ primesUpTo (L T a), log (p : ℝ) := + fun a _ => by rw [sum_primesUpTo_eq_theta]; exact hθ _ + have h2 := sum_le_sum h1 + rw [sum_sub_distrib, ← mul_sum, sum_const, nsmul_eq_mul, ← hndef] at h2 + have h3 := sum_theta_L_le T hpos + have h4 : ∑ b ∈ T, ∑ p ∈ b.primeFactors, log (p : ℝ) ≤ + ∑ _b ∈ T, K * log n * log (log n) := + sum_le_sum fun b hb => hK T hdiv hshift hℓℓ b hb + rw [sum_const, nsmul_eq_mul, ← hndef] at h4 + have h5 : n ≤ n * log n * log (log n) := by + have : 1 ≤ log n * log (log n) := one_le_mul_of_one_le_of_one_le hℓ1 hℓℓ + calc n = n * 1 := (mul_one n).symm + _ ≤ n * (log n * log (log n)) := mul_le_mul_of_nonneg_left this hn0.le + _ = n * log n * log (log n) := by ring + have h6 : C₀ * n ≤ C₀ * (n * log n * log (log n)) := mul_le_mul_of_nonneg_left h5 hC₀ + rw [show (K + C₀) / c * n * log n * log (log n) = + ((K + C₀) * (n * log n * log (log n))) / c by ring, le_div_iff₀ hc] + linarith + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Alt/Upper.lean b/LeanPool/RunsOfMultiples/Alt/Upper.lean new file mode 100644 index 0000000000..b68169d0da --- /dev/null +++ b/LeanPool/RunsOfMultiples/Alt/Upper.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Alt.Chains +public import LeanPool.RunsOfMultiples.Alt.Radical + +/-! +# The upper bound via compression + +Compress `S` to a closed set `T` (`exists_closed`, Lemma 2), then bound the runs of `T` by the +radicals of its elements (`sum_L_le_of_closed`, Lemma 3 and equation (7)). +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +/-- `∑_{a ∈ S} L S a = ∑_{t = 1}^{|S|} |A S t|`. -/ +lemma sum_L_eq_sum_card_A (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : + ∑ a ∈ S, L S a = ∑ t ∈ Icc 1 S.card, (A S t).card := by + have hA : ∀ t, (A S t).card = ∑ a ∈ S, if t ≤ L S a then 1 else 0 := by + intro t + rw [← card_filter] + congr 1 + ext a + rw [mem_A_iff S hS, mem_filter] + simp_rw [hA] + rw [sum_comm] + refine sum_congr rfl fun a ha => ?_ + rw [← card_filter] + have : (Icc 1 S.card).filter (fun t => t ≤ L S a) = Icc 1 (L S a) := by + ext t + simp only [mem_filter, mem_Icc] + have := L_le_card S hS ha + omega + rw [this, Nat.card_Icc] + omega + +/-- **Upper bound, second proof.** -/ +theorem upper_bound_alt : ∃ C : ℝ, ∃ N : ℕ, ∀ S : Finset ℕ, (∀ a ∈ S, 0 < a) → N ≤ S.card → + ((∑ a ∈ S, kVal S a : ℕ) : ℝ) ≤ + C * S.card * Real.log S.card * Real.log (Real.log S.card) := by + obtain ⟨C, N, hCN⟩ := sum_L_le_of_closed + refine ⟨C + 1, max N ⌈exp (exp 1)⌉₊, fun S hS hSN => ?_⟩ + obtain ⟨T, hT, hcard, hdiv, hshift, hA⟩ := exists_closed S hS + have hTN : N ≤ T.card := by rw [hcard]; exact (le_max_left _ _).trans hSN + have hT' := hCN T hT hdiv hshift hTN + rw [hcard] at hT' + -- `∑ L S ≤ ∑ L T` + have hLL : (∑ a ∈ S, L S a : ℕ) ≤ ∑ a ∈ T, L T a := by + rw [sum_L_eq_sum_card_A S hS, sum_L_eq_sum_card_A T hT, hcard] + exact sum_le_sum fun t _ => hA t + have hLLr : (∑ a ∈ S, (L S a : ℝ)) ≤ ∑ a ∈ T, (L T a : ℝ) := by + exact_mod_cast hLL + -- `log n · log log n ≥ 1` + set n : ℝ := (S.card : ℝ) with hn + have hn_big : exp (exp 1) ≤ n := by + have := (le_max_right _ _).trans hSN + exact (Nat.ceil_le.1 this) + have hlog : exp 1 ≤ log n := by + rw [le_log_iff_exp_le (lt_of_lt_of_le (exp_pos _) hn_big)] + exact hn_big + have hll : 1 ≤ log (log n) := by + rw [le_log_iff_exp_le (lt_of_lt_of_le (exp_pos _) hlog)] + exact hlog + have hl1 : 1 ≤ log n := le_trans (by linarith [add_one_le_exp (1 : ℝ)]) hlog + have hn1 : 1 ≤ n := le_trans (by linarith [add_one_le_exp (exp 1), exp_pos 1]) hn_big + have hprod : n ≤ n * log n * log (log n) := by + have : 1 ≤ log n * log (log n) := by nlinarith + nlinarith + have hk := sum_kVal_eq S hS + have hk' : ((∑ a ∈ S, kVal S a : ℕ) : ℝ) = n + ∑ a ∈ S, (L S a : ℝ) := by + rw [hk]; push_cast; rfl + rw [hk'] + calc n + ∑ a ∈ S, (L S a : ℝ) ≤ n + C * n * log n * log (log n) := by linarith + _ ≤ (C + 1) * n * log n * log (log n) := by nlinarith + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/BlockLower.lean b/LeanPool/RunsOfMultiples/BlockLower.lean new file mode 100644 index 0000000000..2007cfc43e --- /dev/null +++ b/LeanPool/RunsOfMultiples/BlockLower.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Replication +public import Mathlib.Analysis.SpecialFunctions.Pow.Real + +/-! +# Transferring multiplicative blocks to every large cardinality + +Positive-density blocks with controlled size produce the sharp lower asymptotic order. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +/-- A positive-density block with exponential size bounds yields the sharp lower order. -/ +theorem lower_bound_of_block {δ C₂ : ℝ} (hδ : 0 < δ) (hC₂ : 0 < C₂) + (hblock : ∀ y : ℕ, 2 ≤ y → ∃ B G : Finset ℕ, + (∀ a ∈ B, 0 < a) ∧ G ⊆ B ∧ + (∀ a ∈ G, ∀ j, 1 ≤ j → j ≤ y → j * a ∈ B) ∧ 0 < B.card ∧ + δ * B.card ≤ G.card ∧ (B.card : ℝ) ≤ exp (C₂ * (y / log y))) : + ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ S : Finset ℕ, + (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ + c * n * Real.log n * Real.log (Real.log n) ≤ ((∑ a ∈ S, kVal S a : ℕ) : ℝ) := by + set ε := 1 / (2 * C₂) with hεdef + have hε : 0 < ε := by positivity + refine ⟨ε * δ / 2, by positivity, ?_⟩ + have hev : ∀ᶠ n : ℕ in Filter.atTop, 4 ≤ n ∧ 2 / ε ≤ log (log (n : ℝ)) := + (Filter.eventually_ge_atTop 4).and + ((tendsto_log_atTop.comp + (tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)).eventually_ge_atTop (2 / ε)) + obtain ⟨N, hN⟩ := Filter.eventually_atTop.1 hev + refine ⟨N, fun n hn => ?_⟩ + obtain ⟨hn4, hLL⟩ := hN n hn + set L := log (n : ℝ) with hLdef + set LL := log L with hLLdef + have hL0 : 0 ≤ L := Real.log_natCast_nonneg n + have hLLpos : 0 < LL := lt_of_lt_of_le (by positivity) hLL + have hL1 : 1 < L := (log_pos_iff hL0).1 hLLpos + have hεLL : 2 ≤ ε * LL := by + rw [div_le_iff₀ hε] at hLL; linarith + set y := ⌊ε * L * LL⌋₊ with hydef + have hyle : (y : ℝ) ≤ ε * L * LL := Nat.floor_le (by positivity) + have hylt : ε * L * LL < y + 1 := Nat.lt_floor_add_one _ + have hεLLL : 2 * L ≤ ε * L * LL := by + nlinarith only [mul_le_mul_of_nonneg_right hεLL hL0] + have hLy : L ≤ y := by linarith only [hεLLL, hylt, hL1] + have hy2 : 2 ≤ y := by + have h1 : (1 : ℝ) < y := by linarith + have h2 : 1 < y := by exact_mod_cast h1 + omega + obtain ⟨B, G, hBpos, hGB, hG, hBcard, hGcard, hBle⟩ := hblock y hy2 + have hlogy : LL ≤ log y := log_le_log (by linarith) hLy + have hQ : (y : ℝ) / log y ≤ ε * L := by + rw [div_le_iff₀ (by linarith)] + have : 0 ≤ ε * L := by positivity + nlinarith only [hyle, mul_le_mul_of_nonneg_left hlogy this] + have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega) + have hexp : exp (L / 2) ≤ n / 2 := by + set e := exp (L / 2) with he + have hepos : 0 < e := exp_pos _ + have hee : e * e = n := by rw [he, ← exp_add, add_halves, hLdef, exp_log hn0] + have hn4' : (4 : ℝ) ≤ n := by exact_mod_cast hn4 + have he2 : 2 ≤ e := by + by_contra h + push Not at h + nlinarith only [hepos, h, hee, hn4'] + nlinarith only [he2, hee, hepos] + have hBn : (B.card : ℝ) ≤ n / 2 := by + calc (B.card : ℝ) ≤ exp (C₂ * (y / log y)) := hBle + _ ≤ exp (L / 2) := by + refine exp_le_exp.2 ?_ + calc C₂ * (y / log y) ≤ C₂ * (ε * L) := mul_le_mul_of_nonneg_left hQ hC₂.le + _ = L / 2 := by rw [hεdef]; field_simp + _ ≤ n / 2 := hexp + have hBn' : 2 * B.card ≤ n := by + have : (2 * B.card : ℝ) ≤ n := by linarith + exact_mod_cast this + obtain ⟨S, hSpos, hScard, hSsum⟩ := replicate B G y n hBpos hGB hG + refine ⟨S, hSpos, hScard, ?_⟩ + have htB : n ≤ 2 * (n / B.card * B.card) := by + have := Nat.lt_div_mul_add (a := n) hBcard + generalize n / B.card * B.card = q at * + omega + have htB' : (n : ℝ) / 2 ≤ ((n / B.card : ℕ) : ℝ) * B.card := by + have : (n : ℝ) ≤ 2 * (((n / B.card : ℕ) : ℝ) * B.card) := by exact_mod_cast htB + linarith + have hsum : (((n / B.card * G.card * (y + 1) : ℕ)) : ℝ) ≤ ((∑ a ∈ S, kVal S a : ℕ) : ℝ) := by + exact_mod_cast hSsum + have ht0 : (0 : ℝ) ≤ ((n / B.card : ℕ) : ℝ) := Nat.cast_nonneg _ + have hLLL : 0 ≤ ε * L * LL := by positivity + calc ε * δ / 2 * n * L * LL = δ * (n / 2) * (ε * L * LL) := by ring + _ ≤ δ * (((n / B.card : ℕ) : ℝ) * B.card) * (y + 1) := by + gcongr + _ = ((n / B.card : ℕ) : ℝ) * (δ * B.card) * (y + 1) := by ring + _ ≤ ((n / B.card : ℕ) : ℝ) * G.card * (y + 1) := by + gcongr + _ = (((n / B.card * G.card * (y + 1) : ℕ)) : ℝ) := by push_cast; ring + _ ≤ _ := hsum + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Defs.lean b/LeanPool/RunsOfMultiples/Defs.lean new file mode 100644 index 0000000000..a6e17706ef --- /dev/null +++ b/LeanPool/RunsOfMultiples/Defs.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import Mathlib.Order.Lattice.Nat +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Order.Interval.Finset.Nat + +/-! +# Runs of multiples: definitions + +For a finite set `S` of positive integers and `a ∈ S`, `kVal S a` is the least positive +integer `k` with `k * a ∉ S`. We write `L S a = kVal S a - 1` for the length of the run +`a, 2a, …, L a` inside `S`, and `A S t` for the set of `a ∈ S` whose run has length `≥ t`. +-/ + +open Finset + +@[expose] public section + +namespace RunsOfMultiples + +/-- `kVal S a` is the least positive integer `k` with `k * a ∉ S`. -/ +noncomputable def kVal (S : Finset ℕ) (a : ℕ) : ℕ := sInf {k : ℕ | 0 < k ∧ k * a ∉ S} + +/-- The elements of `S` whose first `t` multiples all lie in `S`. -/ +def A (S : Finset ℕ) (t : ℕ) : Finset ℕ := S.filter (fun a => ∀ i ∈ Icc 1 t, i * a ∈ S) + +/-- Run length `L S a = kVal S a - 1`. -/ +noncomputable def L (S : Finset ℕ) (a : ℕ) : ℕ := kVal S a - 1 + +lemma kVal_set_nonempty (S : Finset ℕ) {a : ℕ} (ha : 0 < a) : + {k : ℕ | 0 < k ∧ k * a ∉ S}.Nonempty := by + refine ⟨S.sup id + 1, Nat.succ_pos _, fun h => ?_⟩ + have h1 : (S.sup id + 1) * a ≤ S.sup id := Finset.le_sup (f := id) h + have h2 : S.sup id + 1 ≤ (S.sup id + 1) * a := Nat.le_mul_of_pos_right _ ha + omega + +lemma kVal_pos (S : Finset ℕ) {a : ℕ} (ha : 0 < a) : 0 < kVal S a := + (Nat.sInf_mem (kVal_set_nonempty S ha)).1 + +lemma kVal_not_mem (S : Finset ℕ) {a : ℕ} (ha : 0 < a) : kVal S a * a ∉ S := + (Nat.sInf_mem (kVal_set_nonempty S ha)).2 + +lemma mul_mem_of_lt_kVal (S : Finset ℕ) {a i : ℕ} (hi : 0 < i) (hik : i < kVal S a) : + i * a ∈ S := by + by_contra h + exact Nat.notMem_of_lt_sInf hik ⟨hi, h⟩ + +/-- The run characterisation: the first `t` multiples of `a` lie in `S` iff `t < kVal S a`. -/ +lemma forall_mul_mem_iff (S : Finset ℕ) {a : ℕ} (ha : 0 < a) (t : ℕ) : + (∀ i ∈ Icc 1 t, i * a ∈ S) ↔ t < kVal S a := by + constructor + · intro h + by_contra hle + push Not at hle + exact kVal_not_mem S ha (h _ (mem_Icc.2 ⟨kVal_pos S ha, hle⟩)) + · intro h i hi + rw [mem_Icc] at hi + exact mul_mem_of_lt_kVal S (by omega) (by omega) + +lemma mem_A_iff (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {a t : ℕ} : + a ∈ A S t ↔ a ∈ S ∧ t ≤ L S a := by + unfold A L + rw [mem_filter] + constructor + · rintro ⟨haS, h⟩ + have := (forall_mul_mem_iff S (hS a haS) t).1 h + exact ⟨haS, by omega⟩ + · rintro ⟨haS, h⟩ + refine ⟨haS, (forall_mul_mem_iff S (hS a haS) t).2 ?_⟩ + have := kVal_pos S (hS a haS) + omega + +lemma A_subset (S : Finset ℕ) (t : ℕ) : A S t ⊆ S := filter_subset _ _ + +lemma A_anti (S : Finset ℕ) {s t : ℕ} (hst : s ≤ t) : A S t ⊆ A S s := by + intro a ha + simp only [A, mem_filter, mem_Icc] at ha ⊢ + exact ⟨ha.1, fun i hi => ha.2 i ⟨hi.1, hi.2.trans hst⟩⟩ + +/-- If `a ∈ A S t` and `1 ≤ i ≤ t` then `i * a ∈ S`. -/ +lemma mul_mem_of_mem_A {S : Finset ℕ} {t a i : ℕ} (ha : a ∈ A S t) (hi1 : 1 ≤ i) (hit : i ≤ t) : + i * a ∈ S := by + simp only [A, mem_filter, mem_Icc] at ha + exact ha.2 i ⟨hi1, hit⟩ + +/-- The run length is at most `|S|`. -/ +lemma L_le_card (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {a : ℕ} (haS : a ∈ S) : + L S a ≤ S.card := by + have ha := hS a haS + have hsub : (Icc 1 (L S a)).image (fun i => i * a) ⊆ S := by + intro x hx + rw [mem_image] at hx + obtain ⟨i, hi, rfl⟩ := hx + rw [mem_Icc] at hi + have := kVal_pos S ha + exact mul_mem_of_lt_kVal S (by omega) (by unfold L at hi; omega) + have hinj : Set.InjOn (fun i => i * a) (Icc 1 (L S a) : Set ℕ) := by + intro i _ j _ h + exact Nat.eq_of_mul_eq_mul_right ha h + have := card_le_card hsub + rw [card_image_of_injOn hinj, Nat.card_Icc] at this + omega + +lemma sum_kVal_eq (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : + ∑ a ∈ S, kVal S a = S.card + ∑ a ∈ S, L S a := by + rw [card_eq_sum_ones, ← sum_add_distrib] + refine sum_congr rfl fun a ha => ?_ + have := kVal_pos S (hS a ha) + unfold L + omega + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Edges.lean b/LeanPool/RunsOfMultiples/Edges.lean new file mode 100644 index 0000000000..c9583a5a7f --- /dev/null +++ b/LeanPool/RunsOfMultiples/Edges.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.OneStep + +/-! +# Counting prime edges with entropy (Lemma 4) + +For each prime `p`, the fibres of the `p`-smooth part split `T`; on each fibre Lemma 3 applies +with level `v_p`. Summing over primes and using the chain rule gives the edge bound. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +/-- Per prime: if `p * m ∈ T` for all `m ∈ G ⊆ T`, then the fibrewise Lemma 3 bounds hold. -/ +lemma mem_fibre_of_prime_mul {T : Finset ℕ} (hT : ∀ m ∈ T, 0 < m) {p q : ℕ} (hp : p.Prime) + (hqp : q ≤ p) {m : ℕ} (hm : m ∈ T) (hpm : p * m ∈ T) : + p * m ∈ T.filter (fun x => key q x = key q m) := by + rw [mem_filter] + exact ⟨hpm, key_prime_mul hp hqp (hT m hm).ne'⟩ + +/-- `D T p ≥ (log 2 / 2) |G|` whenever multiplication by the prime `p` maps `G ⊆ T` into `T`. -/ +lemma D_ge_log_two (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {p : ℕ} (hp : p.Prime) + (G : Finset ℕ) (hGT : G ⊆ T) (hG : ∀ m ∈ G, p * m ∈ T) : + log 2 / 2 * G.card ≤ D T p := by + unfold D + have hcard : (G.card : ℝ) = + ∑ c ∈ T.image (key p), ((G.filter (fun m => key p m = c)).card : ℝ) := by + rw [← Nat.cast_sum, card_eq_sum_card_fiberwise (f := key p)] + intro m hm + exact mem_image_of_mem _ (hGT hm) + rw [hcard, mul_sum] + refine sum_le_sum fun c _ => ?_ + refine ent_ge_log_two _ _ _ p hp.pos ?_ ?_ + · intro m hm + rw [mem_filter] at hm ⊢ + exact ⟨hGT hm.1, hm.2⟩ + · intro m hm + rw [mem_filter] at hm + have hmT := hGT hm.1 + refine ⟨?_, factorization_prime_mul_self hp (hT m hmT).ne'⟩ + rw [mem_filter] + refine ⟨hG m hm.1, ?_⟩ + rw [key_prime_mul hp le_rfl (hT m hmT).ne', hm.2] + +/-- **Lemma 4** (edge count). -/ +theorem edge_bound (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) + (E : ℕ → Finset ℕ) (hET : ∀ p ∈ P, E p ⊆ T) (hE : ∀ p ∈ P, ∀ m ∈ E p, p * m ∈ T) : + log 2 / 2 * ∑ p ∈ P, ((E p).card : ℝ) ≤ T.card * log T.card := by + set B := T.sup id + 1 + have hB : ∀ m ∈ T, m < B := fun m hm => Nat.lt_succ_of_le (le_sup (f := id) hm) + -- primes with a nonempty `E p` are below `B` + have hsplit : ∑ p ∈ P, ((E p).card : ℝ) = ∑ p ∈ P.filter (· < B), ((E p).card : ℝ) := by + rw [sum_filter] + refine sum_congr rfl fun p hp => ?_ + split_ifs with h + · rfl + · push Not at h + rw [card_eq_zero.2, Nat.cast_zero] + rw [eq_empty_iff_forall_notMem] + intro m hm + have hpm := hB _ (hE p hp m hm) + have hm0 := hT m (hET p hp hm) + have : p ≤ p * m := Nat.le_mul_of_pos_right p hm0 + omega + rw [hsplit, mul_sum] + calc ∑ p ∈ P.filter (· < B), log 2 / 2 * ((E p).card : ℝ) + ≤ ∑ p ∈ P.filter (· < B), D T p := by + refine sum_le_sum fun p hp => ?_ + rw [mem_filter] at hp + exact D_ge_log_two T hT (hP p hp.1) (E p) (hET p hp.1) (hE p hp.1) + _ ≤ T.card * log T.card := by + refine sum_D_le T hT hB _ ?_ + intro p hp + rw [mem_filter] at hp + exact mem_range.2 hp.2 + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Entropy.lean b/LeanPool/RunsOfMultiples/Entropy.lean new file mode 100644 index 0000000000..ca7395ff96 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Entropy.lean @@ -0,0 +1,197 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.Data.Nat.Factorization.Basic +public import LeanPool.RunsOfMultiples.Defs + +/-! +# Counting entropy along the prime factorisation + +For a finite set `R` and a function `f`, `ent R f = ∑_{m ∈ R} log (|R| / |fibre of m|)`; this is +`|R|` times the Shannon entropy of `f(X)` for `X` uniform on `R`. + +`key t m` records the exponents of the primes `< t` in `m` (the `t`-smooth part of `m`). +`D T t` is `|T|` times the conditional entropy of `v_t(X)` given `key t X`; the chain rule +`∑_{t < B} D T t = |T| log |T|` is `sum_D`. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +section ent + +variable {β : Type*} [DecidableEq β] + +/-- Counting entropy: `|R|` times the entropy of `f(X)`, `X` uniform on `R`. -/ +noncomputable def ent (R : Finset ℕ) (f : ℕ → β) : ℝ := + ∑ m ∈ R, Real.log ((R.card : ℝ) / ((R.filter (fun x => f x = f m)).card : ℝ)) + +lemma fibre_card_pos {R : Finset ℕ} {f : ℕ → β} {m : ℕ} (hm : m ∈ R) : + 0 < (R.filter (fun x => f x = f m)).card := + card_pos.2 ⟨m, mem_filter.2 ⟨hm, rfl⟩⟩ + +lemma fibre_card_le (R : Finset ℕ) (f : ℕ → β) (m : ℕ) : + (R.filter (fun x => f x = f m)).card ≤ R.card := + card_le_card (filter_subset _ _) + +lemma log_card_div_fibre_nonneg {R : Finset ℕ} {f : ℕ → β} {m : ℕ} (hm : m ∈ R) : + 0 ≤ Real.log ((R.card : ℝ) / ((R.filter (fun x => f x = f m)).card : ℝ)) := by + have h1 : (0 : ℝ) < (R.filter (fun x => f x = f m)).card := by + exact_mod_cast fibre_card_pos hm + have h2 : ((R.filter (fun x => f x = f m)).card : ℝ) ≤ R.card := by + exact_mod_cast fibre_card_le R f m + exact Real.log_nonneg ((one_le_div h1).2 h2) + +lemma ent_nonneg (R : Finset ℕ) (f : ℕ → β) : 0 ≤ ent R f := + sum_nonneg fun _ hm => log_card_div_fibre_nonneg hm + +end ent + +/-- The exponents of the primes `< t` in `m`. -/ +noncomputable def key (t m : ℕ) : ℕ →₀ ℕ := m.factorization.filter (· < t) + +lemma key_apply (t m p : ℕ) : key t m p = if p < t then m.factorization p else 0 := by + simp [key, Finsupp.filter_apply] + +lemma key_zero (m : ℕ) : key 0 m = 0 := by + ext p + simp [key_apply] + +lemma key_succ_eq_iff (t m m' : ℕ) : + key (t + 1) m = key (t + 1) m' ↔ + key t m = key t m' ∧ m.factorization t = m'.factorization t := by + constructor + · intro h + refine ⟨?_, ?_⟩ + · ext p + have := DFunLike.congr_fun h p + simp only [key_apply] at this ⊢ + split_ifs with hp + · simpa [show p < t + 1 by omega] using this + · rfl + · have := DFunLike.congr_fun h t + simpa [key_apply] using this + · rintro ⟨h1, h2⟩ + ext p + have := DFunLike.congr_fun h1 p + simp only [key_apply] at this ⊢ + split_ifs at this ⊢ with hp hp' + · exact this + · have : p = t := by omega + subst this + exact h2 + · omega + · rfl + +lemma key_eq_factorization {t m : ℕ} (hm : ∀ p ∈ m.primeFactors, p < t) : + key t m = m.factorization := by + ext p + rw [key_apply] + split_ifs with hp + · rfl + · rw [Finsupp.notMem_support_iff.1] + rw [Nat.support_factorization] + intro hp' + exact hp (hm p hp') + +/-- Multiplying by a prime `p ≥ t` does not change the `t`-smooth part. -/ +lemma key_prime_mul {t p m : ℕ} (hp : p.Prime) (htp : t ≤ p) (hm : m ≠ 0) : + key t (p * m) = key t m := by + ext x + rw [key_apply, key_apply, Nat.factorization_mul hp.ne_zero hm, hp.factorization] + split_ifs with hx + · simp [show p ≠ x by omega] + · rfl + +lemma factorization_prime_mul_self {p m : ℕ} (hp : p.Prime) (hm : m ≠ 0) : + (p * m).factorization p = m.factorization p + 1 := by + rw [Nat.factorization_mul hp.ne_zero hm, hp.factorization] + simp [add_comm] + +/-- `D T t`: `|T|` times the conditional entropy of `v_t(X)` given the `t`-smooth part of `X`. -/ +noncomputable def D (T : Finset ℕ) (t : ℕ) : ℝ := + ∑ c ∈ T.image (key t), ent (T.filter (fun m => key t m = c)) (fun m => m.factorization t) + +lemma D_nonneg (T : Finset ℕ) (t : ℕ) : 0 ≤ D T t := + sum_nonneg fun _ _ => ent_nonneg _ _ + +/-- Regrouping: `D T t` is the increase of `ent T (key ·)` from `t` to `t + 1`. -/ +lemma D_eq (T : Finset ℕ) (t : ℕ) : D T t = ent T (key (t + 1)) - ent T (key t) := by + unfold D ent + rw [← sum_sub_distrib] + rw [← sum_fiberwise_of_maps_to (s := T) (t := T.image (key t)) (g := key t) + (fun m hm => mem_image_of_mem _ hm)] + refine sum_congr rfl fun c _ => sum_congr rfl fun m hm => ?_ + rw [mem_filter] at hm + obtain ⟨hmT, rfl⟩ := hm + -- the fibre of `m` for `key t` and its refinement + have hF : (T.filter (fun x => key t x = key t m)).filter + (fun x => x.factorization t = m.factorization t) = + T.filter (fun x => key (t + 1) x = key (t + 1) m) := by + ext x + simp only [mem_filter, key_succ_eq_iff] + tauto + rw [hF] + have hT : (0 : ℝ) < T.card := by exact_mod_cast card_pos.2 ⟨m, hmT⟩ + have h1 : (0 : ℝ) < (T.filter (fun x => key (t + 1) x = key (t + 1) m)).card := by + exact_mod_cast fibre_card_pos hmT + have h2 : (0 : ℝ) < (T.filter (fun x => key t x = key t m)).card := by + exact_mod_cast fibre_card_pos hmT + rw [Real.log_div h2.ne' h1.ne', Real.log_div hT.ne' h1.ne', Real.log_div hT.ne' h2.ne'] + ring + +lemma ent_key_zero (T : Finset ℕ) : ent T (key 0) = 0 := by + unfold ent + refine sum_eq_zero fun m hm => ?_ + have : T.filter (fun x => key 0 x = key 0 m) = T := by + ext x + simp [key_zero] + rw [this, div_self] + · simp + · exact_mod_cast (card_pos.2 ⟨m, hm⟩).ne' + +lemma ent_key_large (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {B : ℕ} (hB : ∀ m ∈ T, m < B) : + ent T (key B) = T.card * Real.log T.card := by + unfold ent + have hsing : ∀ m ∈ T, T.filter (fun x => key B x = key B m) = {m} := by + intro m hm + ext x + simp only [mem_filter, mem_singleton] + constructor + · rintro ⟨hx, hkey⟩ + have hkx : ∀ p ∈ x.primeFactors, p < B := fun p hp => + lt_of_le_of_lt (Nat.le_of_dvd (hT x hx) (Nat.dvd_of_mem_primeFactors hp)) (hB x hx) + have hkm : ∀ p ∈ m.primeFactors, p < B := fun p hp => + lt_of_le_of_lt (Nat.le_of_dvd (hT m hm) (Nat.dvd_of_mem_primeFactors hp)) (hB m hm) + rw [key_eq_factorization hkx, key_eq_factorization hkm] at hkey + exact Nat.factorization_inj (Nat.pos_iff_ne_zero.1 (hT x hx)) + (Nat.pos_iff_ne_zero.1 (hT m hm)) hkey + · rintro rfl + exact ⟨hm, rfl⟩ + rw [sum_congr rfl fun m hm => by rw [hsing m hm]] + simp + +/-- Chain rule: the conditional entropies along all primes add up to `|T| log |T|`. -/ +theorem sum_D (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {B : ℕ} (hB : ∀ m ∈ T, m < B) : + ∑ t ∈ range B, D T t = T.card * Real.log T.card := by + simp_rw [D_eq] + rw [sum_range_sub (fun t => ent T (key t)), ent_key_large T hT hB, ent_key_zero, sub_zero] + +/-- Restricting the chain-rule sum to a sub-family of indices. -/ +lemma sum_D_le (T : Finset ℕ) (hT : ∀ m ∈ T, 0 < m) {B : ℕ} (hB : ∀ m ∈ T, m < B) + (P : Finset ℕ) (hP : P ⊆ range B) : + ∑ t ∈ P, D T t ≤ T.card * Real.log T.card := by + rw [← sum_D T hT hB] + exact sum_le_sum_of_subset_of_nonneg hP fun t _ _ => D_nonneg T t + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Examples.lean b/LeanPool/RunsOfMultiples/Examples.lean new file mode 100644 index 0000000000..beab51733b --- /dev/null +++ b/LeanPool/RunsOfMultiples/Examples.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Defs + +/-! +# Sanity checks for `kVal` + +`kVal S a` is computed on a small example: for `S = {1, 2, 3, 4, 6}` the values are +`k(1) = 5, k(2) = 4, k(3) = 3, k(4) = 2, k(6) = 2`, so `∑ k = 16`, beating `{1, …, 5}` (`∑ k = 15`). +-/ + +open Finset + +@[expose] public section + +namespace RunsOfMultiples + +/-- `kVal` is characterised by: `k * a ∉ S`, and `j * a ∈ S` for `0 < j < k`. -/ +lemma kVal_eq_of {S : Finset ℕ} {a k : ℕ} (hk : 0 < k) (hnot : k * a ∉ S) + (hall : ∀ j ∈ Ioo 0 k, j * a ∈ S) : kVal S a = k := by + have hne : {k : ℕ | 0 < k ∧ k * a ∉ S}.Nonempty := ⟨k, hk, hnot⟩ + apply le_antisymm (Nat.sInf_le (show k ∈ {k : ℕ | 0 < k ∧ k * a ∉ S} from ⟨hk, hnot⟩)) + by_contra h + push Not at h + obtain ⟨hpos, hm⟩ := Nat.sInf_mem hne + exact hm (hall _ (mem_Ioo.2 ⟨hpos, h⟩)) + +example : ∑ a ∈ ({1, 2, 3, 4, 6} : Finset ℕ), kVal {1, 2, 3, 4, 6} a = 16 := by + simp only [sum_insert (by decide : (1 : ℕ) ∉ ({2, 3, 4, 6} : Finset ℕ)), + sum_insert (by decide : (2 : ℕ) ∉ ({3, 4, 6} : Finset ℕ)), + sum_insert (by decide : (3 : ℕ) ∉ ({4, 6} : Finset ℕ)), + sum_insert (by decide : (4 : ℕ) ∉ ({6} : Finset ℕ)), sum_singleton, + kVal_eq_of (S := {1, 2, 3, 4, 6}) (a := 1) (k := 5) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 6}) (a := 2) (k := 4) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 6}) (a := 3) (k := 3) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 6}) (a := 4) (k := 2) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 6}) (a := 6) (k := 2) (by decide) (by decide) (by decide)] + rfl + +example : ∑ a ∈ Icc 1 5, kVal (Icc 1 5) a = 15 := by + simp only [show Icc 1 5 = ({1, 2, 3, 4, 5} : Finset ℕ) by decide] + simp only [sum_insert (by decide : (1 : ℕ) ∉ ({2, 3, 4, 5} : Finset ℕ)), + sum_insert (by decide : (2 : ℕ) ∉ ({3, 4, 5} : Finset ℕ)), + sum_insert (by decide : (3 : ℕ) ∉ ({4, 5} : Finset ℕ)), + sum_insert (by decide : (4 : ℕ) ∉ ({5} : Finset ℕ)), sum_singleton, + kVal_eq_of (S := {1, 2, 3, 4, 5}) (a := 1) (k := 6) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 5}) (a := 2) (k := 3) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 5}) (a := 3) (k := 2) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 5}) (a := 4) (k := 2) (by decide) (by decide) (by decide), + kVal_eq_of (S := {1, 2, 3, 4, 5}) (a := 5) (k := 2) (by decide) (by decide) (by decide)] + rfl + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Imports.lean b/LeanPool/RunsOfMultiples/Imports.lean new file mode 100644 index 0000000000..0fe12a8403 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Imports.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.RunsOfMultiples +public import LeanPool.RunsOfMultiples.Alt.Chains +public import LeanPool.RunsOfMultiples.Alt.Compression +public import LeanPool.RunsOfMultiples.Alt.Defs +public import LeanPool.RunsOfMultiples.Alt.Lower +public import LeanPool.RunsOfMultiples.Alt.Main +public import LeanPool.RunsOfMultiples.Alt.Radical +public import LeanPool.RunsOfMultiples.Alt.Upper +public import LeanPool.RunsOfMultiples.BlockLower +public import LeanPool.RunsOfMultiples.Defs +public import LeanPool.RunsOfMultiples.Edges +public import LeanPool.RunsOfMultiples.Entropy +public import LeanPool.RunsOfMultiples.Examples +public import LeanPool.RunsOfMultiples.Lower +public import LeanPool.RunsOfMultiples.LowerEstimates +public import LeanPool.RunsOfMultiples.Main +public import LeanPool.RunsOfMultiples.OneStep +public import LeanPool.RunsOfMultiples.PrimeEstimates +public import LeanPool.RunsOfMultiples.PrimeInput +public import LeanPool.RunsOfMultiples.Primes +public import LeanPool.RunsOfMultiples.Replication +public import LeanPool.RunsOfMultiples.Upper diff --git a/LeanPool/RunsOfMultiples/Lower.lean b/LeanPool/RunsOfMultiples/Lower.lean new file mode 100644 index 0000000000..2eb95ff249 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Lower.lean @@ -0,0 +1,294 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.BlockLower +public import LeanPool.RunsOfMultiples.LowerEstimates +public import Mathlib.NumberTheory.EulerProduct.Basic +public import Mathlib.NumberTheory.SmoothNumbers + +/-! +# Runs of multiples: the lower bound + +For every large `n` there is an `n`-element set `S` of positive integers with +`∑ a ∈ S, kVal S a ≥ c n log n log log n`. + +Route (see `docs/runs-of-multiples.pdf`, §2): +* `Sm X y` is the set of `y`-smooth numbers in `[1, X]`. If `a ∈ Sm X y` then `j * a ∈ Sm (X * y) y` + for all `1 ≤ j ≤ y`. +* Rankin's trick (via Mathlib's Euler product over smooth numbers) with `σ = 1 / log y` gives + `|Sm (y ^ K) y| ≤ exp (K + C₀ y / log y)`. +* Pigeonhole over `X_i = y ^ i`, `i ≤ K = ⌈y / log y⌉`, gives a block `B = Sm (y ^ (i+1)) y` + with `|B| ≤ exp (C₂ y / log y)` containing `G = Sm (y ^ i) y`, `|G| ≥ δ |B|`, all of whose + first `y` multiples lie in `B`. +* `⌊n / |B|⌋` scaled copies `M ^ j • B` plus padding give the set for every large `n`. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +/-! ### Elementary analytic estimates -/ + +lemma inv_one_sub_exp_neg_le {u : ℝ} (hu : 0 < u) : (1 - exp (-u))⁻¹ ≤ exp (1 / u) := by + have h1 : 1 + u ≤ exp u := by linarith [add_one_le_exp u] + have h2 : exp (-u) ≤ (1 + u)⁻¹ := by rw [exp_neg]; exact inv_anti₀ (by linarith) h1 + have h3 : u / (1 + u) ≤ 1 - exp (-u) := by + have : u / (1 + u) = 1 - (1 + u)⁻¹ := by field_simp; ring + linarith + have h4 : 0 < u / (1 + u) := by positivity + calc (1 - exp (-u))⁻¹ ≤ (u / (1 + u))⁻¹ := inv_anti₀ h4 h3 + _ = 1 / u + 1 := by field_simp + _ ≤ exp (1 / u) := add_one_le_exp _ + +/-! ### Smooth numbers and Rankin's bound -/ + +/-- The `y`-smooth numbers in `[1, X]`. -/ +def Sm (X y : ℕ) : Finset ℕ := Nat.smoothNumbersUpTo X (y + 1) + +lemma pos_of_mem_Sm {X y m : ℕ} (hm : m ∈ Sm X y) : 0 < m := + Nat.pos_of_ne_zero (Nat.ne_zero_of_mem_smoothNumbers (Nat.mem_smoothNumbersUpTo.1 hm).2) + +lemma one_mem_Sm {X y : ℕ} (hX : 1 ≤ X) : 1 ∈ Sm X y := + Nat.mem_smoothNumbersUpTo.2 ⟨hX, Nat.mem_smoothNumbers.2 ⟨one_ne_zero, fun p hp => by simp at hp⟩⟩ + +lemma Sm_mono {X X' y : ℕ} (h : X ≤ X') : Sm X y ⊆ Sm X' y := by + intro m hm + rw [Sm, Nat.mem_smoothNumbersUpTo] at hm ⊢ + exact ⟨hm.1.trans h, hm.2⟩ + +lemma mul_mem_Sm {X y a j : ℕ} (ha : a ∈ Sm X y) (hj1 : 1 ≤ j) (hjy : j ≤ y) : + j * a ∈ Sm (X * y) y := by + rw [Sm, Nat.mem_smoothNumbersUpTo] at ha ⊢ + refine ⟨?_, Nat.mul_mem_smoothNumbers (Nat.mem_smoothNumbers_of_lt hj1 (by omega)) ha.2⟩ + rw [mul_comm X y] + exact Nat.mul_le_mul hjy ha.1 + +/-- The completely multiplicative function `m ↦ m ^ (-σ)`. -/ +noncomputable def rpowHom (σ : ℝ) : ℕ →* ℝ where + toFun n := (n : ℝ) ^ (-σ) + map_one' := by simp + map_mul' m n := by push_cast; exact Real.mul_rpow m.cast_nonneg n.cast_nonneg + +lemma rankin_sum (σ : ℝ) (hσ : 0 < σ) (y X : ℕ) : + ∑ m ∈ Sm X y, (m : ℝ) ^ (-σ) ≤ ∏ p ∈ (y + 1).primesBelow, (1 - (p : ℝ) ^ (-σ))⁻¹ := by + have h := (EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric + (f := rpowHom σ) ?_ (y + 1)).2 + · have h' := (hasSum_subtype_iff_indicator (f := fun m => rpowHom σ m)).mp h + refine le_trans (le_of_eq ?_) (sum_le_hasSum (Nat.smoothNumbersUpTo X (y + 1)) ?_ h') + · refine Finset.sum_congr rfl fun m hm => ?_ + rw [Set.indicator_of_mem (Nat.mem_smoothNumbersUpTo.mp hm).2] + rfl + · intro i _ + apply Set.indicator_nonneg + intro j _ + exact Real.rpow_nonneg (Nat.cast_nonneg _) _ + · intro p hp + simp only [rpowHom, MonoidHom.coe_mk, OneHom.coe_mk] + rw [Real.norm_of_nonneg (Real.rpow_nonneg (Nat.cast_nonneg _) _)] + exact Real.rpow_lt_one_of_one_lt_of_neg (by exact_mod_cast hp.one_lt) (by linarith) + +/-- Rankin's trick: `|Sm X y| ≤ X ^ σ ∏_{p ≤ y} (1 - p ^ (-σ))⁻¹`. -/ +lemma rankin_card (σ : ℝ) (hσ : 0 < σ) (y X : ℕ) (hX : 0 < X) : + ((Sm X y).card : ℝ) ≤ (X : ℝ) ^ σ * ∏ p ∈ (y + 1).primesBelow, (1 - (p : ℝ) ^ (-σ))⁻¹ := by + have hXpos : (0 : ℝ) < X := by exact_mod_cast hX + have h1 : ∀ m ∈ Sm X y, (X : ℝ) ^ (-σ) ≤ (m : ℝ) ^ (-σ) := by + intro m hm + have hm0 : (0 : ℝ) < m := by exact_mod_cast pos_of_mem_Sm hm + rw [Sm, Nat.mem_smoothNumbersUpTo] at hm + exact Real.rpow_le_rpow_of_nonpos hm0 (by exact_mod_cast hm.1) (by linarith) + have h2 : ((Sm X y).card : ℝ) * (X : ℝ) ^ (-σ) ≤ + ∏ p ∈ (y + 1).primesBelow, (1 - (p : ℝ) ^ (-σ))⁻¹ := by + calc ((Sm X y).card : ℝ) * (X : ℝ) ^ (-σ) = ∑ m ∈ Sm X y, (X : ℝ) ^ (-σ) := by + rw [sum_const, nsmul_eq_mul] + _ ≤ ∑ m ∈ Sm X y, (m : ℝ) ^ (-σ) := sum_le_sum h1 + _ ≤ _ := rankin_sum σ hσ y X + have h3 : (X : ℝ) ^ σ * (X : ℝ) ^ (-σ) = 1 := by + rw [← Real.rpow_add hXpos]; simp + calc ((Sm X y).card : ℝ) = ((Sm X y).card : ℝ) * ((X : ℝ) ^ σ * (X : ℝ) ^ (-σ)) := by + rw [h3, mul_one] + _ = (X : ℝ) ^ σ * (((Sm X y).card : ℝ) * (X : ℝ) ^ (-σ)) := by ring + _ ≤ _ := mul_le_mul_of_nonneg_left h2 (by positivity) + +/-- Each Euler factor with `σ = 1 / log y` is at most `exp (log y / log p)`. -/ +lemma factor_le {y p : ℕ} (hy : 2 ≤ y) (hp : 2 ≤ p) : + (1 - (p : ℝ) ^ (-(1 / log y)))⁻¹ ≤ exp (log y / log p) := by + have hly : 0 < log (y : ℝ) := log_pos (by exact_mod_cast (show 1 < y by omega)) + have hlp : 0 < log (p : ℝ) := log_pos (by exact_mod_cast (show 1 < p by omega)) + have hpos : (0 : ℝ) < p := by positivity + have : (p : ℝ) ^ (-(1 / log y)) = exp (-(log p / log y)) := by + rw [rpow_def_of_pos hpos]; congr 1; ring + rw [this] + have := inv_one_sub_exp_neg_le (div_pos hlp hly) + rwa [one_div_div] at this + +/-- Splitting the primes at `√y`. -/ +lemma sum_log_div_le (y : ℕ) (hy : 2 ≤ y) : + ∑ p ∈ (y + 1).primesBelow, log y / log p ≤ + 2 * (y + 1).primesBelow.card + Nat.sqrt y * (log y / log 2) := by + have hly : 0 < log (y : ℝ) := log_pos (by exact_mod_cast (show 1 < y by omega)) + have hl2 : 0 < log (2 : ℝ) := log_pos (by norm_num) + set P := (y + 1).primesBelow with hP + rw [← sum_filter_add_sum_filter_not P (fun p => p * p ≤ y)] + have hsmall : ∑ p ∈ P with p * p ≤ y, log y / log p ≤ Nat.sqrt y * (log y / log 2) := by + have hcard : (P.filter (fun p => p * p ≤ y)).card ≤ Nat.sqrt y := by + calc (P.filter (fun p => p * p ≤ y)).card ≤ (Icc 1 (Nat.sqrt y)).card := by + refine card_le_card fun p hp => ?_ + rw [mem_filter, hP, Nat.mem_primesBelow] at hp + exact mem_Icc.2 ⟨hp.1.2.one_lt.le, Nat.le_sqrt.2 hp.2⟩ + _ = Nat.sqrt y := by simp + calc ∑ p ∈ P with p * p ≤ y, log y / log p ≤ ∑ p ∈ P with p * p ≤ y, log y / log 2 := by + refine sum_le_sum fun p hp => ?_ + rw [mem_filter, hP, Nat.mem_primesBelow] at hp + exact div_le_div_of_nonneg_left hly.le hl2 + (log_le_log (by norm_num) (by exact_mod_cast hp.1.2.two_le)) + _ = (P.filter (fun p => p * p ≤ y)).card * (log y / log 2) := by + rw [sum_const, nsmul_eq_mul] + _ ≤ Nat.sqrt y * (log y / log 2) := + mul_le_mul_of_nonneg_right (by exact_mod_cast hcard) (by positivity) + have hbig : ∑ p ∈ P with ¬ p * p ≤ y, log y / log p ≤ 2 * P.card := by + calc ∑ p ∈ P with ¬ p * p ≤ y, log y / log p ≤ ∑ p ∈ P with ¬ p * p ≤ y, (2 : ℝ) := by + refine sum_le_sum fun p hp => ?_ + rw [mem_filter, hP, Nat.mem_primesBelow] at hp + have hp1 : (1 : ℝ) < p := by exact_mod_cast hp.1.2.one_lt + have hlp : 0 < log (p : ℝ) := log_pos hp1 + rw [div_le_iff₀ hlp] + have hyp : (y : ℝ) ≤ (p : ℝ) * p := by exact_mod_cast (not_le.1 hp.2).le + have := log_le_log (by positivity) hyp + rw [log_mul (by positivity) (by positivity)] at this + linarith + _ = 2 * (P.filter (fun p => ¬ p * p ≤ y)).card := by rw [sum_const, nsmul_eq_mul]; ring + _ ≤ 2 * P.card := by gcongr; exact filter_subset _ _ + linarith + +/-- The constant in the Rankin bound. -/ +noncomputable def C₀ : ℝ := 2 * (2 * log 4 + 2) + 16 / log 2 + +lemma C₀_pos : 0 < C₀ := by + have : 0 < log (4 : ℝ) := log_pos (by norm_num) + have : 0 < log (2 : ℝ) := log_pos (by norm_num) + unfold C₀; positivity + +lemma sum_log_div_le' (y : ℕ) (hy : 2 ≤ y) : + ∑ p ∈ (y + 1).primesBelow, log y / log p ≤ C₀ * (y / log y) := by + have hy1 : (1 : ℝ) < y := by exact_mod_cast (show 1 < y by omega) + have hl2 : 0 < log (2 : ℝ) := log_pos (by norm_num) + have h1 := sum_log_div_le y hy + have h2 := card_primesBelow_le y hy + have h3 : (Nat.sqrt y : ℝ) * (log y / log 2) ≤ 16 / log 2 * (y / log y) := by + calc (Nat.sqrt y : ℝ) * (log y / log 2) ≤ √(y : ℝ) * (log y / log 2) := + mul_le_mul_of_nonneg_right Real.nat_sqrt_le_real_sqrt + (div_nonneg (log_nonneg hy1.le) hl2.le) + _ = (√(y : ℝ) * log y) / log 2 := by ring + _ ≤ (16 * (y / log y)) / log 2 := div_le_div_of_nonneg_right (sqrt_mul_log_le hy1) hl2.le + _ = 16 / log 2 * (y / log y) := by ring + unfold C₀ + nlinarith + +/-- `|Sm (y ^ K) y| ≤ exp (K + C₀ y / log y)`. -/ +lemma card_Sm_le (y K : ℕ) (hy : 2 ≤ y) : + ((Sm (y ^ K) y).card : ℝ) ≤ exp (K + C₀ * (y / log y)) := by + have hy1 : (1 : ℝ) < y := by exact_mod_cast (show 1 < y by omega) + have hly : 0 < log (y : ℝ) := log_pos hy1 + set σ := 1 / log (y : ℝ) with hσdef + have hσ : 0 < σ := by positivity + have h1 := rankin_card σ hσ y (y ^ K) (pow_pos (by omega) K) + have h2 : ((y ^ K : ℕ) : ℝ) ^ σ = exp K := by + rw [Nat.cast_pow, rpow_def_of_pos (by positivity), log_pow, hσdef] + congr 1 + field_simp + have h3 : ∏ p ∈ (y + 1).primesBelow, (1 - (p : ℝ) ^ (-σ))⁻¹ ≤ + exp (∑ p ∈ (y + 1).primesBelow, log y / log p) := by + rw [exp_sum] + apply prod_le_prod₀ + · intro p hp + have hp1 : (1 : ℝ) < p := by exact_mod_cast (Nat.mem_primesBelow.1 hp).2.one_lt + have := Real.rpow_lt_one_of_one_lt_of_neg hp1 (show -σ < 0 by linarith) + exact inv_nonneg.2 (by linarith) + · intro p hp + exact factor_le hy (Nat.mem_primesBelow.1 hp).2.two_le + have h4 := sum_log_div_le' y hy + rw [h2] at h1 + calc ((Sm (y ^ K) y).card : ℝ) ≤ exp K * ∏ p ∈ (y + 1).primesBelow, (1 - (p : ℝ) ^ (-σ))⁻¹ := + h1 + _ ≤ exp K * exp (∑ p ∈ (y + 1).primesBelow, log y / log p) := + mul_le_mul_of_nonneg_left h3 (exp_pos _).le + _ = exp (K + ∑ p ∈ (y + 1).primesBelow, log y / log p) := (exp_add _ _).symm + _ ≤ exp (K + C₀ * (y / log y)) := exp_le_exp.2 (by linarith) + +/-! ### Pigeonhole: a block with many elements having long runs -/ + +lemma pigeon (f : ℕ → ℝ) (r : ℝ) (h0 : 1 ≤ f 0) (hr : 0 ≤ r) (K : ℕ) (hK : f K < r ^ K) : + ∃ i < K, f (i + 1) < r * f i := by + by_contra h + push Not at h + have : ∀ i ≤ K, r ^ i ≤ f i := by + intro i + induction i with + | zero => intro _; simpa using h0 + | succ i ih => + intro hi + calc r ^ (i + 1) = r * r ^ i := by ring + _ ≤ r * f i := mul_le_mul_of_nonneg_left (ih (by omega)) hr + _ ≤ f (i + 1) := h i (by omega) + exact absurd (this K le_rfl) (not_le.2 hK) + +/-- The block: for every `y ≥ 2` there are `G ⊆ B`, `|G| ≥ δ |B|`, `|B| ≤ exp (C₂ y / log y)`, +such that the first `y` multiples of every `a ∈ G` lie in `B`. -/ +lemma block : ∃ δ : ℝ, 0 < δ ∧ ∃ C₂ : ℝ, 0 < C₂ ∧ ∀ y : ℕ, 2 ≤ y → ∃ B G : Finset ℕ, + (∀ a ∈ B, 0 < a) ∧ G ⊆ B ∧ (∀ a ∈ G, ∀ j, 1 ≤ j → j ≤ y → j * a ∈ B) ∧ 0 < B.card ∧ + δ * B.card ≤ G.card ∧ (B.card : ℝ) ≤ exp (C₂ * (y / log y)) := by + have hC₀ := C₀_pos + refine ⟨exp (-(2 + C₀)), exp_pos _, 2 + C₀, by linarith, fun y hy => ?_⟩ + have hy1 : (1 : ℝ) < y := by exact_mod_cast (show 1 < y by omega) + have hly : 0 < log (y : ℝ) := log_pos hy1 + set Q := (y : ℝ) / log y with hQdef + have hQ1 : 1 < Q := by + rw [hQdef, one_lt_div hly] + linarith [log_le_sub_one_of_pos (show (0 : ℝ) < y by linarith)] + set K := ⌈Q⌉₊ with hKdef + have hKQ : Q ≤ K := Nat.le_ceil Q + have hKQ' : (K : ℝ) < Q + 1 := Nat.ceil_lt_add_one (by linarith) + have hKpos : (0 : ℝ) < K := by linarith + set f : ℕ → ℝ := fun i => ((Sm (y ^ i) y).card : ℝ) with hf + have hf0 : 1 ≤ f 0 := by + simp only [hf, pow_zero, Nat.one_le_cast] + exact card_pos.2 ⟨1, one_mem_Sm le_rfl⟩ + have hfK : f K ≤ exp ((2 + C₀) * Q) := by + refine (card_Sm_le y K hy).trans (exp_le_exp.2 ?_) + nlinarith + have hfK' : f K < exp (2 + C₀) ^ K := by + rw [← exp_nat_mul] + refine (card_Sm_le y K hy).trans_lt (exp_lt_exp.2 ?_) + nlinarith + obtain ⟨i, hiK, hi⟩ := pigeon f (exp (2 + C₀)) hf0 (exp_pos _).le K hfK' + have hmono : ∀ {i j : ℕ}, i ≤ j → Sm (y ^ i) y ⊆ Sm (y ^ j) y := + fun hij => Sm_mono (Nat.pow_le_pow_right (by omega) hij) + refine ⟨Sm (y ^ (i + 1)) y, Sm (y ^ i) y, fun a ha => pos_of_mem_Sm ha, + hmono (Nat.le_succ i), ?_, card_pos.2 ⟨1, one_mem_Sm (Nat.one_le_pow _ _ (by omega))⟩, ?_, ?_⟩ + · intro a ha j hj1 hjy + rw [pow_succ] + exact mul_mem_Sm ha hj1 hjy + · rw [exp_neg, inv_mul_le_iff₀ (exp_pos _)] + exact hi.le + · calc ((Sm (y ^ (i + 1)) y).card : ℝ) ≤ f K := by + simp only [hf] + exact_mod_cast card_le_card (hmono (by omega)) + _ ≤ _ := hfK + +/-! ### The lower bound -/ + +theorem lower_bound : ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ S : Finset ℕ, + (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ + c * n * Real.log n * Real.log (Real.log n) ≤ ((∑ a ∈ S, kVal S a : ℕ) : ℝ) := by + obtain ⟨δ, hδ, C₂, hC₂, hblock⟩ := block + exact lower_bound_of_block hδ hC₂ hblock + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/LowerEstimates.lean b/LeanPool/RunsOfMultiples/LowerEstimates.lean new file mode 100644 index 0000000000..203caba72b --- /dev/null +++ b/LeanPool/RunsOfMultiples/LowerEstimates.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import Mathlib.NumberTheory.Chebyshev + +/-! +# Analytic estimates for multiplicative block constructions + +Elementary logarithm and prime-count bounds used by both lower-bound constructions. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +lemma log_le_two_sqrt {x : ℝ} (hx : 1 ≤ x) : log x ≤ 2 * √x := by + have h1 : log √x = log x / 2 := log_sqrt (by linarith) + have h2 : log √x ≤ √x - 1 := log_le_sub_one_of_pos (sqrt_pos.2 (by linarith)) + linarith + +lemma log_sq_le {x : ℝ} (hx : 1 ≤ x) : log x ^ 2 ≤ 16 * √x := by + have hs : 1 ≤ √x := by rw [show (1:ℝ) = √1 by simp]; exact sqrt_le_sqrt hx + have h1 : log x = 4 * log √(√x) := by + rw [log_sqrt (sqrt_nonneg _), log_sqrt (by linarith)]; ring + have h2 : log √(√x) ≤ √(√x) - 1 := log_le_sub_one_of_pos (sqrt_pos.2 (by linarith)) + have h3 : √(√x) ^ 2 = √x := sq_sqrt (sqrt_nonneg _) + have h4 : 0 ≤ log √(√x) := log_nonneg (by rw [show (1:ℝ) = √1 by simp]; exact sqrt_le_sqrt hs) + have h5 : log √(√x) ^ 2 ≤ √(√x) ^ 2 := pow_le_pow_left₀ h4 (by linarith) 2 + rw [h1] + nlinarith + +lemma sqrt_le_div_log {x : ℝ} (hx : 1 < x) : √x ≤ 2 * (x / log x) := by + have hl : 0 < log x := log_pos hx + have h1 := log_le_two_sqrt hx.le + have h2 : √x * √x = x := mul_self_sqrt (by linarith) + rw [mul_div_assoc', le_div_iff₀ hl] + have : 0 ≤ √x := sqrt_nonneg _ + nlinarith + +lemma sqrt_mul_log_le {x : ℝ} (hx : 1 < x) : √x * log x ≤ 16 * (x / log x) := by + have hl : 0 < log x := log_pos hx + have h1 := log_sq_le hx.le + have h2 : √x * √x = x := mul_self_sqrt (by linarith) + rw [mul_div_assoc', le_div_iff₀ hl] + have : 0 ≤ √x := sqrt_nonneg _ + nlinarith + +/-- Chebyshev: `π(y) ≤ (2 log 4 + 2) y / log y`. -/ +lemma card_primesBelow_le (y : ℕ) (hy : 2 ≤ y) : + ((y + 1).primesBelow.card : ℝ) ≤ (2 * log 4 + 2) * (y / log y) := by + have hy1 : (1 : ℝ) < y := by exact_mod_cast (show 1 < y by omega) + have hly : 0 < log (y : ℝ) := log_pos hy1 + have h1 : (y + 1).primesBelow.card = Nat.primeCounting y := by + rw [Nat.primesBelow_card_eq_primeCounting']; rfl + have h2 := Chebyshev.pi_le_log4_mul_div hy1 + rw [Nat.floor_natCast, log_sqrt (by linarith)] at h2 + rw [h1] + have h3 := sqrt_le_div_log hy1 + have h4 : log 4 * (y : ℝ) / (log y / 2) = 2 * log 4 * (y / log y) := by + field_simp + linarith + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Main.lean b/LeanPool/RunsOfMultiples/Main.lean new file mode 100644 index 0000000000..e3bcdb4f30 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Main.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Primes +public import LeanPool.RunsOfMultiples.Lower + +/-! +# Main theorem + +For a finite set `S` of positive integers and `a ∈ S`, let `k(a) = kVal S a` be the least positive +integer `k` with `k * a ∉ S`. Then `max_{|S| = n} ∑_{a ∈ S} k(a) = Θ(n log n log log n)`: + +* `upper_bound` (`Primes.lean`, via the entropy argument in `Upper.lean`): every such `S` with + `|S| = n ≥ N` has `∑ k(a) ≤ C n log n log log n`; +* `lower_bound` (`Lower.lean`, smooth numbers): for every `n ≥ N` some such `S` with `|S| = n` has + `∑ k(a) ≥ c n log n log log n`. + +Lemma and equation numbers outside `Alt/` refer to `docs/runs-of-multiples.pdf`; `Alt/` contains a +second proof (`main_theorem_alt`) following `docs/first-missing-multiple.pdf`. +-/ + +@[expose] public section + +namespace RunsOfMultiples + +theorem main_theorem : + (∃ C : ℝ, ∃ N : ℕ, ∀ S : Finset ℕ, (∀ a ∈ S, 0 < a) → N ≤ S.card → + ((∑ a ∈ S, kVal S a : ℕ) : ℝ) ≤ + C * S.card * Real.log S.card * Real.log (Real.log S.card)) ∧ + (∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∃ S : Finset ℕ, (∀ a ∈ S, 0 < a) ∧ + S.card = n ∧ c * n * Real.log n * Real.log (Real.log n) ≤ ((∑ a ∈ S, kVal S a : ℕ) : ℝ)) := + ⟨upper_bound, lower_bound⟩ + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/OneStep.lean b/LeanPool/RunsOfMultiples/OneStep.lean new file mode 100644 index 0000000000..8a405b4545 --- /dev/null +++ b/LeanPool/RunsOfMultiples/OneStep.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Entropy + +/-! +# The one-step entropy lemma + +If `G ⊆ R` and multiplication by `q` maps `G` into `R`, raising a "level" function by one, +then the counting entropy of the level on `R` is at least `(|G|/2) log (2|R|/|G|)`. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +/-- `x ↦ x log (N/x)` is monotone on `(0, N/e]`. -/ +lemma mul_log_div_mono {a b N : ℝ} (ha : 0 < a) (hab : a ≤ b) (hbN : b * exp 1 ≤ N) : + a * log (N / a) ≤ b * log (N / b) := by + have hb : 0 < b := ha.trans_le hab + have hN : 0 < N := lt_of_lt_of_le (mul_pos hb (exp_pos 1)) hbN + have h1 : 1 ≤ log (N / b) := by + rw [le_log_iff_exp_le (div_pos hN hb), le_div_iff₀ hb] + linarith [mul_comm b (exp 1)] + have h2 : log (b / a) ≤ b / a - 1 := log_le_sub_one_of_pos (div_pos hb ha) + have h3 : log (N / a) = log (N / b) + log (b / a) := by + rw [← log_mul (div_pos hN hb).ne' (div_pos hb ha).ne'] + congr 1 + field_simp + have h4 : a * log (b / a) ≤ b - a := by + have := mul_le_mul_of_nonneg_left h2 ha.le + have e : a * (b / a - 1) = b - a := by field_simp + linarith + rw [h3] + nlinarith [mul_le_mul_of_nonneg_left h1 (sub_nonneg.2 hab)] + +/-- `x log (N/x) ≤ N/e`. -/ +lemma mul_log_div_le {x N : ℝ} (hx : 0 < x) (hN : 0 < N) : x * log (N / x) ≤ N * exp (-1) := by + have h := log_le_sub_one_of_pos (div_pos (div_pos hN hx) (exp_pos 1)) + rw [log_div (div_pos hN hx).ne' (exp_pos 1).ne', log_exp] at h + have h' : log (N / x) ≤ N / x / exp 1 := by linarith + calc x * log (N / x) ≤ x * (N / x / exp 1) := mul_le_mul_of_nonneg_left h' hx.le + _ = N * exp (-1) := by rw [exp_neg]; field_simp + +/-- `δ ≤ N log (N / (N - δ))` for `0 ≤ δ < N`. -/ +lemma le_mul_log_div_sub {δ N : ℝ} (hδ : 0 ≤ δ) (hδN : δ < N) : + δ ≤ N * log (N / (N - δ)) := by + have hN : 0 < N := lt_of_le_of_lt hδ hδN + have hNd : 0 < N - δ := by linarith + have h := log_le_sub_one_of_pos (div_pos hNd hN) + have e : log (N / (N - δ)) = - log ((N - δ) / N) := by + rw [← log_inv, inv_div] + rw [e] + have : (N - δ) / N - 1 = -(δ / N) := by field_simp; ring + rw [this] at h + have h' : δ / N ≤ -log ((N - δ) / N) := by linarith + calc δ = N * (δ / N) := by field_simp + _ ≤ N * -log ((N - δ) / N) := mul_le_mul_of_nonneg_left h' hN.le + +/-- **Lemma 3** (one-step entropy). -/ +theorem ent_ge_of_shift (R G : Finset ℕ) (lev : ℕ → ℕ) (q : ℕ) (hq : 0 < q) (hGR : G ⊆ R) + (hmap : ∀ m ∈ G, q * m ∈ R ∧ lev (q * m) = lev m + 1) (hG : G.Nonempty) : + (G.card : ℝ) / 2 * log (2 * R.card / G.card) ≤ ent R lev := by + have hR : R.Nonempty := hG.mono hGR + obtain ⟨j0, hj0, hmax⟩ := + exists_max_image R (fun m => (R.filter (fun x => lev x = lev m)).card) hR + set j := lev j0 with hj + set N := R.card with hNdef + set M := (R.filter (fun x => lev x = j)).card with hMdef + set δ := (R.filter (fun x => ¬ lev x = j)).card with hδdef + have hNMδ : M + δ = N := card_filter_add_card_filter_not _ + have hMpos : 0 < M := fibre_card_pos hj0 + -- (i) min-entropy bound + have hi : (N : ℝ) * log (N / M) ≤ ent R lev := by + unfold ent + have : (N : ℝ) * log (N / M) = ∑ m ∈ R, log ((N : ℝ) / M) := by + rw [sum_const, nsmul_eq_mul] + rw [this] + refine sum_le_sum fun m hm => ?_ + have hF : (0 : ℝ) < (R.filter (fun x => lev x = lev m)).card := by + exact_mod_cast fibre_card_pos hm + have hFM : ((R.filter (fun x => lev x = lev m)).card : ℝ) ≤ M := by + exact_mod_cast hmax m hm + have hMpos' : (0 : ℝ) < M := by exact_mod_cast hMpos + have hNpos : (0 : ℝ) < N := by exact_mod_cast card_pos.2 hR + exact log_le_log (div_pos hNpos hMpos') (div_le_div_of_nonneg_left hNpos.le hF hFM) + -- (iii) |G| ≤ 2 δ + have hiii : G.card ≤ 2 * δ := by + have h1 : (G.filter (fun x => ¬ lev x = j)).card ≤ δ := + card_le_card (filter_subset_filter _ hGR) + have h2 : (G.filter (fun x => lev x = j)).card ≤ δ := by + have hsub : (G.filter (fun x => lev x = j)).image (q * ·) ⊆ + R.filter (fun x => ¬ lev x = j) := by + intro y hy + rw [mem_image] at hy + obtain ⟨x, hx, rfl⟩ := hy + rw [mem_filter] at hx ⊢ + obtain ⟨hR', hlev⟩ := hmap x hx.1 + refine ⟨hR', ?_⟩ + rw [hlev, hx.2] + omega + have := card_le_card hsub + rwa [card_image_of_injective _ (mul_right_injective₀ hq.ne')] at this + have := card_filter_add_card_filter_not (s := G) (fun x => lev x = j) + omega + have hgpos : 0 < G.card := card_pos.2 hG + have hδpos : 0 < δ := by omega + -- (ii) bound from the off-`j` part + have hii : (δ : ℝ) * log (N / δ) ≤ ent R lev := by + unfold ent + have hδpos' : (0 : ℝ) < δ := by exact_mod_cast hδpos + have hNpos : (0 : ℝ) < N := by exact_mod_cast card_pos.2 hR + calc (δ : ℝ) * log (N / δ) + = ∑ m ∈ R.filter (fun x => ¬ lev x = j), log ((N : ℝ) / δ) := by + rw [sum_const, nsmul_eq_mul] + _ ≤ ∑ m ∈ R.filter (fun x => ¬ lev x = j), + log ((N : ℝ) / (R.filter (fun x => lev x = lev m)).card) := by + refine sum_le_sum fun m hm => ?_ + rw [mem_filter] at hm + have hF : (0 : ℝ) < (R.filter (fun x => lev x = lev m)).card := by + exact_mod_cast fibre_card_pos hm.1 + have hFδ : ((R.filter (fun x => lev x = lev m)).card : ℝ) ≤ δ := by + have : R.filter (fun x => lev x = lev m) ⊆ R.filter (fun x => ¬ lev x = j) := by + intro x hx + rw [mem_filter] at hx ⊢ + exact ⟨hx.1, by rw [hx.2]; exact hm.2⟩ + exact_mod_cast card_le_card this + exact log_le_log (div_pos hNpos hδpos') (div_le_div_of_nonneg_left hNpos.le hF hFδ) + _ ≤ ∑ m ∈ R, log ((N : ℝ) / (R.filter (fun x => lev x = lev m)).card) := + sum_le_sum_of_subset_of_nonneg (filter_subset _ _) + fun m hm _ => log_card_div_fibre_nonneg hm + -- conclude + have hg : (0 : ℝ) < G.card := by exact_mod_cast hgpos + have hNpos : (0 : ℝ) < N := by exact_mod_cast card_pos.2 hR + have hx : (0 : ℝ) < (G.card : ℝ) / 2 := by positivity + have hxδ : (G.card : ℝ) / 2 ≤ δ := by + have : (G.card : ℝ) ≤ 2 * δ := by exact_mod_cast hiii + linarith + have hrw : (G.card : ℝ) / 2 * log (2 * N / G.card) = + (G.card : ℝ) / 2 * log (N / (G.card / 2)) := by + congr 2 + field_simp + rw [hrw] + by_cases hcase : (δ : ℝ) * exp 1 ≤ N + · exact (mul_log_div_mono hx hxδ hcase).trans hii + · push Not at hcase + have hδN : (δ : ℝ) < N := by + have : (δ : ℕ) < N := by omega + exact_mod_cast this + have hMeq : (M : ℝ) = N - δ := by + have : ((M + δ : ℕ) : ℝ) = N := by exact_mod_cast hNMδ + push_cast at this + linarith + calc (G.card : ℝ) / 2 * log (N / (G.card / 2)) ≤ N * exp (-1) := mul_log_div_le hx hNpos + _ ≤ δ := by + rw [exp_neg] + rw [mul_inv_le_iff₀ (exp_pos 1)] + linarith + _ ≤ N * log (N / (N - δ)) := le_mul_log_div_sub (by positivity) hδN + _ = N * log (N / M) := by rw [hMeq] + _ ≤ ent R lev := hi + +/-- Weak form: every shifted element contributes `log 2 / 2`. -/ +theorem ent_ge_log_two (R G : Finset ℕ) (lev : ℕ → ℕ) (q : ℕ) (hq : 0 < q) (hGR : G ⊆ R) + (hmap : ∀ m ∈ G, q * m ∈ R ∧ lev (q * m) = lev m + 1) : + log 2 / 2 * G.card ≤ ent R lev := by + rcases G.eq_empty_or_nonempty with rfl | hG + · simpa using ent_nonneg R lev + have h := ent_ge_of_shift R G lev q hq hGR hmap hG + have hg : (0 : ℝ) < G.card := by exact_mod_cast card_pos.2 hG + have hGRc : (G.card : ℝ) ≤ R.card := by exact_mod_cast card_le_card hGR + have h2 : log 2 ≤ log (2 * R.card / G.card) := by + apply log_le_log two_pos + rw [le_div_iff₀ hg] + linarith + nlinarith + +/-- Sparse form: if `|G| √q ≤ |R|` then the entropy is at least `(|G|/4) log q`. -/ +theorem ent_ge_sparse (R G : Finset ℕ) (lev : ℕ → ℕ) (q : ℕ) (hq : 0 < q) (hGR : G ⊆ R) + (hmap : ∀ m ∈ G, q * m ∈ R ∧ lev (q * m) = lev m + 1) + (hsparse : (G.card : ℝ) * √(q : ℝ) ≤ R.card) : + (G.card : ℝ) / 4 * log q ≤ ent R lev := by + rcases G.eq_empty_or_nonempty with rfl | hG + · simpa using ent_nonneg R lev + have h := ent_ge_of_shift R G lev q hq hGR hmap hG + have hg : (0 : ℝ) < G.card := by exact_mod_cast card_pos.2 hG + have hq' : (0 : ℝ) < q := by exact_mod_cast hq + have hsq : 0 < √(q : ℝ) := Real.sqrt_pos.2 hq' + have h2 : log q / 2 ≤ log (2 * R.card / G.card) := by + rw [show log (q : ℝ) / 2 = log √(q : ℝ) by rw [Real.log_sqrt hq'.le]] + apply log_le_log hsq + rw [le_div_iff₀ hg] + nlinarith + nlinarith + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/PrimeEstimates.lean b/LeanPool/RunsOfMultiples/PrimeEstimates.lean new file mode 100644 index 0000000000..97d91d9f63 --- /dev/null +++ b/LeanPool/RunsOfMultiples/PrimeEstimates.lean @@ -0,0 +1,219 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.PrimeInput +public import Mathlib.NumberTheory.Chebyshev + +/-! +# Elementary prime estimates from Chebyshev bounds + +The lower theta bound and prime interval estimates use Mathlib without the entropy upper bound. +-/ + +@[expose] public section + +open Finset Real Chebyshev + +namespace RunsOfMultiples + +lemma primesUpTo_eq (m : ℕ) : primesUpTo m = Nat.primesLE m := by + ext p + simp [primesUpTo, Nat.mem_primesLE] + +lemma sum_primesUpTo_eq_theta (m : ℕ) : ∑ p ∈ primesUpTo m, log (p : ℝ) = θ m := by + rw [primesUpTo_eq, theta_eq_sum_primesLE_log] + +/-- `log x ≤ k x^(1/k)` for `x ≥ 0`, in the form we use. -/ +lemma log_le_mul_rpow {x ε : ℝ} (hx : 0 ≤ x) (hε : 0 < ε) : log x ≤ ε⁻¹ * x ^ ε := by + have := log_le_rpow_div hx hε + rwa [div_eq_inv_mul] at this + +lemma log_two_le_one : log (2 : ℝ) ≤ 1 := by + have := log_le_sub_one_of_pos (show (0 : ℝ) < 2 by norm_num) + linarith + +/-- Chebyshev lower bound in the form `θ(m) ≥ (log 2 / 2) m - C`. -/ +theorem theta_lower : ∃ C : ℝ, 0 ≤ C ∧ ∀ m : ℕ, log 2 / 2 * m - C ≤ θ m := by + have hl2 : 0 < log (2 : ℝ) := log_pos one_lt_two + set A : ℝ := (24 / log 2) ^ (4 : ℕ) with hA + refine ⟨log 2 / 2 * A + 1, by positivity, fun m => ?_⟩ + by_cases hm : (m : ℝ) < A + · have : log 2 / 2 * (m : ℝ) ≤ log 2 / 2 * A := by gcongr + have := theta_nonneg (m : ℝ) + linarith + push Not at hm + have hA1 : 1 ≤ A := by + rw [hA] + apply one_le_pow₀ + rw [le_div_iff₀ hl2] + linarith [log_two_le_one] + have hm1 : (1 : ℝ) ≤ m := hA1.trans hm + have hm0 : (0 : ℝ) < m := by linarith + set r : ℝ := (m : ℝ) ^ ((1 : ℝ) / 4) with hr + have hr0 : 0 ≤ r := by positivity + have hr1 : 1 ≤ r := one_le_rpow hm1 (by norm_num) + -- m = r^4 and √m = r^2 + have hm4 : (m : ℝ) = r ^ (4 : ℕ) := by + rw [hr, ← rpow_natCast, ← rpow_mul hm0.le] + norm_num + have hsq : √(m : ℝ) = r ^ (2 : ℕ) := by + rw [hm4, show (4 : ℕ) = 2 * 2 by rfl, pow_mul, sqrt_sq (by positivity)] + have hlogm : log (m : ℝ) ≤ 4 * r := by + have := log_le_mul_rpow hm0.le (show (0 : ℝ) < 1 / 4 by norm_num) + rw [← hr] at this + linarith [show ((1 : ℝ) / 4)⁻¹ = 4 by norm_num] + have hlogm1 : log ((m : ℝ) + 1) ≤ 1 + 4 * r := by + have h2m : (m : ℝ) + 1 ≤ 2 * m := by linarith + have := log_le_log (by linarith) h2m + rw [log_mul two_ne_zero hm0.ne'] at this + linarith [log_two_le_one] + -- r ≥ 24 / log 2 + have hr24 : 24 / log 2 ≤ r := by + have h1 : A ^ ((1 : ℝ) / 4) ≤ r := rpow_le_rpow (by positivity) hm (by norm_num) + have h2 : A ^ ((1 : ℝ) / 4) = 24 / log 2 := by + rw [hA, ← rpow_natCast, ← rpow_mul (by positivity)] + norm_num + linarith + have hθ := theta_ge m + have hlogm0 : 0 ≤ log (m : ℝ) := log_nonneg hm1 + -- error terms are at most 1 + 12 r^3 ≤ 1 + (log 2 / 2) m + have herr : log ((m : ℝ) + 1) + 2 * √(m : ℝ) * log m ≤ 1 + log 2 / 2 * m := by + have h1 : 2 * √(m : ℝ) * log m ≤ 8 * r ^ (3 : ℕ) := by + rw [hsq] + have := mul_le_mul_of_nonneg_left hlogm (show (0 : ℝ) ≤ 2 * r ^ (2 : ℕ) by positivity) + nlinarith only [this] + have h2 : r ≤ r ^ (3 : ℕ) := by + calc r = r ^ (1 : ℕ) := by simp + _ ≤ r ^ (3 : ℕ) := pow_le_pow_right₀ hr1 (by norm_num) + have h3 : 12 * r ^ (3 : ℕ) ≤ log 2 / 2 * m := by + rw [hm4] + have : 24 ≤ log 2 * r := by + rw [div_le_iff₀ hl2] at hr24 + linarith + have h3' : 0 ≤ r ^ (3 : ℕ) := by positivity + nlinarith only [mul_le_mul_of_nonneg_right this h3'] + linarith only [hlogm1, h1, h2, h3] + have hA0 : 0 ≤ log 2 / 2 * A := by positivity + linarith + +/-- At least `q^(3/4)` primes in `(q, 4q]` for large `q`. -/ +theorem many_primes : ∃ q₀ : ℕ, ∀ q : ℕ, q₀ ≤ q → + (q : ℝ) ^ ((3 : ℝ) / 4) ≤ (((Ioc q (4 * q)).filter Nat.Prime).card : ℝ) := by + have hl2 : 0 < log (2 : ℝ) := log_pos one_lt_two + set B : ℝ := (48 / log 2) ^ (8 : ℕ) with hB + refine ⟨⌈B⌉₊, fun q hq => ?_⟩ + have hqB : B ≤ q := (Nat.le_ceil B).trans (by exact_mod_cast hq) + have hB1 : 1 ≤ B := by + rw [hB] + apply one_le_pow₀ + rw [le_div_iff₀ hl2] + linarith [log_two_le_one] + have hq1 : (1 : ℝ) ≤ q := hB1.trans hqB + have hq0 : (0 : ℝ) < q := by linarith + set P := (Ioc q (4 * q)).filter Nat.Prime with hP + -- θ(4q) - θ(q) = ∑_{p ∈ P} log p ≤ |P| log (4q) + have hsplit : θ ((4 * q : ℕ) : ℝ) = θ (q : ℝ) + ∑ p ∈ P, log (p : ℝ) := by + rw [theta_eq_sum_primesLE_log, theta_eq_sum_primesLE_log] + have hsub : Nat.primesLE q ⊆ Nat.primesLE (4 * q) := Nat.primesLE_mono (by omega) + rw [← sum_sdiff hsub, add_comm] + congr 2 + ext p + simp only [mem_sdiff, Nat.mem_primesLE, hP, mem_filter, mem_Ioc] + constructor + · rintro ⟨⟨h1, h2⟩, h3⟩ + exact ⟨⟨by by_contra h; exact h3 ⟨by omega, h2⟩, h1⟩, h2⟩ + · rintro ⟨⟨h1, h2⟩, h3⟩ + exact ⟨⟨h2, h3⟩, fun h => by omega⟩ + have hPle : ∑ p ∈ P, log (p : ℝ) ≤ P.card * log (4 * q) := by + have : ∑ p ∈ P, log (p : ℝ) ≤ ∑ p ∈ P, log (4 * (q : ℝ)) := by + refine sum_le_sum fun p hp => ?_ + rw [hP, mem_filter, mem_Ioc] at hp + have hp0 : (0 : ℝ) < p := by exact_mod_cast hp.2.pos + exact log_le_log hp0 (by exact_mod_cast hp.1.2) + rwa [sum_const, nsmul_eq_mul] at this + have hlo := theta_ge (4 * q) + have hup := theta_le_log4_mul_x hq0.le + have hlog4 : log (4 : ℝ) = 2 * log 2 := by + rw [show (4 : ℝ) = 2 ^ (2 : ℕ) by norm_num, log_pow] + norm_num + push_cast at hlo hsplit + -- abbreviations + set r : ℝ := (q : ℝ) ^ ((1 : ℝ) / 8) with hr + have hr1 : 1 ≤ r := one_le_rpow hq1 (by norm_num) + have hq8 : (q : ℝ) = r ^ (8 : ℕ) := by + rw [hr, ← rpow_natCast, ← rpow_mul hq0.le] + norm_num + have hq34 : (q : ℝ) ^ ((3 : ℝ) / 4) = r ^ (6 : ℕ) := by + rw [hr, ← rpow_natCast, ← rpow_mul hq0.le] + norm_num + have hsq : √(4 * (q : ℝ)) = 2 * r ^ (4 : ℕ) := by + rw [hq8, show (8 : ℕ) = 4 * 2 by rfl, pow_mul, show (4 : ℝ) = 2 ^ (2 : ℕ) by norm_num, + ← mul_pow, sqrt_sq (by positivity)] + -- ℓ = log (8q) bounds both logarithms, and ℓ ≤ 16 r + set ℓ : ℝ := log (8 * (q : ℝ)) with hℓ + have hℓ1 : log (4 * (q : ℝ) + 1) ≤ ℓ := log_le_log (by positivity) (by linarith) + have hℓ2 : log (4 * (q : ℝ)) ≤ ℓ := log_le_log (by positivity) (by linarith) + have hl4q : 0 < log (4 * (q : ℝ)) := log_pos (by linarith) + have hℓr : ℓ ≤ 16 * r := by + have h := log_le_mul_rpow (show (0 : ℝ) ≤ 8 * q by positivity) + (show (0 : ℝ) < 1 / 8 by norm_num) + rw [mul_rpow (by norm_num) hq0.le, ← hr] at h + have h8 : (8 : ℝ) ^ ((1 : ℝ) / 8) ≤ 2 := by + rw [show (2 : ℝ) = ((2 : ℝ) ^ (8 : ℕ)) ^ ((1 : ℝ) / 8) by + rw [← rpow_natCast, ← rpow_mul (by norm_num)]; norm_num] + exact rpow_le_rpow (by norm_num) (by norm_num) (by norm_num) + have : ((1 : ℝ) / 8)⁻¹ = 8 := by norm_num + rw [this] at h + nlinarith only [h, h8, show (0 : ℝ) ≤ r by positivity] + have hr48 : 48 / log 2 ≤ r := by + have h1 : B ^ ((1 : ℝ) / 8) ≤ r := rpow_le_rpow (by positivity) hqB (by norm_num) + have h2 : B ^ ((1 : ℝ) / 8) = 48 / log 2 := by + rw [hB, ← rpow_natCast, ← rpow_mul (by positivity)] + norm_num + linarith + have hr48' : 48 ≤ log 2 * r := by + rw [div_le_iff₀ hl2] at hr48 + linarith + -- main inequality: |P| log(4q) ≥ 2 q log 2 - ℓ (1 + 4 r^4) ≥ r^6 ℓ ≥ r^6 log (4q) + have hmain : r ^ (6 : ℕ) * log (4 * (q : ℝ)) ≤ P.card * log (4 * (q : ℝ)) := by + have hℓ0 : 0 ≤ ℓ := hl4q.le.trans hℓ2 + have hsq' : 2 * √(4 * (q : ℝ)) * log (4 * (q : ℝ)) ≤ 4 * r ^ (4 : ℕ) * ℓ := by + rw [hsq] + have h := mul_le_mul_of_nonneg_left hℓ2 (show 0 ≤ 4 * r ^ (4 : ℕ) by positivity) + nlinarith only [h] + have hr46 : r ^ (4 : ℕ) ≤ r ^ (6 : ℕ) := pow_le_pow_right₀ hr1 (by norm_num) + have hr06 : 1 ≤ r ^ (6 : ℕ) := one_le_pow₀ hr1 + -- ℓ (1 + 4 r^4 + r^6) ≤ 6 r^6 ℓ ≤ 96 r^7 ≤ 2 log 2 · r^8 + have hbig : ℓ * (1 + 4 * r ^ (4 : ℕ) + r ^ (6 : ℕ)) ≤ 2 * log 2 * r ^ (8 : ℕ) := by + have e1 : ℓ * (1 + 4 * r ^ (4 : ℕ) + r ^ (6 : ℕ)) ≤ 6 * r ^ (6 : ℕ) * ℓ := by + have hsum : 1 + 4 * r ^ (4 : ℕ) + r ^ (6 : ℕ) ≤ 6 * r ^ (6 : ℕ) := by + linarith only [hr06, hr46] + nlinarith only [mul_le_mul_of_nonneg_left hsum hℓ0] + have e2 : 6 * r ^ (6 : ℕ) * ℓ ≤ 96 * r ^ (7 : ℕ) := by + have : 0 ≤ 6 * r ^ (6 : ℕ) := by positivity + have := mul_le_mul_of_nonneg_left hℓr this + nlinarith only [this] + have e3 : 96 * r ^ (7 : ℕ) ≤ 2 * log 2 * r ^ (8 : ℕ) := by + have h7 : 0 ≤ r ^ (7 : ℕ) := by positivity + have : r ^ (8 : ℕ) = r ^ (7 : ℕ) * r := by ring + rw [this] + nlinarith only [mul_le_mul_of_nonneg_right hr48' h7] + linarith + have hθ : 4 * (q : ℝ) * log 2 - log (4 * q + 1) - 2 * √(4 * (q : ℝ)) * log (4 * q) ≤ + θ (q : ℝ) + ∑ p ∈ P, log (p : ℝ) := by + rw [← hsplit]; exact hlo + rw [hlog4] at hup + have : r ^ (6 : ℕ) * log (4 * (q : ℝ)) ≤ r ^ (6 : ℕ) * ℓ := + mul_le_mul_of_nonneg_left hℓ2 (by positivity) + have hq8' : log 2 * (q : ℝ) = log 2 * r ^ (8 : ℕ) := by rw [hq8] + linarith only [hθ, hup, hPle, hℓ1, hsq', hbig, this, hq8'] + rw [hq34] + exact le_of_mul_le_mul_right hmain hl4q + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/PrimeInput.lean b/LeanPool/RunsOfMultiples/PrimeInput.lean new file mode 100644 index 0000000000..6d411ade18 --- /dev/null +++ b/LeanPool/RunsOfMultiples/PrimeInput.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import Mathlib.Analysis.SpecialFunctions.Pow.Real + +/-! +# Prime-counting hypotheses for runs of multiples + +Separating the numerical prime input lets the entropy and Chebyshev arguments compile independently. +-/ + +@[expose] public section + +open Finset Real + +namespace RunsOfMultiples + +/-- The primes `≤ m`. -/ +def primesUpTo (m : ℕ) : Finset ℕ := (range (m + 1)).filter Nat.Prime + +/-- Prime-number input for the upper bound. -/ +structure PrimeInput (K : ℕ) (c₁ C₁ : ℝ) (q₀ : ℕ) : Prop where + K_pos : 0 < K + c₁_pos : 0 < c₁ + C₁_nonneg : 0 ≤ C₁ + theta : ∀ m : ℕ, c₁ * m - C₁ ≤ ∑ p ∈ primesUpTo m, log p + gap : ∀ q : ℕ, q₀ ≤ q → + (q : ℝ) ^ ((3 : ℝ) / 4) ≤ (((Ioc q (K * q)).filter Nat.Prime).card : ℝ) + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Primes.lean b/LeanPool/RunsOfMultiples/Primes.lean new file mode 100644 index 0000000000..5630502d41 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Primes.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Upper +public import LeanPool.RunsOfMultiples.PrimeEstimates + +/-! +# The unconditional upper bound + +The Chebyshev estimates discharge every field of the prime-counting input. +-/ + +@[expose] public section + +open Finset Real + +namespace RunsOfMultiples + +/-- The prime-number input for the upper bound, with `K = 4`. -/ +theorem primeInput : ∃ C₁ q₀, PrimeInput 4 (log 2 / 2) C₁ q₀ := by + obtain ⟨C₁, hC₁, hθ⟩ := theta_lower + obtain ⟨q₀, hq₀⟩ := many_primes + exact ⟨C₁, q₀, { + K_pos := by norm_num + c₁_pos := by have := log_pos (one_lt_two : (1 : ℝ) < 2); positivity + C₁_nonneg := hC₁ + theta := fun m => by rw [sum_primesUpTo_eq_theta]; exact hθ m + gap := hq₀ }⟩ + +end RunsOfMultiples + +namespace RunsOfMultiples + +/-- **Upper bound.** `∑_{a ∈ S} k(a) = O(n log n log log n)` for sets `S` of `n` positive +integers. -/ +theorem upper_bound : ∃ C : ℝ, ∃ N : ℕ, ∀ S : Finset ℕ, (∀ a ∈ S, 0 < a) → N ≤ S.card → + ((∑ a ∈ S, kVal S a : ℕ) : ℝ) ≤ + C * S.card * Real.log S.card * Real.log (Real.log S.card) := by + obtain ⟨C₁, q₀, h⟩ := primeInput + exact upper_of_primeInput h + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Replication.lean b/LeanPool/RunsOfMultiples/Replication.lean new file mode 100644 index 0000000000..e5fceb2ae0 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Replication.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Defs +public import Mathlib.Algebra.Order.Monoid.Unbundled.Pow +public import Mathlib.Tactic.Ring + +/-! +# Replicating finite multiplicative blocks + +Disjoint dilates and padding preserve cardinality and a quantitative lower bound on runs. +-/ + +@[expose] public section + +open Finset + +namespace RunsOfMultiples + +/-! ### Replication of a block -/ + +lemma pow_mul_inj {M j j' a a' : ℕ} (ha : 0 < a) (ha' : 0 < a') (haM : a < M) (haM' : a' < M) + (h : M ^ j * a = M ^ j' * a') : j = j' ∧ a = a' := by + have hM : 0 < M := by omega + have key : ∀ {j j' a a' : ℕ}, 0 < a' → a < M → j < j' → M ^ j * a ≠ M ^ j' * a' := by + intro j j' a a' ha' haM hjj' h + obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_lt hjj' + have h' : M ^ j * a = M ^ j * (M ^ d * M * a') := by rw [h]; ring + have h2 := Nat.eq_of_mul_eq_mul_left (pow_pos hM j) h' + have h1 : 1 ≤ M ^ d := Nat.one_le_pow _ _ hM + have h3 : 1 * M * 1 ≤ M ^ d * M * a' := Nat.mul_le_mul (Nat.mul_le_mul h1 le_rfl) ha' + omega + rcases lt_trichotomy j j' with hlt | rfl | hgt + · exact absurd h (key ha' haM hlt) + · exact ⟨rfl, Nat.eq_of_mul_eq_mul_left (pow_pos hM j) h⟩ + · exact absurd h.symm (key ha haM' hgt) + +/-- Replication: from a block `B` with a subset `G` whose first `y` multiples lie in `B`, +build an `n`-element set of positive integers whose `kVal`-sum is at least +`⌊n / |B|⌋ · |G| · (y + 1)`. -/ +lemma replicate (B G : Finset ℕ) (y n : ℕ) (hB : ∀ a ∈ B, 0 < a) (hGB : G ⊆ B) + (hG : ∀ a ∈ G, ∀ j, 1 ≤ j → j ≤ y → j * a ∈ B) : + ∃ S : Finset ℕ, (∀ a ∈ S, 0 < a) ∧ S.card = n ∧ + n / B.card * G.card * (y + 1) ≤ ∑ a ∈ S, kVal S a := by + set M := B.sup id + 1 with hM + set t := n / B.card with ht + have hMpos : 0 < M := Nat.succ_pos _ + have hltM : ∀ a ∈ B, a < M := fun a ha => Nat.lt_succ_of_le (Finset.le_sup (f := id) ha) + set φ : ℕ × ℕ → ℕ := fun p => M ^ p.1 * p.2 with hφ + have hinj : Set.InjOn φ ↑(range t ×ˢ B) := by + rintro ⟨j, a⟩ hja ⟨j', a'⟩ hja' h + simp only [coe_product, coe_range, Set.mem_prod, Set.mem_Iio, mem_coe] at hja hja' + obtain ⟨h1, h2⟩ := pow_mul_inj (hB a hja.2) (hB a' hja'.2) (hltM a hja.2) (hltM a' hja'.2) h + exact Prod.ext h1 h2 + set T := (range t ×ˢ B).image φ with hT + set G' := (range t ×ˢ G).image φ with hG' + have hTcard : T.card ≤ n := by + refine card_image_le.trans ?_ + rw [card_product, card_range] + exact Nat.div_mul_le_self n B.card + have hUcard : n ≤ (T ∪ Icc 1 n).card := by + have := card_le_card (subset_union_right (s₁ := T) (s₂ := Icc 1 n)) + simpa using this + obtain ⟨S, hTS, hSU, hScard⟩ := exists_subsuperset_card_eq subset_union_left hTcard hUcard + have hTpos : ∀ x ∈ T, 0 < x := by + intro x hx + obtain ⟨⟨j, a⟩, hja, rfl⟩ := mem_image.1 hx + rw [mem_product] at hja + exact Nat.mul_pos (pow_pos hMpos j) (hB a hja.2) + have hSpos : ∀ a ∈ S, 0 < a := by + intro a ha + rcases mem_union.1 (hSU ha) with h | h + · exact hTpos a h + · exact (mem_Icc.1 h).1 + have hG'T : G' ⊆ T := image_subset_image (product_subset_product_right hGB) + have hk : ∀ x ∈ G', y + 1 ≤ kVal S x := by + intro x hx + obtain ⟨⟨j, a⟩, hja, rfl⟩ := mem_image.1 hx + rw [mem_product] at hja + have hxpos : 0 < φ (j, a) := hTpos _ (hG'T hx) + have := (forall_mul_mem_iff S hxpos y).1 (fun i hi => by + rw [mem_Icc] at hi + refine hTS (mem_image.2 ⟨(j, i * a), mem_product.2 ⟨hja.1, hG a hja.2 i hi.1 hi.2⟩, ?_⟩) + simp only [hφ] + ring) + omega + have hG'card : G'.card = t * G.card := by + rw [card_image_of_injOn (hinj.mono (coe_subset.2 (product_subset_product_right hGB))), + card_product, card_range] + refine ⟨S, hSpos, hScard, ?_⟩ + calc t * G.card * (y + 1) = ∑ x ∈ G', (y + 1) := by rw [sum_const, nsmul_eq_mul, hG'card]; rfl + _ ≤ ∑ x ∈ G', kVal S x := sum_le_sum hk + _ ≤ ∑ x ∈ S, kVal S x := sum_le_sum_of_subset (hG'T.trans hTS) + +end RunsOfMultiples diff --git a/LeanPool/RunsOfMultiples/Upper.lean b/LeanPool/RunsOfMultiples/Upper.lean new file mode 100644 index 0000000000..ace4988654 --- /dev/null +++ b/LeanPool/RunsOfMultiples/Upper.lean @@ -0,0 +1,381 @@ +/- +Copyright (c) 2026 Jason Hoelscher-Obermaier. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 +-/ +module + +-- Adapted for Lean Pool: module visibility, imports, and proof organization. + +public import LeanPool.RunsOfMultiples.Edges +public import LeanPool.RunsOfMultiples.PrimeInput +public import Mathlib.Analysis.SpecialFunctions.Pow.Real + +/-! +# The upper bound + +The main argument, with the two prime-number inputs (a Chebyshev lower bound for `θ` and a +lower bound for the number of primes in `(q, K q]`) taken as the hypothesis `PrimeInput`. +These are discharged from Mathlib's `Chebyshev` file in `Primes.lean`. +-/ + +open Finset Real + +@[expose] public section + +namespace RunsOfMultiples + +lemma card_le_sup (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : S.card ≤ S.sup id := by + have : S ⊆ Icc 1 (S.sup id) := fun a ha => + mem_Icc.2 ⟨hS a ha, le_sup (f := id) ha⟩ + simpa using card_le_card this + +lemma card_mul_log_le {T S : Finset ℕ} (hTS : T ⊆ S) : + (T.card : ℝ) * log T.card ≤ T.card * log S.card := by + rcases Nat.eq_zero_or_pos T.card with h | h + · simp [h] + · have h' : (0 : ℝ) < T.card := by exact_mod_cast h + exact mul_le_mul_of_nonneg_left (log_le_log h' (by exact_mod_cast card_le_card hTS)) h'.le + +/-- The per-fibre estimate: weight `log q` on the pairs `(a, q)` with `a ∈ A (K q)`. -/ +lemma fibre_bound (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K : ℕ} (hK : 1 ≤ K) {q₀ : ℕ} + (hgap : ∀ q : ℕ, q₀ ≤ q → + (q : ℝ) ^ ((3 : ℝ) / 4) ≤ (((Ioc q (K * q)).filter Nat.Prime).card : ℝ)) + {Q₀ : ℝ} (hQ₀1 : 1 ≤ Q₀) (hQ₀q₀ : (q₀ : ℝ) ≤ Q₀) + (hQ₀ : ∀ q : ℕ, Q₀ ≤ q → log q * log S.card ≤ (q : ℝ) ^ ((1 : ℝ) / 4)) + {q : ℕ} (hq : q.Prime) (c : ℕ →₀ ℕ) : + log q * ((A S (K * q)).filter (fun m => key q m = c)).card ≤ + (log Q₀ + 2 / log 2) * ((A S q).filter (fun m => key q m = c)).card + + 4 * ent (S.filter (fun m => key q m = c)) (fun m => m.factorization q) := by + set T := S.filter (fun m => key q m = c) with hTdef + set G := (A S q).filter (fun m => key q m = c) with hGdef + set H := (A S (K * q)).filter (fun m => key q m = c) with hHdef + have hTpos : ∀ m ∈ T, 0 < m := fun m hm => hS m (mem_filter.1 hm).1 + have hHG : H ⊆ G := filter_subset_filter _ (A_anti S (Nat.le_mul_of_pos_left q hK)) + have hGT : G ⊆ T := filter_subset_filter _ (A_subset S q) + have hmapG : ∀ m ∈ G, q * m ∈ T ∧ (q * m).factorization q = m.factorization q + 1 := by + intro m hm + rw [mem_filter] at hm + have hmS : m ∈ S := A_subset S q hm.1 + refine ⟨?_, factorization_prime_mul_self hq (hS m hmS).ne'⟩ + rw [mem_filter] + exact ⟨mul_mem_of_mem_A hm.1 hq.one_le le_rfl, + by rw [key_prime_mul hq le_rfl (hS m hmS).ne', hm.2]⟩ + have hent : 0 ≤ ent T (fun m => m.factorization q) := ent_nonneg _ _ + have hq1 : (1 : ℝ) ≤ q := by exact_mod_cast hq.one_le + have hqpos : (0 : ℝ) < q := by linarith + have hlogq : 0 ≤ log (q : ℝ) := log_nonneg hq1 + have hlog2 : 0 < log (2 : ℝ) := log_pos one_lt_two + have hlogQ₀ : 0 ≤ log Q₀ := log_nonneg hQ₀1 + have hHGc : (H.card : ℝ) ≤ G.card := by exact_mod_cast card_le_card hHG + have hc2 : 0 ≤ 2 / log (2 : ℝ) := by positivity + have hGc : (0 : ℝ) ≤ G.card := by positivity + by_cases hsmall : (q : ℝ) < Q₀ + · -- small primes + have : log (q : ℝ) ≤ log Q₀ := log_le_log hqpos hsmall.le + calc log q * (H.card : ℝ) ≤ log Q₀ * G.card := + mul_le_mul this hHGc (by positivity) hlogQ₀ + _ ≤ _ := by nlinarith only [mul_nonneg hc2 hGc, hent] + push Not at hsmall + by_cases hsparse : (G.card : ℝ) * √(q : ℝ) ≤ T.card + · -- sparse fibre: pure entropy + have := ent_ge_sparse T G (fun m => m.factorization q) q hq.pos hGT hmapG hsparse + calc log q * (H.card : ℝ) ≤ log q * G.card := mul_le_mul_of_nonneg_left hHGc hlogq + _ ≤ 4 * ent T (fun m => m.factorization q) := by linarith + _ ≤ _ := by nlinarith only [mul_nonneg (add_nonneg hlogQ₀ hc2) hGc] + · -- dense fibre: runs past `K q` are rare + push Not at hsparse + set P := (Ioc q (K * q)).filter Nat.Prime with hPdef + have hedge := edge_bound T hTpos P (fun p hp => (mem_filter.1 hp).2) (fun _ => H) + (fun _ _ => hHG.trans hGT) (by + intro p hp m hm + rw [mem_filter, mem_Ioc] at hp + have hmS : m ∈ S := A_subset S _ (mem_filter.1 hm).1 + rw [mem_filter] + refine ⟨mul_mem_of_mem_A (mem_filter.1 hm).1 hp.2.one_le hp.1.2, ?_⟩ + rw [key_prime_mul hp.2 hp.1.1.le (hS m hmS).ne', (mem_filter.1 hm).2]) + simp only [sum_const, nsmul_eq_mul] at hedge + have hT1 := card_mul_log_le (filter_subset (fun m => key q m = c) S) + have hq₀q : q₀ ≤ q := by + have : (q₀ : ℝ) ≤ q := hQ₀q₀.trans hsmall + exact_mod_cast this + have hP := hgap q hq₀q + have hlogn : 0 ≤ log (S.card : ℝ) := by + rcases Nat.eq_zero_or_pos S.card with h | h + · simp [h] + · exact log_nonneg (by exact_mod_cast h) + have hq34 : (0 : ℝ) < (q : ℝ) ^ ((3 : ℝ) / 4) := rpow_pos_of_pos hqpos _ + have hsq : √(q : ℝ) * (q : ℝ) ^ ((1 : ℝ) / 4) = (q : ℝ) ^ ((3 : ℝ) / 4) := by + rw [sqrt_eq_rpow, ← rpow_add hqpos] + norm_num + have hsqpos : 0 ≤ √(q : ℝ) := sqrt_nonneg _ + have hHc : (0 : ℝ) ≤ H.card := by positivity + -- (log 2 / 2) q^(3/4) |H| ≤ √q |G| log n + have key1 : log 2 / 2 * ((q : ℝ) ^ ((3 : ℝ) / 4) * H.card) ≤ + G.card * √(q : ℝ) * log S.card := by + calc log 2 / 2 * ((q : ℝ) ^ ((3 : ℝ) / 4) * H.card) + ≤ log 2 / 2 * ((P.card : ℝ) * H.card) := by gcongr + _ ≤ T.card * log T.card := hedge + _ ≤ T.card * log S.card := hT1 + _ ≤ G.card * √(q : ℝ) * log S.card := mul_le_mul_of_nonneg_right hsparse.le hlogn + -- multiply by `log q` and use `log q log n ≤ q^(1/4)` + have key2 : log 2 / 2 * ((q : ℝ) ^ ((3 : ℝ) / 4) * (log q * H.card)) ≤ + G.card * (q : ℝ) ^ ((3 : ℝ) / 4) := by + have h1 := mul_le_mul_of_nonneg_left key1 hlogq + have h2 : G.card * √(q : ℝ) * (log q * log S.card) ≤ + G.card * √(q : ℝ) * (q : ℝ) ^ ((1 : ℝ) / 4) := + mul_le_mul_of_nonneg_left (hQ₀ q hsmall) (by positivity) + calc log 2 / 2 * ((q : ℝ) ^ ((3 : ℝ) / 4) * (log q * H.card)) + = log q * (log 2 / 2 * ((q : ℝ) ^ ((3 : ℝ) / 4) * H.card)) := by ring + _ ≤ log q * (G.card * √(q : ℝ) * log S.card) := h1 + _ = G.card * √(q : ℝ) * (log q * log S.card) := by ring + _ ≤ G.card * √(q : ℝ) * (q : ℝ) ^ ((1 : ℝ) / 4) := h2 + _ = G.card * (q : ℝ) ^ ((3 : ℝ) / 4) := by rw [mul_assoc, hsq] + have key3 : log 2 / 2 * (log q * H.card) ≤ G.card := by + have : (q : ℝ) ^ ((3 : ℝ) / 4) * (log 2 / 2 * (log q * H.card)) ≤ + (q : ℝ) ^ ((3 : ℝ) / 4) * G.card := by + calc (q : ℝ) ^ ((3 : ℝ) / 4) * (log 2 / 2 * (log q * H.card)) + = log 2 / 2 * ((q : ℝ) ^ ((3 : ℝ) / 4) * (log q * H.card)) := by ring + _ ≤ G.card * (q : ℝ) ^ ((3 : ℝ) / 4) := key2 + _ = (q : ℝ) ^ ((3 : ℝ) / 4) * G.card := by ring + exact le_of_mul_le_mul_left this hq34 + have key4 : log q * (H.card : ℝ) ≤ 2 / log 2 * G.card := by + rw [div_mul_eq_mul_div, le_div_iff₀ hlog2] + linarith only [key3] + nlinarith only [key4, hent, mul_nonneg hlogQ₀ hGc] + +/-- Summing the fibre estimate over the fibres of the `q`-smooth part. -/ +lemma prime_bound (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K : ℕ} (hK : 1 ≤ K) {q₀ : ℕ} + (hgap : ∀ q : ℕ, q₀ ≤ q → + (q : ℝ) ^ ((3 : ℝ) / 4) ≤ (((Ioc q (K * q)).filter Nat.Prime).card : ℝ)) + {Q₀ : ℝ} (hQ₀1 : 1 ≤ Q₀) (hQ₀q₀ : (q₀ : ℝ) ≤ Q₀) + (hQ₀ : ∀ q : ℕ, Q₀ ≤ q → log q * log S.card ≤ (q : ℝ) ^ ((1 : ℝ) / 4)) + {q : ℕ} (hq : q.Prime) : + log q * (A S (K * q)).card ≤ (log Q₀ + 2 / log 2) * (A S q).card + 4 * D S q := by + have hfib : ∀ t : ℕ, ((A S t).card : ℝ) = + ∑ c ∈ S.image (key q), (((A S t).filter (fun m => key q m = c)).card : ℝ) := by + intro t + rw [← Nat.cast_sum, card_eq_sum_card_fiberwise (f := key q)] + intro m hm + exact mem_image_of_mem _ (A_subset S t hm) + rw [hfib, hfib, D, mul_sum, mul_sum, mul_sum, ← sum_add_distrib] + exact sum_le_sum fun c _ => fibre_bound S hS hK hgap hQ₀1 hQ₀q₀ hQ₀ hq c + +/-- Double counting: `∑_q log q |A (K q)| = ∑_a θ(L a / K)`. -/ +lemma double_count (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K : ℕ} (hK : 0 < K) : + ∑ q ∈ (range (S.sup id + 1)).filter Nat.Prime, log q * ((A S (K * q)).card : ℝ) = + ∑ a ∈ S, ∑ p ∈ primesUpTo (L S a / K), log p := by + have h1 : ∀ q : ℕ, log (q : ℝ) * ((A S (K * q)).card : ℝ) = + ∑ a ∈ S, if a ∈ A S (K * q) then log (q : ℝ) else 0 := by + intro q + have hA : S.filter (fun a => a ∈ A S (K * q)) = A S (K * q) := by + ext a + simp only [mem_filter] + exact ⟨fun h => h.2, fun h => ⟨A_subset S _ h, h⟩⟩ + rw [← sum_filter, hA, sum_const, nsmul_eq_mul, mul_comm] + simp_rw [h1] + rw [sum_comm] + refine sum_congr rfl fun a ha => ?_ + rw [← sum_filter] + congr 1 + ext p + simp only [mem_filter, mem_range, primesUpTo, mem_A_iff S hS] + have hLn := L_le_card S hS ha + have hnB := card_le_sup S hS + constructor + · rintro ⟨⟨_, hp⟩, -, hpL⟩ + exact ⟨by rw [Nat.lt_succ_iff, Nat.le_div_iff_mul_le hK, mul_comm]; exact hpL, hp⟩ + · rintro ⟨hpL, hp⟩ + rw [Nat.lt_succ_iff, Nat.le_div_iff_mul_le hK] at hpL + refine ⟨⟨?_, hp⟩, ha, by rw [mul_comm]; exact hpL⟩ + have : p ≤ L S a := le_trans (Nat.le_mul_of_pos_right p hK) hpL + omega + +/-- The explicit form of the upper bound. -/ +theorem upper_core (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) {K q₀ : ℕ} {c₁ C₁ : ℝ} + (hPI : PrimeInput K c₁ C₁ q₀) {Q₀ : ℝ} (hQ₀1 : 1 ≤ Q₀) (hQ₀q₀ : (q₀ : ℝ) ≤ Q₀) + (hQ₀ : ∀ q : ℕ, Q₀ ≤ q → log q * log S.card ≤ (q : ℝ) ^ ((1 : ℝ) / 4)) : + c₁ / K * ∑ a ∈ S, (L S a : ℝ) ≤ + (log Q₀ + 2 / log 2) * (2 / log 2) * (S.card * log S.card) + + 4 * (S.card * log S.card) + (c₁ + C₁) * S.card := by + have hK : 1 ≤ K := hPI.K_pos + set B := S.sup id + 1 + set PB := (range B).filter Nat.Prime + have hSB : ∀ m ∈ S, m < B := fun m hm => Nat.lt_succ_of_le (le_sup (f := id) hm) + have hlog2 : 0 < log (2 : ℝ) := log_pos one_lt_two + have hc : 0 ≤ log Q₀ + 2 / log 2 := by + have := log_nonneg hQ₀1 + positivity + -- ∑_q |A q| ≤ (2 / log 2) n log n + have hedge := edge_bound S hS PB (fun p hp => (mem_filter.1 hp).2) (fun q => A S q) + (fun q _ => A_subset S q) + (fun q hq m hm => mul_mem_of_mem_A hm (mem_filter.1 hq).2.one_le le_rfl) + have hsumA : ∑ q ∈ PB, ((A S q).card : ℝ) ≤ 2 / log 2 * (S.card * log S.card) := by + rw [div_mul_eq_mul_div, le_div_iff₀ hlog2] + linarith only [hedge] + have hsumD : ∑ q ∈ PB, D S q ≤ S.card * log S.card := + sum_D_le S hS hSB PB (filter_subset _ _) + -- the weighted sum + have hPhi : ∑ q ∈ PB, log q * ((A S (K * q)).card : ℝ) ≤ + (log Q₀ + 2 / log 2) * (2 / log 2) * (S.card * log S.card) + + 4 * (S.card * log S.card) := by + calc ∑ q ∈ PB, log q * ((A S (K * q)).card : ℝ) + ≤ ∑ q ∈ PB, ((log Q₀ + 2 / log 2) * (A S q).card + 4 * D S q) := + sum_le_sum fun q hq => prime_bound S hS hK hPI.gap hQ₀1 hQ₀q₀ hQ₀ (mem_filter.1 hq).2 + _ = (log Q₀ + 2 / log 2) * ∑ q ∈ PB, ((A S q).card : ℝ) + 4 * ∑ q ∈ PB, D S q := by + rw [sum_add_distrib, mul_sum, mul_sum] + _ ≤ _ := by + have := mul_le_mul_of_nonneg_left hsumA hc + nlinarith only [this, hsumD] + rw [double_count S hS hPI.K_pos] at hPhi + -- θ lower bound for each element + have hKpos : (0 : ℝ) < K := by exact_mod_cast hPI.K_pos + have helt : ∀ a ∈ S, c₁ / K * (L S a : ℝ) - (c₁ + C₁) ≤ + ∑ p ∈ primesUpTo (L S a / K), log p := by + intro a _ + have ht := hPI.theta (L S a / K) + have hdiv : (L S a : ℝ) / K - 1 ≤ ((L S a / K : ℕ) : ℝ) := by + have h := Nat.div_add_mod (L S a) K + have hmod := Nat.mod_lt (L S a) hPI.K_pos + have h' : (L S a : ℝ) = K * ((L S a / K : ℕ) : ℝ) + ((L S a % K : ℕ) : ℝ) := by + exact_mod_cast h.symm + have hmod' : ((L S a % K : ℕ) : ℝ) < K := by exact_mod_cast hmod + rw [div_sub_one hKpos.ne', div_le_iff₀ hKpos] + linarith only [h', hmod'] + have hc₁ := hPI.c₁_pos + calc c₁ / K * (L S a : ℝ) - (c₁ + C₁) = c₁ * ((L S a : ℝ) / K - 1) - C₁ := by + field_simp + ring + _ ≤ c₁ * ((L S a / K : ℕ) : ℝ) - C₁ := by gcongr + _ ≤ _ := ht + have hsum := sum_le_sum helt + rw [sum_sub_distrib, sum_const, nsmul_eq_mul, ← mul_sum] at hsum + linarith only [hsum, hPhi] + +/-- The upper bound in asymptotic form, given the prime-number input. -/ +theorem upper_of_primeInput {K q₀ : ℕ} {c₁ C₁ : ℝ} (hPI : PrimeInput K c₁ C₁ q₀) : + ∃ C : ℝ, ∃ N : ℕ, ∀ S : Finset ℕ, (∀ a ∈ S, 0 < a) → N ≤ S.card → + ((∑ a ∈ S, kVal S a : ℕ) : ℝ) ≤ + C * S.card * log S.card * log (log S.card) := by + set M₀ : ℝ := max (q₀ : ℝ) ((2 : ℝ) ^ (64 : ℕ)) with hM₀ + -- eventually: (log n)^8 ≥ M₀ and log log n ≥ 1 + have hev : ∀ᶠ n : ℕ in Filter.atTop, M₀ ≤ (log n) ^ (8 : ℕ) ∧ 1 ≤ log (log n) := by + have hlog : Filter.Tendsto (fun n : ℕ => log (n : ℝ)) Filter.atTop Filter.atTop := + tendsto_log_atTop.comp tendsto_natCast_atTop_atTop + have h8 : Filter.Tendsto (fun n : ℕ => (log (n : ℝ)) ^ (8 : ℕ)) Filter.atTop Filter.atTop := + (Filter.tendsto_pow_atTop (by norm_num)).comp hlog + have hll : Filter.Tendsto (fun n : ℕ => log (log (n : ℝ))) Filter.atTop Filter.atTop := + tendsto_log_atTop.comp hlog + exact (h8.eventually_ge_atTop M₀).and (hll.eventually_ge_atTop 1) + obtain ⟨N, hN⟩ := Filter.eventually_atTop.1 hev + have hlog2 : 0 < log (2 : ℝ) := log_pos one_lt_two + have hc₁ := hPI.c₁_pos + have hC₁ := hPI.C₁_nonneg + have hKpos : (0 : ℝ) < K := by exact_mod_cast hPI.K_pos + refine ⟨1 + K / c₁ * ((8 + 2 / log 2) * (2 / log 2) + 4 + c₁ + C₁), N, fun S hS hSN => ?_⟩ + obtain ⟨hM, hLL⟩ := hN S.card hSN + set n : ℝ := (S.card : ℝ) with hn + set Lg := log n with hLg + set LL := log Lg with hLL' + have hLg0 : 0 ≤ Lg := by rw [hLg, hn]; exact log_natCast_nonneg _ + have hLg1 : 1 ≤ Lg := by + by_contra h + push Not at h + have : log Lg ≤ 0 := log_nonpos hLg0 h.le + linarith + have hnpos : 1 ≤ n := by + by_contra h + push Not at h + have : Lg ≤ 0 := log_nonpos (by positivity) h.le + linarith + -- choose Q₀ = (log n)^8 + set Q₀ : ℝ := Lg ^ (8 : ℕ) with hQ₀def + have hQ₀1 : 1 ≤ Q₀ := one_le_pow₀ hLg1 + have hQ₀M : M₀ ≤ Q₀ := hM + have hQ₀q₀ : (q₀ : ℝ) ≤ Q₀ := (le_max_left _ _).trans hQ₀M + have hQ₀big : (2 : ℝ) ^ (64 : ℕ) ≤ Q₀ := (le_max_right _ _).trans hQ₀M + have hQ₀ : ∀ q : ℕ, Q₀ ≤ q → log q * log S.card ≤ (q : ℝ) ^ ((1 : ℝ) / 4) := by + intro q hq + have hqpos : (0 : ℝ) < q := lt_of_lt_of_le (by positivity) hq + -- log q ≤ q^(1/8) + have hlq : log (q : ℝ) ≤ (q : ℝ) ^ ((1 : ℝ) / 8) := by + have h1 := log_le_rpow_div hqpos.le (show (0 : ℝ) < 1 / 16 by norm_num) + have h2 : (16 : ℝ) ≤ (q : ℝ) ^ ((1 : ℝ) / 16) := by + have : (16 : ℝ) = ((2 : ℝ) ^ (64 : ℕ)) ^ ((1 : ℝ) / 16) := by + rw [← rpow_natCast, ← rpow_mul (by norm_num)] + norm_num + calc (16 : ℝ) = ((2 : ℝ) ^ (64 : ℕ)) ^ ((1 : ℝ) / 16) := this + _ ≤ (q : ℝ) ^ ((1 : ℝ) / 16) := + rpow_le_rpow (by norm_num) (hQ₀big.trans hq) (by norm_num) + have h3 : (q : ℝ) ^ ((1 : ℝ) / 8) = (q : ℝ) ^ ((1 : ℝ) / 16) * (q : ℝ) ^ ((1 : ℝ) / 16) := by + rw [← rpow_add hqpos] + norm_num + have h4 : 0 ≤ (q : ℝ) ^ ((1 : ℝ) / 16) := by positivity + rw [h3] + calc log (q : ℝ) ≤ (q : ℝ) ^ ((1 : ℝ) / 16) / (1 / 16) := h1 + _ = 16 * (q : ℝ) ^ ((1 : ℝ) / 16) := by ring + _ ≤ _ := by nlinarith + -- log n ≤ q^(1/8) + have hln : log (S.card : ℝ) ≤ (q : ℝ) ^ ((1 : ℝ) / 8) := by + have : Lg = (Lg ^ (8 : ℕ)) ^ ((1 : ℝ) / 8) := by + rw [← rpow_natCast, ← rpow_mul (by linarith)] + norm_num + rw [← hn, ← hLg, this] + exact rpow_le_rpow (by positivity) hq (by norm_num) + have hlq0 : 0 ≤ log (q : ℝ) := by + apply log_nonneg + have : (1 : ℝ) ≤ Q₀ := hQ₀1 + linarith + have hsplit : (q : ℝ) ^ ((1 : ℝ) / 4) = + (q : ℝ) ^ ((1 : ℝ) / 8) * (q : ℝ) ^ ((1 : ℝ) / 8) := by + rw [← rpow_add hqpos] + norm_num + rw [hsplit] + exact mul_le_mul hlq hln (by rw [← hn, ← hLg]; linarith) (by positivity) + have hcore := upper_core S hS hPI hQ₀1 hQ₀q₀ hQ₀ + have hlogQ₀ : log Q₀ = 8 * LL := by + rw [hQ₀def, log_pow, hLL'] + push_cast + ring + rw [hlogQ₀] at hcore + -- ∑ kVal = n + ∑ L + have hk := sum_kVal_eq S hS + have hk' : ((∑ a ∈ S, kVal S a : ℕ) : ℝ) = n + ∑ a ∈ S, (L S a : ℝ) := by + rw [hk] + push_cast + rfl + rw [hk'] + have hsumL : ∑ a ∈ S, (L S a : ℝ) ≤ K / c₁ * + ((8 * LL + 2 / log 2) * (2 / log 2) * (n * Lg) + 4 * (n * Lg) + (c₁ + C₁) * n) := by + rw [← hn, ← hLg] at hcore + calc ∑ a ∈ S, (L S a : ℝ) = K / c₁ * (c₁ / K * ∑ a ∈ S, (L S a : ℝ)) := by + field_simp + _ ≤ _ := mul_le_mul_of_nonneg_left hcore (by positivity) + -- absorb everything into `n Lg LL` + have hnLL : 0 ≤ n * Lg * LL := by positivity + have hA : n ≤ n * Lg * LL := by + have h := one_le_mul_of_one_le_of_one_le hLg1 hLL + simpa only [mul_one, mul_assoc] using mul_le_mul_of_nonneg_left h (by positivity : 0 ≤ n) + have hB : (8 * LL + 2 / log 2) * (2 / log 2) * (n * Lg) ≤ + (8 + 2 / log 2) * (2 / log 2) * (n * Lg * LL) := by + have h22 : 0 ≤ 2 / log (2 : ℝ) := by positivity + have : (8 * LL + 2 / log 2) ≤ (8 + 2 / log 2) * LL := by + nlinarith only [mul_le_mul_of_nonneg_left hLL h22] + have hnL : 0 ≤ n * Lg := by positivity + calc (8 * LL + 2 / log 2) * (2 / log 2) * (n * Lg) + ≤ (8 + 2 / log 2) * LL * (2 / log 2) * (n * Lg) := by gcongr + _ = _ := by ring + have hC : 4 * (n * Lg) ≤ 4 * (n * Lg * LL) := by + have h := mul_le_mul_of_nonneg_left hLL (show 0 ≤ 4 * (n * Lg) by positivity) + simpa only [mul_one, mul_assoc] using h + have hD : (c₁ + C₁) * n ≤ (c₁ + C₁) * (n * Lg * LL) := by + apply mul_le_mul_of_nonneg_left hA + linarith + have hKc : 0 ≤ K / c₁ := by positivity + have := mul_le_mul_of_nonneg_left (add_le_add (add_le_add hB hC) hD) hKc + calc n + ∑ a ∈ S, (L S a : ℝ) + ≤ n * Lg * LL + K / c₁ * ((8 + 2 / log 2) * (2 / log 2) * (n * Lg * LL) + + 4 * (n * Lg * LL) + (c₁ + C₁) * (n * Lg * LL)) := by linarith + _ = (1 + K / c₁ * ((8 + 2 / log 2) * (2 / log 2) + 4 + c₁ + C₁)) * n * Lg * LL := by ring + +end RunsOfMultiples diff --git a/LeanPool/projects/runs-of-multiples.yaml b/LeanPool/projects/runs-of-multiples.yaml new file mode 100644 index 0000000000..095247f736 --- /dev/null +++ b/LeanPool/projects/runs-of-multiples.yaml @@ -0,0 +1,48 @@ +slug: runs-of-multiples +title: Sharp asymptotic bounds for runs of multiples in finite sets +summary: >- + For a finite set S of n positive integers, let k(S,a) be the least positive + integer k for which k*a is outside S. Proves an upper bound for every such S + and a matching positive lower bound attained by some set of every sufficiently + large cardinality n, establishing the extremal order n log n log log n. + Contains entropy and chain-compression upper bounds and two lower-bound + constructions, sharing definitions, prime estimates and padding. Preserves + prime-weighted entropy estimates, smooth-number constructions and abstract + cardinality-preserving compression lemmas. +branch: number theory +entry_module: LeanPool.RunsOfMultiples +authors: + - Jason Hoelscher-Obermaier + - Claude Opus 5.5 (Lean proofs) +source: + title: Runs of multiples in a finite set of integers + authors: + - Claude Opus 5.5 (AI; published by Jason Hoelscher-Obermaier) + url: https://github.com/jas-ho/runs-of-multiples-lean/blob/8b7e5f23534c321722725f78b6e64981557f0ef5/docs/runs-of-multiples.pdf + github_repo: jas-ho/runs-of-multiples-lean +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: + - RunsOfMultiples.main_theorem + - RunsOfMultiples.main_theorem_alt +main_results: + - declaration: RunsOfMultiples.main_theorem + informal: >- + Every sufficiently large finite set S of positive integers has sum of its + first missing multiple indices at most C*n*log(n)*log(log(n)); for every + sufficiently large n, a set of exactly n positive integers attains at least + c*n*log(n)*log(log(n)), for a fixed c>0. This proof uses entropy and smooth numbers. + - declaration: RunsOfMultiples.main_theorem_alt + informal: >- + The identical sharp asymptotic statement, proved using compression + to divisor-closed, prime-shift-closed sets and a box-times-simplex construction. +tags: + - extremal-number-theory + - smooth-numbers + - entropy + - compression +msc: + - 11N25 + - 11B75 + - 05D05