proposition: Lemma fun_ratio_test_conv : {N : nat | {c : IR | c [<] [1] | [0] [<=] c /\ (forall x, I x -> forall n, N <= n -> forall Hx Hx', AbsIR (f (S n) x Hx') [<=] c[*]AbsIR (f n x Hx))}} -> fun_series_convergent _ _ Hab f.
proof: Proof. intro H. elim H; clear H; intros N H. elim H; clear H; intros c Hc1 H. elim H; clear H; intros H0c H. cut (forall x : IR, I x -> forall n : nat, N <= n -> forall Hx Hx', AbsIR (f n x Hx') [<=] AbsIR (f N x Hx) [*]c[^] (n - N)). intro H0. apply fun_str_comparison with (fun n : nat => FAbs (f N) {*} [-C-] (c[^] (n - N))). 2: exists N; intros. 2: eapply leEq_wdr. 2: apply H0 with (Hx' := Hx) (Hx := ProjIR1 (ProjIR1 Hx')); auto with arith. Opaque FAbs. 2: simpl in |- *; apply mult_wd; [ apply eq_symmetric_unfolded; apply FAbs_char | algebra ]. apply conv_fun_series_scal with (f := fun n : nat => [-C-] (c[^] (n - N))). apply conv_fun_const_series with (x := fun n : nat => c[^] (n - N)). apply join_series with (power_series c). apply power_series_conv. apply AbsIR_less. assumption. apply less_leEq_trans with [0]. rstepr ([--][0]:IR). apply inv_resp_less. apply pos_one. assumption. exists N. exists 0. intro. rewrite Nat.add_sub. algebra. Contin. intros x H0 n; induction n as [| n Hrecn]. intro. cut (N = 0); [ intro | auto with arith ]. rewrite H2. intros. apply eq_imp_leEq. simpl in |- *. astepl (AbsIR (Part _ _ Hx') [*][1]); apply mult_wdl; apply AbsIR_wd; algebra. intro. elim (le_lt_eq_dec _ _ H1); intro. intros; apply leEq_transitive with (c[*]AbsIR (f n x (contin_imp_inc _ _ _ _ (contF n) x H0))). apply H; auto with arith. apply leEq_wdr with (AbsIR (f N x Hx) [*]c[^] (n - N) [*]c). rstepr (c[*] (AbsIR (Part _ _ Hx) [*]c[^] (n - N))). apply mult_resp_leEq_lft. apply Hrecn; auto with arith. assumption. rewrite Nat.sub_succ_l. simpl in |- *; rational. auto with arith. rewrite b0; intros. rewrite Nat.sub_diag. apply eq_imp_leEq. simpl in |- *; eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply mult_one. apply AbsIR_wd; algebra. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series