Let qK be a real between 0 and 1, with
forall (p : C[X]), (monic n p) -> forall (c : IR), ((AbsCC (p!Zero)) [<] 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!Zero)) < c0.
forall (p : C[X]), (monic n p) -> forall (c : IR), ((AbsCC (p!Zero)) [<] 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!Zero)) < c0.
Section Kneser_Sequence.
Variable qK : IR.
Variable zltq : 0 [<=] qK.
Variable qlt1 : qK [<] 1.
Hypothesis q_prop : forall p : cpoly C, monic n p -> forall c : IR,
AbsCC p ! 0 [<] c -> {z : C | AbsCC z[^]n [<=] c | AbsCC p ! z [<] qK[*]c}.
Variable p : cpoly C.
Hypothesis mp : monic n p.
Variable c0 : IR.
Hypothesis p0ltc0 : AbsCC p ! 0 [<] c0.
Record Knes_tup : Type :=
{z_el :> C;
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 : forall tup : Knes_tup, Knes_tupp tup.
Defined.
Fixpoint Knes_fun_it (i : N) : Knes_tup :=
match i with
| O => Build_Knes_tup 0 c0 p0ltc0
| S j => Knes_fun (Knes_fun_it j):Knes_tup
end.
Definition sK := Knes_fun_it:nat -> C.
Lemma sK_c : forall tup : Knes_tup, c_el (Knes_fun tup) [=] qK[*]c_el tup.
Lemma sK_c0 : forall i : N, c_el (Knes_fun_it i) [=] qK[^]i[*]c0.
Lemma sK_prop1 : forall i : N, AbsCC p ! (sK i) [<=] qK[^]i[*]c0.
Lemma sK_it : forall tup : Knes_tup, AbsCC (Knes_fun tup[-]tup) [^]n [<=] c_el tup.
Lemma sK_prop2 : forall i : N, AbsCC (sK (S i) [-]sK i) [^]n [<=] qK[^]i[*]c0.
End Kneser_Sequence.
Section Seq_Exists_Main.
Lemma seq_exists : {q : IR | 0 [<=] q | q [<] 1 and (forall p : cpoly C,
monic n p -> forall c : IR, AbsCC p ! 0 [<] c -> {s : N -> C | forall i,
AbsCC p ! (s i) [<=] q[^]i[*]c /\ AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c})}.
End Seq_Exists_Main.
End Seq_Exists.
Section N_Exists.
Variable n : N.
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 : N | forall m, N <= m -> (q[^]m[-]q[^]N[/] q[-]1[//]q_) [*]c [<=] e}.
End N_Exists.
Section Seq_is_CC_CAuchy.
Variable n : N.
Hypothesis lt0n : 0 < n.
Variable q : IR.
Hypothesis zleq : 0 [<=] q.
Hypothesis qlt1 : q [<] 1.
Variable c : IR.
Hypothesis zltc : 0 [<] c.
Let:
- q_ prove q−1 [#] 0
- nrtq := NRoot q n
- nrtc := Nroot c n
- nrtqlt1 prove nrtq < 1
- nrtq_ prove nrtq−1 [#] 0
Lemma zlt_nrtq : 0 [<=] nrtq.
Lemma zlt_nrtc : 0 [<] nrtc.
Lemma nrt_pow : forall i (H : 0 [<=] q[^]i[*]c), NRoot H lt0n [=] nrtq[^]i[*]nrtc.
Lemma abs_pow_ltRe : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) ->
forall i, AbsIR (ℜ (s (S i)) [-]ℜ (s i)) [<=] nrtq[^]i[*]nrtc.
Lemma abs_pow_ltIm : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) ->
forall i, AbsIR (ℑ (s (S i)) [-]ℑ (s i)) [<=] nrtq[^]i[*]nrtc.
Lemma SublemmaRe : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) -> forall N m,
N <= m -> AbsIR (ℜ (s m) [-]ℜ (s N)) [<=] (nrtq[^]m[-]nrtq[^]N[/] nrtq[-]1[//]nrtq_) [*]nrtc.
Lemma SublemmaIm : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) -> forall N m,
N <= m -> AbsIR (ℑ (s m) [-]ℑ (s N)) [<=] (nrtq[^]m[-]nrtq[^]N[/] nrtq[-]1[//]nrtq_) [*]nrtc.
Lemma seq_is_CC_Cauchy : forall s,
(forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) -> CC_Cauchy_prop s.
End Seq_is_CC_CAuchy.
Lemma FTA_monic : forall (p : cpoly C) (n : N),
0 < n -> monic n p -> {c : C | p ! c [=] 0}.
Lemma FTA_reg : forall (p : cpoly C) (n : N),
0 < n -> degree n p -> {c : C | p ! c [=] 0}.