Let a : N->IR, n : N, a_0 : IR and ε : IR such that 0 < n,
(0 < ε), forall (k : N)(0 ≤ (a k)), (a n) = 1, and
(ε ≤ a_0).
Variable a : N -> IR.
Variable n : N.
Hypothesis gt_n_0 : 0 < n.
Variable ε : IR.
Hypothesis eps_pos : 0 [<] ε.
Hypothesis a_nonneg : forall k : N, 0 [<=] a k.
Hypothesis a_n_1 : a n [=] 1.
Variable a_0 : IR.
Hypothesis eps_le_a_0 : ε [<=] a_0.
Lemma a_0_pos : 0 [<] a_0.
We define the following local abbreviations:
- 2n := 2 * n
- Small := p3m n
- Smaller := p3m (2n * n)
Lemma Main_1a' : forall (t : IR) (j k : N),
let r' := t[*]p3m (S (S j)) in let r := t[*]p3m (S j) in
(forall i, 1 <= i -> i <= n -> a i[*]r'[^]i[-]ε [<=] a k[*]r'[^]k) ->
forall i : N, 1 <= i -> i <= n -> a i[*] (r [/]3) [^]i[-]ε [<=] a k[*] (r [/]3) [^]k.
Lemma Main_1b' : forall (t : IR) (j k : N),
let r' := t[*]p3m j in let r := t[*]p3m (S j) in
(forall i, 1 <= i -> i <= n -> a i[*]r'[^]i[-]ε [<=] a k[*]r'[^]k) ->
forall i, 1 <= i -> i <= n -> a i[*] (r[*]3) [^]i[-]ε [<=] a k[*] (r[*]3) [^]k.
Lemma Main_1a : forall (r : IR) (k : N), 0 [<=] r -> 1 <= k -> k <= n ->
(forall i, 1 <= i -> i <= n -> a i[*] (r [/]3) [^]i[-]ε [<=] a k[*] (r [/]3) [^]k) ->
let p_ := fun i : N => a i[*]r[^]i in let p_k := a k[*]r[^]k in
∑ 1 (pred k) p_ [<=] ½[*] (1[-]Small) [*]p_k[+]½[*]3[^]n[*]ε.
Lemma Main_1b : forall (r : IR) (k : N), 0 [<=] r -> 1 <= k -> k <= n ->
(forall i, 1 <= i -> i <= n -> a i[*] (r[*]3) [^]i[-]ε [<=] a k[*] (r[*]3) [^]k) ->
let p_ := fun i => a i[*]r[^]i in let p_k := a k[*]r[^]k in
∑ (S k) n p_ [<=] ½[*] (1[-]Small) [*]p_k[+]½[*]3[^]n[*]ε.
Lemma Main_1 : forall (r : IR) (k : N), 0 [<=] r -> 1 <= k -> k <= n ->
(forall i, 1 <= i -> i <= n -> a i[*] (r [/]3) [^]i[-]ε [<=] a k[*] (r [/]3) [^]k) ->
(forall i, 1 <= i -> i <= n -> a i[*] (r[*]3) [^]i[-]ε [<=] a k[*] (r[*]3) [^]k) ->
let p_ := fun i => a i[*]r[^]i in let p_k := a k[*]r[^]k in
∑ 1 (pred k) p_[+]∑ (S k) n p_ [<=] (1[-]Small) [*]p_k[+]3[^]n[*]ε.
Lemma Main_2' : forall (t : IR) (i k : N),
a i[*] (t[*]p3m 0) [^]i[-]ε [<=] a k[*] (t[*]p3m 0) [^]k -> a i[*]t[^]i[-]ε [<=] a k[*]t[^]k.
Lemma Main_2 : forall (t : IR) (j k : N), let r := t[*]p3m j in
0 [<=] t -> a k[*]t[^]k [=] a_0[-]ε -> (forall i, 1 <= i -> i <= n -> a i[*]t[^]i[-]ε [<=] a k[*]t[^]k) ->
forall i, 1 <= i -> i <= n -> a i[*]r[^]i [<=] a_0.
Lemma Main_3a : forall (t : IR) (j k k_0 : N), let r := t[*]p3m j in
k_0 <= n -> a k_0[*]t[^]k_0 [=] a_0[-]ε -> a k_0[*]r[^]k_0[-]ε [<=] a k[*]r[^]k ->
p3m (j * n) [*]a_0[-]2[*]ε [<=] a k[*]r[^]k.
Lemma Main_3 : forall (t : IR) (j k k_0 : N), let r := t[*]p3m j in
j < 2n -> k_0 <= n -> a k_0[*]t[^]k_0 [=] a_0[-]ε -> a k_0[*]r[^]k_0[-]ε [<=] a k[*]r[^]k ->
Smaller[*]a_0[-]2[*]ε [<=] a k[*]r[^]k.
Lemma Main : {r : IR | 0 [<=] r | {k : N | 1 <= k /\ k <= n /\
(let p_ := fun i => a i[*]r[^]i in let p_k := a k[*]r[^]k in
∑ 1 (pred k) p_[+]∑ (S k) n p_ [<=] (1[-]Small) [*]p_k[+]3[^]n[*]ε /\
r[^]n [<=] a_0 /\ Smaller[*]a_0[-]2[*]ε [<=] p_k /\ p_k [<=] a_0)}}.
End Main_Lemma.