Let b : N->CC, n : N and c : IR
such that 0 < n, b_0 := b 0, b_n := (b n) = 1 and
(AbsCC b_0) < c.
Variable b : N -> C.
Variable n : N.
Hypothesis gt_n_0 : 0 < n.
Hypothesis b_n_1 : b_n [=] 1.
Variable c : IR.
Hypothesis b_0_lt_c : AbsCC b_0 [<] c.
We define the following local abbreviations:
- 2n := 2 * n
- Small := p3m n
- Smaller := p3m (2n * n)
- Smallest := Small×Smaller
- q := 1−Smallest
- a i := AbsCC (b i)
Lemma b_0'_exists : forall η : IR, 0 [<] η -> {b_0' : C | AbsCC (b_0'[-]b_0) [<=] η | b_0' [#] 0}.
Let η0 := ((c[-]AbsCC b_0) [/]4) [/]2.
Lemma eta_0_pos : 0 [<] η0.
Lemma eta_exists : {η : IR | 0 [<] η |
{b_0' : C | AbsCC (b_0'[-]b_0) [<=] η | b_0' [#] 0 and AbsCC b_0'[+]3[*]η [<] c}}.
Lemma eps_exists_1 : forall ε x y : IR, 0 [<] ε -> 0 [<] x -> 0 [<] y ->
{eps' : IR | 0 [<] eps' | eps' [<=] ε /\ x[*]eps' [<=] y}.
Lemma eps_exists : forall η a_0 : IR, 0 [<] η -> 0 [<] a_0 ->
{ε : IR | 0 [<] ε | 2[*] (3[^]n[+]1) [*]ε [<=] η /\ 3[*]ε [<=] Smaller[*]a_0 /\ ε [<=] a_0}.
Lemma z_exists : forall (b_0' : C) (k : N) (r η : IR), let a_0 := AbsCC b_0' in
0 [<] a_0 -> 0 [<] a k -> 1 <= k -> k <= n -> 0 [<=] r -> 0 [<] η ->
AbsCC (b_0'[-]b_0) [<=] η -> a k[*]r[^]k [<=] a_0 ->
{z : C | AbsCC z [=] r | AbsCC (b_0[+]b k[*]z[^]k) [<=] a_0[-]a k[*]r[^]k[+]η}.
Lemma Kneser_1' : ½ [<=] q.
Lemma Kneser_1'' : q [<] 1.
Lemma Kneser_1 : forall a_0 η ε : IR, 0 [<] η -> 0 [<] ε ->
a_0[+]3[*]η [<] c -> 2[*] (3[^]n[+]1) [*]ε [<=] η -> q[*]a_0[+]3[^]n[*]ε[+]ε[+]η [<] q[*]c.
Lemma Kneser_2a : forall (R : CRing) (m n i : N) (f : N -> R), 1 <= i ->
∑ m n f [=] f m[+]f i[+] (∑ (S m) (pred i) f[+]∑ (S i) n f).
Lemma Kneser_2b : forall (k : N) (z : C), 1 <= k ->
let p_ := fun i => b i[*]z[^]i in
∑ 0 n (fun i => b i[*]z[^]i) [=] b_0[+]b k[*]z[^]k[+] (∑ 1 (pred k) p_[+]∑ (S k) n p_).
Lemma Kneser_2c : forall (m n : N) (z : C), m <= S n ->
let r := AbsCC z in
AbsCC (∑ m n (fun i => b i[*]z[^]i)) [<=] ∑ m n (fun i => a i[*]r[^]i).
Lemma Kneser_2 : forall (k : N) (z : C), 1 <= k -> k <= n ->
let r := AbsCC z in let p_ := fun i => a i[*]r[^]i in
AbsCC (∑ 0 n (fun i => b i[*]z[^]i)) [<=]
AbsCC (b_0[+]b k[*]z[^]k) [+] (∑ 1 (pred k) p_[+]∑ (S k) n p_).
Lemma Kneser_3 : {z : C | AbsCC z[^]n [<=] c | AbsCC (∑ 0 n (fun i => b i[*]z[^]i)) [<] q[*]c}.
End Kneser_Lemma.
Lemma Kneser : forall n : N, 0 < n -> {q : IR | 0 [<=] q |
q [<] 1 and (forall p : cpoly C, monic n p -> forall c : IR,
AbsCC p ! 0 [<] c -> {z : C | AbsCC z[^]n [<=] c | AbsCC p ! z [<] q[*]c})}.