proposition: Lemma reste1_maj : forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste1 x y N) <= Majxy x y (pred N).
proof: Proof. intros. set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). unfold Reste1. 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))) * x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) * y ^ (2 * (N - l))) (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))) * x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) * y ^ (2 * (N - l))) (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))) * x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) * y ^ (2 * (N - l)))) (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))) * x ^ (2 * S (l + n)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) * y ^ (2 * (N - l))) (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)) * fact (2 * (N - l))) * C ^ (2 * 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))))). 2:apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. rewrite (Rabs_right (/ INR (fact (2 * (N - n0))))). 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))))). 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)) * C ^ (2 * (N - n0))). { 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)) * C ^ (2 * (N - n0))). { do 2 rewrite <- (Rmult_comm (C ^ (2 * (N - n0)))). 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. } right. replace (2 * S (N + n))%nat with (2 * (N - n0) + 2 * S (n0 + n))%nat by lia. rewrite pow_add. apply Rmult_comm. } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => / INR (fact (2 * S (l + k)) * fact (2 * (N - l))) * C ^ (4 * 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 * N) * Rsqr (/ INR (fact (S (N + k))))) (pred (N - k))) (pred N)). { apply sum_Rle; intros. apply sum_Rle; intros. rewrite <- (Rmult_comm (C ^ (4 * 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)) * fact (2 * (N - n0)))) with (Binomial.C (2 * S (N + n)) (2 * S (n0 + n)) / INR (fact (2 * S (N + n)))). 2:{ unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. unfold Rdiv; repeat rewrite <- Rmult_assoc. rewrite Rinv_l. { rewrite Rmult_1_l. replace (2 * S (N + n) - 2 * S (n0 + n))%nat with (2 * (N - n0))%nat by lia. rewrite mult_INR. reflexivity. } apply INR_fact_neq_0. } apply Rle_trans with (Binomial.C (2 * S (N + n)) (S (N + n)) / INR (fact (2 * S (N + n)))). { unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ INR (fact (2 * 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 (N + n) - S (N + n))%nat with (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 N)) * C ^ (4 * N)) (pred N)). { apply sum_Rle; intros. rewrite <- (scal_sum (fun _:nat => C ^ (4 * N)) (pred (N - n)) (Rsqr (/ INR (fact (S (N + n)))))). rewrite sum_cte. rewrite <- Rmult_assoc. do 2 rewrite <- (Rmult_comm (C ^ (4 * 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 (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 (N + n)))). { pattern (/ INR (fact (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 (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 (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 N))). { apply INR_fact_lt_0. } rewrite Rmult_1_r. rewrite (Rmult_comm (INR (fact (S N)))). rewrite Rmult_assoc. rewrite Rinv_l. 2:apply INR_fact_neq_0. rewrite Rmult_1_r. apply le_INR. apply fact_le. apply -> Nat.succ_le_mono. apply Nat.le_add_r. } rewrite sum_cte. apply Rle_trans with (C ^ (4 * N) / INR (fact (pred N))). 2:{ right. unfold Majxy. unfold C. replace (S (pred N)) with N by lia. reflexivity. } rewrite <- (Rmult_comm (C ^ (4 * 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. pattern N at 2; rewrite <- H0. do 2 rewrite fact_simpl. rewrite H0. repeat rewrite mult_INR. repeat rewrite Rinv_mult. rewrite (Rmult_comm (/ INR (S N))). repeat rewrite <- Rmult_assoc. rewrite Rinv_r. 2:apply not_O_INR;lia. rewrite Rmult_1_l. pattern (/ INR (fact (pred N))) at 2; rewrite <- Rmult_1_r. rewrite Rmult_assoc. apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply Rmult_le_reg_l with (INR (S N)). { apply lt_INR_0; apply Nat.lt_0_succ. } rewrite <- Rmult_assoc; rewrite Rinv_r. { rewrite Rmult_1_r; rewrite Rmult_1_l. apply le_INR; apply Nat.le_succ_diag_r. } apply not_O_INR; discriminate. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Cos_rel Lia Lra