Poly.lean — FrcCore

1import FrcCore.Series23/-!4# FrcCore.Poly — polynomials over the shell and the root criterion (1:E3)56A polynomial is its coefficient sequence `Nat → Shell p` with a degree bound (`Bound f n`: the coefficients7beyond `n` vanish); equality is coefficientwise, so no function extensionality is needed.  The Cauchy8product, evaluation as a finite sum, the evaluation homomorphism (`eval_mul`, by a triangular reindexing of9sums), synthetic division by `X − a` at a root (`quot_linear_spec`), and the root bound over any shell without10zero divisors (a polynomial of degree `n` vanishing at `n + 1` distinct points is zero, `root_bound_of`).  No11axioms.1213Since task LM22 the module stands on `Series.lean` alone, without the frame: the frame's root bound14(`Frame.root_bound`) and 1:E3's criterion (`root_iff_common_factor`) are in the numbers theme's15`Theme/Numbers.lean`, under their names.16-/1718namespace FRC19namespace Shell2021variable {p : Nat} [Pos p]2223theorem sum_split (f : Nat → Shell p) (n k : Nat) :24    sumRange f (n + k) = sumRange f n + sumRange (fun t => f (n + t)) k := by25  induction k with26  | zero => rw [Nat.add_zero, sumRange_zero, add_zero]27  | succ k ih =>28    show sumRange f (n + k + 1) = _29    rw [sumRange_succ, sumRange_succ, ih, add_assoc]3031/-- The triangular reindexing `Σ_{l<N} Σ_{j≤l} F j (l − j) = Σ_{j<N} Σ_{k<N−j} F j k`. -/32theorem sum_triangle (F : Nat → Nat → Shell p) (N : Nat) :33    sumRange (fun l => sumRange (fun j => F j (l - j)) (l + 1)) N =34    sumRange (fun j => sumRange (fun k => F j k) (N - j)) N := by35  induction N with36  | zero => rfl37  | succ N ih =>38    rw [sumRange_succ, ih, sumRange_succ (fun j => sumRange (fun k => F j k) (N + 1 - j)) N]39    have h1 : sumRange (fun j => sumRange (fun k => F j k) (N + 1 - j)) N =40        sumRange (fun j => sumRange (fun k => F j k) (N - j) + F j (N - j)) N := by41      apply sum_congr42      intro j hj43      show sumRange (fun k => F j k) (N + 1 - j) = sumRange (fun k => F j k) (N - j) + F j (N - j)44      have e : N + 1 - j = (N - j) + 1 := by45        have := FRC.Nat.add_sub_of_le (Nat.le_of_lt hj)46        -- this : j + (N - j) = N47        calc N + 1 - j = j + (N - j) + 1 - j := by rw [this]48          _ = (N - j) + 1 + j - j := by rw [Nat.add_comm j (N - j), Nat.add_right_comm (N - j) j 1]49          _ = (N - j) + 1 := FRC.Nat.add_sub_cancel _ _50      rw [e, sumRange_succ]51    rw [h1, sum_add]52    have e2 : N + 1 - N = 1 := FRC.Nat.add_sub_cancel_left N 153    rw [e2, sumRange_succ (fun k => F N k) 0, sumRange_zero, zero_add,54      sumRange_succ (fun j => F j (N - j)) N, Nat.sub_self, add_assoc]5556/-- A polynomial as its coefficient sequence. -/57abbrev Poly (p : Nat) [Pos p] := Nat → Shell p5859namespace Poly6061/-- `f` has degree at most `n`: the coefficients beyond `n` vanish. -/62def Bound (f : Poly p) (n : Nat) : Prop := ∀ i, n < i → f i = 06364/-- The Cauchy product `(f·g) i = Σ_{j ≤ i} f j · g (i − j)`. -/65def mul (f g : Poly p) : Poly p := fun i => sumRange (fun j => f j * g (i - j)) (i + 1)6667/-- `f(a)` summed to the bound `n`: `Σ_{i ≤ n} f i · a^i`. -/68def eval (f : Poly p) (n : Nat) (a : Shell p) : Shell p := sumRange (fun i => f i * a ^ i) (n + 1)6970/-- `X − a`. -/71def linear (a : Shell p) : Poly p72  | 0 => -a73  | 1 => 174  | _ + 2 => 07576/-- `X^p − X`. -/77def xpx : Poly p := fun i => if i = p then 1 else if i = 1 then -1 else 07879theorem eval_congr {f h : Poly p} (e : ∀ i, f i = h i) (n : Nat) (a : Shell p) : eval f n a = eval h n a :=80  sum_congr (n + 1) (fun i _ => by show f i * a ^ i = h i * a ^ i; rw [e i])8182theorem eval_bound {f : Poly p} {n N : Nat} (hf : Bound f n) (hN : n ≤ N) (a : Shell p) :83    eval f N a = eval f n a := by84  unfold eval85  have e : N + 1 = (n + 1) + (N - n) := by86    rw [Nat.add_right_comm, FRC.Nat.add_sub_of_le hN]87  rw [e, sum_split, sum_zero (N - n) (fun t _ => by88    show f (n + 1 + t) * a ^ (n + 1 + t) = 089    rw [hf _ (Nat.lt_of_lt_of_le (Nat.lt_succ_self n) (Nat.le_add_right (n + 1) t)), zero_mul]), add_zero]9091theorem mul_bound {d q : Poly p} {m k : Nat} (hd : Bound d m) (hq : Bound q k) : Bound (mul d q) (m + k) := by92  intro i hi93  apply sum_zero94  intro j hj95  show d j * q (i - j) = 096  match Nat.decLe j m with97  | .isTrue hjm =>98    have : k < i - j := by99      apply FRC.Nat.le_sub_of_add_le100      -- k + 1 + j ≤ i  from  m + k < i and j ≤ m101      show k + 1 + j ≤ i102      calc k + 1 + j ≤ k + 1 + m := Nat.add_le_add_left hjm _103        _ = m + k + 1 := by rw [Nat.add_comm (k + 1) m, Nat.add_assoc]104        _ ≤ i := hi105    rw [hq _ this, mul_zero]106  | .isFalse hjm => rw [hd j (Nat.lt_of_not_le hjm), zero_mul]107108/-- The evaluation is multiplicative: `(f·g)(a) = f(a)·g(a)`, with the bounds added. -/109theorem eval_mul {f g : Poly p} {n m : Nat} (hf : Bound f n) (hg : Bound g m) (a : Shell p) :110    eval (mul f g) (n + m) a = eval f n a * eval g m a := by111  unfold eval mul112  have h1 : sumRange (fun l => sumRange (fun j => f j * g (l - j)) (l + 1) * a ^ l) (n + m + 1) =113      sumRange (fun l => sumRange (fun j => f j * a ^ j * (g (l - j) * a ^ (l - j))) (l + 1)) (n + m + 1) := by114    apply sum_congr115    intro l _116    show sumRange (fun j => f j * g (l - j)) (l + 1) * a ^ l =117      sumRange (fun j => f j * a ^ j * (g (l - j) * a ^ (l - j))) (l + 1)118    rw [← sum_mul_right]119    apply sum_congr120    intro j hj121    show f j * g (l - j) * a ^ l = f j * a ^ j * (g (l - j) * a ^ (l - j))122    have : a ^ l = a ^ j * a ^ (l - j) := by rw [← pow_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt_succ hj)]123    rw [this, mul_assoc, mul_assoc, mul_left_comm (g (l - j))]124  rw [h1, sum_triangle (fun j k => f j * a ^ j * (g k * a ^ k)) (n + m + 1)]125  have h2 : sumRange (fun j => sumRange (fun k => f j * a ^ j * (g k * a ^ k)) (n + m + 1 - j)) (n + m + 1) =126      sumRange (fun j => f j * a ^ j * sumRange (fun i => g i * a ^ i) (m + 1)) (n + m + 1) := by127    apply sum_congr128    intro j hj129    show sumRange (fun k => f j * a ^ j * (g k * a ^ k)) (n + m + 1 - j) =130      f j * a ^ j * sumRange (fun i => g i * a ^ i) (m + 1)131    rw [sum_mul_left]132    match Nat.decLe j n with133    | .isTrue hjn =>134      have e : n + m + 1 - j = (n + m - j) + 1 := by135        have := FRC.Nat.add_sub_of_le (Nat.le_trans hjn (Nat.le_add_right n m))136        calc n + m + 1 - j = j + (n + m - j) + 1 - j := by rw [this]137          _ = (n + m - j) + 1 + j - j := by rw [Nat.add_comm j (n + m - j), Nat.add_right_comm (n + m - j) j 1]138          _ = (n + m - j) + 1 := FRC.Nat.add_sub_cancel _ _139      rw [e]140      have hm : m ≤ n + m - j := by141        apply FRC.Nat.le_sub_of_add_le142        rw [Nat.add_comm n m]; exact Nat.add_le_add_left hjn m143      exact congrArg (f j * a ^ j * ·) (eval_bound hg hm a)144    | .isFalse hjn =>145      rw [hf j (Nat.lt_of_not_le hjn), zero_mul, zero_mul, zero_mul]146  rw [h2, sum_mul_right]147  exact congrArg (· * sumRange (fun i => g i * a ^ i) (m + 1)) (eval_bound hf (Nat.le_add_right n m) a)148149theorem linear_bound (a : Shell p) : Bound (linear a) 1 := by150  intro i hi151  match i, hi with152  | _ + 2, _ => rfl153154theorem mul_linear_zero (a : Shell p) (q : Poly p) : mul (linear a) q 0 = -(a * q 0) := by155  show sumRange (fun j => linear a j * q (0 - j)) 1 = _156  rw [sumRange_succ, sumRange_zero, zero_add]157  show -a * q 0 = -(a * q 0)158  exact (neg_mul a (q 0)).symm159160theorem mul_linear_succ (a : Shell p) (q : Poly p) (i : Nat) :161    mul (linear a) q (i + 1) = q i + -(a * q (i + 1)) := by162  show sumRange (fun j => linear a j * q (i + 1 - j)) (i + 1 + 1) = _163  have e : i + 1 + 1 = 2 + i := Nat.add_comm i 2164  rw [e, sum_split, sum_zero i (fun t _ => by165    show linear a (2 + t) * q (i + 1 - (2 + t)) = 0166    rw [Nat.add_comm 2 t]167    show (0 : Shell p) * _ = 0168    exact zero_mul _), add_zero, sumRange_succ, sumRange_succ, sumRange_zero, zero_add]169  show -a * q (i + 1) + 1 * q i = q i + -(a * q (i + 1))170  rw [← neg_mul, one_mul, add_comm]171172/-- The quotient of `f` (bound `n`) by `X − a`: `q i = Σ_{t < n − i} f (i + 1 + t) · a^t`. -/173def quotLinear (f : Poly p) (n : Nat) (a : Shell p) : Poly p :=174  fun i => sumRange (fun t => f (i + 1 + t) * a ^ t) (n - i)175176/-- Synthetic division: at a root `a` of `f`, `f = (X − a)·q` with `q` of degree one less. -/177theorem quot_linear_spec {f : Poly p} {n : Nat} (hf : Bound f n) {a : Shell p} (ha : eval f n a = 0) :178    Bound (quotLinear f n a) (n - 1) ∧ ∀ i, f i = mul (linear a) (quotLinear f n a) i := by179  constructor180  · intro i hi181    have hni : n ≤ i := by182      match n, hi with183      | 0, _ => exact Nat.zero_le i184      | n' + 1, hi => exact Nat.succ_le_of_lt hi185    show sumRange (fun t => f (i + 1 + t) * a ^ t) (n - i) = 0186    rw [FRC.Nat.sub_eq_zero_of_le hni]187    rfl188  · intro i189    match i with190    | 0 =>191      rw [mul_linear_zero]192      -- f 0 + a · q 0 = f(a) = 0193      have e1 : n + 1 = 1 + n := Nat.add_comm n 1194      unfold eval at ha195      rw [e1, sum_split, sumRange_succ, sumRange_zero, zero_add] at ha196      have ha' : f 0 * a ^ 0 + sumRange (fun t => f (1 + t) * a ^ (1 + t)) n = 0 := ha197      rw [pow_zero, mul_one] at ha'198      have h2 : sumRange (fun t => f (1 + t) * a ^ (1 + t)) n = a * quotLinear f n a 0 := by199        show _ = a * sumRange (fun t => f (0 + 1 + t) * a ^ t) (n - 0)200        rw [← sum_mul_left]201        apply sum_congr202        intro t _203        show f (1 + t) * a ^ (1 + t) = a * (f (0 + 1 + t) * a ^ t)204        rw [pow_add, pow_one, mul_left_comm]205      rw [h2] at ha'206      exact eq_neg_of_add_eq_zero ha'207    | i + 1 =>208      rw [mul_linear_succ]209      match Nat.decLt i n with210      | .isTrue hin =>211        -- n − i = (n − (i + 1)) + 1212        have hk := FRC.Nat.add_sub_of_le (Nat.succ_le_of_lt hin)213        -- hk : i + 1 + (n - (i + 1)) = n214        have e : n - i = (n - (i + 1)) + 1 := by215          calc n - i = i + 1 + (n - (i + 1)) - i := by rw [hk]216            _ = i + ((n - (i + 1)) + 1) - i := by rw [Nat.add_assoc, Nat.add_comm 1]217            _ = (n - (i + 1)) + 1 := FRC.Nat.add_sub_cancel_left _ _218        show f (i + 1) = sumRange (fun t => f (i + 1 + t) * a ^ t) (n - i) +219          -(a * sumRange (fun t => f (i + 1 + 1 + t) * a ^ t) (n - (i + 1)))220        rw [e, Nat.add_comm (n - (i + 1)) 1, sum_split, sumRange_succ, sumRange_zero, zero_add]221        show f (i + 1) = f (i + 1 + 0) * a ^ 0 + sumRange (fun t => f (i + 1 + (1 + t)) * a ^ (1 + t)) (n - (i + 1)) +222          -(a * sumRange (fun t => f (i + 1 + 1 + t) * a ^ t) (n - (i + 1)))223        have h3 : sumRange (fun t => f (i + 1 + (1 + t)) * a ^ (1 + t)) (n - (i + 1)) =224            a * sumRange (fun t => f (i + 1 + 1 + t) * a ^ t) (n - (i + 1)) := by225          rw [← sum_mul_left]226          apply sum_congr227          intro t _228          show f (i + 1 + (1 + t)) * a ^ (1 + t) = a * (f (i + 1 + 1 + t) * a ^ t)229          rw [← Nat.add_assoc, pow_add, pow_one, mul_left_comm]230        rw [h3, Nat.add_zero, pow_zero, mul_one, add_assoc, add_neg, add_zero]231      | .isFalse hin =>232        have hni : n ≤ i := Nat.le_of_not_lt hin233        have z1 : n - i = 0 := FRC.Nat.sub_eq_zero_of_le hni234        have z2 : n - (i + 1) = 0 := FRC.Nat.sub_eq_zero_of_le (Nat.le_succ_of_le hni)235        show f (i + 1) = sumRange (fun t => f (i + 1 + t) * a ^ t) (n - i) +236          -(a * sumRange (fun t => f (i + 1 + 1 + t) * a ^ t) (n - (i + 1)))237        rw [z1, z2, sumRange_zero, sumRange_zero, mul_zero, neg_zero, add_zero]238        exact hf _ (Nat.lt_succ_of_le hni)239240theorem eval_linear (a b : Shell p) : eval (linear a) 1 b = b + -a := by241  show sumRange (fun i => linear a i * b ^ i) 2 = _242  rw [sumRange_succ, sumRange_succ, sumRange_zero, zero_add]243  show -a * b ^ 0 + 1 * b ^ 1 = b + -a244  rw [pow_zero, mul_one, pow_one, one_mul, add_comm]245246theorem eval_mul_linear {q : Poly p} {n : Nat} (hq : Bound q n) (a b : Shell p) :247    eval (mul (linear a) q) (n + 1) b = (b + -a) * eval q n b := by248  rw [Nat.add_comm n 1, eval_mul (linear_bound a) hq, eval_linear]249250/-- The root bound over any shell without zero divisors (task LM22): a polynomial of degree at most `n` that251vanishes at `n + 1` distinct points is zero. `Frame.root_bound` is its case of a frame; the prime shell's252(`Theme/Field`) needs no generator. -/253theorem root_bound_of (hzd : ∀ {a b : Shell p}, a * b = 0 → a = 0 ∨ b = 0) : ∀ (n : Nat) (f : Poly p), Bound f n →254    ∀ (r : Nat → Shell p), (∀ i j, i ≤ n → j ≤ n → r i = r j → i = j) → (∀ i, i ≤ n → eval f n (r i) = 0) →255    ∀ i, f i = 0 := by256  intro n257  induction n with258  | zero =>259    intro f hf r _ hroot i260    have h0 := hroot 0 (Nat.le_refl 0)261    unfold eval at h0262    rw [sumRange_succ, sumRange_zero, zero_add] at h0263    have h0' : f 0 * r 0 ^ 0 = 0 := h0264    rw [pow_zero, mul_one] at h0'265    match i with266    | 0 => exact h0'267    | i + 1 => exact hf _ (Nat.zero_lt_succ i)268  | succ n ih =>269    intro f hf r hinj hroot270    have ha := hroot 0 (Nat.zero_le _)271    have spec := quot_linear_spec hf ha272    have hq : Bound (quotLinear f (n + 1) (r 0)) n := spec.1273    have hf' : ∀ b, eval f (n + 1) b = (b + -(r 0)) * eval (quotLinear f (n + 1) (r 0)) n b := fun b => by274      rw [eval_congr spec.2, eval_mul_linear hq]275    have hz : ∀ i, quotLinear f (n + 1) (r 0) i = 0 := by276      apply ih _ hq (fun k => r (k + 1))277      · intro i j hi hj e278        exact Nat.succ.inj (hinj (i + 1) (j + 1) (Nat.succ_le_succ hi) (Nat.succ_le_succ hj) e)279      · intro k hk280        have h := hroot (k + 1) (Nat.succ_le_succ hk)281        rw [hf'] at h282        match hzd h with283        | .inl e =>284          have : r (k + 1) = r 0 := by285            calc r (k + 1) = r (k + 1) + 0 := (add_zero _).symm286              _ = r (k + 1) + (-(r 0) + r 0) := by rw [neg_add]287              _ = (r (k + 1) + -(r 0)) + r 0 := (add_assoc _ _ _).symm288              _ = r 0 := by rw [e, zero_add]289          exact absurd (hinj (k + 1) 0 (Nat.succ_le_succ hk) (Nat.zero_le _) this) (FRC.Nat.succ_ne_zero k)290        | .inr e => exact e291    intro i292    rw [spec.2 i]293    match i with294    | 0 => rw [mul_linear_zero, hz, mul_zero, neg_zero]295    | i + 1 => rw [mul_linear_succ, hz, hz, mul_zero, neg_zero, add_zero]296297namespace Frame298299theorem ofNat_inj_lt {i j : Nat} (hi : i < p) (hj : j < p) (h : (ofNat i : Shell p) = ofNat j) : i = j := by300  have := val_injective h301  rw [val_ofNat, val_ofNat, FRC.Nat.mod_eq_of_lt hi, FRC.Nat.mod_eq_of_lt hj] at this302  exact this303304end Frame305end Poly306end Shell307end FRC308