CoRN.fta.FTAreg


Require Export KneserLemma.
Require Export CPoly_Shift.
Require Export CPoly_Contin1.

FTA for regular polynomials

The Kneser sequence

Let n be a positive natural number.

Section Seq_Exists.
Variable n : nat.
Hypothesis lt0n : 0 < n.

Let qK be a real between 0 and 1, with
(p : CCX), (monic n p) → (c : IR), ((AbsCC (p![0])) [<] c) →
 {z:CC | ((AbsCC z) [^]n [<] c) | ((AbsCC (p!z)) [<] qK[*]c)}.
Let p be a monic polynomial over the complex numbers with degree n, and let c0 be such that (AbsCC (p![0])) [<] c0.

Section Kneser_Sequence.
Variable qK : IR.
Variable zltq : [0] [<=] qK.
Variable qlt1 : qK [<] [1].
Hypothesis q_prop : p : cpoly CC, monic n p c : IR,
AbsCC p ! [0] [<] c{z : CC | AbsCC z[^]n [<=] c | AbsCC p ! z [<] qK[*]c}.

Variable p : cpoly CC.
Hypothesis mp : monic n p.

Variable c0 : IR.
Hypothesis p0ltc0 : AbsCC p ! [0] [<] c0.

Record Knes_tup : Type :=
 {z_el :> CC;
  c_el : IR;
  Kt_prop : AbsCC p ! z_el [<] c_el}.

Record Knes_tupp (tup : Knes_tup) : Type :=
  {Kntup :> Knes_tup;
   Ktp_prop : c_el Kntup [=] qK[*]c_el tup;
   Ktpp_prop : AbsCC (Kntup[-]tup) [^]n [<=] c_el tup}.

