proposition: Lemma Vn_maj : Vn = O(Qn 2).
proof: Proof. eapply Rseq_big_O_asymptotic. intros; eassumption. exists 1%nat. eapply Rseq_big_O_eq_compat with (Un := fun n => (INR (1 + n) + / 2) * Sn (1 + n) + / 12 * Qn 2 (1 + n) + / 6 * Qn 3 (1 + n)). intros n ; unfold Rseq_shifts. set (p := (1 + n)%nat). assert (Hp : INR p <> 0). unfold p. replace (1 + n)%nat with (S n) by auto. auto with real. rewrite Vn_simpl; [|unfold p; lia]. replace (ln (1 + / INR p)) with (Sn p + Rn p). repeat (rewrite Qn_S; [|unfold p; lia]). unfold Rn. field; assumption. unfold Sn, Rn; field; assumption. apply Rseq_eq_refl. repeat apply Rseq_big_O_plus_compat_l. eapply Rseq_big_O_eq_compat with (Vn := fun n => INR (1 + n) * Qn 3 (1 + n)) (Un := fun n => (INR (1 + n) + / 2) * Sn (1 + n)). reflexivity. intros n; unfold Rseq_shifts ; repeat (rewrite Qn_S; [|lia]). rewrite <- tech_pow_Rmult. field; replace (1 + n)%nat with (S n) by auto; auto with real. apply Rseq_big_O_mult_compat. exists 2; split; [lra|]. exists 0%nat; intros n Hn. assert (Hle : 1 <= INR (1 + n)). replace (1 + n)%nat with (S n) by auto. rewrite S_INR. assert (H := pos_INR n); lra. rewrite Rabs_right; [|lra]. rewrite Rabs_right; [|lra]. lra. destruct ln_taylor_3 as [K [HK [N HN]]]. exists K; split; [assumption|]. exists (S N); intros n Hn. eapply Rle_trans. apply HN; lia. apply Rmult_le_compat_l; [lra|]. assert (Hle : 1 <= INR (1 + n)). replace (1 + n)%nat with (S n) by auto. rewrite S_INR. assert (H := pos_INR n); lra. assert (Qn 4 (1 + n) = Qn 1 (1 + n) * Qn 3 (1 + n)) as ->; swap 1 2. rewrite Rabs_mult. rewrite <- Rmult_1_l. apply Rmult_le_compat_r; [apply Rabs_pos|]. rewrite Qn_S; [|lia]; rewrite pow_1. rewrite Rabs_right; [|left; apply Rinv_0_lt_compat; lra]. apply (Rmult_le_reg_l (INR (1 + n))); [lra|]. rewrite Rinv_r; [|intros Hc; lra]. rewrite Rmult_1_r; assumption. repeat (rewrite Qn_S; [|lia]). repeat rewrite <- tech_pow_Rmult. field; intros Hc; lra. apply Rseq_big_O_Rmult_compat_l; apply Rseq_big_O_refl. apply Rseq_big_O_Rmult_compat_l. exists 1; split; [lra|]. exists 0%nat; intros n _ ; unfold Rseq_shifts. rewrite Rmult_1_l. assert (HINR : 0 < INR (1 + n)). replace (1 + n)%nat with (S n) by lia. rewrite S_INR; assert (H := pos_INR n); lra. repeat (rewrite Qn_S; [|lia]). rewrite Rabs_right; [|apply Rle_ge; apply pow_le; auto with real]. rewrite Rabs_right; [|apply Rle_ge; apply pow_le; auto with real]. repeat rewrite <- tech_pow_Rmult; rewrite pow_O. repeat apply Rmult_le_compat_l; auto with real. rewrite Rmult_1_r. apply (Rmult_le_reg_l (INR (1 + n))); auto. rewrite Rinv_r; [|auto with stirling]. rewrite Rmult_1_r. replace (1 + n)%nat with (S n) by auto. rewrite S_INR. assert (H := pos_INR n); lra. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis