proposition: Lemma Rseq_poly_pow_gt_1_little_O : forall d r, r > 1 -> (Rseq_poly d) = o(Rseq_pow r).
proof: Proof. intros d r Hr. pose (npow := (fix F m d := match d with O => 1 | S d => m * F m d end)%nat). assert (Hpow : (forall x y n, pow (x * y) n = pow x n * pow y n)%R). intros x y n; induction n. simpl; rewrite Rmult_1_l; reflexivity. repeat rewrite <- tech_pow_Rmult; rewrite IHn; field. assert (Ho : forall k, Rseq_poly (npow 2%nat k) = o(Rseq_pow r)). induction k; simpl. set (x := (r - 1)%R). assert (Hx : x > 0); [unfold x; lra|]. assert (Hdev : forall n, (2 <= n)%nat -> (1 + x) ^ n >= 1 + INR n * x + (INR n * (INR n - 1)) * /2 * x * x). intros n H; induction H. simpl; right; field. rewrite <- tech_pow_Rmult. eapply Rge_trans. apply Rmult_ge_compat_l; [lra|apply IHle]. repeat rewrite S_INR. field_simplify. unfold Rdiv; apply Rmult_ge_compat_r; [lra|]. assert (HINR : 1 < INR m); [apply lt_1_INR; lia|]. rewrite <- Rplus_0_l. unfold Rminus; repeat rewrite Rplus_assoc. rewrite <- Rplus_assoc. apply Rplus_ge_compat_r. rewrite <- Ropp_mult_distr_r_reverse. rewrite <- Rmult_plus_distr_l. rewrite <- (Rmult_0_l 0). apply Rmult_ge_compat; try lra. apply Rle_ge; apply pow_le; lra. simpl. pattern (INR m) at 3; rewrite <- Rmult_1_r. rewrite <- Ropp_mult_distr_r_reverse. rewrite <- Rmult_plus_distr_l. rewrite <- (Rmult_0_l 0). apply Rmult_ge_compat; try lra. assert (Hmin : forall n, (2 <= n)%nat -> r ^ n > (INR n * (INR n - 1) * / 2 * x * x)). intros n Hd. replace r with (1 + x)%R by (unfold x; field). rewrite <- Rplus_0_l. eapply Rlt_le_trans; [|apply Rge_le; apply Hdev; assumption]. apply Rplus_lt_compat_r. assert (HINR: 0 <= INR n); [apply pos_INR; lia|]. pattern 0; rewrite <- Rplus_0_l. apply Rplus_lt_le_compat; [lra|]. apply Rmult_le_pos; lra. assert (HO : (Rseq_poly 2) = O(fun n => INR n * (INR n - 1) * / 2 * x * x)%R). unfold Rseq_poly. exists (INR 4 * / x * / x)%R; split. apply Rle_ge; rewrite <- (Rmult_0_r 0). rewrite Rmult_assoc. apply Rmult_le_compat; try apply Rle_refl. apply pos_INR. left; apply Rmult_lt_0_compat; apply Rinv_0_lt_compat; assumption. exists 2%nat; intros n Hn. repeat rewrite Rabs_mult. repeat rewrite Rabs_right; try lra. simpl; field_simplify; [|apply Rgt_not_eq; assumption]. replace ((4 * INR n ^ 2 - 4 * INR n) / 2)%R with (INR n * (2 * (INR n - 1)))%R by field. replace (INR n ^ 2 / 1)%R with (INR n * INR n)%R by field. apply Rmult_le_compat_l; [apply pos_INR|]. replace 1%R with (INR 1) by reflexivity. rewrite <- minus_INR; [|lia]. change 2 with (INR 2). rewrite <- 2mult_INR. apply le_INR; lia. replace 1%R with (INR 1) by reflexivity. rewrite <- minus_INR; [apply Rle_ge; apply pos_INR|lia]. apply Rle_ge; apply pos_INR. apply Rle_ge; apply pow_le; apply pos_INR. assert (HO2 : (fun n => INR n * (INR n - 1) * / 2 * x * x)%R = O(Rseq_pow r)). exists 1; split; [lra|]. exists 2%nat; intros n Hn. rewrite Rabs_right; [rewrite Rabs_right|]. left; rewrite Rmult_1_l; apply Hmin; assumption. apply Rle_ge; apply pow_le; lra. apply Rle_ge; left; repeat apply Rmult_lt_0_compat; try lra. apply lt_0_INR; lia. replace 1 with (INR 1) by reflexivity; rewrite <- minus_INR; [|lia]. apply lt_0_INR; lia. eapply Rseq_little_O_big_O_trans. apply (Rseq_poly_little_O 1 2); lia. eapply Rseq_big_O_trans. apply HO. apply HO2. set (kk := npow 2%nat k). rewrite Nat.add_0_r. replace (kk + kk)%nat with (2 * kk)%nat by ring. intros eps Heps. destruct (IHk (/ Rabs (2 ^ kk) * sqrt eps * / sqrt r))%R as [N HN]. repeat apply Rmult_lt_0_compat. apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply pow_nonzero; apply Rgt_not_eq; lra. apply sqrt_lt_R0; lra. apply Rinv_0_lt_compat; apply sqrt_lt_R0; lra. exists (2 * N)%nat; intros n Hn. unfold Rseq_poly; unfold Rseq_pow. pose (m := match Nat.Even_Odd_dec n with | left evn => proj1_sig (even_2n n evn) | right odd => S (proj1_sig (odd_S2n n odd)) end). assert (Hm : (n <= 2 * m /\ 2 * m <= S n)%nat). destruct (Nat.Even_Odd_dec n) as [Hm|Hm]; [destruct (even_2n n Hm) as [p Hp]|destruct (odd_S2n n Hm) as [p Hp]]; simpl in m; unfold Nat.double in Hp; unfold m; lia. destruct Hm as [Hml Hmr]. apply Rle_trans with (Rabs (INR (2 * m) ^ (2 * kk))). repeat rewrite Rabs_right. apply pow_incr; split; [apply pos_INR|apply le_INR; assumption]. apply Rle_ge; apply pow_le; apply pos_INR. apply Rle_ge; apply pow_le; apply pos_INR. rewrite pow_Rsqr; rewrite mult_INR. unfold Rsqr; repeat rewrite Hpow; repeat rewrite Rabs_mult; simpl. eapply Rle_trans. apply Rmult_le_compat. replace 0 with (0 * 0)%R by field; apply Rmult_le_compat; (apply Rle_refl || apply Rabs_pos). replace 0 with (0 * 0)%R by field; apply Rmult_le_compat; (apply Rle_refl || apply Rabs_pos). change (1 + 1) with 2. apply Rmult_le_compat_l; [apply Rabs_pos|]; apply HN; lia. apply Rmult_le_compat_l; [apply Rabs_pos|]; apply HN; lia. unfold Rseq_pow. change (1 + 1) with 2. field_simplify. simpl; unfold Rdiv; repeat rewrite Rinv_1; repeat rewrite Rmult_1_r. rewrite sqrt_sqrt; [|lra]. rewrite sqrt_sqrt; [|lra]. rewrite Rmult_assoc. apply Rmult_le_compat_l; [lra|]. pattern (/ r)%R at 1; rewrite <- Rabs_right; [|left; apply Rinv_0_lt_compat; lra]. repeat rewrite <- Rabs_mult. rewrite <- pow_add. repeat rewrite Rabs_right. apply (Rmult_le_reg_l r); [lra|]. field_simplify. unfold Rdiv; repeat rewrite Rinv_1; repeat rewrite Rmult_1_r. rewrite tech_pow_Rmult. apply Rle_pow; [lra|]. replace (m + m)%nat with (2 * m)%nat by ring; assumption. apply Rgt_not_eq; lra. apply Rle_ge; apply pow_le; lra. replace 0 with (0 * 0)%R by field. apply Rmult_ge_compat; try lra. left; apply pow_lt; lra. left; apply Rinv_0_lt_compat; lra. split; apply Rgt_not_eq. apply sqrt_lt_R0; lra. apply Rabs_pos_lt; apply pow_nonzero; apply Rgt_not_eq; lra. assert (Hp : (forall n, exists p, n < npow 2 p)%nat). intros n. destruct (zerop n) as [H|H]. exists 0%nat; simpl; lia. induction H. exists 1%nat; simpl; lia. destruct IHle as [p Hp]. exists (S p); simpl; lia. destruct (Hp d) as [dm Hdm]. apply Rseq_little_O_trans with (Rseq_poly (npow 2 dm)%nat). apply Rseq_poly_little_O; assumption. apply Ho. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra