proposition: Lemma Main_1b : forall (r : IR) (k : nat), [0] [<=] r -> 1 <= k -> k <= n -> (forall 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: Proof. intros r k H H0 H1 H2 p_ p_k. unfold p_, p_k in |- *. cut (forall i : nat, Three[^]i [#] ZeroR). intro H3. 2: intro i; apply pos_ap_zero. 2: apply nexp_resp_pos. 2: apply pos_three. apply leEq_transitive with (Sum (S k) n (fun i : nat => a k[*] (r[*]Three) [^]k[+]eps[/] Three[^]i[//]H3 i)). apply Sum_resp_leEq. auto with arith. intros i H4 H5. apply shift_leEq_div. apply nexp_resp_pos; apply pos_three. rstepr (eps[+]a k[*] (r[*]Three) [^]k). apply shift_leEq_plus'. rstepl (a i[*] (r[^]i[*]Three[^]i) [-]eps). astepl (a i[*] (r[*]Three) [^]i[-]eps). apply H2; auto with arith. apply Nat.le_trans with (S k); auto. astepl (Sum (S k) n (fun i : nat => (a k[*] (r[*]Three) [^]k[+]eps) [*][1][/] Three[^]i[//]H3 i)). astepl (Sum (S k) n (fun i : nat => (a k[*] (r[*]Three) [^]k[+]eps) [*] ([1][/] Three[^]i[//]H3 i))). apply leEq_wdl with ((a k[*] (r[*]Three) [^]k[+]eps) [*] Sum (S k) n (fun i : nat => [1][/] Three[^]i[//]H3 i)). 2: apply eq_symmetric_unfolded. 2: apply mult_distr_sum_lft with (f := fun i : nat => [1][/] Three[^]i[//]H3 i). astepl ((a k[*] (r[*]Three) [^]k[+]eps) [*] Sum (S k) n (fun i : nat => ([1] [/]ThreeNZ) [^]i)). cut ([1][-][1] [/]ThreeNZ [#] ZeroR). 2: rstepl ((Two:IR) [/]ThreeNZ). 2: apply div_resp_ap_zero_rev. 2: apply two_ap_zero. intro H4. astepl ((a k[*] (r[*]Three) [^]k[+]eps) [*] (([1] [/]ThreeNZ) [^]S k[-] ([1] [/]ThreeNZ) [^]S n[/] [1][-][1] [/]ThreeNZ[//]H4)). astepl ((a k[*] (r[*]Three) [^]k[+]eps) [*] ([1] [/]ThreeNZ[*] ([1] [/]ThreeNZ) [^]k[-] [1] [/]ThreeNZ[*] ([1] [/]ThreeNZ) [^]n[/] [1][-][1] [/]ThreeNZ[//]H4)). rstepl ([1] [/]TwoNZ[*] (a k[*] (r[*]Three) [^]k) [*] (([1] [/]ThreeNZ) [^]k[-] ([1] [/]ThreeNZ) [^]n) [+] [1] [/]TwoNZ[*]eps[*] (([1] [/]ThreeNZ) [^]k[-] ([1] [/]ThreeNZ) [^]n)). apply leEq_transitive with (Half[*] ([1][-]Small) [*] (a k[*]r[^]k) [+] [1] [/]TwoNZ[*]eps[*] (([1] [/]ThreeNZ) [^]k[-] ([1] [/]ThreeNZ) [^]n)). apply plus_resp_leEq. astepl ([1] [/]TwoNZ[*] (a k[*] (r[^]k[*]Three[^]k)) [*] (([1] [/]ThreeNZ) [^]k[-] ([1] [/]ThreeNZ) [^]n)). rstepl ([1] [/]TwoNZ[*]a k[*]r[^]k[*] (Three[^]k[*] ([1] [/]ThreeNZ) [^]k[-]Three[^]k[*] ([1] [/]ThreeNZ) [^]n)). unfold Half in |- *. rstepr ([1] [/]TwoNZ[*]a k[*]r[^]k[*] ([1][-]Small)). apply mult_resp_leEq_lft. astepl (((Three:IR) [*][1] [/]ThreeNZ) [^]k[-]Three[^]k[*] ([1] [/]ThreeNZ) [^]n). astepl ((((Three:IR) [*][1]) [/]ThreeNZ) [^]k[-]Three[^]k[*] ([1] [/]ThreeNZ) [^]n). astepl (((Three:IR) [/]ThreeNZ) [^]k[-]Three[^]k[*] ([1] [/]ThreeNZ) [^]n). astepl (OneR[^]k[-]Three[^]k[*] ([1] [/]ThreeNZ) [^]n). astepl (OneR[-]Three[^]k[*] ([1] [/]ThreeNZ) [^]n). apply less_leEq. apply minus_resp_less_rht. unfold Small in |- *. unfold p3m in |- *. rstepl (OneR[*] ([1] [/]ThreeNZ) [^]n). apply mult_resp_less. astepl (OneR[^]k). apply nexp_resp_less; auto. apply less_leEq; apply pos_one. apply one_less_three. apply nexp_resp_pos. apply pos_div_three; apply pos_one. apply mult_resp_nonneg. apply mult_resp_nonneg. apply less_leEq. apply pos_div_two; apply pos_one. apply a_nonneg. apply nexp_resp_nonneg; assumption. apply plus_resp_leEq_lft. rstepr (Half[*]eps[*]Three[^]n). unfold Half in |- *. apply mult_resp_leEq_lft. apply leEq_transitive with OneR. apply leEq_transitive with ((OneR [/]ThreeNZ) [^]k). astepr ((OneR [/]ThreeNZ) [^]k[-][0]). apply less_leEq. apply minus_resp_less_rht. apply nexp_resp_pos. apply pos_div_three; apply pos_one. astepr ([1][^]k:IR). apply nexp_resp_leEq. apply less_leEq; apply pos_div_three; apply pos_one. astepr (OneR [/]OneNZ). apply less_leEq; apply recip_resp_less. apply pos_one. apply one_less_three. astepl (OneR[^]n). apply nexp_resp_leEq; apply less_leEq. apply pos_one. apply one_less_three. apply less_leEq. apply mult_resp_pos; auto. apply pos_div_two; apply pos_one. Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)