feat(NumberTheory): characterize elliptic divisibility sequences #13057
+1,032
−55
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
alreadydone
added
WIP
…ver-community/mathlib4 into IsEllDivSequence_normEDS
1 task
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
leanprover-community-mathlib4-bot
added
the
merge-conflict
alreadydone
added
awaiting-review
and removed
merge-conflict
alreadydone
commented
May 23, 2024
Comment on lines
+1132
to
+1168
| /-- The expression `W(m+1)W(m)W(m-1)/W₃W₂` for a normalised EDS. -/ | ||
| def redInvarDenom : R := | ||
| letI C := complEDS b c d | ||
| letI W := normEDS b c d | ||
| letI r₆ := normEDS b c d 5 - d ^ 2 -- W₆/W₃W₂ | ||
| if m % 6 = 0 then r₆ * C 6 (m / 6) * W (m + 1) * W (m - 1) else | ||
| if m % 6 = 1 then r₆ * C 6 ((m - 1) / 6) * W (m + 1) * W m else | ||
| if m % 6 = 5 then r₆ * C 6 ((m + 1) / 6) * W m * W (m - 1) else | ||
| if m % 6 = 2 then C 3 ((m + 1) / 3) * C 2 (m / 2) * W (m - 1) else | ||
| if m % 6 = 4 then C 3 ((m - 1) / 3) * C 2 (m / 2) * W (m + 1) else | ||
| if m % 6 = 3 then C 3 (m / 3) * C 2 ((m - 1) / 2) * W (m + 1) else 0 | ||
|
|
||
| lemma invarDenom_eq_redInvarDenom_mul : | ||
| invarDenom (normEDS b c d) 1 m = redInvarDenom b c d m * b * c := by | ||
| have h6 : (6 : ℤ) ≠ 0 := by decide | ||
| have h3 : (3 : ℤ) ≠ 0 := by decide | ||
| have hd k m dvd eq := | ||
| (Int.dvd_iff_emod_eq_zero k m).mpr ((@Int.emod_emod_of_dvd m k 6 dvd).symm.trans eq) | ||
| have hd2 {m} := hd 2 m ⟨3, rfl⟩ | ||
| have hd3 {m} := hd 3 m ⟨2, rfl⟩ | ||
| have mul_eq := @normEDS_mul_complEDS_div _ _ b c d | ||
| rw [invarDenom, redInvarDenom]; split_ifs with h h h h h h | ||
| · rw [← mul_eq _ h6 _ (Int.dvd_of_emod_eq_zero h), normEDS_six_eq_mul]; ring | ||
| · rw [← mul_eq _ h6 _ (Int.dvd_sub_of_emod_eq h), normEDS_six_eq_mul]; ring | ||
| · rw [show m + 1 = m + 6 - 5 by abel, ← mul_eq _ h6, normEDS_six_eq_mul]; ring | ||
| exact Int.dvd_sub_of_emod_eq (Int.add_emod_self.trans h) | ||
| on_goal 1 => rw [← mul_eq _ h3 _ (hd3 <| by simp [h, Int.add_emod]), | ||
| ← mul_eq _ two_ne_zero m (hd2 <| by simp [h])] | ||
| on_goal 2 => rw [← mul_eq _ h3 (m - 1) (hd3 <| by simp [h, Int.sub_emod]), | ||
| ← mul_eq _ two_ne_zero m (hd2 <| by simp [h])] | ||
| on_goal 3 => rw [← mul_eq _ h3 m (hd3 <| by simp [h]), | ||
| ← mul_eq _ two_ne_zero (m - 1) (hd2 <| by simp [h, Int.sub_emod])] | ||
| on_goal 4 => | ||
| have h0 := Int.emod_nonneg m h6 | ||
| have lt := Int.emod_lt_of_pos m (show 0 < 6 by decide) | ||
| interval_cases m % 6 <;> contradiction | ||
| all_goals rw [normEDS_three, normEDS_two]; ring |
There was a problem hiding this comment.
The proof is a bit cumbersome; cf. this Zulip message.
|
I think this is a massive PR, especially because it's a long argument. Can you try to split it to smaller self-contained chunks, so it's easier to review? |
kbuzzard
reviewed
May 23, 2024
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
1 task
leanprover-community-mathlib4-bot
added
the
merge-conflict
1 task
alreadydone
commented
Jun 27, 2024
Comment on lines
+1110
to
+1111
| def invarNumAux : R := | ||
| preNormEDS (b ^ 4) c d (m - 2) * preNormEDS (b ^ 4) c d (m + 1) ^ 2 * if Even m then 1 else b |
There was a problem hiding this comment.
This file is getting long so I think I'll split everything about invar, invarNumAux, redInvar etc. into another file Invar. The compl stuff can't be split because they're used to show normEDS IsDivSequence.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Main results:
Every
normEDSis an elliptic divisibility sequence (EDS). The key proof isrel₄_of_anti_oddRec_evenRec, based on my original argument first published on MathSEConversely, every EDS is equal to some
normEDS(assuming that the first two terms are not zero divisors)