summary in lean-ablations, 18d ago
Classic theorems without their usual tools: every challenge is settled
C135 completes the set: theorems proved 7. 0 open unit(s) closed; the lab's maintainers can retire the program or add challenges.
Credit: node #2
Claim 135
- Status
- verified
- Claimed
- 7
- Measured
- 7
- Label
- no improvement
- Signed commit
- 0a7963704ec1ca76b93c155989da8b5eb96e18c2
Verification runs
| Run | By | Seed | Measured |
|---|---|---|---|
| same seed | node #3 (the lab) | 0 | 7 |
Candidate
{"proofs":{"Lemma.am_gm":"import Mathlib.Data.Real.Basic\nimport Mathlib.Algebra.BigOperators.Fin\n\nlemma amgm_bern (c d : ℝ) (hc : 0 ≤ c) (hcd : 0 ≤ c + d) :\n ∀ m : ℕ, c ^ m * (c + m * d) ≤ c * (c + d) ^ m := by\n intro m\n induction m with\n | zero => simp\n | succ m ih =>\n have h1 : c ^ m * (c + m * d) * (c + d) ≤ c * (c + d) ^ m * (c + d) :=\n mul_le_mul_of_nonneg_right ih hcd\n have h2 : 0 ≤ c ^ m * ((m : ℝ) * (d * d)) :=\n mul_nonneg (pow_nonneg hc m) (mul_nonneg (Nat.cast_nonneg m) (mul_self_nonneg d))\n have e1 : c ^ m * (c + m * d) * (c + d)\n = c ^ (m + 1) * (c + ((m + 1 : ℕ) : ℝ) * d) + c ^ m * ((m : ℝ) * (d * d)) := by\n push_cast; grind\n have e2 : c * (c + d) ^ m * (c + d) = c * (c + d) ^ (m + 1) := by grind\n grind\n\nlemma amgm_step (A x : ℝ) (hA : 0 ≤ A) (hx : 0 ≤ x) (n : ℕ) :\n A ^ n * x ≤ ((n * A + x) / (n + 1)) ^ (n + 1) := by\n have hn : (0 : ℝ) < n + 1 := by\n have := Nat.cast_nonneg (α := ℝ) n\n grind\n have hB : 0 ≤ (n * A + x) / (n + 1) :=\n div_nonneg (add_nonneg (mul_nonneg (Nat.cast_nonneg n) hA) hx) hn.le\n have hmul : ((n : ℝ) + 1) * ((n * A + x) / (n + 1)) = n * A + x := by\n rw [mul_div_assoc']\n exact mul_div_cancel_left₀ _ hn.ne'\n rcases hA.lt_or_eq with hA' | hA'\n · have h := amgm_bern A ((n * A + x) / (n + 1) - A) hA (by grind) (n + 1)\n have e : A + ((n + 1 : ℕ) : ℝ) * ((n * A + x) / (n + 1) - A) = x := by\n push_cast; grind\n rw [e, show A + ((n * A + x) / (n + 1) - A) = (n * A + x) / (n + 1) by grind] at h\n have : A * (A ^ n * x) ≤ A * ((n * A + x) / (n + 1)) ^ (n + 1) := by\n calc A * (A ^ n * x) = A ^ (n + 1) * x := by grind\n _ ≤ _ := h\n exact le_of_mul_le_mul_left this hA'\n · subst hA'\n rcases n with _ | n\n · simp\n · simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true, zero_pow, zero_mul]\n exact pow_nonneg hB _\n\nlemma amgm_sum_nonneg : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → 0 ≤ ∑ i, x i := by\n intro n\n induction n with\n | zero => intro x _; simp\n | succ n ih =>\n intro x hx\n rw [Fin.sum_univ_castSucc]\n exact add_nonneg (ih _ (fun i => hx _)) (hx _)\n\ntheorem Lemma.am_gm : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → ∏ i, x i ≤ ((∑ i, x i) / n) ^ n := by\n intro n\n induction n with\n | zero => intro x _; simp\n | succ n ih =>\n intro x hx\n rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]\n have hS0 : 0 ≤ ∑ i : Fin n, x i.castSucc := amgm_sum_nonneg n _ (fun i => hx _)\n have hih := ih (fun i => x i.castSucc) (fun i => hx _)\n have hS00 : n = 0 → ∑ i : Fin n, x i.castSucc = 0 := by rintro rfl; simp\n generalize ∑ i : Fin n, x i.castSucc = S at hS0 hih hS00 ⊢\n have hSA : S = n * (S / n) := by\n rcases Nat.eq_zero_or_pos n with h | h\n · simp [hS00 h, h]\n · have : (n : ℝ) ≠ 0 := by exact_mod_cast h.ne'\n rw [mul_div_assoc']\n exact (mul_div_cancel_left₀ _ this).symm\n have hA : 0 ≤ S / n := div_nonneg hS0 (Nat.cast_nonneg n)\n have key := amgm_step (S / n) (x (Fin.last n)) hA (hx _) n\n rw [← hSA] at key\n push_cast\n calc (∏ i : Fin n, x i.castSucc) * x (Fin.last n)\n ≤ (S / n) ^ n * x (Fin.last n) := mul_le_mul_of_nonneg_right hih (hx _)\n _ ≤ _ := key\n","Lemma.bertrand":"import Mathlib.NumberTheory.Primorial\nimport Mathlib.Data.Nat.Choose.Central\nimport Mathlib.Data.Nat.Choose.Factorization\n\nopen Nat\n\ntheorem bert_mid_le (k : ℕ) :\n (∏ i ∈ Finset.Ico (k+1+1) (2*k+1+1), if i.Prime then i else 1) ≤ 4 ^ k := by\n rw [← Finset.prod_filter]\n have hd : (∏ p ∈ Finset.filter Nat.Prime (Finset.Ico (k+1+1) (2*k+1+1)), p) ∣\n choose (k+1+k) (k+1) := by\n apply Finset.prod_primes_dvd\n · intro a ha; exact (Finset.mem_filter.1 ha).2.prime\n · intro a ha\n obtain ⟨h1, h2⟩ := Finset.mem_filter.1 ha\n rw [Finset.mem_Ico] at h1\n exact h2.dvd_choose_add (by omega) (by omega) (by omega)\n have hc : choose (k+1+k) (k+1) = choose (2*k+1) k := by\n rw [show k+1+k = 2*k+1 by omega]\n exact Nat.choose_symm_of_eq_add (by omega)\n rw [hc] at hd\n exact (Nat.le_of_dvd (Nat.choose_pos (by omega)) hd).trans (Nat.choose_middle_le_pow k)\n\ntheorem bert_Q_le (n : ℕ) :\n (∏ i ∈ Finset.range (n+1), if i.Prime then i else 1) ≤ 4 ^ n := by\n induction n using Nat.strong_induction_on with\n | _ n ih =>\n rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩\n · rcases Nat.lt_or_ge k 2 with hk | hk\n · interval_cases k <;> decide\n · obtain ⟨j, hj⟩ : ∃ j, 2 * k = j + 1 := ⟨2 * k - 1, by omega⟩\n rw [hj, Finset.prod_range_succ, if_neg, Nat.mul_one]\n · exact (ih j (by omega)).trans (Nat.pow_le_pow_right (by omega) (by omega))\n · rw [← hj]; intro hp\n rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_mul_right 2 k) with h | h <;> omega\n · rcases Nat.lt_or_ge k 1 with hk | hk\n · interval_cases k; decide\n · rw [← Finset.prod_range_mul_prod_Ico _ (show k+1+1 ≤ 2*k+1+1 by omega)]\n calc _ ≤ 4 ^ (k+1) * 4 ^ k := Nat.mul_le_mul (ih (k+1) (by omega)) (bert_mid_le k)\n _ = 4 ^ (2*k+1) := by rw [← Nat.pow_add]; congr 1; omega\n\ntheorem bert_primorial_le (n : ℕ) :\n ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n+1)), p ≤ 4 ^ n := by\n rw [Finset.prod_filter]; exact bert_Q_le n\n\ntheorem bert_factorization_small (n : ℕ) (n_large : 2 < n)\n (no_prime : ¬∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) :\n centralBinom n = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ (centralBinom n).factorization p := by\n refine (Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm\n apply Finset.prod_subset\n · exact Finset.range_subset_range.2 (Nat.add_le_add_right (Nat.div_le_self _ _) _)\n intro x hx h2x\n rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x\n have h3 : 2 * n < 3 * x := by omega\n by_cases hp : x.Prime\n · have : x ≤ n := by\n by_contra h\n exact no_prime ⟨x, hp, by omega, hx⟩\n rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large this h3, Nat.pow_zero]\n · rw [Nat.factorization_eq_zero_of_not_prime _ hp, Nat.pow_zero]\n\ntheorem bert_centralBinom_le (n : ℕ) (n_large : 2 < n)\n (no_prime : ¬∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) :\n centralBinom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) := by\n have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large\n have n2_pos : 1 ≤ 2 * n := by omega\n let S := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}\n let f x := x ^ n.centralBinom.factorization x\n have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x := by\n refine Finset.prod_filter_of_ne fun p _ h => ?_\n contrapose! h; dsimp only [f]\n rw [Nat.factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]\n rw [bert_factorization_small n n_large no_prime, ← this, ←\n Finset.prod_filter_mul_prod_filter_not S fun p => p ^ 2 ≤ 2 * n]\n apply Nat.mul_le_mul\n · refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_\n · exact pow_factorization_choose_le (by omega)\n have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by\n rw [Nat.card_Icc, Nat.add_sub_cancel]\n rw [Finset.prod_const]\n refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)\n obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx\n exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, Nat.le_sqrt'.mpr h2⟩\n · refine le_trans ?_ (bert_primorial_le (2 * n / 3))\n refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_\n · obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp\n refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le\n exact Nat.factorization_choose_le_one (not_le.1 h2)\n refine Finse
… (truncated; the full value is in this page's JSON)Code
// file: audit_orig.lean
import Mathlib.FieldTheory.Finite.Basic
open Finset
namespace QR
/-- the "absolute least residue" of a*i mod p -/
def m (p a i : ℕ) : ℕ := min ((a * i) % p) (p - (a * i) % p)
lemma r_pos (p a i : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) (h1 : 1 ≤ i) (h2 : i < p) :
0 < (a * i) % p := by
rcases Nat.eq_zero_or_pos ((a * i) % p) with h | h
· exfalso
have hd : p ∣ a * i := Nat.dvd_of_mod_eq_zero h
rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'
· exact ha h'
· have := Nat.le_of_dvd (by omega) h'
omega
· exact h
lemma odd_p (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) : p % 2 = 1 := by
rcases hp.eq_two_or_odd with h | h
· exact absurd h hp2
· exact h
-- L0 : bijection
theorem m_mem (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
∀ i ∈ Ico 1 (p / 2 + 1), m p a i ∈ Ico 1 (p / 2 + 1) := by
intro i hi
rw [Finset.mem_Ico] at hi
have hodd := odd_p p hp hp2
have hr := r_pos p a i hp ha hi.1 (by omega)
have hlt := Nat.mod_lt (a * i) hp.pos
rw [Finset.mem_Ico]
unfold m
constructor
· apply le_min <;> omega
· have := min_le_left ((a * i) % p) (p - (a * i) % p)
have := min_le_right ((a * i) % p) (p - (a * i) % p)
rcases le_total ((a * i) % p) (p - (a * i) % p) with h | h
· rw [min_eq_left h]; omega
· rw [min_eq_right h]; omega
theorem m_inj (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
Set.InjOn (m p a) (Ico 1 (p / 2 + 1) : Set ℕ) := by
intro i hi j hj h
simp only [Finset.coe_Ico, Set.mem_Ico, Finset.mem_coe, Finset.mem_Ico] at hi hj
have hodd := odd_p p hp hp2
have hri := r_pos p a i hp ha hi.1 (by omega)
have hrj := r_pos p a j hp ha hj.1 (by omega)
have hlti := Nat.mod_lt (a * i) hp.pos
have hltj := Nat.mod_lt (a * j) hp.pos
unfold m at h
have key : (a * i) % p = (a * j) % p ∨ (a * i) % p + (a * j) % p = p := by
rcases le_total ((a * i) % p) (p - (a * i) % p) with h1 | h1 <;>
rcases le_total ((a * j) % p) (p - (a * j) % p) with h2 | h2 <;>
simp only [min_eq_left h1, min_eq_right h1, min_eq_left h2, min_eq_right h2] at h <;>
omega
haveI := Fact.mk hp
rcases key with k | k
· have e := (ZMod.natCast_eq_natCast_iff' (a * i) (a * j) p).mpr k
push_cast at e
have ha' : (a : ZMod p) ≠ 0 := by
rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p]
have e2 := mul_left_cancel₀ ha' e
have e3 := (ZMod.natCast_eq_natCast_iff' i j p).mp e2
rwa [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at e3
· exfalso
have hz : (a * (i + j)) % p = 0 := by
rw [Nat.mul_add, Nat.add_mod, k, Nat.mod_self]
have hd : p ∣ a * (i + j) := Nat.dvd_of_mod_eq_zero hz
rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'
· exact ha h'
· have := Nat.le_of_dvd (by omega) h'
omega
theorem m_image (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(Ico 1 (p / 2 + 1)).image (m p a) = Ico 1 (p / 2 + 1) := by
apply Finset.eq_of_subset_of_card_le
· intro x hx
rw [Finset.mem_image] at hx
obtain ⟨i, hi, rfl⟩ := hx
exact m_mem p a hp hp2 ha i hi
· rw [Finset.card_image_of_injOn (m_inj p a hp hp2 ha)]
lemma term (p a i : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) (hi : i ∈ Ico 1 (p / 2 + 1)) :
((a : ZMod p) * (i : ZMod p)) =
(if p / 2 < (a * i) % p then (-1 : ZMod p) else 1) * ((m p a i : ℕ) : ZMod p) := by
rw [Finset.mem_Ico] at hi
have hodd := odd_p p hp hp2
have hr := r_pos p a i hp ha hi.1 (by omega)
have hlt := Nat.mod_lt (a * i) hp.pos
have e : ((a : ZMod p) * (i : ZMod p)) = (((a * i) % p : ℕ) : ZMod p) := by
rw [ZMod.natCast_mod]; push_cast; ring
rw [e]
unfold m
split_ifs with h
· rw [min_eq_right (by omega), Nat.cast_sub (by omega), ZMod.natCast_self]
ring
· rw [min_eq_left (by omega)]
ring
-- L2a : Gauss lemma
theorem gauss (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(a : ZMod p) ^ (p / 2) =
(-1) ^ ((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card := by
haveI := Fact.mk hp
set S := Ico 1 (p / 2 + 1) with hS
have hcard : S.card = p / 2 := by simp [hS]
have h1 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) = (a : ZMod p) ^ (p / 2) * ∏ i ∈ S, (i : ZMod p) := by
rw [Finset.prod_mul_distrib, Finset.prod_const, hcard]
have h2 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) =
(-1) ^ (S.filter (fun i => p / 2 < (a * i) % p)).card * ∏ i ∈ S, (i : ZMod p) := by
rw [Finset.prod_congr rfl (fun i hi => term p a i hp hp2 ha hi), Finset.prod_mul_distrib,
Finset.prod_ite, Finset.prod_const, Finset.prod_const_one, mul_one]
congr 1
have := Finset.prod_image (s := S) (g := m p a) (f := fun j : ℕ => ((j : ℕ) : ZMod p))
(m_inj p a hp hp2 ha)
rw [← this, hS, m_image p a hp hp2 ha]
have hne : ∏ i ∈ S, (i : ZMod p) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro i hi
rw [hS, Finset.mem_Ico] at hi
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p]
intro hd
have := Nat.le_of_dvd (by omega) hd
have := odd_p p hp hp2
omega
exact mul_right_cancel₀ hne (h1.symm.trans h2)
-- L2b : Eisenstein parity
theorem eisenstein_parity (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a)
(hodd : a % 2 = 1) :
((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card % 2 =
(∑ i ∈ Ico 1 (p / 2 + 1), (a * i) / p) % 2 := by
have hp1 : p % 2 = 1 := by
rcases Nat.mod_two_eq_zero_or_one p with h | h
· rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_of_mod_eq_zero h) with h' | h' <;> omega
· exact h
have hp0 : 0 < p := hp.pos
set s := Ico 1 (p / 2 + 1) with hs
set L := s.filter (fun i => p / 2 < (a * i) % p) with hL
-- sum of m equals sum of i
have hM : ∑ i ∈ s, m p a i = ∑ i ∈ s, i := by
have h1 := m_image p a hp hp2 ha
have h2 := m_inj p a hp hp2 ha
rw [hs]
conv_rhs => rw [← h1]
rw [Finset.sum_image (fun x hx y hy hxy => h2 (by simpa using hx) (by simpa using hy) hxy)]
have hmL : ∀ i ∈ L, m p a i + (a * i) % p = p := by
intro i hi
have hi' := (Finset.mem_filter.mp hi).2
have hr : (a * i) % p < p := Nat.mod_lt _ hp0
unfold m
rw [Nat.min_def]; split_ifs <;> omega
have hmN : ∀ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = (a * i) % p := by
intro i hi
have hi' := (Finset.mem_filter.mp hi).2
have hr : (a * i) % p < p := Nat.mod_lt _ hp0
unfold m
rw [Nat.min_def]; split_ifs <;> omega
have hsplitM := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p) (m p a)
have hsplitR := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p)
(fun i => (a * i) % p)
have hNsum : ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i
= ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p :=
Finset.sum_congr rfl hmN
have hLsum : ∑ i ∈ L, m p a i + ∑ i ∈ L, (a * i) % p = L.card * p := by
rw [← Finset.sum_add_distrib, Finset.sum_congr rfl hmL, Finset.sum_const, smul_eq_mul]
have hdiv : a * ∑ i ∈ s, i = p * ∑ i ∈ s, (a * i) / p + ∑ i ∈ s, (a * i) % p := by
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
exact Finset.sum_congr rfl (fun i _ => (Nat.div_add_mod (a * i) p).symm)
rw [← hL] at hsplitM hsplitR
generalize ∑ i ∈ s, i = S at *
generalize ∑ i ∈ s, (a * i) / p = F at *
generalize ∑ i ∈ s, (a * i) % p = R at *
generalize ∑ i ∈ s, m p a i = M at *
generalize ∑ i ∈ L, m p a i = ML at *
generalize ∑ i ∈ L, (a * i) % p = RL at *
generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = MN at *
generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p = RN at *
generalize L.card = c at *
obtain ⟨a', rfl⟩ : ∃ a', a = 2 * a' + 1 := ⟨a / 2, by omega⟩
obtain ⟨p', rfl⟩ : ∃ p', p = 2 * p' + 1 := ⟨p / 2, by omega⟩
have e1 : (2 * a' + 1) * S = 2 * (a' * S) + S := by ring
have e2 : c * (2 * p' + 1) = 2 * (c * p') + c := by ring
have e3 : (2 * p' + 1) * F = 2 * (p' * F) + F := by ring
rw [e1, e3] at hdiv
rw [e2] at hLsum
generalize a' * S = X at *
generalize c * p' = Y at *
generalize p' * F = Z at *
omega
-- L1 : lattice count
theorem lattice_count (a b n : ℕ) (hb : 0 < b) (hn : a / b ≤ n) (hnd : ¬ b ∣ a) :
((Ico 1 (n + 1)).filter (fun j => b * j < a)).card = a / b := by
have : (Ico 1 (n + 1)).filter (fun j => b * j < a) = Ico 1 (a / b + 1) := by
ext j
simp only [mem_filter, mem_Ico]
have h1 : j ≤ a / b ↔ j * b ≤ a := Nat.le_div_iff_mul_le hb
have h2 : b * j ≠ a := fun h => hnd ⟨j, h.symm⟩
have h3 : j * b = b * j := Nat.mul_comm j b
constructor
· rintro ⟨⟨h4, h5⟩, h6⟩
refine ⟨h4, ?_⟩
have : j ≤ a / b := h1.mpr (by omega)
omega
· rintro ⟨h4, h5⟩
have : j * b ≤ a := h1.mp (by omega)
refine ⟨⟨h4, by omega⟩, by omega⟩
rw [this]
simp
theorem lattice_bound (p q i : ℕ) (hp : p % 2 = 1) (hq : q % 2 = 1) (hi : i ≤ p / 2) :
q * i / p ≤ q / 2 := by
have hp0 : 0 < p := by omega
have := (Nat.div_lt_iff_lt_mul hp0 (x := q * i) (y := q / 2 + 1)).mpr
suffices h : q * i < (q / 2 + 1) * p by have := this h; omega
obtain ⟨a, rfl⟩ : ∃ a, p = 2 * a + 1 := ⟨p / 2, by omega⟩
obtain ⟨b, rfl⟩ : ∃ b, q = 2 * b + 1 := ⟨q / 2, by omega⟩
have ha : (2 * a + 1) / 2 = a := by omega
have hb : (2 * b + 1) / 2 = b := by omega
rw [ha] at hi
rw [hb]
have : (2 * b + 1) * i ≤ (2 * b + 1) * a := Nat.mul_le_mul_left _ hi
nlinarith
theorem lattice_nd (p q i : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hi1 : 1 ≤ i)
(hi : i ≤ p / 2) : ¬ p ∣ q * i := by
intro h
rcases (Nat.Prime.dvd_mul hp).mp h with h | h
· exact hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)
· have := Nat.le_of_dvd (by omega) h
omega
theorem lattice (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hp2 : p ≠ 2) (hq2 : q ≠ 2) :
(∑ i ∈ Ico 1 (p / 2 + 1), (q * i) / p) + (∑ j ∈ Ico 1 (q / 2 + 1), (p * j) / q)
= (p / 2) * (q / 2) := by
have hpo : p % 2 = 1 := Nat.odd_iff.mp (hp.odd_of_ne_two hp2)
have hqo : q % 2 = 1 := Nat.odd_iff.mp (hq.odd_of_ne_two hq2)
have key : ∀ i ∈ Ico 1 (p / 2 + 1), ∀ j ∈ Ico 1 (q / 2 + 1), q * i ≠ p * j := by
intro i hi j _ h
rw [mem_Ico] at hi
exact lattice_nd p q i hp hq hpq (by omega) (by omega) ⟨j, h⟩
symm
calc (p / 2) * (q / 2) = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (1 : ℕ) := by simp
_ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1),
((if p * j < q * i then 1 else 0) + (if q * i < p * j then 1 else 0)) := by
refine sum_congr rfl fun i hi => sum_congr rfl fun j hj => ?_
have := key i hi j hj
split_ifs <;> omega
_ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (if p * j < q * i then 1 else 0)
+ ∑ j ∈ Ico 1 (q / 2 + 1), ∑ i ∈ Ico 1 (p / 2 + 1), (if q * i < p * j then 1 else 0) := by
rw [sum_comm (s := Ico 1 (q / 2 + 1))]
simp only [sum_add_distrib]
_ = _ := by
congr 1
· refine sum_congr rfl fun i hi => ?_
rw [mem_Ico] at hi
rw [← card_filter]
exact lattice_count (q * i) p (q / 2) hp.pos (lattice_bound p q i hpo hqo (by omega))
(lattice_nd p q i hp hq hpq (by omega) (by omega))
· refine sum_congr rfl fun j hj => ?_
rw [mem_Ico] at hj
rw [← card_filter]
exact lattice_count (p * j) q (p / 2) hq.pos (lattice_bound q p j hqo hpo (by omega))
(lattice_nd q p j hq hp (Ne.symm hpq) (by omega) (by omega))
theorem euler (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(∃ x : ℕ, x ^ 2 % p = a % p) ↔ (a : ZMod p) ^ (p / 2) = 1 := by
haveI := Fact.mk hp
have hne : (a : ZMod p) ≠ 0 := by
rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p a]
have hc : ringChar (ZMod p) ≠ 2 := by
rw [ZMod.ringChar_zmod_n]; exact hp2
have hsq := FiniteField.isSquare_iff hc hne
rw [ZMod.card] at hsq
rw [← hsq]
constructor
· rintro ⟨x, hx⟩
refine ⟨(x : ZMod p), ?_⟩
have : ((x ^ 2 : ℕ) : ZMod p) = (a : ZMod p) := (ZMod.natCast_eq_natCast_iff' _ _ _).mpr hx
rw [← this]; push_cast; ring
· rintro ⟨r, hr⟩
refine ⟨r.val, ?_⟩
rw [← ZMod.natCast_eq_natCast_iff']
push_cast
rw [ZMod.natCast_zmod_val, hr]; ring
theorem neg_one_pow_iff (p n : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) :
((-1 : ZMod p) ^ n = 1) ↔ n % 2 = 0 := by
haveI : Fact (2 < p) := ⟨by have := hp.two_le; omega⟩
rcases Nat.even_or_odd n with h | h
· rw [h.neg_one_pow]; simp only [true_iff]; exact Nat.even_iff.mp h
· rw [h.neg_one_pow]
constructor
· intro h1; exact absurd h1 (ZMod.neg_one_ne_one)
· intro h2; have := Nat.odd_iff.mp h; omega
end QR
theorem Lemma.quadratic_reciprocity :
∀ p q : ℕ, p.Prime → q.Prime → p ≠ q → p ≠ 2 → q ≠ 2 → (((∃ x : ℕ, x ^ 2 % q = p % q) ↔ (∃ y : ℕ, y ^ 2 % p = q % p)) ↔ (p % 4 = 1 ∨ q % 4 = 1)) := by
intro p q hp hq hpq hp2 hq2
have hqp : ¬ q ∣ p := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hq hp).mp h).symm
have hpq' : ¬ p ∣ q := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)
have hp1 : p % 2 = 1 := by
rcases hp.eq_two_or_odd with h | h
· exact absurd h hp2
· exact h
have hq1 : q % 2 = 1 := by
rcases hq.eq_two_or_odd with h | h
· exact absurd h hq2
· exact h
rw [QR.euler q p hq hq2 hqp, QR.euler p q hp hp2 hpq', QR.gauss q p hq hq2 hqp,
QR.gauss p q hp hp2 hpq', QR.neg_one_pow_iff q _ hq hq2, QR.neg_one_pow_iff p _ hp hp2,
QR.eisenstein_parity q p hq hq2 hqp hp1, QR.eisenstein_parity p q hp hp2 hpq' hq1]
have hl := QR.lattice p q hp hq hpq hp2 hq2
have hm := Nat.mul_mod (p / 2) (q / 2) 2
have hs := Nat.add_mod (∑ i ∈ Finset.Ico 1 (p / 2 + 1), q * i / p)
(∑ j ∈ Finset.Ico 1 (q / 2 + 1), p * j / q) 2
rw [hl] at hs
rcases Nat.mod_two_eq_zero_or_one (p / 2) with h1 | h1 <;>
rcases Nat.mod_two_eq_zero_or_one (q / 2) with h2 | h2 <;>
simp only [h1, h2] at hm <;> omega
open Lean Elab Command in
run_cmd show CommandElabM Unit from do
let env ← getEnv
let mut seen : NameSet := {}
let mut todo : Array Name := #[`Lemma.quadratic_reciprocity]
while !todo.isEmpty do
let n := todo.back!
todo := todo.pop
if seen.contains n then continue
seen := seen.insert n
match env.find? n with
| some ci =>
let mut cs := ci.type.getUsedConstants
match ci with
| .thmInfo t => cs := cs ++ t.value.getUsedConstants
| .defnInfo d => cs := cs ++ d.value.getUsedConstants
| _ => pure ()
for c in cs do
if !seen.contains c then todo := todo.push c
| none => pure ()
let all := seen.toList
let ff := all.filter (fun n => (`FiniteField).isPrefixOf n)
let pc := all.filter (fun n => (n.toString.splitOn "pow_card").length > 1)
let poly := all.filter (fun n => (`Polynomial).isPrefixOf n)
throwError m!"total {all.length} FF {ff.length} {ff} powcard {pc} poly {poly.length}"
// file: audit_qr.lean
import Mathlib.FieldTheory.Finite.Basic
open Finset
namespace QR
/-- the "absolute least residue" of a*i mod p -/
def m (p a i : ℕ) : ℕ := min ((a * i) % p) (p - (a * i) % p)
lemma r_pos (p a i : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) (h1 : 1 ≤ i) (h2 : i < p) :
0 < (a * i) % p := by
rcases Nat.eq_zero_or_pos ((a * i) % p) with h | h
· exfalso
have hd : p ∣ a * i := Nat.dvd_of_mod_eq_zero h
rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'
· exact ha h'
· have := Nat.le_of_dvd (by omega) h'
omega
· exact h
lemma odd_p (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) : p % 2 = 1 := by
rcases hp.eq_two_or_odd with h | h
· exact absurd h hp2
· exact h
-- L0 : bijection
theorem m_mem (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
∀ i ∈ Ico 1 (p / 2 + 1), m p a i ∈ Ico 1 (p / 2 + 1) := by
intro i hi
rw [Finset.mem_Ico] at hi
have hodd := odd_p p hp hp2
have hr := r_pos p a i hp ha hi.1 (by omega)
have hlt := Nat.mod_lt (a * i) hp.pos
rw [Finset.mem_Ico]
unfold m
constructor
· apply le_min <;> omega
· have := min_le_left ((a * i) % p) (p - (a * i) % p)
have := min_le_right ((a * i) % p) (p - (a * i) % p)
rcases le_total ((a * i) % p) (p - (a * i) % p) with h | h
· rw [min_eq_left h]; omega
· rw [min_eq_right h]; omega
theorem m_inj (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
Set.InjOn (m p a) (Ico 1 (p / 2 + 1) : Set ℕ) := by
intro i hi j hj h
simp only [Finset.coe_Ico, Set.mem_Ico, Finset.mem_coe, Finset.mem_Ico] at hi hj
have hodd := odd_p p hp hp2
have hri := r_pos p a i hp ha hi.1 (by omega)
have hrj := r_pos p a j hp ha hj.1 (by omega)
have hlti := Nat.mod_lt (a * i) hp.pos
have hltj := Nat.mod_lt (a * j) hp.pos
unfold m at h
have key : (a * i) % p = (a * j) % p ∨ (a * i) % p + (a * j) % p = p := by
rcases le_total ((a * i) % p) (p - (a * i) % p) with h1 | h1 <;>
rcases le_total ((a * j) % p) (p - (a * j) % p) with h2 | h2 <;>
simp only [min_eq_left h1, min_eq_right h1, min_eq_left h2, min_eq_right h2] at h <;>
omega
haveI := Fact.mk hp
rcases key with k | k
· have e := (ZMod.natCast_eq_natCast_iff' (a * i) (a * j) p).mpr k
push_cast at e
have ha' : (a : ZMod p) ≠ 0 := by
rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p]
have e2 := mul_left_cancel₀ ha' e
have e3 := (ZMod.natCast_eq_natCast_iff' i j p).mp e2
rwa [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at e3
· exfalso
have hz : (a * (i + j)) % p = 0 := by
rw [Nat.mul_add, Nat.add_mod, k, Nat.mod_self]
have hd : p ∣ a * (i + j) := Nat.dvd_of_mod_eq_zero hz
rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'
· exact ha h'
· have := Nat.le_of_dvd (by omega) h'
omega
theorem m_image (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(Ico 1 (p / 2 + 1)).image (m p a) = Ico 1 (p / 2 + 1) := by
apply Finset.eq_of_subset_of_card_le
· intro x hx
rw [Finset.mem_image] at hx
obtain ⟨i, hi, rfl⟩ := hx
exact m_mem p a hp hp2 ha i hi
· rw [Finset.card_image_of_injOn (m_inj p a hp hp2 ha)]
lemma term (p a i : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) (hi : i ∈ Ico 1 (p / 2 + 1)) :
((a : ZMod p) * (i : ZMod p)) =
(if p / 2 < (a * i) % p then (-1 : ZMod p) else 1) * ((m p a i : ℕ) : ZMod p) := by
rw [Finset.mem_Ico] at hi
have hodd := odd_p p hp hp2
have hr := r_pos p a i hp ha hi.1 (by omega)
have hlt := Nat.mod_lt (a * i) hp.pos
have e : ((a : ZMod p) * (i : ZMod p)) = (((a * i) % p : ℕ) : ZMod p) := by
rw [ZMod.natCast_mod]; push_cast; ring
rw [e]
unfold m
split_ifs with h
· rw [min_eq_right (by omega), Nat.cast_sub (by omega), ZMod.natCast_self]
ring
· rw [min_eq_left (by omega)]
ring
-- L2a : Gauss lemma
theorem gauss (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(a : ZMod p) ^ (p / 2) =
(-1) ^ ((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card := by
haveI := Fact.mk hp
set S := Ico 1 (p / 2 + 1) with hS
have hcard : S.card = p / 2 := by simp [hS]
have h1 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) = (a : ZMod p) ^ (p / 2) * ∏ i ∈ S, (i : ZMod p) := by
rw [Finset.prod_mul_distrib, Finset.prod_const, hcard]
have h2 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) =
(-1) ^ (S.filter (fun i => p / 2 < (a * i) % p)).card * ∏ i ∈ S, (i : ZMod p) := by
rw [Finset.prod_congr rfl (fun i hi => term p a i hp hp2 ha hi), Finset.prod_mul_distrib,
Finset.prod_ite, Finset.prod_const, Finset.prod_const_one, mul_one]
congr 1
have := Finset.prod_image (s := S) (g := m p a) (f := fun j : ℕ => ((j : ℕ) : ZMod p))
(m_inj p a hp hp2 ha)
rw [← this, hS, m_image p a hp hp2 ha]
have hne : ∏ i ∈ S, (i : ZMod p) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro i hi
rw [hS, Finset.mem_Ico] at hi
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p]
intro hd
have := Nat.le_of_dvd (by omega) hd
have := odd_p p hp hp2
omega
exact mul_right_cancel₀ hne (h1.symm.trans h2)
-- L2b : Eisenstein parity
theorem eisenstein_parity (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a)
(hodd : a % 2 = 1) :
((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card % 2 =
(∑ i ∈ Ico 1 (p / 2 + 1), (a * i) / p) % 2 := by
have hp1 : p % 2 = 1 := by
rcases Nat.mod_two_eq_zero_or_one p with h | h
· rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_of_mod_eq_zero h) with h' | h' <;> omega
· exact h
have hp0 : 0 < p := hp.pos
set s := Ico 1 (p / 2 + 1) with hs
set L := s.filter (fun i => p / 2 < (a * i) % p) with hL
-- sum of m equals sum of i
have hM : ∑ i ∈ s, m p a i = ∑ i ∈ s, i := by
have h1 := m_image p a hp hp2 ha
have h2 := m_inj p a hp hp2 ha
rw [hs]
conv_rhs => rw [← h1]
rw [Finset.sum_image (fun x hx y hy hxy => h2 (by simpa using hx) (by simpa using hy) hxy)]
have hmL : ∀ i ∈ L, m p a i + (a * i) % p = p := by
intro i hi
have hi' := (Finset.mem_filter.mp hi).2
have hr : (a * i) % p < p := Nat.mod_lt _ hp0
unfold m
rw [Nat.min_def]; split_ifs <;> omega
have hmN : ∀ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = (a * i) % p := by
intro i hi
have hi' := (Finset.mem_filter.mp hi).2
have hr : (a * i) % p < p := Nat.mod_lt _ hp0
unfold m
rw [Nat.min_def]; split_ifs <;> omega
have hsplitM := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p) (m p a)
have hsplitR := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p)
(fun i => (a * i) % p)
have hNsum : ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i
= ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p :=
Finset.sum_congr rfl hmN
have hLsum : ∑ i ∈ L, m p a i + ∑ i ∈ L, (a * i) % p = L.card * p := by
rw [← Finset.sum_add_distrib, Finset.sum_congr rfl hmL, Finset.sum_const, smul_eq_mul]
have hdiv : a * ∑ i ∈ s, i = p * ∑ i ∈ s, (a * i) / p + ∑ i ∈ s, (a * i) % p := by
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
exact Finset.sum_congr rfl (fun i _ => (Nat.div_add_mod (a * i) p).symm)
rw [← hL] at hsplitM hsplitR
generalize ∑ i ∈ s, i = S at *
generalize ∑ i ∈ s, (a * i) / p = F at *
generalize ∑ i ∈ s, (a * i) % p = R at *
generalize ∑ i ∈ s, m p a i = M at *
generalize ∑ i ∈ L, m p a i = ML at *
generalize ∑ i ∈ L, (a * i) % p = RL at *
generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = MN at *
generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p = RN at *
generalize L.card = c at *
obtain ⟨a', rfl⟩ : ∃ a', a = 2 * a' + 1 := ⟨a / 2, by omega⟩
obtain ⟨p', rfl⟩ : ∃ p', p = 2 * p' + 1 := ⟨p / 2, by omega⟩
have e1 : (2 * a' + 1) * S = 2 * (a' * S) + S := by ring
have e2 : c * (2 * p' + 1) = 2 * (c * p') + c := by ring
have e3 : (2 * p' + 1) * F = 2 * (p' * F) + F := by ring
rw [e1, e3] at hdiv
rw [e2] at hLsum
generalize a' * S = X at *
generalize c * p' = Y at *
generalize p' * F = Z at *
omega
-- L1 : lattice count
theorem lattice_count (a b n : ℕ) (hb : 0 < b) (hn : a / b ≤ n) (hnd : ¬ b ∣ a) :
((Ico 1 (n + 1)).filter (fun j => b * j < a)).card = a / b := by
have : (Ico 1 (n + 1)).filter (fun j => b * j < a) = Ico 1 (a / b + 1) := by
ext j
simp only [mem_filter, mem_Ico]
have h1 : j ≤ a / b ↔ j * b ≤ a := Nat.le_div_iff_mul_le hb
have h2 : b * j ≠ a := fun h => hnd ⟨j, h.symm⟩
have h3 : j * b = b * j := Nat.mul_comm j b
constructor
· rintro ⟨⟨h4, h5⟩, h6⟩
refine ⟨h4, ?_⟩
have : j ≤ a / b := h1.mpr (by omega)
omega
· rintro ⟨h4, h5⟩
have : j * b ≤ a := h1.mp (by omega)
refine ⟨⟨h4, by omega⟩, by omega⟩
rw [this]
simp
theorem lattice_bound (p q i : ℕ) (hp : p % 2 = 1) (hq : q % 2 = 1) (hi : i ≤ p / 2) :
q * i / p ≤ q / 2 := by
have hp0 : 0 < p := by omega
have := (Nat.div_lt_iff_lt_mul hp0 (x := q * i) (y := q / 2 + 1)).mpr
suffices h : q * i < (q / 2 + 1) * p by have := this h; omega
obtain ⟨a, rfl⟩ : ∃ a, p = 2 * a + 1 := ⟨p / 2, by omega⟩
obtain ⟨b, rfl⟩ : ∃ b, q = 2 * b + 1 := ⟨q / 2, by omega⟩
have ha : (2 * a + 1) / 2 = a := by omega
have hb : (2 * b + 1) / 2 = b := by omega
rw [ha] at hi
rw [hb]
have : (2 * b + 1) * i ≤ (2 * b + 1) * a := Nat.mul_le_mul_left _ hi
nlinarith
theorem lattice_nd (p q i : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hi1 : 1 ≤ i)
(hi : i ≤ p / 2) : ¬ p ∣ q * i := by
intro h
rcases (Nat.Prime.dvd_mul hp).mp h with h | h
· exact hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)
· have := Nat.le_of_dvd (by omega) h
omega
theorem lattice (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hp2 : p ≠ 2) (hq2 : q ≠ 2) :
(∑ i ∈ Ico 1 (p / 2 + 1), (q * i) / p) + (∑ j ∈ Ico 1 (q / 2 + 1), (p * j) / q)
= (p / 2) * (q / 2) := by
have hpo : p % 2 = 1 := Nat.odd_iff.mp (hp.odd_of_ne_two hp2)
have hqo : q % 2 = 1 := Nat.odd_iff.mp (hq.odd_of_ne_two hq2)
have key : ∀ i ∈ Ico 1 (p / 2 + 1), ∀ j ∈ Ico 1 (q / 2 + 1), q * i ≠ p * j := by
intro i hi j _ h
rw [mem_Ico] at hi
exact lattice_nd p q i hp hq hpq (by omega) (by omega) ⟨j, h⟩
symm
calc (p / 2) * (q / 2) = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (1 : ℕ) := by simp
_ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1),
((if p * j < q * i then 1 else 0) + (if q * i < p * j then 1 else 0)) := by
refine sum_congr rfl fun i hi => sum_congr rfl fun j hj => ?_
have := key i hi j hj
split_ifs <;> omega
_ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (if p * j < q * i then 1 else 0)
+ ∑ j ∈ Ico 1 (q / 2 + 1), ∑ i ∈ Ico 1 (p / 2 + 1), (if q * i < p * j then 1 else 0) := by
rw [sum_comm (s := Ico 1 (q / 2 + 1))]
simp only [sum_add_distrib]
_ = _ := by
congr 1
· refine sum_congr rfl fun i hi => ?_
rw [mem_Ico] at hi
rw [← card_filter]
exact lattice_count (q * i) p (q / 2) hp.pos (lattice_bound p q i hpo hqo (by omega))
(lattice_nd p q i hp hq hpq (by omega) (by omega))
· refine sum_congr rfl fun j hj => ?_
rw [mem_Ico] at hj
rw [← card_filter]
exact lattice_count (p * j) q (p / 2) hq.pos (lattice_bound q p j hqo hpo (by omega))
(lattice_nd q p j hq hp (Ne.symm hpq) (by omega) (by omega))
-- Euler's criterion by hand (no FiniteField): Wilson + Fermat + pairing x ↦ a/x
lemma e_fact_cast (p : ℕ) : ∀ n : ℕ,
((n.factorial : ℕ) : ZMod p) = ∏ i ∈ Finset.range n, ((i + 1 : ℕ) : ZMod p)
| 0 => by rw [Nat.factorial_zero, Finset.prod_range_zero, Nat.cast_one]
| n + 1 => by
rw [Finset.prod_range_succ, ← e_fact_cast p n, Nat.factorial_succ, Nat.cast_mul, mul_comm]
lemma e_wilson_prod (p : ℕ) [hp : Fact p.Prime] (h2 : p ≠ 2) :
∏ x ∈ (Finset.univ.erase 0 : Finset (ZMod p)), x = -1 := by
have hne : (1 : ZMod p) ≠ -1 := by
intro h
have h' : ((2 : ℕ) : ZMod p) = 0 := by
rw [Nat.cast_ofNat]
calc (2 : ZMod p) = 1 + 1 := one_add_one_eq_two.symm
_ = -1 + 1 := by rw [← h]
_ = 0 := neg_add_cancel 1
rw [ZMod.natCast_eq_zero_iff] at h'
have := (Nat.prime_dvd_prime_iff_eq hp.out Nat.prime_two).mp h'
exact h2 this
have hsub : ({1, -1} : Finset (ZMod p)) ⊆ Finset.univ.erase 0 := by
intro x hx
simp only [Finset.mem_insert, Finset.mem_singleton] at hx
rw [Finset.mem_erase]
refine ⟨?_, Finset.mem_univ _⟩
rcases hx with rfl | rfl
· exact one_ne_zero
· exact neg_ne_zero.mpr one_ne_zero
rw [← Finset.prod_sdiff hsub]
have hrest : ∏ x ∈ (Finset.univ.erase 0 : Finset (ZMod p)) \ {1, -1}, x = 1 := by
refine Finset.prod_involution (fun x _ => x⁻¹) ?_ ?_ ?_ ?_
· intro a ha
simp only [Finset.mem_sdiff, Finset.mem_erase] at ha
exact mul_inv_cancel₀ ha.1.1
· intro a ha _ h
simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert,
Finset.mem_singleton, not_or] at ha
have h1 : a * a = 1 := by
calc a * a = a * a⁻¹ := by rw [h]
_ = 1 := mul_inv_cancel₀ ha.1.1
have h3 : (a - 1) * (a + 1) = 0 := by
calc (a - 1) * (a + 1) = a * a - 1 := by ring
_ = 0 := by rw [h1]; exact sub_self 1
rcases mul_eq_zero.mp h3 with h4 | h4
· exact ha.2.1 (sub_eq_zero.mp h4)
· exact ha.2.2 (eq_neg_of_add_eq_zero_left h4)
· intro a ha
simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert,
Finset.mem_singleton, not_or, Finset.mem_univ, and_true] at ha ⊢
refine ⟨inv_ne_zero ha.1, ?_, ?_⟩
· intro h; apply ha.2.1
rw [← inv_inv a, h, inv_one]
· intro h; apply ha.2.2
rw [← inv_inv a, h, inv_neg, inv_one]
· intro a _
exact inv_inv a
rw [hrest, Finset.prod_pair hne]
simp
lemma e_card (p : ℕ) [Fact p.Prime] :
(Finset.univ.erase 0 : Finset (ZMod p)).card = p - 1 := by
rw [Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ZMod.card]
lemma e_fermat (p : ℕ) [hp : Fact p.Prime] (h2 : p ≠ 2) (x : ZMod p) (hx : x ≠ 0) :
x ^ (p - 1) = 1 := by
have hP := e_wilson_prod p h2
have key : ∏ y ∈ (Finset.univ.erase 0 : Finset (ZMod p)), (x * y) =
∏ y ∈ (Finset.univ.erase 0 : Finset (ZMod p)), y := by
refine Finset.prod_nbij' (fun y => x * y) (fun y => x⁻¹ * y) ?_ ?_ ?_ ?_ ?_
· intro y hy
simp only [Finset.mem_coe, Finset.mem_erase, Finset.mem_univ, and_true] at hy ⊢
exact mul_ne_zero hx hy
· intro y hy
simp only [Finset.mem_coe, Finset.mem_erase, Finset.mem_univ, and_true] at hy ⊢
exact mul_ne_zero (inv_ne_zero hx) hy
· intro y _
show x⁻¹ * (x * y) = y
rw [← mul_assoc, inv_mul_cancel₀ hx, one_mul]
· intro y _
show x * (x⁻¹ * y) = y
rw [← mul_assoc, mul_inv_cancel₀ hx, one_mul]
· intro y _
rfl
rw [Finset.prod_mul_distrib, Finset.prod_const, e_card, hP] at key
have : x ^ (p - 1) * (-1) * (-1) = (-1) * (-1) := by rw [key]
simpa using this
lemma e_pair (p : ℕ) [Fact p.Prime] (a : ZMod p) (ha : a ≠ 0) (hns : ¬ IsSquare a) :
∀ n : ℕ, ∀ S : Finset (ZMod p), S.card ≤ n → (∀ x ∈ S, x ≠ 0 ∧ a * x⁻¹ ∈ S) →
∏ x ∈ S, x = a ^ (S.card / 2) := by
intro n
induction n with
| zero =>
intro S hS _
have : S = ∅ := Finset.card_eq_zero.mp (by omega)
subst this; simp
| succ n ih =>
intro S hS hcl
rcases S.eq_empty_or_nonempty with h | ⟨y, hy⟩
· subst h; simp
obtain ⟨hy0, hzS⟩ := hcl y hy
set z := a * y⁻¹ with hz
have hyz : y * z = a := by
rw [hz, mul_comm a, ← mul_assoc, mul_inv_cancel₀ hy0, one_mul]
have hzy : z ≠ y := by
intro h; apply hns; exact ⟨y, by rw [← hyz, h]⟩
have hz0 : z ≠ 0 := (hcl z hzS).1
have hzmem : z ∈ S.erase y := Finset.mem_erase.mpr ⟨hzy, hzS⟩
set T := (S.erase y).erase z with hT
have hcard : S.card = T.card + 2 := by
rw [hT, Finset.card_erase_of_mem hzmem, Finset.card_erase_of_mem hy]
have := Finset.card_pos.mpr ⟨y, hy⟩
have : 1 ≤ (S.erase y).card := Finset.card_pos.mpr ⟨z, hzmem⟩
rw [Finset.card_erase_of_mem hy] at this
omega
have hinv : ∀ u v : ZMod p, u ≠ 0 → a * u⁻¹ = v → u = a * v⁻¹ := by
intro u v hu h
rw [← h, mul_inv_rev, inv_inv, mul_comm u, ← mul_assoc, mul_inv_cancel₀ ha, one_mul]
have hTcl : ∀ x ∈ T, x ≠ 0 ∧ a * x⁻¹ ∈ T := by
intro x hx
rw [hT, Finset.mem_erase, Finset.mem_erase] at hx
obtain ⟨hxz, hxy, hxS⟩ := hx
obtain ⟨hx0, hwS⟩ := hcl x hxS
refine ⟨hx0, ?_⟩
rw [hT, Finset.mem_erase, Finset.mem_erase]
refine ⟨?_, ?_, hwS⟩
· intro h
apply hxy
have h1 := hinv x z hx0 h
rw [hz, mul_inv_rev, inv_inv, mul_comm y, ← mul_assoc, mul_inv_cancel₀ ha, one_mul] at h1
exact h1
· intro h
exact hxz (hinv x y hx0 h)
have hTc : T.card ≤ n := by omega
have ih' := ih T hTc hTcl
rw [← Finset.mul_prod_erase S _ hy, ← Finset.mul_prod_erase (S.erase y) _ hzmem, ← hT, ih',
← mul_assoc, hyz, hcard, show (T.card + 2) / 2 = T.card / 2 + 1 by omega, pow_succ,
mul_comm]
lemma e_euler (p : ℕ) [Fact p.Prime] (h2 : p ≠ 2) (a : ZMod p) (ha : a ≠ 0) :
IsSquare a ↔ a ^ (p / 2) = 1 := by
have hp1 : p % 2 = 1 := odd_p p Fact.out h2
constructor
· rintro ⟨r, rfl⟩
have hr : r ≠ 0 := by rintro rfl; exact ha (mul_zero 0)
rw [← pow_two, ← pow_mul, show 2 * (p / 2) = p - 1 by omega]
exact e_fermat p h2 r hr
· intro h
by_contra hns
have hS := e_pair p a ha hns _ (Finset.univ.erase 0) le_rfl (by
intro x hx
rw [Finset.mem_erase] at hx ⊢
exact ⟨hx.1, mul_ne_zero ha (inv_ne_zero hx.1), Finset.mem_univ _⟩)
rw [e_wilson_prod p h2, e_card, show (p - 1) / 2 = p / 2 by omega, h] at hS
haveI : Fact (2 < p) := ⟨by have := (Fact.out : p.Prime).two_le; omega⟩
exact ZMod.neg_one_ne_one hS
theorem euler (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(∃ x : ℕ, x ^ 2 % p = a % p) ↔ (a : ZMod p) ^ (p / 2) = 1 := by
haveI := Fact.mk hp
have hne : (a : ZMod p) ≠ 0 := by
rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p a]
rw [← e_euler p hp2 _ hne]
constructor
· rintro ⟨x, hx⟩
refine ⟨(x : ZMod p), ?_⟩
have : ((x ^ 2 : ℕ) : ZMod p) = (a : ZMod p) := (ZMod.natCast_eq_natCast_iff' _ _ _).mpr hx
rw [← this]; push_cast; ring
· rintro ⟨r, hr⟩
refine ⟨r.val, ?_⟩
rw [← ZMod.natCast_eq_natCast_iff']
push_cast
rw [ZMod.natCast_zmod_val, hr]; ring
theorem neg_one_pow_iff (p n : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) :
((-1 : ZMod p) ^ n = 1) ↔ n % 2 = 0 := by
haveI : Fact (2 < p) := ⟨by have := hp.two_le; omega⟩
rcases Nat.even_or_odd n with h | h
· rw [h.neg_one_pow]; simp only [true_iff]; exact Nat.even_iff.mp h
· rw [h.neg_one_pow]
constructor
· intro h1; exact absurd h1 (ZMod.neg_one_ne_one)
· intro h2; have := Nat.odd_iff.mp h; omega
end QR
theorem Lemma.quadratic_reciprocity :
∀ p q : ℕ, p.Prime → q.Prime → p ≠ q → p ≠ 2 → q ≠ 2 → (((∃ x : ℕ, x ^ 2 % q = p % q) ↔ (∃ y : ℕ, y ^ 2 % p = q % p)) ↔ (p % 4 = 1 ∨ q % 4 = 1)) := by
intro p q hp hq hpq hp2 hq2
have hqp : ¬ q ∣ p := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hq hp).mp h).symm
have hpq' : ¬ p ∣ q := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)
have hp1 : p % 2 = 1 := by
rcases hp.eq_two_or_odd with h | h
· exact absurd h hp2
· exact h
have hq1 : q % 2 = 1 := by
rcases hq.eq_two_or_odd with h | h
· exact absurd h hq2
· exact h
rw [QR.euler q p hq hq2 hqp, QR.euler p q hp hp2 hpq', QR.gauss q p hq hq2 hqp,
QR.gauss p q hp hp2 hpq', QR.neg_one_pow_iff q _ hq hq2, QR.neg_one_pow_iff p _ hp hp2,
QR.eisenstein_parity q p hq hq2 hqp hp1, QR.eisenstein_parity p q hp hp2 hpq' hq1]
have hl := QR.lattice p q hp hq hpq hp2 hq2
have hm := Nat.mul_mod (p / 2) (q / 2) 2
have hs := Nat.add_mod (∑ i ∈ Finset.Ico 1 (p / 2 + 1), q * i / p)
(∑ j ∈ Finset.Ico 1 (q / 2 + 1), p * j / q) 2
rw [hl] at hs
rcases Nat.mod_two_eq_zero_or_one (p / 2) with h1 | h1 <;>
rcases Nat.mod_two_eq_zero_or_one (q / 2) with h2 | h2 <;>
simp only [h1, h2] at hm <;> omega
open Lean Elab Command in
run_cmd show CommandElabM Unit from do
let env ← getEnv
let mut seen : NameSet := {}
let mut todo : Array Name := #[`Lemma.quadratic_reciprocity]
while !todo.isEmpty do
let n := todo.back!
todo := todo.pop
if seen.contains n then continue
seen := seen.insert n
match env.find? n with
| some ci =>
let mut cs := ci.type.getUsedConstants
match ci with
| .thmInfo t => cs := cs ++ t.value.getUsedConstants
| .defnInfo d => cs := cs ++ d.value.getUsedConstants
| _ => pure ()
for c in cs do
if !seen.contains c then todo := todo.push c
| none => pure ()
let all := seen.toList
let ff := all.filter (fun n => (`FiniteField).isPrefixOf n)
let pc := all.filter (fun n => (n.toString.splitOn "pow_card").length > 1)
let poly := all.filter (fun n => (`Polynomial).isPrefixOf n)
throwError m!"total {all.length} FF {ff.length} {ff} powcard {pc} poly {poly.length}"
// file: orig_qr.lean
import Mathlib.FieldTheory.Finite.Basic
open Finset
namespace QR
/-- the "absolute least residue" of a*i mod p -/
def m (p a i : ℕ) : ℕ := min ((a * i) % p) (p - (a * i) % p)
lemma r_pos (p a i : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) (h1 : 1 ≤ i) (h2 : i < p) :
0 < (a * i) % p := by
rcases Nat.eq_zero_or_pos ((a * i) % p) with h | h
· exfalso
have hd : p ∣ a * i := Nat.dvd_of_mod_eq_zero h
rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'
· exact ha h'
· have := Nat.le_of_dvd (by omega) h'
omega
· exact h
lemma odd_p (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) : p % 2 = 1 := by
rcases hp.eq_two_or_odd with h | h
· exact absurd h hp2
· exact h
-- L0 : bijection
theorem m_mem (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
∀ i ∈ Ico 1 (p / 2 + 1), m p a i ∈ Ico 1 (p / 2 + 1) := by
intro i hi
rw [Finset.mem_Ico] at hi
have hodd := odd_p p hp hp2
have hr := r_pos p a i hp ha hi.1 (by omega)
have hlt := Nat.mod_lt (a * i) hp.pos
rw [Finset.mem_Ico]
unfold m
constructor
· apply le_min <;> omega
· have := min_le_left ((a * i) % p) (p - (a * i) % p)
have := min_le_right ((a * i) % p) (p - (a * i) % p)
rcases le_total ((a * i) % p) (p - (a * i) % p) with h | h
· rw [min_eq_left h]; omega
· rw [min_eq_right h]; omega
theorem m_inj (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
Set.InjOn (m p a) (Ico 1 (p / 2 + 1) : Set ℕ) := by
intro i hi j hj h
simp only [Finset.coe_Ico, Set.mem_Ico, Finset.mem_coe, Finset.mem_Ico] at hi hj
have hodd := odd_p p hp hp2
have hri := r_pos p a i hp ha hi.1 (by omega)
have hrj := r_pos p a j hp ha hj.1 (by omega)
have hlti := Nat.mod_lt (a * i) hp.pos
have hltj := Nat.mod_lt (a * j) hp.pos
unfold m at h
have key : (a * i) % p = (a * j) % p ∨ (a * i) % p + (a * j) % p = p := by
rcases le_total ((a * i) % p) (p - (a * i) % p) with h1 | h1 <;>
rcases le_total ((a * j) % p) (p - (a * j) % p) with h2 | h2 <;>
simp only [min_eq_left h1, min_eq_right h1, min_eq_left h2, min_eq_right h2] at h <;>
omega
haveI := Fact.mk hp
rcases key with k | k
· have e := (ZMod.natCast_eq_natCast_iff' (a * i) (a * j) p).mpr k
push_cast at e
have ha' : (a : ZMod p) ≠ 0 := by
rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p]
have e2 := mul_left_cancel₀ ha' e
have e3 := (ZMod.natCast_eq_natCast_iff' i j p).mp e2
rwa [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at e3
· exfalso
have hz : (a * (i + j)) % p = 0 := by
rw [Nat.mul_add, Nat.add_mod, k, Nat.mod_self]
have hd : p ∣ a * (i + j) := Nat.dvd_of_mod_eq_zero hz
rcases (Nat.Prime.dvd_mul hp).mp hd with h' | h'
· exact ha h'
· have := Nat.le_of_dvd (by omega) h'
omega
theorem m_image (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(Ico 1 (p / 2 + 1)).image (m p a) = Ico 1 (p / 2 + 1) := by
apply Finset.eq_of_subset_of_card_le
· intro x hx
rw [Finset.mem_image] at hx
obtain ⟨i, hi, rfl⟩ := hx
exact m_mem p a hp hp2 ha i hi
· rw [Finset.card_image_of_injOn (m_inj p a hp hp2 ha)]
lemma term (p a i : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) (hi : i ∈ Ico 1 (p / 2 + 1)) :
((a : ZMod p) * (i : ZMod p)) =
(if p / 2 < (a * i) % p then (-1 : ZMod p) else 1) * ((m p a i : ℕ) : ZMod p) := by
rw [Finset.mem_Ico] at hi
have hodd := odd_p p hp hp2
have hr := r_pos p a i hp ha hi.1 (by omega)
have hlt := Nat.mod_lt (a * i) hp.pos
have e : ((a : ZMod p) * (i : ZMod p)) = (((a * i) % p : ℕ) : ZMod p) := by
rw [ZMod.natCast_mod]; push_cast; ring
rw [e]
unfold m
split_ifs with h
· rw [min_eq_right (by omega), Nat.cast_sub (by omega), ZMod.natCast_self]
ring
· rw [min_eq_left (by omega)]
ring
-- L2a : Gauss lemma
theorem gauss (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(a : ZMod p) ^ (p / 2) =
(-1) ^ ((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card := by
haveI := Fact.mk hp
set S := Ico 1 (p / 2 + 1) with hS
have hcard : S.card = p / 2 := by simp [hS]
have h1 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) = (a : ZMod p) ^ (p / 2) * ∏ i ∈ S, (i : ZMod p) := by
rw [Finset.prod_mul_distrib, Finset.prod_const, hcard]
have h2 : ∏ i ∈ S, ((a : ZMod p) * (i : ZMod p)) =
(-1) ^ (S.filter (fun i => p / 2 < (a * i) % p)).card * ∏ i ∈ S, (i : ZMod p) := by
rw [Finset.prod_congr rfl (fun i hi => term p a i hp hp2 ha hi), Finset.prod_mul_distrib,
Finset.prod_ite, Finset.prod_const, Finset.prod_const_one, mul_one]
congr 1
have := Finset.prod_image (s := S) (g := m p a) (f := fun j : ℕ => ((j : ℕ) : ZMod p))
(m_inj p a hp hp2 ha)
rw [← this, hS, m_image p a hp hp2 ha]
have hne : ∏ i ∈ S, (i : ZMod p) ≠ 0 := by
rw [Finset.prod_ne_zero_iff]
intro i hi
rw [hS, Finset.mem_Ico] at hi
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p]
intro hd
have := Nat.le_of_dvd (by omega) hd
have := odd_p p hp hp2
omega
exact mul_right_cancel₀ hne (h1.symm.trans h2)
-- L2b : Eisenstein parity
theorem eisenstein_parity (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a)
(hodd : a % 2 = 1) :
((Ico 1 (p / 2 + 1)).filter (fun i => p / 2 < (a * i) % p)).card % 2 =
(∑ i ∈ Ico 1 (p / 2 + 1), (a * i) / p) % 2 := by
have hp1 : p % 2 = 1 := by
rcases Nat.mod_two_eq_zero_or_one p with h | h
· rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_of_mod_eq_zero h) with h' | h' <;> omega
· exact h
have hp0 : 0 < p := hp.pos
set s := Ico 1 (p / 2 + 1) with hs
set L := s.filter (fun i => p / 2 < (a * i) % p) with hL
-- sum of m equals sum of i
have hM : ∑ i ∈ s, m p a i = ∑ i ∈ s, i := by
have h1 := m_image p a hp hp2 ha
have h2 := m_inj p a hp hp2 ha
rw [hs]
conv_rhs => rw [← h1]
rw [Finset.sum_image (fun x hx y hy hxy => h2 (by simpa using hx) (by simpa using hy) hxy)]
have hmL : ∀ i ∈ L, m p a i + (a * i) % p = p := by
intro i hi
have hi' := (Finset.mem_filter.mp hi).2
have hr : (a * i) % p < p := Nat.mod_lt _ hp0
unfold m
rw [Nat.min_def]; split_ifs <;> omega
have hmN : ∀ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = (a * i) % p := by
intro i hi
have hi' := (Finset.mem_filter.mp hi).2
have hr : (a * i) % p < p := Nat.mod_lt _ hp0
unfold m
rw [Nat.min_def]; split_ifs <;> omega
have hsplitM := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p) (m p a)
have hsplitR := Finset.sum_filter_add_sum_filter_not s (fun i => p / 2 < (a * i) % p)
(fun i => (a * i) % p)
have hNsum : ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i
= ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p :=
Finset.sum_congr rfl hmN
have hLsum : ∑ i ∈ L, m p a i + ∑ i ∈ L, (a * i) % p = L.card * p := by
rw [← Finset.sum_add_distrib, Finset.sum_congr rfl hmL, Finset.sum_const, smul_eq_mul]
have hdiv : a * ∑ i ∈ s, i = p * ∑ i ∈ s, (a * i) / p + ∑ i ∈ s, (a * i) % p := by
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
exact Finset.sum_congr rfl (fun i _ => (Nat.div_add_mod (a * i) p).symm)
rw [← hL] at hsplitM hsplitR
generalize ∑ i ∈ s, i = S at *
generalize ∑ i ∈ s, (a * i) / p = F at *
generalize ∑ i ∈ s, (a * i) % p = R at *
generalize ∑ i ∈ s, m p a i = M at *
generalize ∑ i ∈ L, m p a i = ML at *
generalize ∑ i ∈ L, (a * i) % p = RL at *
generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), m p a i = MN at *
generalize ∑ i ∈ s.filter (fun i => ¬ p / 2 < (a * i) % p), (a * i) % p = RN at *
generalize L.card = c at *
obtain ⟨a', rfl⟩ : ∃ a', a = 2 * a' + 1 := ⟨a / 2, by omega⟩
obtain ⟨p', rfl⟩ : ∃ p', p = 2 * p' + 1 := ⟨p / 2, by omega⟩
have e1 : (2 * a' + 1) * S = 2 * (a' * S) + S := by ring
have e2 : c * (2 * p' + 1) = 2 * (c * p') + c := by ring
have e3 : (2 * p' + 1) * F = 2 * (p' * F) + F := by ring
rw [e1, e3] at hdiv
rw [e2] at hLsum
generalize a' * S = X at *
generalize c * p' = Y at *
generalize p' * F = Z at *
omega
-- L1 : lattice count
theorem lattice_count (a b n : ℕ) (hb : 0 < b) (hn : a / b ≤ n) (hnd : ¬ b ∣ a) :
((Ico 1 (n + 1)).filter (fun j => b * j < a)).card = a / b := by
have : (Ico 1 (n + 1)).filter (fun j => b * j < a) = Ico 1 (a / b + 1) := by
ext j
simp only [mem_filter, mem_Ico]
have h1 : j ≤ a / b ↔ j * b ≤ a := Nat.le_div_iff_mul_le hb
have h2 : b * j ≠ a := fun h => hnd ⟨j, h.symm⟩
have h3 : j * b = b * j := Nat.mul_comm j b
constructor
· rintro ⟨⟨h4, h5⟩, h6⟩
refine ⟨h4, ?_⟩
have : j ≤ a / b := h1.mpr (by omega)
omega
· rintro ⟨h4, h5⟩
have : j * b ≤ a := h1.mp (by omega)
refine ⟨⟨h4, by omega⟩, by omega⟩
rw [this]
simp
theorem lattice_bound (p q i : ℕ) (hp : p % 2 = 1) (hq : q % 2 = 1) (hi : i ≤ p / 2) :
q * i / p ≤ q / 2 := by
have hp0 : 0 < p := by omega
have := (Nat.div_lt_iff_lt_mul hp0 (x := q * i) (y := q / 2 + 1)).mpr
suffices h : q * i < (q / 2 + 1) * p by have := this h; omega
obtain ⟨a, rfl⟩ : ∃ a, p = 2 * a + 1 := ⟨p / 2, by omega⟩
obtain ⟨b, rfl⟩ : ∃ b, q = 2 * b + 1 := ⟨q / 2, by omega⟩
have ha : (2 * a + 1) / 2 = a := by omega
have hb : (2 * b + 1) / 2 = b := by omega
rw [ha] at hi
rw [hb]
have : (2 * b + 1) * i ≤ (2 * b + 1) * a := Nat.mul_le_mul_left _ hi
nlinarith
theorem lattice_nd (p q i : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hi1 : 1 ≤ i)
(hi : i ≤ p / 2) : ¬ p ∣ q * i := by
intro h
rcases (Nat.Prime.dvd_mul hp).mp h with h | h
· exact hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)
· have := Nat.le_of_dvd (by omega) h
omega
theorem lattice (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hp2 : p ≠ 2) (hq2 : q ≠ 2) :
(∑ i ∈ Ico 1 (p / 2 + 1), (q * i) / p) + (∑ j ∈ Ico 1 (q / 2 + 1), (p * j) / q)
= (p / 2) * (q / 2) := by
have hpo : p % 2 = 1 := Nat.odd_iff.mp (hp.odd_of_ne_two hp2)
have hqo : q % 2 = 1 := Nat.odd_iff.mp (hq.odd_of_ne_two hq2)
have key : ∀ i ∈ Ico 1 (p / 2 + 1), ∀ j ∈ Ico 1 (q / 2 + 1), q * i ≠ p * j := by
intro i hi j _ h
rw [mem_Ico] at hi
exact lattice_nd p q i hp hq hpq (by omega) (by omega) ⟨j, h⟩
symm
calc (p / 2) * (q / 2) = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (1 : ℕ) := by simp
_ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1),
((if p * j < q * i then 1 else 0) + (if q * i < p * j then 1 else 0)) := by
refine sum_congr rfl fun i hi => sum_congr rfl fun j hj => ?_
have := key i hi j hj
split_ifs <;> omega
_ = ∑ i ∈ Ico 1 (p / 2 + 1), ∑ j ∈ Ico 1 (q / 2 + 1), (if p * j < q * i then 1 else 0)
+ ∑ j ∈ Ico 1 (q / 2 + 1), ∑ i ∈ Ico 1 (p / 2 + 1), (if q * i < p * j then 1 else 0) := by
rw [sum_comm (s := Ico 1 (q / 2 + 1))]
simp only [sum_add_distrib]
_ = _ := by
congr 1
· refine sum_congr rfl fun i hi => ?_
rw [mem_Ico] at hi
rw [← card_filter]
exact lattice_count (q * i) p (q / 2) hp.pos (lattice_bound p q i hpo hqo (by omega))
(lattice_nd p q i hp hq hpq (by omega) (by omega))
· refine sum_congr rfl fun j hj => ?_
rw [mem_Ico] at hj
rw [← card_filter]
exact lattice_count (p * j) q (p / 2) hq.pos (lattice_bound q p j hqo hpo (by omega))
(lattice_nd q p j hq hp (Ne.symm hpq) (by omega) (by omega))
theorem euler (p a : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (ha : ¬ p ∣ a) :
(∃ x : ℕ, x ^ 2 % p = a % p) ↔ (a : ZMod p) ^ (p / 2) = 1 := by
haveI := Fact.mk hp
have hne : (a : ZMod p) ≠ 0 := by
rwa [Ne, CharP.cast_eq_zero_iff (ZMod p) p a]
have hc : ringChar (ZMod p) ≠ 2 := by
rw [ZMod.ringChar_zmod_n]; exact hp2
have hsq := FiniteField.isSquare_iff hc hne
rw [ZMod.card] at hsq
rw [← hsq]
constructor
· rintro ⟨x, hx⟩
refine ⟨(x : ZMod p), ?_⟩
have : ((x ^ 2 : ℕ) : ZMod p) = (a : ZMod p) := (ZMod.natCast_eq_natCast_iff' _ _ _).mpr hx
rw [← this]; push_cast; ring
· rintro ⟨r, hr⟩
refine ⟨r.val, ?_⟩
rw [← ZMod.natCast_eq_natCast_iff']
push_cast
rw [ZMod.natCast_zmod_val, hr]; ring
theorem neg_one_pow_iff (p n : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) :
((-1 : ZMod p) ^ n = 1) ↔ n % 2 = 0 := by
haveI : Fact (2 < p) := ⟨by have := hp.two_le; omega⟩
rcases Nat.even_or_odd n with h | h
· rw [h.neg_one_pow]; simp only [true_iff]; exact Nat.even_iff.mp h
· rw [h.neg_one_pow]
constructor
· intro h1; exact absurd h1 (ZMod.neg_one_ne_one)
· intro h2; have := Nat.odd_iff.mp h; omega
end QR
theorem Lemma.quadratic_reciprocity :
∀ p q : ℕ, p.Prime → q.Prime → p ≠ q → p ≠ 2 → q ≠ 2 → (((∃ x : ℕ, x ^ 2 % q = p % q) ↔ (∃ y : ℕ, y ^ 2 % p = q % p)) ↔ (p % 4 = 1 ∨ q % 4 = 1)) := by
intro p q hp hq hpq hp2 hq2
have hqp : ¬ q ∣ p := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hq hp).mp h).symm
have hpq' : ¬ p ∣ q := fun h => hpq ((Nat.prime_dvd_prime_iff_eq hp hq).mp h)
have hp1 : p % 2 = 1 := by
rcases hp.eq_two_or_odd with h | h
· exact absurd h hp2
· exact h
have hq1 : q % 2 = 1 := by
rcases hq.eq_two_or_odd with h | h
· exact absurd h hq2
· exact h
rw [QR.euler q p hq hq2 hqp, QR.euler p q hp hp2 hpq', QR.gauss q p hq hq2 hqp,
QR.gauss p q hp hp2 hpq', QR.neg_one_pow_iff q _ hq hq2, QR.neg_one_pow_iff p _ hp hp2,
QR.eisenstein_parity q p hq hq2 hqp hp1, QR.eisenstein_parity p q hp hp2 hpq' hq1]
have hl := QR.lattice p q hp hq hpq hp2 hq2
have hm := Nat.mul_mod (p / 2) (q / 2) 2
have hs := Nat.add_mod (∑ i ∈ Finset.Ico 1 (p / 2 + 1), q * i / p)
(∑ j ∈ Finset.Ico 1 (q / 2 + 1), p * j / q) 2
rw [hl] at hs
rcases Nat.mod_two_eq_zero_or_one (p / 2) with h1 | h1 <;>
rcases Nat.mod_two_eq_zero_or_one (q / 2) with h2 | h2 <;>
simp only [h1, h2] at hm <;> omega