CoRN.fta.MainLemma

Require Export CSumsReals.
Require Export KeyLemma.
Require Import CRing_as_Ring.

Main Lemma

Section Main_Lemma.

Let a : nat→IR, n : nat, a_0 : IR and eps : IR such that 0 < n, ([0] [<] eps), ∀ (k : nat)([0] [<=] (a k)), (a n) [=] [1], and (eps [<=] a_0).

Variable a : nat → IR.
Variable n : nat.
Hypothesis gt_n_0 : 0 < n.
Variable eps : IR.
Hypothesis eps_pos : [0] [<] eps.
Hypothesis a_nonneg : ∀ k : nat, [0] [<=] a k.
Hypothesis a_n_1 : a n [=] [1].
Variable a_0 : IR.
Hypothesis eps_le_a_0 : eps [<=] a_0.

Lemma a_0_pos : [0] [<] a_0.
Proof.
apply less_leEq_trans with eps; auto.
Qed.

We define the following local abbreviations:

2n := 2 × n
Small := p3m n
Smaller := p3m (2n × n)

Lemma Main_1a' : ∀ (t : IR) (j k : nat),
let r' := t [*]p3m (S (S j)) in let r := t [*]p3m (S j) in
(∀ i, 1 ≤ i → i ≤ n → a i [*]r'[^]i [-]eps [<=] a k [*]r'[^]k) →
∀ i : nat, 1 ≤ i → i ≤ n → a i [*] (r [/]ThreeNZ ) [^]i [-]eps [<=] a k [*] (r [/]ThreeNZ ) [^]k.
Proof.

Lemma Main_1b' : ∀ (t : IR) (j k : nat),
let r' := t [*]p3m j in let r := t [*]p3m (S j) in
(∀ i, 1 ≤ i → i ≤ n → a i [*]r'[^]i [-]eps [<=] a k [*]r'[^]k) →
∀ i, 1 ≤ i → i ≤ n → a i [*] (r [*]Three ) [^]i [-]eps [<=] a k [*] (r [*]Three ) [^]k.
Proof.

Lemma Main_1a : ∀ (r : IR) (k : nat), [0] [<=] r → 1 ≤ k → k ≤ n →
(∀ i, 1 ≤ i → i ≤ n → a i [*] (r [/]ThreeNZ ) [^]i [-]eps [<=] a k [*] (r [/]ThreeNZ ) [^]k) →
let p_ := fun i : nat ⇒ a i [*]r [^]i in let p_k := a k [*]r [^]k in
Sum 1 (pred k) p_ [<=] Half [*] ([1][-]Small ) [*]p_k [+]Half [*]Three [^]n [*]eps.
Proof.

Lemma Main_1b : ∀ (r : IR) (k : nat), [0] [<=] r → 1 ≤ k → k ≤ n →
(∀ i, 1 ≤ i → i ≤ n → a i [*] (r [*]Three ) [^]i [-]eps [<=] a k [*] (r [*]Three ) [^]k) →
let p_ := fun i ⇒ a i [*]r [^]i in let p_k := a k [*]r [^]k in
Sum (S k) n p_ [<=] Half [*] ([1][-]Small ) [*]p_k [+]Half [*]Three [^]n [*]eps.
Proof.

Lemma Main_1 : ∀ (r : IR) (k : nat), [0] [<=] r → 1 ≤ k → k ≤ n →
(∀ i, 1 ≤ i → i ≤ n → a i [*] (r [/]ThreeNZ ) [^]i [-]eps [<=] a k [*] (r [/]ThreeNZ ) [^]k) →
(∀ i, 1 ≤ i → i ≤ n → a i [*] (r [*]Three ) [^]i [-]eps [<=] a k [*] (r [*]Three ) [^]k) →
let p_ := fun i ⇒ a i [*]r [^]i in let p_k := a k [*]r [^]k in
Sum 1 (pred k) p_[+]Sum (S k) n p_ [<=] ([1][-]Small ) [*]p_k [+]Three [^]n [*]eps.
Proof.

Lemma Main_2' : ∀ (t : IR) (i k : nat),
a i [*] (t [*]p3m 0) [^]i [-]eps [<=] a k [*] (t [*]p3m 0) [^]k → a i [*]t [^]i [-]eps [<=] a k [*]t [^]k.
Proof.
intros.
cut (t[*]p3m 0 [=] t). intro.
  astepl (a i[*] (t[*]p3m 0) [^]i[-]eps).
  astepr (a k[*] (t[*]p3m 0) [^]k).
  auto.
Step_final (t[*][1]).
Qed.

Lemma Main_2 : ∀ (t : IR) (j k : nat), let r := t [*]p3m j in
[0] [<=] t → a k [*]t [^]k [=] a_0 [-]eps → (∀ i, 1 ≤ i → i ≤ n → a i [*]t [^]i [-]eps [<=] a k [*]t [^]k) →
∀ i, 1 ≤ i → i ≤ n → a i [*]r [^]i [<=] a_0.
Proof.

Lemma Main_3a : ∀ (t : IR) (j k k_0 : nat), let r := t [*]p3m j in
k_0 ≤ n → a k_0 [*]t [^]k_0 [=] a_0 [-]eps → a k_0 [*]r [^]k_0 [-]eps [<=] a k [*]r [^]k →
p3m (j × n) [*]a_0 [-]Two [*]eps [<=] a k [*]r [^]k.
Proof.

Lemma Main_3 : ∀ (t : IR) (j k k_0 : nat), let r := t [*]p3m j in
j < 2n → k_0 ≤ n → a k_0 [*]t [^]k_0 [=] a_0 [-]eps → a k_0 [*]r [^]k_0 [-]eps [<=] a k [*]r [^]k →
Smaller [*]a_0 [-]Two [*]eps [<=] a k [*]r [^]k.
Proof.

Lemma Main : {r : IR | [0] [<=] r | {k : nat | 1 ≤ k ∧ k ≤ n ∧
(let p_ := fun i ⇒ a i [*]r[^]i in let p_k := a k[*]r[^]k in
  Sum 1 (pred k) p_[+]Sum (S k) n p_ [<=] ([1][-]Small ) [*]p_k [+]Three [^]n [*]eps ∧
  r[^]n [<=] a_0 ∧ Smaller [*]a_0 [-]Two [*]eps [<=] p_k ∧ p_k [<=] a_0 )}}.
Proof.

End Main_Lemma.