The proof
Source
Main.lean · 6840 lines · 309.2 kB
Showing the first 500 of 6840 lines. The whole file is 309.2 kB; download it to read the rest.
/-
Submission body for Math15Catalog.source04 (formalized).
Validated against the task's pinned Challenge.lean and fixed header/footer.
The platform supplies the imports and opens namespace Bounty; the first command
closes that namespace so the helper declarations retain their ordinary names.
The final theorem reopens Bounty, and the platform's footer closes it.
The mathematical proof uses no additional axioms. Adapted library material is
attributed at its source component; its Apache 2.0 license is included below.
-/
end Bounty
/- Proof component: GrowthCompatibility -/
section
/-
The primorial definition and elementary divisibility lemmas below are adapted
from Mathlib.NumberTheory.Primorial (Patrick Stevens, Yury Kudryashov,
Bhavik Mehta), licensed under Apache 2.0. They are included explicitly because
the challenge's fixed imports do not expose that module.
-/
open Finset Nat
/-- The product of all primes at most `n`. -/
def primorial (n : ℕ) : ℕ := ∏ p ∈ range (n + 1) with p.Prime, p
theorem primorial_pos (n : ℕ) : 0 < primorial n :=
prod_pos fun _p hp ↦ (mem_filter.1 hp).2.pos
theorem primorial_dvd_primorial {m n : ℕ} (h : m ≤ n) : primorial m ∣ primorial n := by
exact prod_dvd_prod_of_subset _ _ _ (by gcongr)
lemma Nat.Prime.dvd_primorial_iff {p n : ℕ} (hp : Prime p) : p ∣ primorial n ↔ p ≤ n := by
refine ⟨?_, fun h ↦ dvd_prod_of_mem _ (by grind)⟩
intro h
simp only [primorial, hp.prime.dvd_finsetProd_iff, mem_filter, mem_range_succ_iff] at h
obtain ⟨q, ⟨hqn, hq⟩, hpq⟩ := h
exact (Nat.le_of_dvd hq.pos hpq).trans hqn
namespace Bounty.Arithmetic
/-- Quarter-interval primes imply the doubling-interval consequence needed
in the elementary growth estimate; only finitely many small cases remain. -/
theorem doubling_primes_of_quarter
(quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n)
(n : ℕ) (hn : n ≠ 0) : ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2*n := by
by_cases hlarge : 26 ≤ n
· obtain ⟨p, hp, hnp, hpn⟩ := quarter n hlarge
exact ⟨p, hp, hnp, by omega⟩
· have hsmall : ∀ n ∈ Finset.Icc 1 25,
∃ p ∈ Finset.Icc 2 47, Nat.Prime p ∧ n < p ∧ p ≤ 2*n := by decide
obtain ⟨p, _, hp, hnp, hpn⟩ := hsmall n (Finset.mem_Icc.mpr ⟨by omega, by omega⟩)
exact ⟨p, hp, hnp, hpn⟩
private theorem primorial_cubic_small_portable :
∀ k ∈ Finset.Icc 11 63, k ^ 3 < primorial k := by decide
/-- The growth proof needs only this prime-existence input, supplied in the
final assembly by the elementary quarter-interval theorem. -/
theorem cubic_lt_primorial_of_quarter
(quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n)
{k : ℕ} (hk : 11 ≤ k) : k ^ 3 < primorial k := by
induction k using Nat.strong_induction_on with
| h k ih =>
by_cases hsmall : k ≤ 63
· exact primorial_cubic_small_portable k (Finset.mem_Icc.mpr ⟨hk, hsmall⟩)
· let a := k / 2
have ha : 32 ≤ a := by dsimp [a]; omega
have hak : a < k := by dsimp [a]; omega
have hka : k ≤ 3 * a := by dsimp [a]; omega
have h2a : 2 * a ≤ k := by dsimp [a]; omega
obtain ⟨p, hp, hap, hp2a⟩ := doubling_primes_of_quarter quarter a (by omega)
have hpk : p ≤ k := hp2a.trans h2a
have hcop : Nat.Coprime p (primorial a) :=
hp.coprime_iff_not_dvd.mpr (by simpa [hp.dvd_primorial_iff] using (not_le.mpr hap))
have hdvd : p * primorial a ∣ primorial k :=
hcop.mul_dvd_of_dvd_of_dvd (hp.dvd_primorial_iff.mpr hpk)
(primorial_dvd_primorial (by omega))
have hmul : p * primorial a ≤ primorial k := Nat.le_of_dvd (primorial_pos k) hdvd
have hia : a ^ 3 < primorial a := ih a hak (by omega)
calc
k ^ 3 ≤ (3 * a) ^ 3 := Nat.pow_le_pow_left hka 3
_ = 27 * a ^ 3 := by ring
_ < p * primorial a := by nlinarith
_ ≤ primorial k := hmul
end Bounty.Arithmetic
/-- Multiplying distinct small prime divisors preserves divisibility. -/
theorem primorial_dvd_of_prime_support {m r : ℕ}
(h : ∀ p : ℕ, p.Prime → p ≤ m → p ∣ r) : primorial m ∣ r := by
unfold primorial
apply Finset.prod_primes_dvd
· intro p hp
exact (Finset.mem_filter.mp hp).2.prime
· intro p hp
obtain ⟨hpm, hp⟩ := Finset.mem_filter.mp hp
exact h p hp (by simpa using hpm)
namespace Bounty.Arithmetic
private def smallPrimes : Finset ℕ := {2, 3, 5, 7, 11}
private theorem prime_ge_thirteen_of_not_small {p : ℕ} (hp : Nat.Prime p)
(hnot : p ∉ smallPrimes) : 13 ≤ p := by
by_contra hlt
have : p ≤ 12 := by omega
interval_cases p <;> norm_num at hp <;> norm_num [smallPrimes] at hnot
/-- A normalized lower bound for a product of distinct primes. -/
theorem prime_set_product_lower (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) :
2310 * 13 ^ S.card ≤ 13 ^ 5 * ∏ p ∈ S, p := by
let A := S ∩ smallPrimes
let B := S \ smallPrimes
let C := smallPrimes \ S
have hcardS : A.card + B.card = S.card := Finset.card_inter_add_card_sdiff _ _
have hcard0 : A.card + C.card = 5 := by
simpa [A, C, Finset.inter_comm, smallPrimes] using
Finset.card_inter_add_card_sdiff smallPrimes S
have hprodS : (∏ p ∈ A, p) * ∏ p ∈ B, p = ∏ p ∈ S, p :=
Finset.prod_inter_mul_prod_sdiff _ _ _
have hprod0 : (∏ p ∈ A, p) * ∏ p ∈ C, p = 2310 := by
simpa [A, C, Finset.inter_comm, smallPrimes] using
Finset.prod_inter_mul_prod_sdiff smallPrimes S id
have hB : 13 ^ B.card ≤ ∏ p ∈ B, p := by
apply Finset.pow_card_le_prod
intro p hp
have hp' := Finset.mem_sdiff.mp hp
exact prime_ge_thirteen_of_not_small (hS p hp'.1) hp'.2
have hC : (∏ p ∈ C, p) ≤ 13 ^ C.card := by
apply Finset.prod_le_pow_card
intro p hp
have hp' : p ∈ smallPrimes := (Finset.mem_sdiff.mp hp).1
simp only [smallPrimes, Finset.mem_insert, Finset.mem_singleton] at hp'
omega
calc
2310 * 13 ^ S.card = ((∏ p ∈ A, p) * ∏ p ∈ C, p) * 13 ^ (A.card + B.card) := by
rw [hprod0, hcardS]
_ ≤ ((∏ p ∈ A, p) * 13 ^ C.card) * 13 ^ (A.card + B.card) := by gcongr
_ = 13 ^ (A.card + C.card) * ((∏ p ∈ A, p) * 13 ^ B.card) := by
simp only [pow_add]
ring
_ = 13 ^ 5 * ((∏ p ∈ A, p) * 13 ^ B.card) := by rw [hcard0]
_ ≤ 13 ^ 5 * ((∏ p ∈ A, p) * ∏ p ∈ B, p) := by gcongr
_ = 13 ^ 5 * ∏ p ∈ S, p := by rw [hprodS]
/-- Six distinct prime factors force a product at least `30030`, with a
factor of at least `13` for every further distinct prime. -/
theorem primeFactors_product_lower {v : ℕ} (hv : 0 < v)
(hw : 6 ≤ v.primeFactors.card) :
30030 * 13 ^ (v.primeFactors.card - 6) ≤ v := by
have h := prime_set_product_lower v.primeFactors (fun _ hp ↦ Nat.prime_of_mem_primeFactors hp)
have hprod : (∏ p ∈ v.primeFactors, p) ≤ v :=
Nat.le_of_dvd hv (Nat.prod_primeFactors_dvd v)
have heq : v.primeFactors.card = 6 + (v.primeFactors.card - 6) := by omega
conv_lhs at h => rw [heq, pow_add]
norm_num at h
nlinarith
/-- A uniform estimate for the number of distinct prime factors in the large range. -/
theorem primeFactors_pow_bound {v : ℕ} (hv : 10000 ≤ v) :
2 ^ (10 + 3 * v.primeFactors.card) < v ^ 2 := by
by_cases hw : v.primeFactors.card ≤ 5
· have hpow : 2 ^ (10 + 3 * v.primeFactors.card) ≤ 2 ^ 25 :=
Nat.pow_le_pow_right (by norm_num) (by omega)
norm_num at hpow
nlinarith
· have hlow := primeFactors_product_lower (show 0 < v by omega) (show 6 ≤ v.primeFactors.card by omega)
let t := v.primeFactors.card - 6
have hw' : v.primeFactors.card = 6 + t := by dsimp [t]; omega
have heq : 2 ^ (10 + 3 * v.primeFactors.card) = 268435456 * 8 ^ t := by
rw [hw']
have ha : 10 + 3 * (6 + t) = 28 + 3 * t := by omega
rw [ha, pow_add, pow_mul]
norm_num
have hpow : 8 ^ t ≤ (13 ^ t) ^ 2 := by
calc
8 ^ t ≤ 169 ^ t := Nat.pow_le_pow_left (by norm_num) t
_ = (13 ^ t) ^ 2 := by rw [← pow_mul, mul_comm t 2, pow_mul]; norm_num
have hlowsq := Nat.pow_le_pow_left hlow 2
change (30030 * 13 ^ t) ^ 2 ≤ v ^ 2 at hlowsq
rw [mul_pow] at hlowsq
norm_num at hlowsq
have hpos : 0 < (13 ^ t) ^ 2 := by positivity
rw [heq]
nlinarith
/-- The explicit separation estimate used in the unbounded range. -/
theorem separation_bound_of_quarter
(quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n)
{v s k : ℕ} (hv : 10000 ≤ v)
(hs : 0 < s) (hsv : s < 2 * v) (hdiv : primorial k ∣ s) :
8 * k * 2 ^ v.primeFactors.card < v := by
have hv0 : 0 < v := by omega
have hk : k ^ 3 < 2 * v := by
by_cases hsmall : k ≤ 10
· have hp := Nat.pow_le_pow_left hsmall 3
norm_num at hp
omega
· exact (cubic_lt_primorial_of_quarter quarter (by omega)).trans_le
((Nat.le_of_dvd hs hdiv).trans hsv.le)
have hpf := primeFactors_pow_bound hv
have hexp : 10 + 3 * v.primeFactors.card = 10 + v.primeFactors.card * 3 := by omega
rw [hexp, pow_add, pow_mul] at hpf
norm_num at hpf
have hJ : 0 < (2 ^ v.primeFactors.card) ^ 3 := by positivity
have hcube : (8 * k * 2 ^ v.primeFactors.card) ^ 3 < v ^ 3 := by
calc
(8 * k * 2 ^ v.primeFactors.card) ^ 3 =
512 * k ^ 3 * (2 ^ v.primeFactors.card) ^ 3 := by ring
_ < 512 * (2 * v) * (2 ^ v.primeFactors.card) ^ 3 := by
exact Nat.mul_lt_mul_of_pos_right (Nat.mul_lt_mul_of_pos_left hk (by omega)) hJ
_ = (1024 * (2 ^ v.primeFactors.card) ^ 3) * v := by ring
_ < v ^ 2 * v := Nat.mul_lt_mul_of_pos_right hpf hv0
_ = v ^ 3 := by ring
by_contra hnot
have hreverse := Nat.pow_le_pow_left (show v ≤ 8 * k * 2 ^ v.primeFactors.card by omega) 3
omega
private theorem add_nine_le_nine_two_pow (t : ℕ) : t + 9 ≤ 9 * 2 ^ t := by
induction t with
| zero => norm_num
| succ t ih =>
have hp : 0 < 2 ^ t := by positivity
simp only [pow_succ]
nlinarith
/-- The elementary sieve factor can be absorbed in the large-range growth bound. -/
theorem weighted_primeFactors_pow_bound {v : ℕ} (hv : 1100000 ≤ v) :
2 ^ (10 + 3 * v.primeFactors.card) * (v.primeFactors.card + 1) ^ 3 < v ^ 2 := by
by_cases hw : v.primeFactors.card ≤ 7
· have hpow : 2 ^ (10 + 3 * v.primeFactors.card) ≤ 2 ^ 31 :=
Nat.pow_le_pow_right (by norm_num) (by omega)
have hcube : (v.primeFactors.card + 1) ^ 3 ≤ 8 ^ 3 :=
Nat.pow_le_pow_left (by omega) 3
have hmul := Nat.mul_le_mul hpow hcube
norm_num at hmul
nlinarith
· let t := v.primeFactors.card - 8
have hw' : v.primeFactors.card = 8 + t := by dsimp [t]; omega
have hw6 : v.primeFactors.card - 6 = 2 + t := by omega
have hlow := primeFactors_product_lower (show 0 < v by omega) (show 6 ≤ v.primeFactors.card by omega)
rw [hw6, pow_add] at hlow
norm_num at hlow
have hlow' : 5075070 * 13 ^ t ≤ v := by nlinarith
have hlowsq := Nat.pow_le_pow_left hlow' 2
have h169 : (13 ^ t) ^ 2 = 169 ^ t := by
rw [← pow_mul, mul_comm t 2, pow_mul]
norm_num
rw [mul_pow, h169] at hlowsq
have hcube : (t + 9) ^ 3 ≤ 729 * 8 ^ t := by
have hh := Nat.pow_le_pow_left (add_nine_le_nine_two_pow t) 3
have h8 : (2 ^ t) ^ 3 = 8 ^ t := by
rw [← pow_mul, mul_comm t 3, pow_mul]
norm_num
simpa only [mul_pow, h8, Nat.reducePow] using hh
have heq : 2 ^ (10 + 3 * v.primeFactors.card) = 2 ^ 34 * 8 ^ t := by
have hexp : 10 + 3 * v.primeFactors.card = 34 + 3 * t := by omega
rw [hexp, pow_add, pow_mul]
norm_num
have h64 : 64 ^ t = 8 ^ t * 8 ^ t := by rw [← mul_pow]; norm_num
have hpow : 64 ^ t ≤ 169 ^ t := Nat.pow_le_pow_left (by norm_num) t
calc
2 ^ (10 + 3 * v.primeFactors.card) * (v.primeFactors.card + 1) ^ 3 =
(2 ^ 34 * 8 ^ t) * (t + 9) ^ 3 := by rw [heq, hw']; congr 2; omega
_ ≤ (2 ^ 34 * 8 ^ t) * (729 * 8 ^ t) := Nat.mul_le_mul_left _ hcube
_ = (2 ^ 34 * 729) * 64 ^ t := by rw [h64]; ring
_ ≤ (2 ^ 34 * 729) * 169 ^ t := Nat.mul_le_mul_left _ hpow
_ < 5075070 ^ 2 * 169 ^ t := Nat.mul_lt_mul_of_pos_right (by norm_num) (by positivity)
_ ≤ v ^ 2 := hlowsq
private theorem separation_from_weighted_bound {v k w : ℕ}
(hv : 0 < v) (hk : k ^ 3 < 2 * v)
(hweight : 2 ^ (10 + 3 * w) * (w + 1) ^ 3 < v ^ 2) :
8 * k * ((w + 1) * 2 ^ w) < v := by
let J := (w + 1) * 2 ^ w
have hJ : 0 < J := by dsimp [J]; positivity
have hexp : 10 + 3 * w = 10 + w * 3 := by omega
rw [hexp, pow_add, pow_mul] at hweight
norm_num at hweight
have hbound : 1024 * J ^ 3 < v ^ 2 := by
dsimp [J]
convert hweight using 1; ring
have hcube : (8 * k * J) ^ 3 < v ^ 3 := by
calc
(8 * k * J) ^ 3 = 512 * k ^ 3 * J ^ 3 := by ring
_ < 512 * (2 * v) * J ^ 3 :=
Nat.mul_lt_mul_of_pos_right (Nat.mul_lt_mul_of_pos_left hk (by omega)) (by positivity)
_ = (1024 * J ^ 3) * v := by ring
_ < v ^ 2 * v := Nat.mul_lt_mul_of_pos_right hbound hv
_ = v ^ 3 := by ring
by_contra hnot
change ¬ 8 * k * J < v at hnot
have hreverse := Nat.pow_le_pow_left (show v ≤ 8 * k * J by omega) 3
omega
/-- The gap bound `(ω(v)+1)*2^ω(v)` is small enough for the mixed-case
argument once the removed speed is at least `60000`. -/
theorem elementary_separation_bound_of_quarter
(quarter : ∀ n : ℕ, 26 ≤ n → ∃ p : ℕ, p.Prime ∧ n < p ∧ 4*p < 5*n)
{v s k : ℕ} (hv : 60000 ≤ v)
(hs : 0 < s) (hsv : s < 2 * v) (hdiv : primorial k ∣ s) :
8 * k * ((v.primeFactors.card + 1) * 2 ^ v.primeFactors.card) < v := by
have hv0 : 0 < v := by omega
by_cases hlarge : 1100000 ≤ v
· have hk : k ^ 3 < 2 * v := by
by_cases hsmall : k ≤ 10
· have hp := Nat.pow_le_pow_left hsmall 3
norm_num at hp
omega
· exact (cubic_lt_primorial_of_quarter quarter (by omega)).trans_le
((Nat.le_of_dvd hs hdiv).trans hsv.le)
exact separation_from_weighted_bound hv0 hk (weighted_primeFactors_pow_bound hlarge)
· by_cases hmid : 147457 ≤ v
· have hk : k ≤ 18 := by
by_contra hnot
have hdvd := dvd_trans (primorial_dvd_primorial (show 19 ≤ k by omega)) hdiv
have hle := Nat.le_of_dvd hs hdvd
have hval : primorial 19 = 9699690 := by decide
rw [hval] at hle
omega
have hw : v.primeFactors.card ≤ 7 := by
by_contra hnot
have hlow := primeFactors_product_lower hv0 (show 6 ≤ v.primeFactors.card by omega)
have hp : 13 ^ 2 ≤ 13 ^ (v.primeFactors.card - 6) :=
Nat.pow_le_pow_right (by norm_num) (by omega)
norm_num at hp
nlinarith
have hp : 2 ^ v.primeFactors.card ≤ 2 ^ 7 := Nat.pow_le_pow_right (by norm_num) hw
have hj := Nat.mul_le_mul (show v.primeFactors.card + 1 ≤ 8 by omega) hp
have hfinal := Nat.mul_le_mul (Nat.mul_le_mul_left 8 hk) hj
norm_num at hfinal
omega
· have hk : k ≤ 16 := by
by_contra hnot
have hdvd := dvd_trans (primorial_dvd_primorial (show 17 ≤ k by omega)) hdiv
have hle := Nat.le_of_dvd hs hdvd
have hval : primorial 17 = 510510 := by decide
rw [hval] at hle
omega
have hw : v.primeFactors.card ≤ 6 := by
by_contra hnot
have hlow := primeFactors_product_lower hv0 (show 6 ≤ v.primeFactors.card by omega)
have hp : 13 ^ 1 ≤ 13 ^ (v.primeFactors.card - 6) :=
Nat.pow_le_pow_right (by norm_num) (by omega)
norm_num at hp
nlinarith
have hp : 2 ^ v.primeFactors.card ≤ 2 ^ 6 := Nat.pow_le_pow_right (by norm_num) hw
have hj := Nat.mul_le_mul (show v.primeFactors.card + 1 ≤ 7 by omega) hp
have hfinal := Nat.mul_le_mul (Nat.mul_le_mul_left 8 hk) hj
norm_num at hfinal
omega
end Bounty.Arithmetic
/- Additional primorial bounds adapted from Mathlib.NumberTheory.Primorial,
Mathlib.Data.Nat.Choose.Dvd (Chris Hughes, Patrick Stevens), and
Mathlib.Data.Nat.Prime.Factorial (Leonardo de Moura, Jeremy Avigad,
Mario Carneiro), all licensed under Apache 2.0. -/
open Finset Nat
theorem primorial_zero : primorial 0 = 1 := by decide
theorem primorial_one : primorial 1 = 1 := by decide
theorem primorial_two : primorial 2 = 2 := by decide
theorem Nat.Prime.dvd_factorial : ∀ {n p : ℕ} (_ : Nat.Prime p), p ∣ n ! ↔ p ≤ n
| 0, _, hp => iff_of_false hp.not_dvd_one (not_le_of_gt hp.pos)
| n + 1, p, hp => by
rw [factorial_succ, hp.dvd_mul, Nat.Prime.dvd_factorial hp]
exact
⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
(_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
/-- A prime between both summands and their sum divides their binomial coefficient. -/
theorem Nat.Prime.dvd_choose_add {p a b : ℕ} (hp : Nat.Prime p)
(hap : a < p) (hbp : b < p) (h : p ≤ a + b) : p ∣ Nat.choose (a+b) a := by
have h₁ : p ∣ (a+b)! := hp.dvd_factorial.2 h
rw [← Nat.add_choose_mul_factorial_mul_factorial, ← Nat.choose_symm_add,
hp.dvd_mul, hp.dvd_mul, hp.dvd_factorial, hp.dvd_factorial] at h₁
exact (h₁.resolve_right hbp.not_ge).resolve_right hap.not_ge
theorem primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : Odd n) : primorial (n + 1) = primorial n := by
refine prod_congr ?_ fun _ _ ↦ rfl
rw [range_add_one, filter_insert, ite_eq_right fun h ↦ not_even_iff_odd.2 hn _]
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1
theorem primorial_add (m n : ℕ) :
primorial (m + n) = primorial m * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p := by
simp_rw [primorial, ← Ico_zero_eq_range]
rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
exacts [Nat.zero_le _, by omega, disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]
theorem primorial_add_dvd {m n : ℕ} (h : n ≤ m) : primorial (m + n) ∣ primorial m * choose (m + n) m :=
calc
primorial (m + n) = primorial m * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p := primorial_add _ _
_ ∣ primorial m * choose (m + n) m :=
mul_dvd_mul_left _ <|
prod_primes_dvd _ (fun _ hk ↦ (mem_filter.1 hk).2.prime) fun p hp ↦ by
rw [mem_filter, mem_Ico] at hp
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
(Nat.lt_succ_iff.1 hp.1.2)
theorem primorial_add_le {m n : ℕ} (h : n ≤ m) : primorial (m + n) ≤ primorial m * choose (m + n) m :=
le_of_dvd (mul_pos (primorial_pos _) (choose_pos <| Nat.le_add_right _ _)) (primorial_add_dvd h)
theorem primorial_lt_four_pow (n : ℕ) (hn : n ≠ 0) : primorial n < 4 ^ n := by
induction n using Nat.strong_induction_on with | h n ihn =>
rcases n with - | n; · grind
rcases n.even_or_odd with ⟨m, rfl⟩ | ho
· rcases m.eq_zero_or_pos with rfl | hm
· decide
calc
primorial (m + m + 1) = primorial (m + 1 + m) := by rw [add_right_comm]
_ ≤ primorial (m + 1) * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
_ = primorial (m + 1) * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
_ < 4 ^ (m + 1) * 4 ^ m :=
Nat.mul_lt_mul_of_lt_of_le (ihn _ (by omega) (by omega)) (choose_middle_le_pow _) (by simp)
_ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
· rcases Decidable.eq_or_ne n 1 with rfl | hn
· decide
· calc
primorial (n + 1) = primorial n := primorial_succ hn ho
_ < 4 ^ n := ihn n n.lt_succ_self (by grind)
_ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ
theorem primorial_le_four_pow (n : ℕ) : primorial n ≤ 4 ^ n := by
obtain rfl | hn := eq_or_ne n 0
· decide
· exact (primorial_lt_four_pow n hn).le
end
/- Proof component: Core -/
section
noncomputable section
namespace Bounty
open Math15.LonelyRunner
theorem score_le_ML (V : Finset ℕ) (t : Time) : score V t ≤ ML V := by
change score V t ≤ sSup (Set.range (score V))
refine le_csSup ?_ ⟨t, rfl⟩
refine ⟨1 / 2, ?_⟩
rintro _ ⟨s, rfl⟩
by_cases h : V.Nonempty
· simp only [score, dite_eq_left h]
obtain ⟨v, hv⟩ := h
exact (Finset.inf'_le (fun v => distance (v • s)) hv).trans (by
simpa [distance] using AddCircle.norm_le_half_period (1 : ℝ)
(by norm_num) (x := v • s))
· simp [score, h]
theorem ML_le_iff_forall_score_le (V : Finset ℕ) (c : ℝ) :
ML V ≤ c ↔ ∀ t : Time, score V t ≤ c := by
constructor
· exact fun h t => (score_le_ML V t).trans h
· intro h
exact csSup_le (Set.range_nonempty _) (by rintro _ ⟨t, rfl⟩; exact h t)
theorem ML_le_iff_covered (V : Finset ℕ) (hV : V.Nonempty) (c : ℝ) :
ML V ≤ c ↔ ∀ t : Time, ∃ v ∈ V, distance (v • t) ≤ c := by
rw [ML_le_iff_forall_score_le]
simp only [score, dite_eq_left hV, Finset.inf'_le_iff]
theorem ML_gt_of_all_distances_gt {V : Finset ℕ} (hV : V.Nonempty)
{c : ℝ} {t : Time} (h : ∀ v ∈ V, c < distance (v • t)) :
c < ML V := by
apply lt_of_not_ge
intro hc
obtain ⟨v, hv, hh⟩ := (ML_le_iff_covered V hV c).mp hc t
exact (not_lt_of_ge hh) (h v hv)
theorem mem_modified {n r₁ r₂ w₁ w₂ v : ℕ} :
v ∈ modified n r₁ r₂ w₁ w₂ ↔
(1 ≤ v ∧ v ≤ n - 1 ∧ v ≠ r₁ ∧ v ≠ r₂) ∨ v = w₁ ∨ v = w₂ := by
simp only [modified, Finset.mem_union, Finset.mem_sdiff, Finset.mem_Icc,
Finset.mem_insert, Finset.mem_singleton, not_or]
tauto
theorem modified_nonempty (n r₁ r₂ w₁ w₂ : ℕ) :
(modified n r₁ r₂ w₁ w₂).Nonempty := by
exact ⟨w₁, mem_modified.mpr (Or.inr (Or.inl rfl))⟩
theorem modified_positive {n r₁ r₂ w₁ w₂ : ℕ}
(hn : 1 ≤ n) (hw₁ : n ≤ w₁) (hw₂ : n ≤ w₂) :
Positive (modified n r₁ r₂ w₁ w₂) := by
intro v hv
rcases mem_modified.mp hv with h | rfl | rfl <;> omega
theorem inserted_covers_hole {n r₁ r₂ w₁ w₂ : ℕ} {c : ℝ} {t : Time}
(hML : ML (modified n r₁ r₂ w₁ w₂) ≤ c)
(hretained : ∀ v : ℕ, 1 ≤ v → v < n → v ≠ r₁ → v ≠ r₂ →
c < distance (v • t)) :
distance (w₁ • t) ≤ c ∨ distance (w₂ • t) ≤ c := by
obtain ⟨v, hv, hd⟩ := (ML_le_iff_covered _
(modified_nonempty n r₁ r₂ w₁ w₂) c).mp hML t
rcases mem_modified.mp hv with h | rfl | rfl
· have hh := hretained v h.1 (by omega) h.2.2.1 h.2.2.2
exact False.elim ((not_lt_of_ge hd) hh)Provenance