proposition: Lemma Reste_E_maj : forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste_E x y N) <= maj_Reste_E x y N.
proof: Proof. intros; set (M := Rmax 1 (Rmax (Rabs x) (Rabs y))). assert (HM1 : 1 <= M) by apply RmaxLess1. assert (HMx : Rabs x <= M) by (eapply Rle_trans;[apply RmaxLess1|apply RmaxLess2]). assert (HMy : Rabs y <= M) by (eapply Rle_trans;[apply RmaxLess2|apply RmaxLess2]). pose proof (Rabs_pos x) as HPosAbsx. pose proof (Rabs_pos y) as HPosAbsy. apply Rle_trans with (M ^ (2 * N) * sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => / Rsqr (INR (fact (Nat.div2 (S N))))) (pred (N - k))) (pred N)). - unfold Reste_E. apply Rle_trans with (sum_f_R0 (fun k:nat => Rabs (sum_f_R0 (fun l:nat => / INR (fact (S (l + k))) * x ^ S (l + k) * (/ INR (fact (N - l)) * y ^ (N - l))) ( pred (N - k)))) (pred N)). { apply (Rsum_abs (fun k:nat => sum_f_R0 (fun l:nat => / INR (fact (S (l + k))) * x ^ S (l + k) * (/ INR (fact (N - l)) * y ^ (N - l))) ( pred (N - k))) (pred N)). } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => Rabs (/ INR (fact (S (l + k))) * x ^ S (l + k) * (/ INR (fact (N - l)) * y ^ (N - l)))) ( pred (N - k))) (pred N)). { apply sum_Rle; intros. apply (Rsum_abs (fun l:nat => / INR (fact (S (l + n))) * x ^ S (l + n) * (/ INR (fact (N - l)) * y ^ (N - l)))). } apply Rle_trans with (sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => M ^ (2 * N) * / INR (fact (S l)) * / INR (fact (N - l))) (pred (N - k))) (pred N)). + apply sum_Rle; intros. apply sum_Rle; intros. repeat rewrite Rabs_mult. do 2 rewrite <- RPow_abs. rewrite (Rabs_right (/ INR (fact (S (n0 + n))))). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } rewrite (Rabs_right (/ INR (fact (N - n0)))). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } replace (/ INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * (/ INR (fact (N - n0)) * Rabs y ^ (N - n0))) with (/ INR (fact (N - n0)) * / INR (fact (S (n0 + n))) * Rabs x ^ S (n0 + n) * Rabs y ^ (N - n0)) by ring. rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). repeat rewrite Rmult_assoc. apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply Rle_trans with (/ INR (fact (S n0)) * Rabs x ^ S (n0 + n) * Rabs y ^ (N - n0)). { rewrite (Rmult_comm (/ INR (fact (S (n0 + n))))); rewrite (Rmult_comm (/ INR (fact (S n0)))); repeat rewrite Rmult_assoc; apply Rmult_le_compat_l. { apply pow_le; apply Rabs_pos. } rewrite (Rmult_comm (/ INR (fact (S n0)))); apply Rmult_le_compat_l. { apply pow_le; apply Rabs_pos. } apply Rinv_le_contravar. { apply INR_fact_lt_0. } apply le_INR; apply fact_le; lia. } rewrite (Rmult_comm (M ^ (2 * N))); rewrite Rmult_assoc; apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply Rle_trans with (M ^ S (n0 + n) * Rabs y ^ (N - n0)). { do 2 rewrite <- (Rmult_comm (Rabs y ^ (N - n0))). apply Rmult_le_compat_l. { apply pow_le; apply Rabs_pos. } apply pow_incr; split;lra. } apply Rle_trans with (M ^ S (n0 + n) * M ^ (N - n0)). { apply Rmult_le_compat_l. { apply pow_le; lra. } apply pow_incr; split; lra. } rewrite <- pow_add; replace (S (n0 + n) + (N - n0))%nat with (N + S n)%nat by lia. apply Rle_pow. { assumption. } lia. + rewrite scal_sum. apply sum_Rle; intros. rewrite <- Rmult_comm. rewrite scal_sum. apply sum_Rle; intros. rewrite (Rmult_comm (/ Rsqr (INR (fact (Nat.div2 (S N)))))). rewrite Rmult_assoc; apply Rmult_le_compat_l. { apply pow_le. lra. } assert (H2 := even_odd_cor N). elim H2; intros N0 H3. elim H3; intro. * apply Rle_trans with (/ INR (fact n0) * / INR (fact (N - n0))). { do 2 rewrite <- (Rmult_comm (/ INR (fact (N - n0)))). apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply Rinv_le_contravar. { apply INR_fact_lt_0. } apply le_INR. apply fact_le. apply Nat.le_succ_diag_r. } replace (/ INR (fact n0) * / INR (fact (N - n0))) with (C N n0 / INR (fact N)). 2:{ unfold C, Rdiv. rewrite (Rmult_comm (INR (fact N))). repeat rewrite Rmult_assoc. rewrite Rinv_r. 2:{ apply INR_fact_neq_0. } rewrite Rinv_mult. rewrite Rmult_1_r; ring. } pattern N at 1; rewrite H4. apply Rle_trans with (C N N0 / INR (fact N)). { unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ INR (fact N))). apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } rewrite H4. apply C_maj. lia. } replace (C N N0 / INR (fact N)) with (/ Rsqr (INR (fact N0))). { rewrite H4; rewrite div2_S_double; right; reflexivity. } unfold Rsqr, C, Rdiv. repeat rewrite Rinv_mult. rewrite (Rmult_comm (INR (fact N))). repeat rewrite Rmult_assoc. rewrite Rinv_r. 2:apply INR_fact_neq_0. replace (N - N0)%nat with N0 by lia. ring. * replace (/ INR (fact (S n0)) * / INR (fact (N - n0))) with (C (S N) (S n0) / INR (fact (S N))). 2:{ unfold C, Rdiv. rewrite (Rmult_comm (INR (fact (S N)))). rewrite Rmult_assoc; rewrite Rinv_r. 2:{ apply INR_fact_neq_0. } rewrite Rmult_1_r; rewrite Rinv_mult. reflexivity. } apply Rle_trans with (C (S N) (S N0) / INR (fact (S N))). 2:{ assert (S N = (2 * S N0)%nat) by lia. replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))). { rewrite H5; rewrite div2_double. right; reflexivity. } unfold Rsqr, C, Rdiv. repeat rewrite Rinv_mult. replace (S N - S N0)%nat with (S N0) by lia. rewrite (Rmult_comm (INR (fact (S N)))). repeat rewrite Rmult_assoc. rewrite Rinv_r. 2:apply INR_fact_neq_0. ring. } unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ INR (fact (S N)))). apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } assert (S N = (2 * S N0)%nat) by (rewrite H4; ring). rewrite H5; apply C_maj. lia. - unfold maj_Reste_E. fold M. unfold Rdiv; rewrite (Rmult_comm 4). rewrite Rmult_assoc. apply Rmult_le_compat_l. { apply pow_le. lra. } apply Rle_trans with (sum_f_R0 (fun k:nat => INR (N - k) * / Rsqr (INR (fact (Nat.div2 (S N))))) (pred N)). { apply sum_Rle; intros. rewrite sum_cte. replace (S (pred (N - n))) with (N - n)%nat by lia. right; apply Rmult_comm. } apply Rle_trans with (sum_f_R0 (fun k:nat => INR N * / Rsqr (INR (fact (Nat.div2 (S N))))) (pred N)). { apply sum_Rle; intros. do 2 rewrite <- (Rmult_comm (/ Rsqr (INR (fact (Nat.div2 (S N)))))). apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt. apply INR_fact_neq_0. } apply le_INR. lia. } rewrite sum_cte; replace (S (pred N)) with N by lia. assert (Nat.div2 (S N) = S (Nat.div2 (pred N))). { assert (H0 := even_odd_cor N). elim H0; intros N0 H1. elim H1; intro. - assert (0 < N0)%nat by lia. rewrite H2. rewrite div2_S_double. replace (2 * N0)%nat with (S (S (2 * pred N0))) by lia. replace (pred (S (S (2 * pred N0)))) with (S (2 * pred N0)) by lia. rewrite div2_S_double. lia. - rewrite H2. change (pred (S (2 * N0))) with (2 * N0)%nat. replace (S (S (2 * N0))) with (2 * S N0)%nat by ring. do 2 rewrite div2_double. reflexivity. } rewrite H0. rewrite fact_simpl; rewrite Nat.mul_comm; rewrite mult_INR; rewrite Rsqr_mult. rewrite Rinv_mult. rewrite (Rmult_comm (INR N)); repeat rewrite Rmult_assoc; apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. } rewrite <- H0. assert (INR N <= INR (2 * Nat.div2 (S N))). { assert (H1 := even_odd_cor N). elim H1; intros N0 H2. elim H2; intro. - pattern N at 2; rewrite H3. rewrite div2_S_double. rewrite H3. apply Rle_refl. - pattern N at 2; rewrite H3. replace (S (S (2 * N0))) with (2 * S N0)%nat by lia. rewrite div2_double. apply le_INR. lia. } apply Rmult_le_reg_l with (Rsqr (INR (Nat.div2 (S N)))). { apply Rsqr_pos_lt. apply not_O_INR; red; intro. lia. } repeat rewrite <- Rmult_assoc. rewrite Rinv_r. 2:{ unfold Rsqr; apply prod_neq_R0; apply not_O_INR;lia. } rewrite Rmult_1_l. change 4 with (Rsqr 2). rewrite <- Rsqr_mult. apply Rsqr_incr_1. { change 2 with (INR 2). rewrite Rmult_comm, <- mult_INR; apply H1. } { left; apply lt_INR_0; apply H. } change 2 with (INR 2). rewrite <- mult_INR. apply pos_INR. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra