CoRN.fta.FTA
Section FTA_reg'.
Variable f : cpoly_cring CC.
Variable n : nat.
Hypothesis f_degree : degree (S n) f.
Lemma FTA_reg' : {f1 : CCX | degree 1 f1 | {f2 : CCX | degree n f2 | f [=] f1[*]f2}}.
Proof.
elim (FTA_reg f (S n)). intro c. intro H.
cut (degree 1 (_X_[-]_C_ c)). intro.
∃ (_X_[-]_C_ c). auto.
elim (poly_linear_factor _ _ _ H).
intro f2. intros.
∃ f2.
apply degree_mult_imp with (_X_[-]_C_ c) 1. auto.
apply degree_wd with f; auto. auto.
apply degree_minus_lft with 0. apply degree_le_c_. apply degree_x_. auto.
auto with arith.
auto.
Qed.
End FTA_reg'.
Let n:nat, f be a complex polynomial of degree
less than or equal to (S n) and c be a complex number such that
f!c [#] [0].
Section FTA_1.
Variable f : cpoly_cring CC.
Variable n : nat.
Hypothesis f_degree : degree_le (S n) f.
Variable c : CC.
Hypothesis f_c : f ! c [#] [0].
Lemma FTA_1a : degree_le (S n) (Shift c f).
Proof.
apply Shift_degree_le.
auto.
Qed.
Let g := Rev (S n) (Shift c f).
Lemma FTA_1b : degree (S n) g.
Proof.
unfold g in |- ×.
apply Rev_degree.
astepl f ! c. auto.
Step_final f ! ([0][+]c).
Qed.
Lemma FTA_1 : {f1 : CCX | {f2 : CCX | degree_le 1 f1 ∧ degree_le n f2 ∧ f [=] f1[*]f2}}.
Proof.
elim (FTA_reg' g n FTA_1b). intro g1. intros H H0.
elim H0. clear H0. intro g2. intros H0 H1.
cut (degree_le 1 g1). intro.
cut (degree_le n g2). intro.
∃ (Shift [--]c (Rev 1 g1)).
∃ (Shift [--]c (Rev n g2)).
split.
apply Shift_degree_le.
apply Rev_degree_le.
split.
apply Shift_degree_le.
apply Rev_degree_le.
cut (degree_le (1 + n) (g1[*]g2)). intro.
cut (degree_le (1 + n) g). intro.
cut (degree_le (1 + n) (Shift c f)). intro.
astepl (Shift [--]c (Shift c f)).
astepl (Shift [--]c (Rev (1 + n) (Rev (S n) (Shift c f)))).
astepl (Shift [--]c (Rev (1 + n) g)).
astepl (Shift [--]c (Rev (1 + n) (g1[*]g2))).
Step_final (Shift [--]c (Rev 1 g1[*]Rev n g2)).
exact FTA_1a.
apply degree_le_wd with (g1[*]g2); algebra.
apply degree_le_mult; auto.
apply degree_imp_degree_le; auto.
apply degree_imp_degree_le; auto.
Qed.
Lemma FTA_1' : {a : CC | {b : CC | {g : CCX | degree_le n g | f [=] (_C_ a[*]_X_[+]_C_ b) [*]g}}}.
Proof.
elim FTA_1. intro f1. intros H.
elim H. clear H. intros f2 H0.
elim H0. clear H0. intro H. intros H0.
elim H0. clear H0. intros H0 H1.
elim (degree_le_1_imp _ f1); auto. intro a. intros H2. ∃ a.
elim H2. clear H2. intro b. intros. ∃ b.
∃ f2. auto.
Step_final (f1[*]f2).
Qed.
End FTA_1.
Section Fund_Thm_Alg.
Lemma FTA' : ∀ n (f : CCX), degree_le n f → nonConst _ f → {z : CC | f ! z [=] [0]}.
Proof.
intro n. induction n as [| n Hrecn].
unfold nonConst in |- ×. unfold degree_le in |- ×. intros f H H0.
elim H0. clear H0. intro n. intros H0 H1.
elim (eq_imp_not_ap _ _ _ (H _ H0) H1).
unfold nonConst in |- ×. intros f H H0.
elim H0. clear H0. intro m'. intros H0 H1.
elim (poly_apzero_CC f). intro c. intros H2.
elim (FTA_1' f n H c H2). intro a. intros H3.
elim H3. clear H3. intro b. intros H3.
elim H3. clear H3. intro g. intros H3 H4.
elim (O_or_S m'); intro y.
elim y. clear y. intro m. intro y. rewrite <- y in H0. rewrite <- y in H1.
cut (a[*]nth_coeff m g [#] [0] or b[*]nth_coeff (S m) g [#] [0]).
intro H5.
elim H5; clear H5; intros H5.
cut (a [#] [0]). intro H6.
∃ ( [--]b[/] a[//]H6).
astepl ((_C_ a[*]_X_[+]_C_ b) [*]g) ! ( [--]b[/] a[//]H6).
astepl ((_C_ a[*]_X_[+]_C_ b) ! ( [--]b[/] a[//]H6) [*]g ! ( [--]b[/] a[//]H6)).
astepl (((_C_ a[*]_X_) ! ( [--]b[/] a[//]H6) [+] (_C_ b) ! ( [--]b[/] a[//]H6)) [*]
g ! ( [--]b[/] a[//]H6)).
astepl (((_C_ a) ! ( [--]b[/] a[//]H6) [*]_X_ ! ( [--]b[/] a[//]H6) [+]b) [*]
g ! ( [--]b[/] a[//]H6)).
astepl ((a[*] ( [--]b[/] a[//]H6) [+]b) [*]g ! ( [--]b[/] a[//]H6)).
rational.
apply cring_mult_ap_zero with (nth_coeff m g). auto.
elim (Hrecn g); auto. intro z. intros. ∃ z.
astepl ((_C_ a[*]_X_[+]_C_ b) [*]g) ! z.
astepl ((_C_ a[*]_X_[+]_C_ b) ! z[*]g ! z).
Step_final ((_C_ a[*]_X_[+]_C_ b) ! z[*][0]).
unfold nonConst in |- ×. ∃ (S m). auto.
apply cring_mult_ap_zero_op with b. auto.
apply cg_add_ap_zero.
astepl (nth_coeff (S m) f). auto.
Step_final (nth_coeff (S m) ((_C_ a[*]_X_[+]_C_ b) [*]g)).
rewrite <- y in H0. elim (lt_irrefl 0 H0).
apply nth_coeff_ap_zero_imp with m'. auto.
Qed.
Lemma FTA : ∀ f : CCX, nonConst _ f → {z : CC | f ! z [=] [0]}.
Proof.
intros.
elim (Cpoly_ex_degree _ f). intro n. intros. apply FTA' with n; auto.
Qed.
Lemma FTA_a_la_Henk : ∀ f : CCX,
{x : CC | {y : CC | AbsCC (f ! x[-]f ! y) [>][0]}} → {z : CC | f ! z [=] [0]}.
Proof.
intros f H.
elim H.
intros x H0.
elim H0.
intros y H1.
pose (H1':=(CAnd_proj1 _ _ (greater_def _ _ _) H1)).
clearbody H1'.
clear H1.
rename H1' into H1.
generalize (less_imp_ap _ _ _ H1); intro H2.
generalize (AbsCC_ap_zero _ H2); intro H3.
cut (Sum 0 (lth_of_poly f) (fun i : nat ⇒ nth_coeff i f[*] (x[^]i[-]y[^]i)) [#] [0]).
intro H4.
cut (0 ≤ lth_of_poly f); try auto with arith.
intro H5.
generalize (Sum_apzero _ _ _ _ H5 H4); intro H6.
elim H6; intros i H8 H9.
elim H8; intros H10 H11.
apply FTA.
unfold nonConst in |- ×.
generalize (cring_mult_ap_zero _ _ _ H9); intro H12.
∃ i.
elim (zerop i).
intro H13.
elimtype False.
elim (ap_irreflexive_unfolded _ ([0]:CC)).
rstepl (nth_coeff i f[*] (x[^]0[-]y[^]0)).
rewrite <- H13.
assumption.
auto.
assumption.
apply ap_wdl_unfolded with (Sum 0 (lth_of_poly f)
(fun i : nat ⇒ nth_coeff i f[*]x[^]i[-]nth_coeff i f[*]y[^]i)).
2: apply Sum_wd.
2: intro.
2: algebra.
apply ap_wdl_unfolded with (Sum 0 (lth_of_poly f) (fun i : nat ⇒ nth_coeff i f[*]x[^]i) [-]
Sum 0 (lth_of_poly f) (fun i : nat ⇒ nth_coeff i f[*]y[^]i)).
2: apply eq_symmetric_unfolded.
2: change (Sum 0 (lth_of_poly f) (fun j : nat ⇒ (fun i : nat ⇒ nth_coeff i f[*]x[^]i) j[-]
(fun i : nat ⇒ nth_coeff i f[*]y[^]i) j) [=]
Sum 0 (lth_of_poly f) (fun i : nat ⇒ nth_coeff i f[*]x[^]i) [-]
Sum 0 (lth_of_poly f) (fun i : nat ⇒ nth_coeff i f[*]y[^]i)) in |- ×.
2: apply Sum_minus_Sum.
apply ap_wdl_unfolded with (f ! x[-]f ! y).
2: unfold cg_minus in |- ×.
2: apply csbf_wd_unfolded.
2: apply poly_as_sum.
2: apply poly_degree_lth.
2: apply csf_wd_unfolded.
2: apply poly_as_sum.
2: apply poly_degree_lth.
assumption.
Qed.
End Fund_Thm_Alg.