Definition Knes_fun : tup : Knes_tup, Knes_tupp tup.
Proof.
 intro tup.
 elim tup.
 intros z c pzltc.
 cut (AbsCC (Shift z p) ! [0] [<] c).
  intro Hsh.
  generalize (q_prop (Shift z p) (Shift_monic z p n mp) c Hsh).
  intro Hex.
  elim Hex.
  intros z'; intros.
  cut (AbsCC p ! (z'[+]z) [<] qK[*]c).
   intro HH.
   apply (Build_Knes_tupp (Build_Knes_tup z c pzltc) (Build_Knes_tup (z'[+]z) (qK[*]c) HH)).
    simpl in |- *; algebra.
   simpl in |- *; apply leEq_wdl with (AbsCC z'[^]n).
    assumption.
   apply (nexp_wd IR (AbsCC z') (AbsCC (z'[+]z[-]z)) n).
   apply AbsCC_wd.
   rational.
  apply less_wdl with (AbsCC (Shift z p) ! z').
   assumption.
  apply AbsCC_wd.
  apply Shift_apply.
 apply less_wdl with (AbsCC p ! z).
  assumption.
 generalize (Shift_apply z p [0]).
 intro H3.
 apply eq_symmetric_unfolded.
 apply AbsCC_wd.
 apply eq_transitive_unfolded with p ! ([0][+]z).
  assumption.
 algebra.
Defined.

Fixpoint Knes_fun_it (i : nat) : Knes_tup :=
  match i with
  | OBuild_Knes_tup [0] c0 p0ltc0
  | S jKnes_fun (Knes_fun_it j):Knes_tup
  end.

Definition sK := Knes_fun_it:natCC.

Lemma sK_c : tup : Knes_tup, c_el (Knes_fun tup) [=] qK[*]c_el tup.
Proof.
 intro tup.
 generalize (Ktp_prop tup (Knes_fun tup)).
 auto.
Qed.

Lemma sK_c0 : i : nat, c_el (Knes_fun_it i) [=] qK[^]i[*]c0.
Proof.
 simple induction i.
  simpl in |- ×.
  rational.
 intros.
 simpl in |- ×.
 generalize (sK_c (Knes_fun_it n0)).
 intro H1.
 apply eq_transitive_unfolded with (qK[*]c_el (Knes_fun_it n0)).
  assumption.
 rstepr (qK[*] (nexp IR n0 qK[*]c0)).
 apply mult_wdr.
 exact H.
Qed.

Lemma sK_prop1 : i : nat, AbsCC p ! (sK i) [<=] qK[^]i[*]c0.
Proof.
 unfold sK in |- ×.
 simple induction i.
  simpl in |- ×.
  rstepr c0.
  apply less_leEq; exact p0ltc0.
 intros.
 simpl in |- ×.
 generalize (Kt_prop (Knes_fun (Knes_fun_it n0))).
 intro H2.
 apply leEq_wdr with (c_el (Knes_fun (Knes_fun_it n0))).
  apply less_leEq; assumption.
 generalize (sK_c (Knes_fun_it n0)).
 intro H3.
 eapply eq_transitive_unfolded.
  apply H3.
 generalize (sK_c0 n0).
 intro H4.
 rstepr (qK[*] (nexp IR n0 qK[*]c0)).
 apply mult_wdr.
 exact H4.
Qed.

Lemma sK_it : tup : Knes_tup, AbsCC (Knes_fun tup[-]tup) [^]n [<=] c_el tup.
Proof.
 intro tup.
 generalize (Ktpp_prop tup (Knes_fun tup)).
 auto.
Qed.

Lemma sK_prop2 : i : nat, AbsCC (sK (S i) [-]sK i) [^]n [<=] qK[^]i[*]c0.
Proof.
 unfold sK in |- ×.
 simpl in |- ×.
 intro i.
 generalize (sK_it (Knes_fun_it i)).
 intro H0.
 eapply leEq_wdr.
  apply H0.
 exact (sK_c0 i).
Qed.

End Kneser_Sequence.

Section Seq_Exists_Main.

Main results


Lemma seq_exists : {q : IR | [0] [<=] q | q [<] [1] and ( p : cpoly CC,
 monic n p c : IR, AbsCC p ! [0] [<] c{s : natCC | i,
  AbsCC p ! (s i) [<=] q[^]i[*]c AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c})}.
Proof.
 elim (Kneser n lt0n).
 intros q; intros H H0.
  q.
  assumption.
 inversion_clear H0.
 rename X0 into H2.
 split. assumption.
  intros p mp c pzltc.
  (sK q H2 p mp c pzltc).
 split.
  exact (sK_prop1 q H2 p mp c pzltc i).
 exact (sK_prop2 q H2 p mp c pzltc i).
Qed.

End Seq_Exists_Main.

End Seq_Exists.

Section N_Exists.

Variable n : nat.
Hypothesis lt0n : 0 < n.
Variable q : IR.
Hypothesis zleq : [0] [<=] q.
Hypothesis qlt1 : q [<] [1].
Variable c : IR.
Hypothesis zltc : [0] [<] c.
Variable e : IR.
Variable zlte : [0] [<] e.

Lemma N_exists : {N : nat | m, N m(q[^]m[-]q[^]N[/] q[-][1][//]q_) [*]c [<=] e}.
Proof.
 cut ([0] [<] [1][-]q).
  intro H0.
  cut ([1][-]q [#] [0]).
   intro H3.
   cut (c [#] [0]).
    intro H1.
    cut ([0] [<] ([1][-]q) [*] (e[/] c[//]H1)).
     intro H2.
     elim (qi_yields_zero q zleq qlt1 (([1][-]q) [*] (e[/] c[//]H1)) H2).
     intros N HN.
      N.
     intros m leNm.
     rstepl ((q[^]N[-]q[^]m[/] [1][-]q[//]H3) [*]c).
     apply shift_mult_leEq with H1.
      assumption.
     apply shift_div_leEq'.
      assumption.
     apply leEq_transitive with (q[^]N).
      rstepl ([0][+] (q[^]N[-]q[^]m)).
      apply shift_plus_leEq.
      rstepr (q[^]m).
      apply nexp_resp_nonneg.
      assumption.
     assumption.
    apply mult_resp_pos.
     assumption.
    apply div_resp_pos.
     assumption.
    assumption.
   apply ap_symmetric_unfolded.
   apply less_imp_ap.
   assumption.
  apply ap_symmetric_unfolded.
  apply less_imp_ap.
  assumption.
 apply shift_less_minus.
 rstepl q.
 assumption.
Qed.

End N_Exists.

Section Seq_is_CC_CAuchy.

The Kneser sequence is Cauchy in CC


Variable n : nat.
Hypothesis lt0n : 0 < n.
Variable q : IR.
Hypothesis zleq : [0] [<=] q.
Hypothesis qlt1 : q [<] [1].
Variable c : IR.
Hypothesis zltc : [0] [<] c.

Let:


Lemma zlt_nrtq : [0] [<=] nrtq.
Proof.
 unfold nrtq; apply NRoot_nonneg.
Qed.

Lemma zlt_nrtc : [0] [<] nrtc.
Proof.
 unfold nrtc; apply NRoot_pos; auto.
Qed.

Lemma nrt_pow : i (H : [0] [<=] q[^]i[*]c), NRoot H lt0n [=] nrtq[^]i[*]nrtc.
Proof.
 intros.
 apply root_unique with n.
    apply NRoot_nonneg.
   apply mult_resp_nonneg.
    apply nexp_resp_nonneg. exact zlt_nrtq.
    apply less_leEq. exact zlt_nrtc.
   auto.
 astepl (q[^]i[*]c).
 astepr ((nrtq[^]i) [^]n[*]nrtc[^]n).
 astepr (nrtq[^] (i × n) [*]nrtc[^]n).
 rewrite mult_comm.
 astepr ((nrtq[^]n) [^]i[*]nrtc[^]n).
 unfold nrtq in |- ×. unfold nrtc in |- ×.
 apply bin_op_wd_unfolded.
  apply un_op_wd_unfolded.
  algebra.
 algebra.
Qed.

Lemma abs_pow_ltRe : s, ( i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) →
  i, AbsIR (Re (s (S i)) [-]Re (s i)) [<=] nrtq[^]i[*]nrtc.
Proof.
 intros s H i.
 apply leEq_wdl with (AbsIR (Re (s (S i) [-]s i))).
  apply leEq_transitive with (AbsCC (s (S i) [-]s i)).
   apply absCC_absIR_re.
  generalize (H i).
  intro Hi.
  cut ([0] [<=] q[^]i[*]c).
   intro H0.
   cut (AbsCC (s (S i) [-]s i) [<=] NRoot H0 lt0n).
    intro H1.
    apply leEq_wdr with (NRoot H0 lt0n).
     assumption.
    apply nrt_pow.
   apply power_cancel_leEq with n.
     auto with arith.
    apply NRoot_nonneg.
   apply leEq_wdr with (q[^]i[*]c).
    exact (H i).
   algebra.
  apply mult_resp_nonneg.
   apply nexp_resp_nonneg.
   assumption.
  apply less_leEq; assumption.
 apply ABSIR_wd.
 apply Re_resp_inv.
Qed.

Lemma abs_pow_ltIm : s, ( i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) →
  i, AbsIR (Im (s (S i)) [-]Im (s i)) [<=] nrtq[^]i[*]nrtc.
Proof.
 intros s H i.
 apply leEq_wdl with (AbsIR (Im (s (S i) [-]s i))).
  apply leEq_transitive with (AbsCC (s (S i) [-]s i)).
   apply absCC_absIR_im.
  generalize (H i).
  intro Hi.
  cut ([0] [<=] q[^]i[*]c).
   intro H0.
   cut (AbsCC (s (S i) [-]s i) [<=] NRoot H0 lt0n).
    intro H1.
    apply leEq_wdr with (NRoot H0 lt0n).
     assumption.
    apply nrt_pow.
   apply power_cancel_leEq with n.
     auto with arith.
    apply NRoot_nonneg.
   apply leEq_wdr with (q[^]i[*]c).
    exact (H i).
   algebra.
  apply mult_resp_nonneg.
   apply nexp_resp_nonneg.
   assumption.
  apply less_leEq; assumption.
 apply ABSIR_wd.
 apply Im_resp_inv.
Qed.

Lemma SublemmaRe : s, ( i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) → N m,
 N mAbsIR (Re (s m) [-]Re (s N)) [<=] (nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc.
Proof.
 intros s Hi N m leNm.
 elim (le_lt_eq_dec N m leNm).
  intro ltNm.
  generalize (diff_is_sum (fun j : natRe (s j)) N m ltNm).
  intro Hsum.
  generalize (ABSIR_wd _ _ Hsum).   intro Habseq.
  apply leEq_wdl with (ABSIR (Sum N (pred m) (fun i : natRe (s (S i)) [-]Re (s i)))).
   2: apply eq_symmetric_unfolded; apply Habseq.
  cut (N S (pred m)). intro leNm'.
2: clear nrtq_ nrtqlt1 nrtc nrtq; omega.
  generalize (triangle_SumIR N (pred m) (fun i : natRe (s (S i)) [-]Re (s i)) leNm').
  intro Htri.
  apply leEq_transitive with (Sum N (pred m)
    (fun i : natcsf_fun IR IR AbsIR (Re (s (S i)) [-]Re (s i)))).
   exact Htri.
  generalize (Sum_pres_leEq (fun i : natAbsIR (Re (s (S i)) [-]Re (s i)))
    (fun i : natnrtq[^]i[*]nrtc) (abs_pow_ltRe s Hi) N ( pred m)).
  intro Hlt.
  apply leEq_transitive with (Sum N (pred m) (fun i : natnrtq[^]i[*]nrtc)).
   cut (N pred m).
    intro leNpm.
    exact (Hlt leNpm).
   generalize (S_pred m N ltNm).
   intro Heq.
   apply lt_n_Sm_le.
   rewrite <- Heq.
   assumption.
  generalize (Sum_c_exp nrtq nrtq_ N (pred m)).
  intro Hs.
  generalize (Sum_comm_scal (fun i : natnrtq[^]i) nrtc N (pred m)).
  intro Hs2.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply Hs2.
  apply mult_resp_leEq_rht.
   generalize (Sum_c_exp nrtq nrtq_ N (pred m)).
   intro Hs3.
   cut (S (pred m) = m).
    intro Heq.
    rewrite Heq in Hs3.
    apply eq_imp_leEq; assumption.
   generalize (S_pred m N ltNm).
   auto.
  exact (less_leEq _ _ _ zlt_nrtc).
 intro HNm.
 rewrite HNm.
 apply leEq_wdl with (AbsIR [0]).
  apply leEq_wdl with ZeroR.
   apply leEq_wdr with ZeroR.
    exact (leEq_reflexive _ _).
   rational.
  apply eq_symmetric_unfolded; exact AbsIRz_isz.
 apply ABSIR_wd.
 rational.
Qed.

Lemma SublemmaIm : s, ( i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) → N m,
 N mAbsIR (Im (s m) [-]Im (s N)) [<=] (nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc.
Proof.
 intros s Hi N m leNm.
 elim (le_lt_eq_dec N m leNm).
  intro ltNm.
  generalize (diff_is_sum (fun j : natIm (s j)) N m ltNm).
  intro HSum.
  generalize (ABSIR_wd _ _ HSum).   intro Habseq.
  apply leEq_wdl with (ABSIR (Sum N (pred m) (fun i : natIm (s (S i)) [-]Im (s i)))).
   2: apply eq_symmetric_unfolded; apply Habseq.
  cut (N S (pred m)). intro leNm'.
2: clear nrtq_ nrtqlt1 nrtc nrtq; omega.
  generalize (triangle_SumIR N (pred m) (fun i : natIm (s (S i)) [-]Im (s i)) leNm').
  intro Htri.
  apply leEq_transitive with (Sum N (pred m)
    (fun i : natcsf_fun IR IR AbsIR (Im (s (S i)) [-]Im (s i)))).
   exact Htri.
  generalize (Sum_pres_leEq (fun i : natAbsIR (Im (s (S i)) [-]Im (s i)))
    (fun i : natnrtq[^]i[*]nrtc) (abs_pow_ltIm s Hi) N ( pred m)).
  intro Hlt.
  apply leEq_transitive with (Sum N (pred m) (fun i : natnrtq[^]i[*]nrtc)).
   cut (N pred m).
    intro leNpm.
    exact (Hlt leNpm).
   generalize (S_pred m N ltNm).
   intro Heq.
   apply lt_n_Sm_le.
   simpl in |- ×.
   rewrite <- Heq.
   assumption.
  generalize (Sum_c_exp nrtq nrtq_ N (pred m)).
  intro Hs.
  generalize (Sum_comm_scal (fun i : natnrtq[^]i) nrtc N (pred m)).
  intro Hs2.
  eapply leEq_wdl.
   2: apply eq_symmetric_unfolded; apply Hs2.
  apply mult_resp_leEq_rht.
   generalize (Sum_c_exp nrtq nrtq_ N (pred m)).
   intro Hs3.
   cut (S (pred m) = m).
    intro Heq.
    rewrite Heq in Hs3.
    apply eq_imp_leEq; assumption.
   generalize (S_pred m N ltNm).
   auto.
  exact (less_leEq _ _ _ zlt_nrtc).
 intro HNm.
 rewrite HNm.
 apply leEq_wdl with (AbsIR [0]).
  apply leEq_wdl with ZeroR.
   apply leEq_wdr with ZeroR.
    exact (leEq_reflexive _ _).
   rational.
  apply eq_symmetric_unfolded; exact AbsIRz_isz.
 apply ABSIR_wd.
 rational.
Qed.

Lemma seq_is_CC_Cauchy : s,
 ( i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) → CC_Cauchy_prop s.
Proof.
 unfold CC_Cauchy_prop in |- ×.
 split.
  unfold Cauchy_prop in |- ×.
  intros e zlte.
  generalize (N_exists nrtq zlt_nrtq nrtqlt1 nrtc zlt_nrtc e zlte).
  intro Hex.
  elim Hex.
  intros N HN.
   N.
  intros m leNm.
  apply AbsIR_imp_AbsSmall.
  generalize (SublemmaRe s H N m leNm).
  intro H2.
  generalize (HN m leNm).
  intro H3.
  eapply leEq_transitive.
   2: apply H3.
  rstepr ((nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc).
  exact H2.
 unfold Cauchy_prop in |- ×.
 intros e zlte.
 generalize (N_exists nrtq zlt_nrtq nrtqlt1 nrtc zlt_nrtc e zlte).
 intro Hex.
 elim Hex.
 intros N HN.
  N.
 intros m leNm.
 apply AbsIR_imp_AbsSmall.
 generalize (SublemmaIm s H N m leNm).
 intro H2.
 generalize (HN m leNm).
 intro H3.
 eapply leEq_transitive.
  2: apply H3.
 rstepr ((nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc).
 exact H2.
Qed.

End Seq_is_CC_CAuchy.

Lemma FTA_monic : (p : cpoly CC) (n : nat),
 0 < nmonic n p{c : CC | p ! c [=] [0]}.
Proof.
 intros p n H0n mon.
 generalize (seq_exists n H0n).
 intro H.
 elim H.
 intros q qnonneg Hq1.
 elim Hq1.
 intros qlt10 Hq2.
 generalize (Hq2 p mon).
 intro Hq3.
 cut ([0] [<] AbsCC p ! [0][+][1]).
  intro Hp.
  elim (Hq3 (AbsCC p ! [0][+][1])).
   intros s Hs.
   cut ( i : nat, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*] (AbsCC p ! [0][+][1])).
    intro Hs2.
    cut (CC_Cauchy_prop s).
     intro Hs3.
      (LimCC (Build_CC_CauchySeq s Hs3)).
     apply CC_SeqLimit_uniq with (fun n : natp ! (s n)).
      exact (poly_pres_lim (fun x : CCp ! x) (contin_polyCC p) (Build_CC_CauchySeq s Hs3)).
     generalize (seq_yields_zero q qnonneg qlt10 (AbsCC p ! [0][+][1]) Hp (fun n0 : natp ! (s n0))).
     intro H0. apply H0.
     intro i. generalize (Hs i).
     intro H1; inversion_clear H1; assumption.
    exact (seq_is_CC_Cauchy n H0n q qnonneg qlt10 (AbsCC p ! [0][+][1]) Hp s Hs2).
   intro i; generalize (Hs i); intro Ha; elim Ha; intros; assumption.
  exact (less_plusOne _ (AbsCC p ! [0])).
 apply zero_lt_posplus1.
 apply AbsCC_nonneg.
Qed.

Lemma FTA_reg : (p : cpoly CC) (n : nat),
 0 < ndegree n p{c : CC | p ! c [=] [0]}.
Proof.
 intros p n H H0.
 elim (FTA_monic (poly_norm _ p n H0) n); auto.
  intros. x.
  apply poly_norm_apply with n H0; auto.
 apply poly_norm_monic; auto.
Qed.