Library Coqtail.Reals.Rseries.Rseries_usual

Require Import Rsequence.
Require Import Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_cv_facts.

Require Import Fourier Rtactic.

Local Open Scope R_scope.
Local Open Scope Rseq_scope.

Lemma Rser_cv_square_inv : {l | Rser_cv (fun i ⇒ / (Rseq_shift INR i) ^ 2)%R l}.
Proof.
apply Rser_cv_sig_shift_rev.
apply Rser_pos_maj_cv with (/ (Rseq_shift INR × Rseq_shifts INR 2)).
 intro n ; left ; apply Rinv_0_lt_compat, pow_lt, lt_0_INR, lt_O_Sn.
 intro n ; left ; apply Rinv_0_lt_compat, Rmult_lt_0_compat ; apply lt_0_INR, lt_O_Sn.
 intro p ; unfold Rseq_shift, Rseq_shifts, Rseq_mult, Rseq_inv, pow ;
 rewrite Rmult_1_r, Rinv_mult_distr, Rinv_mult_distr ;
 try (now (apply Rgt_not_eq, lt_0_INR, lt_0_Sn)).
 apply Rmult_le_compat ; try (now (left ; apply Rinv_0_lt_compat, lt_0_INR, lt_0_Sn)).
  apply Rle_Rinv ; try (now (apply lt_0_INR, lt_O_Sn)) ; apply le_INR ; apply le_n_Sn.
  reflexivity.
 ∃ 1 ; apply Rseq_cv_eq_compat with (1 - (/ Rseq_shifts INR 2)).
  intro p ; unfold Rseq_minus, Rseq_constant ; induction p.
  unfold Rseq_mult, Rseq_inv, Rseq_shift, Rseq_shifts ; simpl ; field.
  rewrite Rseq_sum_simpl, IHp ; unfold Rseq_constant, Rseq_mult, Rseq_inv,
  Rseq_shifts, Rseq_shift, Rminus ; rewrite Rplus_assoc ; apply Rplus_eq_compat_l.
  simpl ; field ; split ; apply Rgt_not_eq.
  destruct p ; [| assert (H := lt_0_INR _ (lt_0_Sn p))] ; fourier.
  destruct p ; [| assert (H := lt_0_INR _ (lt_0_Sn p))] ; fourier.
  rewrite <- Rminus_0_r ; apply Rseq_cv_minus_compat ; [apply Rseq_constant_cv |].
   apply Rseq_cv_pos_infty_inv_compat ; eapply Rseq_cv_pos_infty_eq_compat ;
   [| eapply Rseq_cv_finite_plus_pos_infty_l ; [eapply (Rseq_poly_cv 1) |
   eexact (Rseq_constant_cv 2)]].
  intro p ; unfold Rseq_shifts, Rseq_poly, Rseq_plus, Rseq_constant, pow ;
   rewrite plus_INR ; simpl ; ring.
  apply lt_O_Sn.
Qed.

Lemma Rser_cv_inv_poly : ∀ d, (2 ≤ d)%nat → {l | Rser_abs_cv (Rseq_inv_poly d) l}.
Proof.
intros d Hd.
unfold Rser_abs_cv.
cut ({l | Rser_cv (Rseq_inv_poly d) l}).
 intros [l Hl]; ∃ l.
 eapply Rser_cv_eq_compat; [|apply Hl]; intro i.
 destruct i; unfold Rseq_abs; symmetry; apply Rabs_right.
  apply Rle_refl.

  unfold Rseq_inv_poly.
  apply Rle_ge; apply pow_le.
  apply Rlt_le; apply Rinv_0_lt_compat; INR_solve.

apply Rser_pos_maj_cv_shift with (fun (i : nat) ⇒ (/ (INR (S i) ^ 2))%R).
 unfold Rseq_inv_poly; intro n; rewrite <- Rinv_pow; [|INR_solve].
 split.
  apply Rlt_le; apply Rinv_0_lt_compat; apply pow_lt; INR_solve.
  apply Rle_Rinv.
   unfold pow; INR_solve; simpl mult; apply lt_O_Sn.
   apply pow_lt; INR_solve.
  apply Rle_pow; auto; INR_solve.
apply Rser_cv_square_inv.
Qed.