Let a:nat->IR and n:nat such that 0 < n,
forall (k : N) (0 ≤ (a k)), (a n) = 1 and a_0 : IR,
and ε : IR such that (0 < ε) 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_eps_nonneg : 0 [<=] a_0[-]ε.
Lemma a_0_eps_fuzz : a_0[-]ε [<] a_0.
Lemma lem_1a : n - (n - 1) = 1.
Lemma lem_1b : forall n j : N, n - S j <= n - j.
Lemma lem_1c : forall n j : N, n - j <= n.
Lemma lem_1 : {t : IR | 0 [<=] t |
{k : N | 1 <= k /\ k <= n /\ a k[*]t[^]k [=] a_0[-]ε /\
(forall i, 1 <= i -> i <= n -> a i[*]t[^]i [<=] a_0)}}.
Definition p3m (i : N) := (1 [/]3) [^]i:IR.
Lemma p3m_pos : forall i : N, 0 [<] p3m i.
Lemma p3m_S : forall i : N, p3m (S i) [=] p3m i [/]3.
Lemma p3m_P : forall i : N, p3m i [=] p3m (S i) [*]3.
Lemma p3m_aux : forall i j : N, p3m (S i) [^]j [=] p3m j[*]p3m i[^]j.
Lemma p3m_pow : forall i j : N, p3m i[^]j [=] p3m (i * j).
Lemma p3m_0 : p3m 0 [=] 1.
Lemma third_pos : 0 [<] 1 [/]3.
Lemma third_less_one : 1 [/]3 [<] 1.
Lemma p3m_mon : forall i j : N, i < j -> p3m j [<] p3m i.
Lemma p3m_mon' : forall i j : N, i <= j -> p3m j [<=] p3m i.
Lemma p3m_small : forall i : N, p3m i [<=] 1.
Lemma p3m_smaller : forall i : N, 0 < i -> p3m i [<=] ½.
Definition chfun (k : N -> N) (a j i : N) : N :=
match le_gt_dec i j with
| left _ => k i
| right _ => a
end.
Lemma chfun_1 : forall k a j i, i <= j -> k i = chfun k a j i.
Lemma chfun_2 : forall k j a i, j < i -> a = chfun k a j i.
Lemma chfun_3 : forall k j a, (forall i, 1 <= k i /\ k i <= n) ->
1 <= a -> a <= n -> forall i, 1 <= chfun k a j i /\ chfun k a j i <= n.
Lemma chfun_4 : forall k j a, (forall i, k (S i) <= k i) ->
a <= k j -> forall i, chfun k a j (S i) <= chfun k a j i.
Definition Halfeps := ½[*]ε.
Lemma Halfeps_pos : 0 [<] Halfeps.
Lemma Halfeps_Halfeps : forall x : IR, x[-]Halfeps[-]Halfeps [=] x[-]ε.
Lemma Halfeps_eps : forall x y : IR, x[-]Halfeps [<=] y -> x[-]ε [<=] y.
Lemma Halfeps_trans : forall x y z : IR, x[-]Halfeps [<=] y -> y[-]Halfeps [<=] z -> x[-]ε [<=] z.
Lemma Key_1a : forall (i j : N) (a t : IR), a[*] (t[*]p3m (S j)) [^]i [=] p3m i[*] (a[*] (t[*]p3m j) [^]i).
Lemma Key_1b : forall k : N, 1 <= k -> p3m k[*]ε [<=] Halfeps.
Lemma Key_1 : forall (i k j : N) (ai ak t : IR),
1 <= k -> k < i -> 0 [<=] ai -> 0 [<=] t -> ai[*] (t[*]p3m j) [^]i[-]ε [<=] ak[*] (t[*]p3m j) [^]k ->
ai[*] (t[*]p3m (S j)) [^]i[-]Halfeps [<=] ak[*] (t[*]p3m (S j)) [^]k.
Lemma Key_2 : forall (i k k' j : N) (ai ak ak' t : IR),
1 <= k -> k < i -> 0 [<=] ai -> 0 [<=] t ->
ak[*] (t[*]p3m (S j)) [^]k[-]Halfeps [<=] ak'[*] (t[*]p3m (S j)) [^]k' ->
ai[*] (t[*]p3m j) [^]i[-]ε [<=] ak[*] (t[*]p3m j) [^]k -> ai[*] (t[*]p3m (S j)) [^]i[-]ε [<=] ak'[*] (t[*]p3m (S j)) [^]k'.
Lemma Key : {t : IR | 0 [<=] t | forall J, {k : N -> N |
(forall i, 1 <= k i /\ k i <= n) /\ (forall i, k (S i) <= k i) /\
(let k_0 := k 0 in a k_0[*]t[^]k_0 [=] a_0[-]ε) /\
(forall j, j <= J -> let k_j := k j in let r := t[*]p3m j in
forall i, 1 <= i -> i <= n -> a i[*]r[^]i[-]ε [<=] a k_j[*]r[^]k_j)}}.
End Key_Lemma.
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_eps_nonneg : 0 [<=] a_0[-]ε.
Lemma a_0_eps_fuzz : a_0[-]ε [<] a_0.
Lemma lem_1a : n - (n - 1) = 1.
Lemma lem_1b : forall n j : N, n - S j <= n - j.
Lemma lem_1c : forall n j : N, n - j <= n.
Lemma lem_1 : {t : IR | 0 [<=] t |
{k : N | 1 <= k /\ k <= n /\ a k[*]t[^]k [=] a_0[-]ε /\
(forall i, 1 <= i -> i <= n -> a i[*]t[^]i [<=] a_0)}}.
Definition p3m (i : N) := (1 [/]3) [^]i:IR.
Lemma p3m_pos : forall i : N, 0 [<] p3m i.
Lemma p3m_S : forall i : N, p3m (S i) [=] p3m i [/]3.
Lemma p3m_P : forall i : N, p3m i [=] p3m (S i) [*]3.
Lemma p3m_aux : forall i j : N, p3m (S i) [^]j [=] p3m j[*]p3m i[^]j.
Lemma p3m_pow : forall i j : N, p3m i[^]j [=] p3m (i * j).
Lemma p3m_0 : p3m 0 [=] 1.
Lemma third_pos : 0 [<] 1 [/]3.
Lemma third_less_one : 1 [/]3 [<] 1.
Lemma p3m_mon : forall i j : N, i < j -> p3m j [<] p3m i.
Lemma p3m_mon' : forall i j : N, i <= j -> p3m j [<=] p3m i.
Lemma p3m_small : forall i : N, p3m i [<=] 1.
Lemma p3m_smaller : forall i : N, 0 < i -> p3m i [<=] ½.
Definition chfun (k : N -> N) (a j i : N) : N :=
match le_gt_dec i j with
| left _ => k i
| right _ => a
end.
Lemma chfun_1 : forall k a j i, i <= j -> k i = chfun k a j i.
Lemma chfun_2 : forall k j a i, j < i -> a = chfun k a j i.
Lemma chfun_3 : forall k j a, (forall i, 1 <= k i /\ k i <= n) ->
1 <= a -> a <= n -> forall i, 1 <= chfun k a j i /\ chfun k a j i <= n.
Lemma chfun_4 : forall k j a, (forall i, k (S i) <= k i) ->
a <= k j -> forall i, chfun k a j (S i) <= chfun k a j i.
Definition Halfeps := ½[*]ε.
Lemma Halfeps_pos : 0 [<] Halfeps.
Lemma Halfeps_Halfeps : forall x : IR, x[-]Halfeps[-]Halfeps [=] x[-]ε.
Lemma Halfeps_eps : forall x y : IR, x[-]Halfeps [<=] y -> x[-]ε [<=] y.
Lemma Halfeps_trans : forall x y z : IR, x[-]Halfeps [<=] y -> y[-]Halfeps [<=] z -> x[-]ε [<=] z.
Lemma Key_1a : forall (i j : N) (a t : IR), a[*] (t[*]p3m (S j)) [^]i [=] p3m i[*] (a[*] (t[*]p3m j) [^]i).
Lemma Key_1b : forall k : N, 1 <= k -> p3m k[*]ε [<=] Halfeps.
Lemma Key_1 : forall (i k j : N) (ai ak t : IR),
1 <= k -> k < i -> 0 [<=] ai -> 0 [<=] t -> ai[*] (t[*]p3m j) [^]i[-]ε [<=] ak[*] (t[*]p3m j) [^]k ->
ai[*] (t[*]p3m (S j)) [^]i[-]Halfeps [<=] ak[*] (t[*]p3m (S j)) [^]k.
Lemma Key_2 : forall (i k k' j : N) (ai ak ak' t : IR),
1 <= k -> k < i -> 0 [<=] ai -> 0 [<=] t ->
ak[*] (t[*]p3m (S j)) [^]k[-]Halfeps [<=] ak'[*] (t[*]p3m (S j)) [^]k' ->
ai[*] (t[*]p3m j) [^]i[-]ε [<=] ak[*] (t[*]p3m j) [^]k -> ai[*] (t[*]p3m (S j)) [^]i[-]ε [<=] ak'[*] (t[*]p3m (S j)) [^]k'.
Lemma Key : {t : IR | 0 [<=] t | forall J, {k : N -> N |
(forall i, 1 <= k i /\ k i <= n) /\ (forall i, k (S i) <= k i) /\
(let k_0 := k 0 in a k_0[*]t[^]k_0 [=] a_0[-]ε) /\
(forall j, j <= J -> let k_j := k j in let r := t[*]p3m j in
forall i, 1 <= i -> i <= n -> a i[*]r[^]i[-]ε [<=] a k_j[*]r[^]k_j)}}.
End Key_Lemma.