proposition: Lemma is_series_mult_pos (a b : nat -> R) (la lb : R) : is_series a la -> is_series b lb -> (forall n, 0 <= a n) -> (forall n, 0 <= b n) -> is_series (fun n => sum_f_R0 (fun k => a k * b (n - k)%nat) n) (la * lb).
proof: Proof. move => Hla Hlb Ha Hb. have H0 : forall n, sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => a p * b (k - p)%nat) k) n <= sum_f_R0 a n * sum_f_R0 b n. case => [ | n]. simpl ; apply Rle_refl. rewrite (cauchy_finite a b (S n) (Nat.lt_0_succ n)). apply Rminus_le_0 ; ring_simplify. apply cond_pos_sum => m. apply cond_pos_sum => k. by apply Rmult_le_pos. have H1 : forall n, sum_f_R0 a n * sum_f_R0 b n <= sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => a p * b (k - p)%nat) k) ((2*n)%nat). case => [ /= | n]. by apply Rle_refl. rewrite (cauchy_finite a b (S n) (Nat.lt_0_succ n)). rewrite Rplus_comm ; apply Rle_minus_r. replace (pred (S n)) with n by auto. replace (2 * S n)%nat with (S n + S n)%nat by ring. rewrite -sum_f_rw. rewrite /sum_f. replace (S n + S n - S (S n))%nat with n. elim: {1 5 8}n (Nat.le_refl n) => [ | m IH] Hm ; rewrite /sum_f_R0 -/sum_f_R0. rewrite Nat.sub_0_r Nat.add_0_l ; simpl pred. rewrite -?sum_f_rw_0. replace (sum_f 0 (S (S n)) (fun p : nat => a p * b (S (S n) - p)%nat)) with ((sum_f 0 (S (S n)) (fun p : nat => a p * b (S (S n) - p)%nat) - (fun p : nat => a p * b (S (S n) - p)%nat) 0%nat) + a O * b (S (S n))) by (rewrite Nat.sub_0_r ; ring). rewrite -(sum_f_Sn_m _ O (S (S n))) ; [ | by apply Nat.lt_0_succ]. rewrite sum_f_u_Sk ; [ | by apply Nat.le_0_l]. rewrite sum_f_n_Sm ; [ | by apply Nat.le_0_l]. apply Rle_trans with (sum_f 0 n (fun l0 : nat => a (S (l0 + 0)) * b (S n - l0)%nat) + a (S (S n)) * b (S (S n) - S (S n))%nat + a 0%nat * b (S (S n))). apply Rminus_le_0 ; ring_simplify. apply Rplus_le_le_0_compat ; by apply Rmult_le_pos. repeat apply Rplus_le_compat_r. apply Req_le. rewrite ?sum_f_rw_0. elim: {1 4 6}n (Nat.le_refl n) => [ | k IH] Hk // ; rewrite /sum_f_R0 -/sum_f_R0. rewrite IH ; try by intuition. apply f_equal. by rewrite Nat.add_0_r /=. apply Rplus_le_compat. apply IH ; intuition. rewrite -?sum_f_rw_0. rewrite MyNat.sub_succ_l ; try by intuition. replace (pred (S (n - S m))) with (n - S m)%nat by auto. rewrite plus_Sn_m -?plus_n_Sm. replace (sum_f 0 (S (S (S (m + n)))) (fun p : nat => a p * b (S (S (S (m + n))) - p)%nat)) with (sum_f 1 (S (S (S (m + n)))) (fun p : nat => a p * b (S (S (S (m + n))) - p)%nat) + a O * b (S (S (S (m + n))))). rewrite -(Rplus_0_r (sum_f O _ _)). apply Rplus_le_compat. rewrite (sum_f_chasles _ O (S m) (S (S (S (m + n))))) ; try by intuition. rewrite -(Rplus_0_l (sum_f O _ _)). apply Rplus_le_compat. rewrite /sum_f. elim: (S m - 1)%nat => {IH} [ | k IH] ; rewrite /sum_f_R0 -/sum_f_R0 //. by apply Rmult_le_pos. apply Rplus_le_le_0_compat. by apply IH. by apply Rmult_le_pos. replace (S (S m)) with (1 + S m)%nat by ring. replace (S (S (S (m + n)))) with (S (S n) + S m )%nat by ring. rewrite sum_f_u_add. rewrite (sum_f_chasles _ O (S (n - S m)) (S (S n))) ; try by intuition. rewrite -(Rplus_0_r (sum_f O _ _)). apply Rplus_le_compat. rewrite sum_f_u_Sk. rewrite ?sum_f_rw_0. apply Req_le. elim: (n - S m)%nat => {IH} [ | k IH] ; rewrite /sum_f_R0 -/sum_f_R0 //. apply f_equal2 ; apply f_equal ; intuition. rewrite IH ; apply f_equal, f_equal2 ; apply f_equal. ring. rewrite ?(Nat.add_comm _ (S m)) -MyNat.add_sub_add_l //=. apply Nat.le_0_l. rewrite /sum_f. elim: (S (S n) - S (S (n - S m)))%nat => {IH} [ | k IH] ; rewrite /sum_f_R0 -/sum_f_R0 //. by apply Rmult_le_pos. apply Rplus_le_le_0_compat => // ; by apply Rmult_le_pos. by apply le_n_S, Nat.le_0_l. by apply Rmult_le_pos. rewrite sum_f_Sn_m ?Nat.sub_0_r ; try by intuition. ring. replace (S (S n)) with (S n + 1)%nat. rewrite -MyNat.add_sub_add_l. simpl; apply eq_sym, Nat.sub_0_r. now rewrite Nat.add_comm. elim: n => [ | n IH] //. rewrite -plus_n_Sm plus_Sn_m. apply Nat.lt_succ_r ; intuition. have H2 : forall n, sum_f_R0 a (Nat.div2 n)%nat * sum_f_R0 b (Nat.div2 n)%nat <= sum_f_R0 (fun k : nat => sum_f_R0 (fun p : nat => a p * b (k - p)%nat) k) n. move => n. case: (even_odd_cor n) => k ; case => -> {n}. rewrite div2_double. by apply H1. rewrite div2_S_double. apply Rle_trans with (1 := H1 _). apply Rminus_le_0 ; rewrite -sum_f_rw ; try by intuition. rewrite /sum_f Nat.sub_diag /sum_f_R0 -/sum_f_R0. apply cond_pos_sum => l ; by apply Rmult_le_pos. change (is_lim_seq (sum_n (fun n : nat => sum_f_R0 (fun k : nat => a k * b (n - k)%nat) n)) (Finite (la * lb))). apply is_lim_seq_le_le with (u := fun n => sum_f_R0 a (Nat.div2 n) * sum_f_R0 b (Nat.div2 n)) (w := fun n => sum_f_R0 a n * sum_f_R0 b n). intros n; rewrite sum_n_Reals. by split. replace (Finite (la * lb)) with (Rbar_mult la lb) by auto. suff H : is_lim_seq (fun n : nat => sum_f_R0 a n * sum_f_R0 b n) (Rbar_mult la lb). apply is_lim_seq_spec in H. apply is_lim_seq_spec. move => eps. case: (H eps) => {H} N H. exists (S (2 * N))%nat => n Hn. apply H. apply le_double. apply le_S_n. apply Nat.le_trans with (1 := Hn). destruct (Nat.Even_or_Odd n) as [He | Ho]. - rewrite {1}(MyNat.Even_double n); [| exact He]. now rewrite Nat.double_twice; apply Nat.le_succ_diag_r. - now rewrite {1}(MyNat.Odd_double n); [| exact Ho]; rewrite Nat.double_twice. apply is_lim_seq_mult'. apply filterlim_ext with (2:=Hla); apply sum_n_Reals. apply filterlim_ext with (2:=Hlb); apply sum_n_Reals. apply is_lim_seq_mult'. apply filterlim_ext with (2:=Hla); apply sum_n_Reals. apply filterlim_ext with (2:=Hlb); apply sum_n_Reals. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy