proposition: Lemma fun_str_comparison : forall g, fun_series_convergent _ _ Hab g -> {k : nat | forall n, k <= n -> forall x, I x -> forall Hx Hx', AbsIR (f n x Hx) [<=] g n x Hx'} -> fun_series_convergent _ _ Hab f.
proof: Proof. set (H0 := contF) in *. intros g H H1. elim H1; intros k Hk. exists H0. apply Cauchy_fun_seq2_seq. intros e H2. elim H; intros contG convG. cut {N : nat | k < N /\ (forall m : nat, N <= m -> forall x : IR, I x -> forall Hx Hx', AbsSmall e (Part (fun_seq_part_sum g m) x Hx[-]Part (fun_seq_part_sum g N) x Hx'))}. intro H3. elim H3; clear H3. intros N HN; elim HN; clear HN; intros HN' HN. exists N; intros. assert (H' := fun n : nat => contin_imp_inc _ _ _ _ (fun_seq_part_sum_cont _ _ _ _ contG n)). apply leEq_transitive with (Part (fun_seq_part_sum g m) x (H' m x Hx) [-] Part (fun_seq_part_sum g N) x (H' N x Hx)). cut (forall n : nat, included (Compact Hab) (Dom (FAbs (f n)))). intro H4. cut (Dom (FSum N (pred m) (fun n : nat => FRestr (H4 n))) x). intro H5. apply leEq_transitive with (Part (FSum N (pred m) (fun n : nat => FRestr (H4 n))) x H5). cut (Dom (FSum N (pred m) (fun n : nat => FRestr (contin_imp_inc _ _ _ _ (H0 n)))) x). intro H6. apply leEq_wdl with (AbsIR (Part (FSum N (pred m) (fun n : nat => FRestr (contin_imp_inc _ _ _ _ (H0 n)))) x H6)). Opaque Frestr. simpl in |- *. Transparent Frestr. eapply leEq_wdr. apply triangle_SumIR. rewrite -> (Nat.lt_succ_pred k m); auto; apply Nat.lt_le_trans with N; auto. apply Sum_wd; intros. Opaque FAbs. simpl in |- *. Transparent FAbs. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply FAbs_char with (Hx' := contin_imp_inc _ _ _ _ (contF i) x Hx). apply AbsIR_wd; rational. apply AbsIR_wd; apply eq_symmetric_unfolded. cut (Dom (fun_seq_part_sum f m{-}fun_seq_part_sum f N) x). intro H7. Opaque fun_seq_part_sum. apply eq_transitive_unfolded with (Part _ _ H7). simpl in |- *; rational. unfold Frestr in |- *. apply Feq_imp_eq with I. apply Feq_transitive with (FSum N (pred m) f). unfold I in |- *; apply fun_seq_part_sum_n; auto with arith. apply Nat.le_lt_trans with k; [ idtac | apply Nat.lt_le_trans with N ]; auto with arith. apply eq_imp_Feq. unfold I in |- *; apply contin_imp_inc; Contin. simpl in |- *. red in |- *; intros; auto. simpl in |- *. intros. apply Sum_wd; intros; rational. auto. split; simpl in |- *. apply (contin_imp_inc _ _ _ _ (fun_seq_part_sum_cont _ _ _ _ H0 m)); auto. apply (contin_imp_inc _ _ _ _ (fun_seq_part_sum_cont _ _ _ _ H0 N)); auto. simpl in |- *; auto. cut (Dom (FSum N (pred m) g) x). intro H6. apply leEq_wdr with (Part _ _ H6). apply FSum_resp_leEq. rewrite -> (Nat.lt_succ_pred k m); auto; apply Nat.lt_le_trans with N; auto. intros. Opaque FAbs. simpl in |- *. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply FAbs_char with (Hx' := contin_imp_inc _ _ _ _ (contF i) x0 (HxF i)). apply Hk. apply Nat.le_trans with N; auto with arith. simpl in HxF. apply (HxF 0). cut (Dom (fun_seq_part_sum g m{-}fun_seq_part_sum g N) x). intro H7. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (Part _ _ H7). simpl in |- *; rational. apply Feq_imp_eq with I. unfold I in |- *; apply fun_seq_part_sum_n; auto with arith. apply Nat.le_lt_trans with k; [ idtac | apply Nat.lt_le_trans with N ]; auto with arith. auto. split; simpl in |- *. apply (contin_imp_inc _ _ _ _ (fun_seq_part_sum_cont _ _ _ _ contG m)); auto. apply (contin_imp_inc _ _ _ _ (fun_seq_part_sum_cont _ _ _ _ contG N)); auto. simpl in |- *; intro; apply (contin_imp_inc _ _ _ _ (contG n)); auto. Transparent FAbs. simpl in |- *; auto. Opaque FAbs. unfold I in |- *; simpl in |- *; Included. eapply leEq_transitive. apply leEq_AbsIR. apply AbsSmall_imp_AbsIR. apply HN; assumption. elim (convG _ H2). intros N HN; exists (S (Nat.max N k)). cut (N <= Nat.max N k); [ intro | apply Nat.le_max_l ]. cut (k <= Nat.max N k); [ intro | apply Nat.le_max_r ]. split. auto with arith. intros m H5 x H6 Hx Hx'. apply AbsIR_imp_AbsSmall. cut (N <= m); [ intro | apply Nat.le_trans with (Nat.max N k); auto with arith ]. eapply leEq_wdl. Transparent fun_seq_part_sum. simpl in Hx'. apply (HN m _ H7 (le_S _ _ H3) x H6). Opaque fun_seq_part_sum. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series