proposition: Lemma reste2_maj : forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste2 x y N) <= Majxy x y N.
proof: Proof. intros. set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). unfold Reste2. apply Rle_trans with (sum_f_R0 (fun k:nat => Rabs (sum_f_R0 (fun l:nat => (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) * x ^ (2 * S (l + k) + 1) * ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) * y ^ (2 * (N - l) + 1)) (pred (N - k)))) ( pred N)). { apply (Rsum_abs (fun k:nat => sum_f_R0 (fun l:nat => (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) * x ^ (2 * S (l + k) + 1) * ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) * y ^ (2 * (N - l) + 1)) (pred (N - k))) ( pred N)). } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => Rabs ((-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) * x ^ (2 * S (l + k) + 1) * ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) * y ^ (2 * (N - l) + 1))) (pred (N - k))) ( pred N)). { apply sum_Rle. intros. apply (Rsum_abs (fun l:nat => (-1) ^ S (l + n) / INR (fact (2 * S (l + n) + 1)) * x ^ (2 * S (l + n) + 1) * ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) * y ^ (2 * (N - l) + 1)) (pred (N - n))). } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => / INR (fact (2 * S (l + k) + 1) * fact (2 * (N - l) + 1)) * C ^ (2 * S (S (N + k)))) (pred (N - k))) ( pred N)). { apply sum_Rle; intros. apply sum_Rle; intros. unfold Rdiv; repeat rewrite Rabs_mult. do 2 rewrite pow_1_abs. do 2 rewrite Rmult_1_l. rewrite (Rabs_right (/ INR (fact (2 * S (n0 + n) + 1)))). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat. apply INR_fact_lt_0. } rewrite (Rabs_right (/ INR (fact (2 * (N - n0) + 1)))). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat. apply INR_fact_lt_0. } rewrite mult_INR. rewrite Rinv_mult. repeat rewrite Rmult_assoc. apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } rewrite <- Rmult_assoc. rewrite <- (Rmult_comm (/ INR (fact (2 * (N - n0) + 1)))). rewrite Rmult_assoc. apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } do 2 rewrite <- RPow_abs. apply Rle_trans with (Rabs x ^ (2 * S (n0 + n) + 1) * C ^ (2 * (N - n0) + 1)). { apply Rmult_le_compat_l. { apply pow_le; apply Rabs_pos. } apply pow_incr. split. { apply Rabs_pos. } unfold C. apply Rle_trans with (Rmax (Rabs x) (Rabs y)); apply RmaxLess2. } apply Rle_trans with (C ^ (2 * S (n0 + n) + 1) * C ^ (2 * (N - n0) + 1)). 2:{ right. replace (2 * S (S (N + n)))%nat with (2 * (N - n0) + 1 + (2 * S (n0 + n) + 1))%nat by lia. repeat rewrite pow_add. ring. } do 2 rewrite <- (Rmult_comm (C ^ (2 * (N - n0) + 1))). apply Rmult_le_compat_l. { apply pow_le. apply Rle_trans with 1. { left; apply Rlt_0_1. } unfold C; apply RmaxLess1. } apply pow_incr. split. { apply Rabs_pos. } unfold C; apply Rle_trans with (Rmax (Rabs x) (Rabs y)). - apply RmaxLess1. - apply RmaxLess2. } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => / INR (fact (2 * S (l + k) + 1) * fact (2 * (N - l) + 1)) * C ^ (4 * S N)) (pred (N - k))) (pred N)). { apply sum_Rle; intros. apply sum_Rle; intros. apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat. rewrite mult_INR; apply Rmult_lt_0_compat; apply INR_fact_lt_0. } apply Rle_pow. { unfold C; apply RmaxLess1. } lia. } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => C ^ (4 * S N) * Rsqr (/ INR (fact (S (S (N + k)))))) (pred (N - k))) (pred N)). { apply sum_Rle; intros. apply sum_Rle; intros. rewrite <- (Rmult_comm (C ^ (4 * S N))). apply Rmult_le_compat_l. { apply pow_le. left; apply Rlt_le_trans with 1. { apply Rlt_0_1. } unfold C; apply RmaxLess1. } replace (/ INR (fact (2 * S (n0 + n) + 1) * fact (2 * (N - n0) + 1))) with (Binomial.C (2 * S (S (N + n))) (2 * S (n0 + n) + 1) / INR (fact (2 * S (S (N + n))))). 2:{ unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. unfold Rdiv; repeat rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ apply INR_fact_neq_0. } rewrite Rmult_1_l. replace (2 * S (S (N + n)) - (2 * S (n0 + n) + 1))%nat with (2 * (N - n0) + 1)%nat by lia. rewrite mult_INR. reflexivity. } apply Rle_trans with (Binomial.C (2 * S (S (N + n))) (S (S (N + n))) / INR (fact (2 * S (S (N + n))))). { unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ INR (fact (2 * S (S (N + n)))))). apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply C_maj. lia. } right. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. unfold Rdiv; repeat rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ apply INR_fact_neq_0. } rewrite Rmult_1_l. replace (2 * S (S (N + n)) - S (S (N + n)))%nat with (S (S (N + n))) by lia. rewrite Rinv_mult. unfold Rsqr; reflexivity. } apply Rle_trans with (sum_f_R0 (fun k:nat => INR N / INR (fact (S (S N))) * C ^ (4 * S N)) (pred N)). { apply sum_Rle; intros. rewrite <- (scal_sum (fun _:nat => C ^ (4 * S N)) (pred (N - n)) (Rsqr (/ INR (fact (S (S (N + n))))))). rewrite sum_cte. rewrite <- Rmult_assoc. do 2 rewrite <- (Rmult_comm (C ^ (4 * S N))). rewrite Rmult_assoc. apply Rmult_le_compat_l. { apply pow_le. left; apply Rlt_le_trans with 1. { apply Rlt_0_1. } unfold C; apply RmaxLess1. } apply Rle_trans with (Rsqr (/ INR (fact (S (S (N + n))))) * INR N). { apply Rmult_le_compat_l. { apply Rle_0_sqr. } apply le_INR. lia. } rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l. { apply pos_INR. } apply Rle_trans with (/ INR (fact (S (S (N + n))))). { pattern (/ INR (fact (S (S (N + n))))) at 2; rewrite <- Rmult_1_r. unfold Rsqr. apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))). { apply INR_fact_lt_0. } rewrite Rinv_r. { rewrite Rmult_1_r. apply (le_INR 1). apply Nat.le_succ_l. apply INR_lt; apply INR_fact_lt_0. } apply INR_fact_neq_0. } apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))). { apply INR_fact_lt_0. } rewrite Rinv_r. 2:{ apply INR_fact_neq_0. } apply Rmult_le_reg_l with (INR (fact (S (S N)))). { apply INR_fact_lt_0. } rewrite Rmult_1_r. rewrite (Rmult_comm (INR (fact (S (S N))))). rewrite Rmult_assoc. rewrite Rinv_l. 2:{ apply INR_fact_neq_0. } rewrite Rmult_1_r. apply le_INR. apply fact_le. lia. } rewrite sum_cte. apply Rle_trans with (C ^ (4 * S N) / INR (fact N)). 2:{ right. unfold Majxy. unfold C. reflexivity. } rewrite <- (Rmult_comm (C ^ (4 * S N))). unfold Rdiv; rewrite Rmult_assoc; apply Rmult_le_compat_l. { apply pow_le. left; apply Rlt_le_trans with 1. { apply Rlt_0_1. } unfold C; apply RmaxLess1. } assert (S (pred N) = N) by lia. rewrite H0. do 2 rewrite fact_simpl. repeat rewrite mult_INR. repeat rewrite Rinv_mult. apply Rle_trans with (INR (S (S N)) * (/ INR (S (S N)) * (/ INR (S N) * / INR (fact N))) * INR N). { repeat rewrite Rmult_assoc. rewrite (Rmult_comm (INR N)). rewrite (Rmult_comm (INR (S (S N)))). apply Rmult_le_compat_l. 2:{ apply le_INR. lia. } repeat apply Rmult_le_pos; left; try apply Rinv_0_lt_compat; try apply INR_fact_lt_0; apply lt_INR_0; try lia. } repeat rewrite <- Rmult_assoc. rewrite Rinv_r. 2:{ apply not_O_INR; discriminate. } rewrite Rmult_1_l. apply Rle_trans with (/ INR (S N) * / INR (fact N) * INR (S N)). { repeat rewrite Rmult_assoc. repeat apply Rmult_le_compat_l. 3:{ apply le_INR; apply Nat.le_succ_diag_r. } 1,2:left; apply Rinv_0_lt_compat. { apply lt_INR_0;lia. } apply INR_fact_lt_0. } rewrite (Rmult_comm (/ INR (S N))). rewrite Rmult_assoc. rewrite Rinv_l. 2:{ apply not_O_INR; discriminate. } rewrite Rmult_1_r; right; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Cos_rel Lia Lra