[Merged by Bors] - feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

@@ -179,16 +179,16 @@ lemma preΨ'_three : W.preΨ' 3 = W.Ψ₃ :=
 lemma preΨ'_four : W.preΨ' 4 = W.preΨ₄ :=
   preNormEDS'_four ..
 
-lemma preΨ'_odd (m : ℕ) : W.preΨ' (2 * (m + 2) + 1) =
-    W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
-      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
-  preNormEDS'_odd ..
-
 lemma preΨ'_even (m : ℕ) : W.preΨ' (2 * (m + 3)) =
     W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
       W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2 :=
   preNormEDS'_even ..
 
+lemma preΨ'_odd (m : ℕ) : W.preΨ' (2 * (m + 2) + 1) =
+    W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
+      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
+  preNormEDS'_odd ..
+
 end preΨ'
 
 section preΨ
@@ -224,20 +224,30 @@ lemma preΨ_three : W.preΨ 3 = W.Ψ₃ :=
 lemma preΨ_four : W.preΨ 4 = W.preΨ₄ :=
   preNormEDS_four ..
 
-lemma preΨ_odd (m : ℕ) : W.preΨ (2 * (m + 2) + 1) =
-    W.preΨ (m + 4) * W.preΨ (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
-      W.preΨ (m + 1) * W.preΨ (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
-  preNormEDS_odd ..
-
-lemma preΨ_even (m : ℕ) : W.preΨ (2 * (m + 3)) =
+lemma preΨ_even' (m : ℕ) : W.preΨ (2 * (m + 3)) =
     W.preΨ (m + 2) ^ 2 * W.preΨ (m + 3) * W.preΨ (m + 5) -
       W.preΨ (m + 1) * W.preΨ (m + 3) * W.preΨ (m + 4) ^ 2 :=
-  preNormEDS_even ..
+  preNormEDS_even' ..
+
+lemma preΨ_odd' (m : ℕ) : W.preΨ (2 * (m + 2) + 1) =
+    W.preΨ (m + 4) * W.preΨ (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
+      W.preΨ (m + 1) * W.preΨ (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
+  preNormEDS_odd' ..
 
 @[simp]
 lemma preΨ_neg (n : ℤ) : W.preΨ (-n) = -W.preΨ n :=
   preNormEDS_neg ..
 
+lemma preΨ_even (m : ℤ) : W.preΨ (2 * m) =
+    W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) -
+      W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2 :=
+  preNormEDS_even ..
+
+lemma preΨ_odd (m : ℤ) : W.preΨ (2 * m + 1) =
+    W.preΨ (m + 2) * W.preΨ m ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
+      W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2) :=
+  preNormEDS_odd ..
+
 end preΨ
 
 section ΨSq
@@ -272,20 +282,30 @@ lemma ΨSq_three : W.ΨSq 3 = W.Ψ₃ ^ 2 := by
 lemma ΨSq_four : W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq := by
   erw [ΨSq_ofNat, preΨ'_four, if_pos <| by decide]
 
-lemma ΨSq_odd (m : ℕ) : W.ΨSq (2 * (m + 2) + 1) =
-    (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
-      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2 := by
-  erw [ΨSq_ofNat, preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, mul_one]
-
-lemma ΨSq_even (m : ℕ) : W.ΨSq (2 * (m + 3)) =
+lemma ΨSq_even' (m : ℕ) : W.ΨSq (2 * (m + 3)) =
     (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
       W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq := by
   erw [ΨSq_ofNat, preΨ'_even, if_pos <| even_two_mul _]
 
+lemma ΨSq_odd' (m : ℕ) : W.ΨSq (2 * (m + 2) + 1) =
+    (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
+      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2 := by
+  erw [ΨSq_ofNat, preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, mul_one]
+
 @[simp]
 lemma ΨSq_neg (n : ℤ) : W.ΨSq (-n) = W.ΨSq n := by
   simp only [ΨSq, preΨ_neg, neg_sq, even_neg]
 
+lemma ΨSq_even (m : ℤ) : W.ΨSq (2 * m) =
+    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) -
+      W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq := by
+  erw [ΨSq, preΨ_even, if_pos <| even_two_mul _]
+
+lemma ΨSq_odd (m : ℤ) : W.ΨSq (2 * m + 1) =
+    (W.preΨ (m + 2) * W.preΨ m ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
+      W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2 := by
+  erw [ΨSq, preΨ_odd, if_neg m.not_even_two_mul_add_one, mul_one]
+
 end ΨSq
 
 section Ψ
@@ -322,25 +342,42 @@ lemma Ψ_three : W.Ψ 3 = C W.Ψ₃ := by
 lemma Ψ_four : W.Ψ 4 = C W.preΨ₄ * W.ψ₂ := by
   erw [Ψ_ofNat, preΨ'_four, if_pos <| by decide]
 
-lemma Ψ_odd (m : ℕ) : W.Ψ (2 * (m + 2) + 1) =
-    W.Ψ (m + 4) * W.Ψ (m + 2) ^ 3 - W.Ψ (m + 1) * W.Ψ (m + 3) ^ 3 +
-      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C
-        (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3
-          else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3) := by
-  repeat erw [Ψ_ofNat]
-  simp_rw [preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, Nat.even_add_one, ite_not]
-  split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1
-
-lemma Ψ_even (m : ℕ) : W.Ψ (2 * (m + 3)) * W.ψ₂ =
+lemma Ψ_even' (m : ℕ) : W.Ψ (2 * (m + 3)) * W.ψ₂ =
     W.Ψ (m + 2) ^ 2 * W.Ψ (m + 3) * W.Ψ (m + 5) - W.Ψ (m + 1) * W.Ψ (m + 3) * W.Ψ (m + 4) ^ 2 := by
   repeat erw [Ψ_ofNat]
   simp_rw [preΨ'_even, if_pos <| even_two_mul _, Nat.even_add_one, ite_not]
   split_ifs <;> C_simp <;> ring1
 
+lemma Ψ_odd' (m : ℕ) : W.Ψ (2 * (m + 2) + 1) =
+    W.Ψ (m + 4) * W.Ψ (m + 2) ^ 3 - W.Ψ (m + 1) * W.Ψ (m + 3) ^ 3 +
+      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
+        C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3
+            else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3) := by
+  repeat erw [Ψ_ofNat]
+  simp_rw [preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, Nat.even_add_one, ite_not]
+  split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1
+
 @[simp]
 lemma Ψ_neg (n : ℤ) : W.Ψ (-n) = -W.Ψ n := by
   simp only [Ψ, preΨ_neg, C_neg, neg_mul (α := R[X][Y]), even_neg]
 
+lemma Ψ_even (m : ℤ) : W.Ψ (2 * m) * W.ψ₂ =
+    W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2 := by
+  repeat erw [Ψ]
+  simp_rw [preΨ_even, if_pos <| even_two_mul _, Int.even_add_one, show m + 2 = m + 1 + 1 by ring1,
+    Int.even_add_one, show m - 2 = m - 1 - 1 by ring1, Int.even_sub_one, ite_not]
+  split_ifs <;> C_simp <;> ring1
+
+lemma Ψ_odd (m : ℤ) : W.Ψ (2 * m + 1) =
+    W.Ψ (m + 2) * W.Ψ m ^ 3 - W.Ψ (m - 1) * W.Ψ (m + 1) ^ 3 +
+      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
+        C (if Even m then W.preΨ (m + 2) * W.preΨ m ^ 3
+            else -W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3) := by
+  repeat erw [Ψ]
+  simp_rw [preΨ_odd, if_neg m.not_even_two_mul_add_one, show m + 2 = m + 1 + 1 by ring1,
+    Int.even_add_one, Int.even_sub_one, ite_not]
+  split_ifs <;> C_simp <;> rw [C_Ψ₂Sq] <;> ring1
+
 lemma Affine.CoordinateRing.mk_Ψ_sq (n : ℤ) : mk W (W.Ψ n) ^ 2 = mk W (C <| W.ΨSq n) := by
   simp only [Ψ, ΨSq, map_one, map_mul, map_pow, one_pow, mul_pow, ite_pow, apply_ite C,
     apply_ite <| mk W, mk_ψ₂_sq]
@@ -426,18 +463,26 @@ lemma ψ_three : W.ψ 3 = C W.Ψ₃ :=
 lemma ψ_four : W.ψ 4 = C W.preΨ₄ * W.ψ₂ :=
   normEDS_four ..
 
-lemma ψ_odd (m : ℕ) : W.ψ (2 * (m + 2) + 1) =
-    W.ψ (m + 4) * W.ψ (m + 2) ^ 3 - W.ψ (m + 1) * W.ψ (m + 3) ^ 3 :=
-  normEDS_odd ..
-
-lemma ψ_even (m : ℕ) : W.ψ (2 * (m + 3)) * W.ψ₂ =
+lemma ψ_even' (m : ℕ) : W.ψ (2 * (m + 3)) * W.ψ₂ =
     W.ψ (m + 2) ^ 2 * W.ψ (m + 3) * W.ψ (m + 5) - W.ψ (m + 1) * W.ψ (m + 3) * W.ψ (m + 4) ^ 2 :=
-  normEDS_even ..
+  normEDS_even' ..
+
+lemma ψ_odd' (m : ℕ) : W.ψ (2 * (m + 2) + 1) =
+    W.ψ (m + 4) * W.ψ (m + 2) ^ 3 - W.ψ (m + 1) * W.ψ (m + 3) ^ 3 :=
+  normEDS_odd' ..
 
 @[simp]
 lemma ψ_neg (n : ℤ) : W.ψ (-n) = -W.ψ n :=
   normEDS_neg ..
 
+lemma ψ_even (m : ℤ) : W.ψ (2 * m) * W.ψ₂ =
+    W.ψ (m - 1) ^ 2 * W.ψ m * W.ψ (m + 2) - W.ψ (m - 2) * W.ψ m * W.ψ (m + 1) ^ 2 :=
+  normEDS_even ..
+
+lemma ψ_odd (m : ℤ) : W.ψ (2 * m + 1) =
+    W.ψ (m + 2) * W.ψ m ^ 3 - W.ψ (m - 1) * W.ψ (m + 1) ^ 3 :=
+  normEDS_odd ..
+
 lemma Affine.CoordinateRing.mk_ψ (n : ℤ) : mk W (W.ψ n) = mk W (W.Ψ n) := by
   simp only [ψ, normEDS, Ψ, preΨ, map_mul, map_pow, map_preNormEDS, ← mk_ψ₂_sq, ← pow_mul]
 

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean

@@ -270,16 +270,16 @@ lemma natDegree_preΨ_le (n : ℤ) : (W.preΨ n).natDegree ≤
     (n.natAbs ^ 2 - if Even n then 4 else 1) / 2 := by
   induction n using Int.negInduction with
   | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
-  | neg => simpa only [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg]
+  | neg ih => simp only [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg, ih]
 
 @[simp]
 lemma coeff_preΨ (n : ℤ) : (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) =
     if Even n then n / 2 else n := by
   induction n using Int.negInduction with
   | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n
-  | neg n ih =>
+  | neg ih n =>
     simp only [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]
-    rcases n.even_or_odd' with ⟨n, rfl | rfl⟩ <;>
+    rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩ <;>
       push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at * <;>
       rw [ih]
 
@@ -288,8 +288,8 @@ lemma coeff_preΨ_ne_zero {n : ℤ} (h : (n : R) ≠ 0) :
   induction n using Int.negInduction with
   | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
       using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
-  | neg n ih => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
-      using ih <| neg_ne_zero.mp <| by exact_mod_cast h
+  | neg ih n => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
+        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h
 
 @[simp]
 lemma natDegree_preΨ {n : ℤ} (h : (n : R) ≠ 0) :
@@ -300,8 +300,8 @@ lemma natDegree_preΨ_pos {n : ℤ} (hn : 2 < n.natAbs) (h : (n : R) ≠ 0) :
     0 < (W.preΨ n).natDegree := by
   induction n using Int.negInduction with
   | nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
-  | neg n ih => simpa only [preΨ_neg, natDegree_neg]
-        using ih (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h
+  | neg ih n => simpa only [preΨ_neg, natDegree_neg]
+        using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h
 
 @[simp]
 lemma leadingCoeff_preΨ {n : ℤ} (h : (n : R) ≠ 0) :
@@ -311,7 +311,8 @@ lemma leadingCoeff_preΨ {n : ℤ} (h : (n : R) ≠ 0) :
 lemma preΨ_ne_zero [Nontrivial R] {n : ℤ} (h : (n : R) ≠ 0) : W.preΨ n ≠ 0 := by
   induction n using Int.negInduction with
   | nat n => simpa only [preΨ_ofNat] using W.preΨ'_ne_zero <| by exact_mod_cast h
-  | neg n ih => simpa only [preΨ_neg, neg_ne_zero] using ih <| neg_ne_zero.mp <| by exact_mod_cast h
+  | neg ih n => simpa only [preΨ_neg, neg_ne_zero]
+        using ih n <| neg_ne_zero.mp <| by exact_mod_cast h
 
 end preΨ
 
@@ -340,13 +341,13 @@ private lemma natDegree_coeff_ΨSq_ofNat (n : ℕ) :
 lemma natDegree_ΨSq_le (n : ℤ) : (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1 := by
   induction n using Int.negInduction with
   | nat n => exact (W.natDegree_coeff_ΨSq_ofNat n).left
-  | neg => rwa [ΨSq_neg, Int.natAbs_neg]
+  | neg ih => simp only [ΨSq_neg, Int.natAbs_neg, ih]
 
 @[simp]
 lemma coeff_ΨSq (n : ℤ) : (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = n ^ 2 := by
   induction n using Int.negInduction with
   | nat n => exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right
-  | neg => rwa [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow]
+  | neg ih => simp_rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]
 
 lemma coeff_ΨSq_ne_zero [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) :
     (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0 := by
@@ -415,13 +416,13 @@ private lemma natDegree_coeff_Φ_ofNat (n : ℕ) :
 lemma natDegree_Φ_le (n : ℤ) : (W.Φ n).natDegree ≤ n.natAbs ^ 2 := by
   induction n using Int.negInduction with
   | nat n => exact (W.natDegree_coeff_Φ_ofNat n).left
-  | neg => rwa [Φ_neg, Int.natAbs_neg]
+  | neg ih => simp only [Φ_neg, Int.natAbs_neg, ih]
 
 @[simp]
 lemma coeff_Φ (n : ℤ) : (W.Φ n).coeff (n.natAbs ^ 2) = 1 := by
   induction n using Int.negInduction with
   | nat n => exact (W.natDegree_coeff_Φ_ofNat n).right
-  | neg => rwa [Φ_neg, Int.natAbs_neg]
+  | neg ih => simp only [Φ_neg, Int.natAbs_neg, ih]
 
 lemma coeff_Φ_ne_zero [Nontrivial R] (n : ℤ) : (W.Φ n).coeff (n.natAbs ^ 2) ≠ 0 :=
   W.coeff_Φ n ▸ one_ne_zero

Mathlib/Data/Int/Defs.lean

@@ -342,9 +342,9 @@ end inductionOn'
 
 /-- Inductively define a function on `ℤ` by defining it on `ℕ` and extending it from `n` to `-n`. -/
 @[elab_as_elim] protected def negInduction {C : ℤ → Sort*} (nat : ∀ n : ℕ, C n)
-    (neg : ∀ n : ℕ, C n → C (-n)) : ∀ n : ℤ, C n
+    (neg : (∀ n : ℕ, C n) → ∀ n : ℕ, C (-n)) : ∀ n : ℤ, C n
   | .ofNat n => nat n
-  | .negSucc n => neg _ <| nat <| n + 1
+  | .negSucc n => neg nat <| n + 1
 
 /-- See `Int.inductionOn'` for an induction in both directions. -/
 protected lemma le_induction {P : ℤ → Prop} {m : ℤ} (h0 : P m)