Library Coqtail.Reals.Rzeta2


Require Import Reals.
Require Import Fourier.
Require Import Rsequence_facts.
Require Export Rseries.
Require Import Rsequence_subsequence.
Require Import Rtactic.

Open Scope R_scope.


Lemma plus_1_S : a, INR (S a) = 1 + (INR a).
Proof.
intros.
INR_solve.
Qed.

Convergence of the 1/n² series


Definition Rseq_square_inv n := / (INR n) ^ 2.
Definition Rseq_square_inv_s n := / (INR (S n)) ^ 2.

Splitting series in odd and even terms


Definition odds Un : Rseq := fun nUn (S (2 × n)).
Definition evens Un : Rseq := fun nUn (mult 2 n).

Convergence of splitting
Lemma Rser_cv_pair_compat : Un l, Rser_cv Un lRser_cv (fun nUn (mult 2 n) + Un (S (mult 2 n))) l.
Proof.
intros Un l Ucv.
intros e epos.
destruct (Ucv e epos) as [N Hu].
N; intros n nN.
replace (Rseq_sum (fun n0 : natUn (2 × n0)%nat + Un (S (2 × n0))) n)
 with (Rseq_sum Un (S (2 × n))).
 intros; apply Hu; omega.

 clear nN.
 induction n.
  intros; simpl; ring.

  simpl Rseq_sum.
  replace (n + S (n + 0))%nat with (S (2 × n)) by ring.
  rewrite IHn.
  ring_simplify.
  assert (SIMPL : a b c d, a = ca + b + d = b + d + c) by (intros; subst; ring).
  apply SIMPL.
  apply Rseq_sum_ext; intro.
  simpl; trivial.
Qed.

Finite sum splitting

Lemma sum_odd_even_split : an n, sum_f_R0 (odds an) n =
  sum_f_R0 an (S (2 × n)) - sum_f_R0 (evens an) n.
Proof.
intros an n.
induction n.
 simpl; unfold odds, evens; simpl; ring.

 simpl.
 rewrite IHn.
 replace (n + S (n + 0))%nat with (S (2 × n)) by ring.
 unfold odds, evens.
 simpl.
 replace (S (S (n + S (n + 0)))) with (S (2 × S n)) by ring.
 replace (S (S (n + (n + 0)))) with (2 × S n)%nat by ring.
 replace (S (n + S (n + 0))) with (2 × S n)%nat by ring.
 ring.
Qed.

Substracting odd terms

Lemma remove_odds : Un l, {lu | Rser_cv Un lu}
  Rser_cv (evens Un) lRser_cv (Un - (odds Un)) l.
Proof.
intros Un lo [lu Hu] Ho.
replace lo with (lu - (lu - lo)) by ring.
apply Rser_cv_minus_compat; try assumption.
apply Rseq_cv_eq_compat with ((fun nsum_f_R0 Un (S (2 × n))) - sum_f_R0 (evens Un))%Rseq.
 intro n; rewrite (sum_odd_even_split); trivial.
 apply Rseq_cv_minus_compat.

 eapply Rseq_subseq_cv_compat; [|apply Hu].
  assert (Hex : is_extractor (fun iS (2 × i))).
    intros n; omega.
   (exist _ _ Hex).
  reflexivity.
  assumption.
Qed.

Substracting even terms

Lemma remove_evens : Un l, {lu | Rser_cv Un lu}
  Rser_cv (odds Un) lRser_cv (Un - evens Un) l.
Proof.
intros Un lo [lu Hu] Ho.
replace lo with (lu - (lu - lo)) by ring.
apply Rser_cv_minus_compat; try assumption.
apply Rseq_cv_eq_compat with ((fun nsum_f_R0 Un (S (2 × n))) - sum_f_R0 (odds Un))%Rseq.
 intro n. symmetry.
 assert (REW : a b c, a - b = ca - c = b) by (intros; subst; ring); apply REW.
 rewrite (sum_odd_even_split); trivial.

 apply Rseq_cv_minus_compat.
  eapply Rseq_subseq_cv_compat; [|apply Hu].
   assert (Hex : is_extractor (fun iS (2 × i))).
     intros n; omega.
    (exist _ _ Hex).

   reflexivity.

  assumption.
Qed.

Introduction of pi


Definition antg : natR := fun n(- 1)^n / (2 × (INR n) + 1).
Definition antg_neg : natR := fun n(- 1)^n / (- 2 × (INR n) + 1).

Lemma Sum_antg : Rser_cv antg (PI / 4).
Proof.
unfold Rser_cv.
eapply Rseq_cv_eq_compat with (sum_f_R0 (tg_alt PI_tg)).
 apply Rseq_sum_ext.
 intros n.
 unfold tg_alt, PI_tg, antg.
 INR_group (2 × INR n + 1).
 field.
 INR_solve.

 unfold PI.
 destruct exist_PI as [pi H].
 replace (4 × pi / 4) with pi by field.
 apply H || admit.
Qed.

Lemma antg_shift_neg_compat : Rseq_shift antg_neg == antg.
Proof.
intro n.
unfold Rseq_shift.
unfold antg.
unfold antg_neg.
rewrite S_INR.
simpl pow.
field; split;
 replace 2 with (INR 2) by reflexivity;
 replace 1 with (INR 1) by reflexivity.
 INR_solve.

 intro Hinv.
 rewrite Ropp_mult_distr_l_reverse in Hinv.
 pose proof (Rplus_opp_r_uniq _ _ Hinv) as H.
 rewrite Ropp_involutive in H.
 rewrite <- plus_INR in H.
 rewrite <- mult_INR in H.
 generalize dependent H.
 apply not_INR.
 omega.
Qed.

Lemma Sum_antg_neg : Rser_cv antg_neg (PI / 4 + 1).
Proof.
 apply Rser_cv_shift_rev2.
 eapply Rser_cv_ext.
 apply antg_shift_neg_compat.
 replace (PI / 4 + 1 - antg_neg 0) with (PI / 4) by (compute; field).
 apply Sum_antg.
Qed.

Definition bntg n := / (2 × (INR n) + 1) ^ 2.
Definition bntg_neg n := / (- 2 × (INR n) + 1) ^ 2.

Lemma bntg_pos : n, 0 < bntg n.
Proof.
intro n.
unfold bntg.
INR_solve.
Qed.

Lemma odd_not_zero : n, 2 × (INR n) + 1 0.
Proof.
intros.
INR_solve.
Qed.

Lemma neg_odd_not_zero : n, 2 × (INR n) - 1 0.
Proof.
intros.
destruct n.
 simpl.
 replace (2 × 0 - 1) with (- 1) by field.
  apply Ropp_neq_0_compat; apply R1_neq_R0.
  INR_solve.
Qed.

Lemma bntg_neg_simpl : n,
  1 / (- 2 × (INR n) + 1) ^ 2 = 1 / (2 × (INR n) - 1) ^ 2.
Proof.
intros; field.
split.
 apply neg_odd_not_zero.
 replace (-2 × INR n + 1) with (- (2 × (INR n) - 1)) by field.
 apply Ropp_neq_0_compat; apply neg_odd_not_zero.
Qed.

Definition pi_tg2 (n : nat) := 2 / ((4 × (INR n) + 1) × (4 × (INR n) + 3)).

Lemma pi_tg2_corresp : n,
  pi_tg2 n = tg_alt PI_tg (2 × n) + tg_alt PI_tg (S (2 × n)).
Proof.
intros.
unfold tg_alt, PI_tg, pi_tg2.
rewrite pow_1_odd.
rewrite pow_1_even.
assert (R1 : INR ((2 × (2 × n) + 1)%nat) = 2 × (2 × (INR n)) + 1) by INR_solve.
assert (R2 : INR ((2 × S (2 × n) + 1)%nat) = 2 × (1 + (2 × (INR n))) + 1) by INR_solve.
rewrite R1.
rewrite R2.
field.
split;
 [replace (1 + 2 × (INR n)) with (INR (1 + 2 × n)); [apply (odd_not_zero) | rewrite plus_INR]
 |replace (2 × (INR n)) with (INR (2 × n)); [apply odd_not_zero | ]];
 rewrite mult_INR; trivial.
Qed.

Lemma pi_tg2_cv : { l | Rser_cv pi_tg2 l }.
Proof.
destruct (exist_PI) as [PI_4 Hc].
PI_4.
apply Rser_cv_ext with (fun ntg_alt PI_tg (2 × n) + tg_alt PI_tg (S (2 × n))).
 intro n; apply pi_tg2_corresp.

 apply Rser_cv_pair_compat.
 intros eps epspos.

 destruct (Hc eps epspos) as [N H].
  N.
 intros n nN.
 apply (H n nN).
Qed.

Lemma Rser_cv_bntg : {l | Rser_cv bntg l}.
Proof.
eapply Rser_pos_maj_cv.
 intro; apply Rlt_le; apply bntg_pos.

 3: apply Rser_cv_square_inv.

 intro; apply Rlt_le; apply Rinv_0_lt_compat; apply pow_lt; INR_solve.

 intro n; apply Rle_Rinv; unfold Rseq_shift ; try (apply pow_lt; INR_solve).
 unfold pow; INR_solve.
 apply mult_le_compat; omega.
Qed.

Sums indexed by relative integers (from -N to N)


Require Import ZArith.

Fixpoint bisum (f : ZR) (N : nat) := match N with
  | Of Z0
  | S n(bisum f n) + f (Z_of_nat N) + f (- Z_of_nat N)%Z
end.

  • 1 to a relative integer Z

Definition pow1_P p := match p with xO _ ⇒ 1 | _ ⇒ -1 end.

Definition pow1 z := match z with
  | Z0 ⇒ 1
  | Zpos n | Zneg npow1_P n
end.

Lemma pow1_P_ind : p, pow1_P (Psucc (Psucc p)) = pow1_P p.
Proof.
destruct p; trivial.
Qed.

Lemma nat_ind2 : (P : natProp),
  P OP (S O) → ( m, P mP (S (S m))) → n, P n.
Proof.
intros P H0 H1 H n.
assert (P n P (S n)).
 induction n; split; try assumption; [ | apply H]; apply IHn.
 apply H2.
Qed.

Lemma pow1_nat : n, pow1 (Z_of_nat n) = (- 1) ^ n.
Proof.
intros n.
destruct n.
 trivial.
 unfold Z_of_nat.
 simpl pow1.
 generalize dependent n; apply nat_ind2; try (simpl; trivial; ring).
 intros n H; simpl.
 rewrite pow1_P_ind.
 rewrite H.
 simpl pow; field.
Qed.

Lemma pow1_nat_neg : n, pow1 (- Z_of_nat n) = (- 1) ^ n.
Proof.
intros n.
destruct n.
 trivial.
 unfold Z_of_nat.
 simpl pow1.
 generalize dependent n; apply nat_ind2; try (simpl; trivial; ring).
 intros n H; simpl.
 rewrite pow1_P_ind.
 rewrite H.
 simpl pow; field.
Qed.

Lemma pow1_squared : z, (pow1 z) ^ 2 = 1.
Proof.
destruct z; [simpl; ring | | ]; unfold pow1;
  destruct p;
    simpl; ring.
Qed.

Lemma pow1_Rabs : z, Rabs (pow1 z) = 1.
Proof.
destruct z; try destruct p; simpl; try rewrite Rabs_Ropp; apply Rabs_R1.
Qed.

Lemma pow1_P_plus : a b, pow1_P (a + b) = pow1_P a × pow1_P b.
Proof.
intros a b.
destruct a; destruct b; simpl; ring.
Qed.

Lemma pow1_succ : z, pow1 (Zsucc z) = - pow1 z.
Proof.
destruct z; trivial;
 destruct p; simpl; try ring;
 destruct p; simpl; ring.
Qed.

Lemma pow1_plus_nat : a b, pow1 (a + Z_of_nat b) = (pow1 a) × (-1) ^ b.
Proof.
intros.
induction b.
 simpl; ring_simplify; inject; omega.

 rewrite inj_S; rewrite <- Zplus_succ_r_reverse; rewrite pow1_succ.
 rewrite IHb.
 simpl; ring.
Qed.

Operations on bisums

Definition zr (op : RR) (f : ZR) z := op (f z).
Definition zr2 (op : RRR) (f g : ZR) z := op (f z) (g z).
Definition zr22 (op : RRR) (f g : ZZR) x y := op (f x y) (g x y).

Lemma bisum_eq_compat : f g n, ( z, f z = g z) → bisum f n = bisum g n.
Proof.
intros.
induction n.
 simpl; apply H.

 simpl; do 2 rewrite H.
 rewrite IHn; trivial.
Qed.

Lemma bisum_plus : f g n, bisum (zr2 Rplus f g) n = bisum f n + bisum g n.
Proof.
induction n.
 trivial.

 simpl bisum; rewrite IHn.
 unfold zr2; ring.
Qed.

Lemma bisum_minus : f g n, bisum (zr2 Rminus f g) n = bisum f n - bisum g n.
Proof.
induction n.
 trivial.

 simpl bisum; rewrite IHn.
 unfold zr2; ring.
Qed.

Lemma bisum_scal_mult : f a n, bisum (zr (Rmult a) f) n = a × (bisum f n).
Proof.
induction n.
 trivial.

 simpl bisum; rewrite IHn.
 unfold zr; ring.
Qed.

Lemma bisum_mult : f g n m, (bisum f n) × (bisum g m) =
  bisum (fun ibisum (fun jf i × g j) m) n.
Proof.
induction n.
 simpl; intro.
 replace (fun j : Zf 0%Z × g j) with (zr (Rmult (f 0%Z)) g) by trivial.
 rewrite bisum_scal_mult; trivial.

 intros m.
 simpl bisum.
 repeat rewrite Rmult_plus_distr_r.
 rewrite IHn.
 replace (fun j : Zf (Zpos (P_of_succ_nat n)) × g j) with (zr (Rmult (f (Zpos (P_of_succ_nat n)))) g) by trivial.
 replace (fun j : Zf (Zneg (P_of_succ_nat n)) × g j) with (zr (Rmult (f (Zneg (P_of_succ_nat n)))) g) by trivial.
 repeat rewrite bisum_scal_mult.
 trivial.
Qed.

Reversing terms

Lemma bisum_reverse : f n, bisum f n = bisum (fun if (- i)%Z) n.
Proof.
induction n.
 trivial.

 simpl.
 rewrite IHn.
 ring.
Qed.

Rewriting a bisum as sums

Lemma sum_bisum : n f, bisum f (S n) =
  sum_f_R0 (fun if (Z_of_nat i)) (S n) + sum_f_R0 (fun if (- Z_of_nat (S i))%Z) n.
Proof.
intros.
induction n.
 trivial.

 replace (bisum f (S (S n))) with (bisum f (S n) + f (Zpos (Psucc (P_of_succ_nat n))) +
   f (Zneg (Psucc (P_of_succ_nat n)))) by trivial.
 rewrite IHn.
 simpl.
 ring.
Qed.

Introducing pi to bisums


Definition anz z := (pow1 z) / (2 × (IZR z) + 1).
Definition bnz z := / (2 × (IZR z) + 1) ^ 2.
Definition An := bisum anz.
Definition Bn := bisum bnz.

Lemma anz_antg : n, antg n = anz (Z_of_nat n).
Proof.
intro n.
unfold antg, anz.
destruct n.
 simpl; field.

 rewrite pow1_nat.
 rewrite <- INR_IZR_INZ.
 trivial.
Qed.

Lemma anz_antg_neg : n, antg_neg n = anz (- Z_of_nat n).
Proof.
intro n.
unfold antg_neg, anz.
destruct n.
 simpl; field.

 rewrite pow1_nat_neg.
 rewrite Ropp_Ropp_IZR.
 rewrite <- INR_IZR_INZ.
 field.
 rewrite plus_1_S.
 replace (2 × - (1 + INR n) + 1) with (- (1 + 2 × INR n)) by ring.
 apply Ropp_neq_0_compat.
 repeat INR_solve.
Qed.

Lemma bisum_anz_antg : (sum_f_R0 antg + (sum_f_R0 antg_neg - 1))%Rseq == bisum anz.
Proof.
intro n.
induction n.
 compute; field.

 simpl bisum.
 rewrite <- IHn.
 unfold Rseq_minus.
 unfold Rseq_plus.
 unfold Rseq_constant.
 repeat rewrite tech5.
 repeat rewrite anz_antg_neg.
 repeat rewrite anz_antg.
 replace (Zneg (P_of_succ_nat n)) with (- Z_of_nat (S n))%Z by trivial.
 replace (Zpos (P_of_succ_nat n)) with (Z_of_nat (S n))%Z by trivial.
 ring.
Qed.

Lemma An_cv : Rseq_cv An (PI / 2).
Proof.
replace (PI / 2) with (PI / 4 + (PI / 4 + 1 - 1)) by field.
eapply Rseq_cv_eq_compat.
 2: apply Rseq_cv_plus_compat.
 2: apply Sum_antg.

 2: eapply Rseq_cv_eq_compat.
  3: apply Rseq_cv_minus_compat.
   3: apply Sum_antg_neg.
   3: apply Rseq_constant_cv.
 symmetry. apply bisum_anz_antg.
 intro; trivial.
Qed.

Lemma An_squared_cv : Rseq_cv (An × An) (PI ^ 2 / 4).
Proof.
replace (PI ^ 2 / 4) with ((PI / 2) × (PI / 2)) by field.
apply Rseq_cv_mult_compat; apply An_cv.
Qed.

Double sums


Definition bisumsum f N := bisum (fun i ⇒ (bisum (f i) N)) N.

Double sum minus its diagonal

Definition bisum_strip f j N := bisum f N - (f j).
Definition bisumsum_strip_diag f N := bisumsum f N - bisum (fun i ⇒ (f i i)) N.

Double sum in which its diagonal terms are null

Definition bisum_strip' f j N := bisum (fun iif Z_eq_dec i j then 0 else f i) N.
Definition bisumsum_strip_diag' f N := bisumsum (fun i jif Z_eq_dec i j then 0 else f i j) N.

Weak extensional equality

Lemma bisumsum_eq_compat : f g n, ( x y, f x y = g x y) →
  bisumsum f n = bisumsum g n.
Proof.
intros; apply bisum_eq_compat.
intros; apply bisum_eq_compat.
apply H.
Qed.

Bounded extensional equality

Lemma bisum_eq_compat_bounded : f g n, ( z, ((-Z_of_nat n) z Z_of_nat n)%Zf z = g z) →
  bisum f n = bisum g n.
Proof.
intros.
induction n.
 simpl; apply H; simpl; omega.

 simpl.
 rewrite H; [ | simpl; split; [apply Zle_neg_pos | omega]].
 rewrite H; [ | simpl; split; [omega | apply Zle_neg_pos]].
 rewrite IHn.
  trivial.

  intros z [H1 H2].
  apply H; split; eapply Zle_trans; [ | apply H1 | apply H2 | ]; rewrite inj_S; omega.
Qed.

Double sum distributivity

Lemma bisumsum_square : f n, bisumsum (fun i jf i × f j) n = bisum f n × bisum f n.
Proof.
intros.
rewrite bisum_mult.
trivial.
Qed.

Inequalities

Lemma Psucc_lt : p, (Zpos p < Zpos (Psucc p))%Z.
Proof.
intros.
replace (Zpos (Psucc p)) with (1 + Zpos p)%Z.
 omega.
 induction p; trivial.
Qed.

Lemma Psucc_lt_neg : p, (Zneg (Psucc p) < Zneg p)%Z.
Proof.
intros.
replace (Zneg (Psucc p)) with (- 1 + Zneg p)%Z.
 omega.
 induction p; trivial.
Qed.

A special term outside the bounds can be ignored

Lemma bisum_not_in : f g j n, (j < (- Z_of_nat n) Z_of_nat n < j)%Z
  bisum (fun i : Zif Z_eq_dec i j then g j else f i) n = bisum f n.
Proof.
intros.
apply bisum_eq_compat_bounded; intros.
destruct H.
 destruct (Z_eq_dec z (- Z_of_nat (S n))).
  subst; destruct H0; rewrite inj_S in × |-; apply False_ind; omega.
  destruct (Z_eq_dec z j).
   subst; apply False_ind; omega.
   trivial.
 destruct (Z_eq_dec z (Z_of_nat (S n))).
  subst; destruct H0; rewrite inj_S in × |-; apply False_ind; omega.
  destruct (Z_eq_dec z j).
   subst; apply False_ind; omega.
   trivial.
Qed.

A special term between the bounds can be extracted

Lemma bisum_in : f g j n, (- Z_of_nat n j Z_of_nat n)%Z
  bisum (fun i : Zif Z_eq_dec i j then g j else f i) n = bisum f n - f j + g j.
Proof.
intros.
induction n.
 assert (j = Z0) by (replace (Z_of_nat O) with Z0 in H by trivial; omega); subst; trivial.
 simpl; ring.

 set (h := fun iif Z_eq_dec i j then g j else f i).
 simpl bisum; unfold h in ×.
 destruct (Z_eq_dec (Zpos (P_of_succ_nat n)) j) as [e|e];
 destruct (Z_eq_dec (Zneg (P_of_succ_nat n)) j) as [e'|e']; subst; try inversion e'.
  rewrite bisum_not_in.
   ring.
   right; destruct n; simpl.
    omega.
    apply Psucc_lt.

  rewrite bisum_not_in.
   ring.
   left; destruct n; simpl.
    omega.
    apply Psucc_lt_neg.

  rewrite IHn.
   ring.
   split; rewrite inj_S in H.
    destruct (Z_le_gt_dec (- Z_of_nat n) j); trivial.
    replace (Zneg (P_of_succ_nat n)) with (- Z_of_nat (S n))%Z in e' by trivial.
    rewrite inj_S in ×.
    omega.

    destruct (Z_le_gt_dec j (Z_of_nat n)); trivial.
    replace (Zpos (P_of_succ_nat n)) with (Z_of_nat (S n))%Z in e by trivial.
    rewrite inj_S in ×.
    omega.
Qed.

Stripping terms

Definition Zzero : ZR := fun _ ⇒ 0.

Lemma bisum_strip_equiv : f n j, ((- Z_of_nat n) j Z_of_nat n)%Z
  bisum_strip f j n = bisum_strip' f j n.
Proof.
intros.
unfold bisum_strip, bisum_strip'.

replace
  (bisum (fun i : Zif Z_eq_dec i j then 0 else f i) n) with
  (bisum (fun i : Zif Z_eq_dec i j then Zzero j else f i) n).

 rewrite bisum_in.
  unfold Zzero; ring.
  apply H.

 unfold Zzero; trivial.
Qed.

Lemma bisum_strip_nothing : f n j, ((- Z_of_nat (S n)) = j j = Z_of_nat (S n))%Z
  bisum_strip' f j n = bisum f n.
Proof.
intros.
unfold bisum_strip'.
apply bisum_eq_compat_bounded; intros.
destruct H; subst.
 destruct (Z_eq_dec z (- Z_of_nat (S n))).
  subst; destruct H0; rewrite inj_S in × |- ; apply False_ind; omega.
  trivial.
 destruct (Z_eq_dec z (Z_of_nat (S n))).
  subst; destruct H0; rewrite inj_S in × |- ; apply False_ind; omega.
  trivial.
Qed.

Steps of calculus in bisums

Lemma bisum_one_step : f n, bisum f (S n) = bisum f n + f (Z_of_nat (S n)) + f (- Z_of_nat (S n))%Z.
Proof.
trivial.
Qed.

Lemma bisumsum_one_step : f n m,
  bisum (fun ibisum (f i) (S n)) m =
  bisum (fun ibisum (f i) n) m +
  bisum (fun if i (Z_of_nat (S n)) ) m +
  bisum (fun if i (- Z_of_nat (S n))%Z ) m.
intros.
simpl.
repeat rewrite <- bisum_plus.
apply bisum_eq_compat; intros.
trivial.
Qed.

Switching indices

Lemma bisum_eq_sym : f z n,
  bisum (fun i : Zif Z_eq_dec i z then 0 else f z i) n =
  bisum (fun j : Zif Z_eq_dec z j then 0 else f z j) n.
Proof.
intros; apply bisum_eq_compat; intros.
destruct (Z_eq_dec z0 z); destruct (Z_eq_dec z z0); try trivial; subst;
  apply False_ind; apply n0; trivial.
Qed.

Substracting the diagonal terms sum makes them null in the main double sum

Lemma strip_diag : f n, bisumsum_strip_diag' f n = bisumsum_strip_diag f n.
Proof.
intros.
induction n.
 unfold bisumsum_strip_diag', bisumsum_strip_diag, bisumsum.
 simpl; ring.

 unfold bisumsum_strip_diag', bisumsum_strip_diag, bisumsum.
 rewrite bisumsum_one_step.
 rewrite bisum_one_step.
 unfold bisumsum_strip_diag', bisumsum_strip_diag, bisumsum in IHn.
 rewrite IHn.
 rewrite (bisum_one_step (fun i : Zf i i)).
 repeat rewrite bisum_one_step.
 destruct (Z_eq_dec (Z_of_nat (S n)) (Z_of_nat (S n))); [ | apply False_ind; omega]; clear e.
 destruct (Z_eq_dec (Z_of_nat (S n)) (- Z_of_nat (S n))); [ apply False_ind; inversion e | ]; clear n0.
 destruct (Z_eq_dec (- Z_of_nat (S n)) (Z_of_nat (S n))); [ apply False_ind; inversion e | ]; clear n0.
 destruct (Z_eq_dec (- Z_of_nat (S n)) (- Z_of_nat (S n))); [ | apply False_ind; omega]; clear e.
 ring_simplify.
 assert (H : BII FNP FPN A B C D BIJ BIJS BPJS BNJS,
  BIJ + A + B + C + D = BIJS + BPJS + BNJS
  BIJ - BII + A + B + C + FNP + D + FPN = - BII + FNP + FPN + BIJS + BPJS + BNJS)
 by (intros; assert (H' : BIJ = - (A + B + C + D) + (BIJS + BPJS + BNJS)) by (rewrite <- H; ring); rewrite H'; ring).
 erewrite H; [reflexivity | ].
 replace (bisum (fun j : Zif Z_eq_dec (Z_of_nat (S n)) j then 0 else f (Z_of_nat (S n)) j) n)
   with (bisum_strip' (f (Z_of_nat (S n))) (Z_of_nat (S n)) n) by apply bisum_eq_sym.
 replace (bisum (fun j : Zif Z_eq_dec (- Z_of_nat (S n)) j then 0 else f (- Z_of_nat (S n))%Z j) n)
   with (bisum_strip' (f (- Z_of_nat (S n)))%Z (- Z_of_nat (S n)) n)%Z by apply bisum_eq_sym.
 replace (bisum (fun i : Zif Z_eq_dec i (- Z_of_nat (S n)) then 0 else f i (- Z_of_nat (S n))%Z) n)
   with (bisum_strip' (fun if i (- Z_of_nat (S n)))%Z (- Z_of_nat (S n)) n)%Z by trivial.
 replace (bisum (fun i : Zif Z_eq_dec i (Z_of_nat (S n)) then 0 else f i (Z_of_nat (S n))) n)
   with (bisum_strip' (fun if i (Z_of_nat (S n)))%Z (Z_of_nat (S n)) n)%Z by trivial.
 repeat rewrite bisum_strip_nothing; [ | left | right | left | right ]; trivial.
 rewrite bisumsum_one_step.
 ring.
Qed.

Rewriting double sums

Switching indices in a double sum

Lemma bisumsum_switch_index : f n, bisumsum (fun i jf j i) n = bisumsum f n.
Proof.
intros.
induction n.
 trivial.

 unfold bisumsum in ×.
 rewrite bisumsum_one_step.
 rewrite bisumsum_one_step.
 simpl.
 rewrite IHn.
 replace (bisum (f (Zneg (P_of_succ_nat n))) n) with (bisum (fun if (Zneg (P_of_succ_nat n)) i) n) by (apply bisum_eq_compat; trivial).
 replace (bisum (f (Zpos (P_of_succ_nat n))) n) with (bisum (fun if (Zpos (P_of_succ_nat n)) i) n) by (apply bisum_eq_compat; trivial).
 ring.
Qed.

Switching indices in a double sum (where diagonal terms are null)

Lemma bisumsum_strip_diag'_switch_index : f n,
  bisumsum_strip_diag' (fun i jf j i) n =
  bisumsum_strip_diag' f n.
Proof.
intros.
unfold bisumsum_strip_diag'.
rewrite bisumsum_switch_index.
apply bisumsum_eq_compat; intros.
destruct (Z_eq_dec y x); destruct (Z_eq_dec x y); try trivial;
  subst; apply False_ind; apply n0; trivial.
Qed.

Adding double sums

Lemma bisumsum_strip_diag'_plus : f g n,
  bisumsum_strip_diag' (fun i jf i j + g i j) n =
  bisumsum_strip_diag' f n +
  bisumsum_strip_diag' g n.
Proof.
intros.
unfold bisumsum_strip_diag'.
unfold bisumsum.
rewrite <- bisum_plus.
apply bisum_eq_compat; intros.
unfold zr2.
rewrite <- bisum_plus.
apply bisum_eq_compat; intros.
unfold zr2.
destruct (Z_eq_dec z z0); ring.
Qed.

Switching indices of only one term in a sum in a double sum

Lemma bisumsum_plus_switch : f g n,
  bisumsum_strip_diag' (fun i jf i j + g i j) n =
  bisumsum_strip_diag' (fun i jf i j + g j i) n.
Proof.
intros.
rewrite bisumsum_strip_diag'_plus.
rewrite <- bisumsum_strip_diag'_switch_index with g n.
rewrite <- bisumsum_strip_diag'_plus.
trivial.
Qed.

Extensional equality but on the diagonal terms

Lemma bisumsum_strip_diag'_eq_but_diag_compat : f g n,
  ( i j, i jf i j = g i j) →
  bisumsum_strip_diag' f n = bisumsum_strip_diag' g n.
Proof.
intros.
apply bisum_eq_compat; intros.
apply bisum_eq_compat; intros.
destruct (Z_eq_dec z z0).
 trivial.
 apply (H _ _ n0).
Qed.

Shifting a sequence (with an integer)
Fixpoint sum1 u n := match n with
  | O ⇒ 0
  | S n'(sum1 u n') + u (Z_of_nat n)
end.

Lemma sum_f_R0_sum1 : u n, sum1 u (S n) =
  sum_f_R0 (fun iu (Z_of_nat (S i))) n.
Proof.
intros.
induction n.
 compute; ring.

 simpl in ×.
 rewrite IHn.
 trivial.
Qed.

Definition shiftp (u:ZR) (p:nat) (i:Z) := u (i + (Z_of_nat p))%Z.

Lemma bisum_shifting_S : u a b,
  bisum (shiftp u (S b)) (S a) =
  bisum (shiftp u b) a +
  u (Z_of_nat (S (a + b))) +
  u (Z_of_nat (S (S (a + b))))
.
Proof.
intros.
induction a.
 unfold bisum, shiftp.
 assert (AP : a b c a' b' c', a = a'b = b'c = c'
   a + b + c = c' + a' + b') by (intros; subst; ring);
   apply AP; clear AP;
   inject;
   simpl (0 + b)%nat; simpl (Z_of_nat 1); repeat rewrite inj_S; omega.
 rewrite bisum_one_step.
 rewrite IHa; clear IHa.
 rewrite bisum_one_step.
 repeat rewrite Rplus_assoc.
 inject.
 unfold shiftp.
 repeat rewrite <- Rplus_assoc.
 assert (AP : a b c d a' b' c' d', a = a'b = b'c = c'd = d'
   a + b + c + d = a' + d' + b' + c') by (intros; subst; ring);
   apply AP; clear AP;
   inject;
   try (simpl (0 + b)%nat; simpl (Z_of_nat 1); repeat rewrite inj_S; omega);
   repeat rewrite inj_S; rewrite inj_plus; repeat rewrite inj_S; omega.
Qed.

Lemma bisum_shifting : u n p,
  bisum (shiftp u p) (n + p) =
  bisum u n + sum1 (shiftp u n) (2 × p)
.
Proof.
intros.
induction p.
 rewrite bisum_eq_compat with _ u _;
   [| intro; unfold shiftp; inject; simpl Z_of_nat; omega].
 simpl.
 ring_simplify; inject; omega.

 rewrite <- plus_n_Sm.
 replace (mult 2 (S p)) with (S (S (2 × p))) by omega.
 replace (sum1 (shiftp u n) (S (S (2 × p))))
   with (sum1 (shiftp u n) (2 × p) +
     (shiftp u n) (Z_of_nat (S (2 × p))) +
     (shiftp u n) (Z_of_nat (S (S (2 × p)))))
   by trivial.
 repeat rewrite <- Rplus_assoc.
 rewrite <- IHp; clear IHp.
 replace (bisum (shiftp u (S p)) (S (n + p)))
   with (bisum (shiftp u p) (n + p) +
     (shiftp u n) (Z_of_nat (S (2 × p))) +
     (shiftp u n) (Z_of_nat (S (S (2 × p)))))
     ; [trivial | ].
 rewrite bisum_shifting_S.
 unfold shiftp.
 replace (mult 2 p) with (plus p p) by omega.
 assert (AP : a b c a' b' c', a = a'b = b'c = c'
   a + b + c = a' + b' + c') by (intros; subst; ring);
   apply AP; clear AP; trivial;
   inject;
   repeat (repeat rewrite inj_S; repeat rewrite inj_plus); omega.
Qed.

Rewriting An * An - Bn


Definition d x := 2 × x + 1.
Definition d' z := d (IZR z).

Lemma splitmn : n m, d n 0 → d m 0 → m n
  / ((d n) × (d m)) = / (2 × (m - n)) × (/ (d n) - / (d m)).
Proof.
intros.
unfold d in ×.
field.
split; [|split].
 assumption.
 assumption.
 apply Rminus_eq_contra; assumption.
Qed.

Lemma d_not_null : z, d' z 0.
Proof.
intros.
unfold d', d.
discrR; omega.
Qed.

Lemma calc1 : N, (An N) × (An N) - Bn N =
  bisumsum_strip_diag' (fun n m
    (pow1 m × pow1 n) × / (2 × (IZR (m - n))) × (/ (d' n) - / (d' m))
  ) N.
Proof.
assert ( z, 2 × IZR z + 1 0) by (intro; discrR; omega).
intros N.
unfold An.
rewrite <- bisumsum_square.
replace (Bn N) with (bisum (fun ianz i × anz i) N).
 rewrite bisumsum_strip_diag'_eq_but_diag_compat with _ (fun i janz i × anz j) _.
  rewrite strip_diag.
  unfold bisumsum_strip_diag.
  trivial.

  intros.
  unfold anz.
  replace (pow1 i / (2 × IZR i + 1) × (pow1 j / (2 × IZR j + 1)))
    with (pow1 i × pow1 j × (/ ((2 × IZR i + 1) × (2 × IZR j + 1)))).
   2:field_simplify; [ trivial | split | split ]; try apply d_not_null.

   replace (2 × IZR i + 1) with (d (IZR i)) by trivial.
   replace (2 × IZR j + 1) with (d (IZR j)) by trivial.
   rewrite splitmn; try apply d_not_null; try (discrR; omega).
    unfold d'.
    rewrite Z_R_minus.
    field; repeat split; try apply d_not_null; discrR; omega.

 apply bisum_eq_compat.
 intro.
 unfold bnz, anz; field_simplify; try apply H.
 rewrite pow1_squared; field.
 unfold pow.
 discrR; omega.
Qed.

Lemma calc2 : N, (An N) × (An N) - Bn N = bisumsum_strip_diag' (fun n m
    (pow1 m × pow1 n) × / ((IZR (m - n)) × (d' n))
  ) N.
Proof.
intros.
rewrite calc1.
rewrite bisumsum_strip_diag'_eq_but_diag_compat with _
  (fun n m : Zpow1 m × pow1 n / (2 × IZR (m - n)) × ( / d' n) +
                  pow1 m × pow1 n / (2 × IZR (m - n)) × (- / d' m)) _.
 rewrite bisumsum_strip_diag'_plus.
 rewrite bisumsum_strip_diag'_switch_index.
 rewrite <- bisumsum_strip_diag'_plus.
 rewrite bisumsum_strip_diag'_switch_index.
 apply bisumsum_strip_diag'_eq_but_diag_compat.
 intros.
 replace (IZR (i - j)) with (- IZR (j - i)).
  field; split.
   apply d_not_null.
   discrR; omega.
  repeat rewrite <- Z_R_minus; ring.
 intros.
 field; repeat split.
  apply d_not_null.
  discrR; omega.
  apply d_not_null.
Qed.

Definition cn n N := bisum (fun mif Z_eq_dec n m then 0 else pow1 m / (IZR (m - n))) N.

Lemma calc3 : N, (An N) × (An N) - Bn N = bisum (fun npow1 n / (d' n) × (cn n N)) N.
Proof.
intros.
rewrite calc2.
apply bisum_eq_compat; intros.
unfold cn.
rewrite <- bisum_scal_mult.
apply bisum_eq_compat; intros.
unfold zr.
destruct (Z_eq_dec z z0); field; [ | split ]; try apply d_not_null.
discrR; omega.
Qed.

Lemma cn_odd : n N, cn (- n)%Z N = - (cn n N).
Proof.
intros.
replace (- cn n N) with (-1 × cn n N) by ring.
unfold cn.
rewrite bisum_reverse.
rewrite <- bisum_scal_mult.
apply bisum_eq_compat; intros.
unfold zr.
destruct (Z_eq_dec (- n) (- z)); destruct (Z_eq_dec n z); subst; try ring.
 assert (n = z) by omega; subst; apply False_ind; apply n0; trivial.
 apply False_ind; apply n0; trivial.
 replace (- z - - n)%Z with (n - z)%Z by omega.
 replace (pow1 (- z)) with (pow1 z).
  replace (IZR (n - z)) with (- IZR (z - n)).
   field.
   discrR; omega.
  rewrite <- Ropp_Ropp_IZR; apply IZR_eq; omega.
  induction z; trivial.
Qed.

Lemma cn_zero_zero : N, cn 0 N = 0.
Proof.
intros.
cut (2 × cn 0 N = 0).
 intro H.
 apply Rmult_integral in H.
 destruct H.
  fourier.
  assumption.
 rewrite double.
 replace (cn 0 N + cn 0 N) with (cn 0 N + cn (- 0) N) by (inject; ring).
 rewrite cn_odd.
 ring.
Qed.

Bounding


Lemma cn_pos : n N, (S n N)%nat
  cn (Zpos (P_of_succ_nat n)) N =
  (pow (-1) (S (S n))) ×
  (sum_f_R0 (fun jpow (-1) (j + N - n) × / (INR (j + N - n)))) (S (2 × n))
.
Proof.
intros.
assert (odd' : a b, cn a b = - (cn (- a) b))
  by (intros; rewrite cn_odd; ring).
rewrite odd'.
pose (N - S n)%nat as k.
replace N with (k + S n)%nat by (unfold k; omega).
unfold cn.

replace
  (bisum
   (fun m : Zif Z_eq_dec (- Zpos (P_of_succ_nat n)) m then 0
    else pow1 m / IZR (m - - Zpos (P_of_succ_nat n))) (k + S n))
  with
  (bisum
   (shiftp (fun j : Z- (-1) ^ n × if Z_eq_dec 0 j then 0 else pow1 j / IZR j) (S n))
   (k + S n)).

 rewrite bisum_shifting.

 assert (bisum (fun j : Z- (-1) ^ n × (if Z_eq_dec 0 j then 0 else pow1 j / IZR j)) k = 0).
  induction k.
   simpl; ring.
   rewrite bisum_one_step.
   rewrite IHk.
   replace 0%Z with (Z_of_nat O) by trivial.
   destruct (Z_eq_dec (Z_of_nat 0) (Z_of_nat (S k))).
    apply inj_eq_rev in e.
    inversion e.
   replace (Z_of_nat O) with (- Z_of_nat O)%Z by trivial.
   destruct (Z_eq_dec (- Z_of_nat O)%Z (- Z_of_nat (S k))).
    apply Zopp_inj in e.
    apply inj_eq_rev in e.
    inversion e.

   ring_simplify.
   rewrite pow1_nat_neg.
   rewrite pow1_nat.
   rewrite Ropp_Ropp_IZR.
   field; discrR.

  rewrite H0; clear H0.
  rewrite Rplus_0_l.
  replace (mult 2 (S n)) with (S (S (2 × n))) by omega.
  rewrite sum_f_R0_sum1.
  assert (RE : x, - x = -1 × x) by (intro; ring);
    rewrite RE; clear RE.
  do 2 rewrite scal_sum.
  apply Rseq_sum_ext; intro i.
  unfold shiftp.
  replace (Z_of_nat (S i) + Z_of_nat k)%Z
    with (Z_of_nat (S i + k)).

   replace 0%Z with (Z_of_nat O) by trivial.
   destruct (Z_eq_dec (Z_of_nat O) (Z_of_nat (S i + k))).
    apply inj_eq_rev in e.
    inversion e.

   rewrite pow1_nat.
   rewrite <- INR_IZR_INZ.
   replace (i + (k + S n) - n)%nat with (S i + k)%nat by omega.
   simpl pow.
   field; INR_solve.

  simpl (S i + k)%nat.
  do 2 rewrite inj_S.
  rewrite Zplus_succ_l.
  inject.
  induction i.
   trivial.
   simpl (S i + k)%nat.
   do 2 rewrite inj_S.
   rewrite IHi.
   omega.

 apply bisum_eq_compat; intro.
 unfold shiftp.
 destruct (Z_eq_dec 0 (z + Z_of_nat (S n)));
 destruct (Z_eq_dec (- Zpos (P_of_succ_nat n)) z).
  auto with ×.

  assert (z = - Z_of_nat (S n))%Z by omega.
  assert (- Zpos (P_of_succ_nat n) = (- Z_of_nat (S n)))%Z by trivial.
  subst; tauto.

  subst.
  assert (- Zpos (P_of_succ_nat n) = (- Z_of_nat (S n)))%Z by trivial.
  apply False_ind; omega.

  repeat rewrite <- Rmult_assoc.
  assert (AP : a b a' a'' b', a = a' × a''b = b' → (b' 0)%Z
    a' × (a'' / IZR b') = a / IZR b) by (intros; subst; field; discrR; auto);
    apply AP; clear AP;
    auto.
   rewrite pow1_plus_nat.
   ring_simplify.
   assert ((-1) ^ n × (-1) ^ S n = -1).
    rewrite <- Rdef_pow_add.
    replace (n + S n)%nat with (S (2 × n)) by omega.
    apply pow_1_odd.

   rewrite Rmult_assoc.
   rewrite H0.
   ring.
Qed.

Lemma alt_bounding :
   u : natR,
  Un_decreasing u
  ( n, 0 u n) →
   n, 0 sum_f_R0 (tg_alt u) n u O.
Proof.
intros Un dec pos n.
pose (sum_f_R0 (tg_alt Un)) as Sn; fold Sn.

assert (Heu : p, Sn (2 × p)%nat Un O).
induction p.
 compute; intuition.
 eapply Rle_trans.
  apply CV_ALT_step1; assumption.
  assumption.

assert (Ho0 : p, 0 Sn (S (2 × p))).
induction p.
 unfold Sn; simpl; unfold tg_alt, pow; ring_simplify.
 assert (Un 1%nat Un O) by auto; fourier.
 eapply Rle_trans.
  apply IHp.
  apply CV_ALT_step0; assumption.

destruct (even_odd_cor n) as [p [he|ho]]; subst; split.
 destruct p.
 unfold Sn; simpl; unfold tg_alt, pow; ring_simplify; apply pos.
 replace (2 × S p)%nat with (S (S (2 × p))) by omega.
 unfold Sn; rewrite tech5; fold Sn.
 apply Rplus_le_le_0_compat.
  apply Ho0.
  replace (S (S (2 × p))) with (2 × S p)%nat by omega.
  unfold tg_alt.
  rewrite pow_1_even.
  rewrite Rmult_1_l.
  apply pos.

 apply Heu.

 apply Ho0.

 unfold Sn; rewrite tech5; fold Sn.
 unfold tg_alt.
 rewrite pow_1_odd.
 assert (AP : a b c, a c → 0 ba + -1 × b c)
   by (intros; fourier); apply AP; clear AP.
  apply Heu.
  apply pos.
Qed.

Lemma cn_maj : n N, (n N)%natRabs (cn (Z_of_nat n) N) / (INR (N - n + 1)).
Proof.
intros.
destruct n.
 simpl; rewrite cn_zero_zero.
 unfold Rabs.
 destruct (Rcase_abs 0); left;
  replace (- 0) with 0 by ring;
  apply Rinv_0_lt_compat;
  INR_solve.

 unfold Z_of_nat.
 rewrite cn_pos with n N; [|assumption].
 rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l.
 replace (sum_f_R0 (fun j : nat(-1) ^ (j + N - n) × / INR (j + N - n)) (S (2 × n)))
   with ((-1) ^ (N - n) × sum_f_R0 (fun j : nat(-1) ^ j × / INR (j + N - n)) (S (2 × n))).
  2:rewrite scal_sum.
  2:apply Rseq_sum_ext; intro.
  2:replace (n0 + N - n)%nat with (n0 + (N - n))%nat by omega.
  2:rewrite Rdef_pow_add; ring.

 rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l.
 cut ( i, Rabs (sum_f_R0 (fun j : nat(-1) ^ j × / INR (j + N - n)) i) / INR (N - S n + 1))
   ;[intuition | ].
 replace (N - S n + 1)%nat with (N - n)%nat by omega.

 pose (N - n)%nat as k; fold k.
 assert (kpos : (0 < k)%nat) by (unfold k; omega).
 pose (fun j/ INR (j + k)) as Un.

 intro i;
 replace (sum_f_R0 (fun j(-1) ^ j × / INR (j + N - n)) i)
   with (sum_f_R0 (fun j(-1) ^ j × / INR (j + k)) i)
   by (apply Rseq_sum_ext; intro; trivial; inject; unfold k; omega).
 replace (sum_f_R0 (fun j(-1) ^ j × / INR (j + k)) i)
   with (sum_f_R0 (tg_alt Un) i)
   by (apply Rseq_sum_ext; intro; trivial).
 replace (/ INR k) with (Un O) by trivial.

 edestruct (alt_bounding Un).
  intro; unfold Un. apply Rle_Rinv; INR_solve.
  intro; unfold Un; apply Rlt_le; apply Rinv_0_lt_compat; INR_solve.

 assert (0 sum_f_R0 (tg_alt Un) i) by apply H0.
 rewrite Rabs_pos_eq by apply H2.
 apply H1.
Qed.

Lemma abound_eq : n N, (O n)%nat → (S n N)%nat
  / (INR (N - n)) × (/ (INR (2 × n + 1)) + / (INR (2 × n + 3))) =
  / (INR (2 × N + 1)) × (2 / (INR (2 × n + 1)) + / (INR (N - n))) +
  / (INR (2 × N + 3)) × (2 / (INR (2 × n + 3)) + / (INR (N - n))).
Proof.
intros.
rewrite minus_INR.
repeat rewrite plus_INR.
repeat rewrite mult_INR.
replace (INR 1) with 1 by trivial.
replace (INR 2) with 2 by trivial.
field; INR_solve.
eapply le_trans.
 constructor 2; constructor.
 assumption.
Qed.

Definition abound N := sum_f_R0 (fun n/ (INR (N - (S n) + 1)) ×
    (/ (INR (2 × n + 1)) + / (INR (2 × n + 3)))
  ) (pred N).

Definition bound1 N := / (INR (2 × N + 1)) ×
  sum_f_R0 (fun n
    2 / (INR (2 × n + 1)) + / (INR (N - (S n) + 1))
  ) (pred N).

Definition bound2 N := / (INR (2 × N + 3)) ×
  sum_f_R0 (fun n
    2 / (INR (2 × n + 3)) + / (INR (N - (S n) + 1))
  ) (pred N).

Definition bound1' N := / INR (2 × N + 1) × sum_f_R0 (fun n ⇒ 2 / INR (2 × n + 1)) (pred N).
Definition bound2' N := / INR (2 × N + 3) × sum_f_R0 (fun n ⇒ 2 / INR (2 × n + 3)) (pred N).
Definition bound1c N := / INR (2 × N + 1) × sum_f_R0 (fun n/ INR (N - (S n) + 1)) (pred N).
Definition bound2c N := / INR (2 × N + 3) × sum_f_R0 (fun n/ INR (N - (S n) + 1)) (pred N).

Lemma An_squared_Bn_maj : N, (1 N)%natRabs (An N × An N - Bn N) abound N.
Proof.
intros N H.
destruct N.
 inversion H.

 rewrite calc3.
 rewrite sum_bisum.
 eapply Rle_trans; [apply Rabs_triang | ].
 unfold abound.
 assert (REWdiv : a b, pow1 a / b = pow1 a × / b) by reflexivity.
 replace (sum_f_R0 (fun n : nat
   / INR (S N - S n + 1) × (/ INR (2 × n + 1) + / INR (2 × n + 3)))
   (pred (S N)))
   with
   (sum_f_R0 (fun n : nat/ INR (S N - S n + 1) × / INR (2 × n + 3)) (pred (S N)) +
   sum_f_R0 (fun n : nat/ INR (S N - S n + 1) × / INR (2 × n + 1)) (pred (S N)))
 by (
   rewrite <- plus_sum; simpl pred;
   apply Rseq_sum_ext; intro n;
   field; INR_solve
 ).
 rewrite decomp_sum by omega; simpl pred; simpl (Z_of_nat 0);
   rewrite cn_zero_zero; rewrite Rmult_0_r; rewrite Rplus_0_l.

 apply Rplus_le_compat.
  eapply Rle_trans; [apply Rsum_abs | ].
  replace (pred (S (S N))) with (S N) by trivial.
  apply sum_Rle; intros n nSN.
  rewrite REWdiv.
  repeat rewrite Rabs_mult.
  rewrite pow1_Rabs; rewrite Rmult_1_l.
  rewrite Rmult_comm.
  apply Rmult_le_compat; try apply Rabs_pos.
   apply (cn_maj (S n) (S N)); omega.
   unfold d', d; rewrite <- INR_IZR_INZ.
   rewrite Rabs_pos_eq; try apply Rle_Rinv;
     try (apply Rlt_le; apply Rinv_0_lt_compat);
     INR_solve.

  eapply Rle_trans; [apply Rsum_abs | ].
  replace (pred (S (S N))) with (S N) by trivial.
  apply sum_Rle; intros n nSN.
  rewrite REWdiv.
  repeat rewrite Rabs_mult.
  rewrite pow1_Rabs; rewrite Rmult_1_l.
  rewrite Rmult_comm.
  apply Rmult_le_compat; try apply Rabs_pos.
   eapply Rle_trans.
    rewrite cn_odd; rewrite Rabs_Ropp.
    apply (cn_maj (S n) (S N)); omega.
    apply Rle_Rinv; INR_solve.
   unfold d', d; rewrite Ropp_Ropp_IZR; rewrite <- INR_IZR_INZ.
   rewrite <- Rabs_Ropp; rewrite Ropp_inv_permute.
   replace (- (2 × - INR (S n) + 1)) with ((2 × INR n + 1)) by (rewrite plus_1_S; ring).
   rewrite Rabs_pos_eq; try apply Rle_Rinv;
     try (apply Rlt_le; apply Rinv_0_lt_compat);
     INR_solve.
   rewrite INR_IZR_INZ; discrR.
Qed.

Lemma bound_eq : N, abound (S N) = bound1 (S N) + bound2 (S N).
Proof.
intros.
unfold abound, bound1, bound2.
simpl (pred (S N)).
do 2 rewrite scal_sum.
erewrite sum_eq.
 apply sum_plus.

 intros n H.
 replace (S N - S n + 1)%nat with (S N - n)%nat by omega.
 rewrite abound_eq; try omega.
 replace (S N - S n + 1)%nat with (S N - n)%nat by omega.
 field; INR_solve.
Qed.

Convergence of the bounds

Definition inverse_mean n := sum_f_R0 (fun i/ INR (S i)) n / INR (S n).

Lemma inverse_cv_0 : Rseq_cv (fun i/ INR (S i)) 0.
Proof.
apply Rseq_cv_pos_infty_inv_compat.
assert (H01 : (1 > 0)%nat) by omega.
pose proof (Rseq_poly_cv 1 H01).
unfold Rseq_poly in H; simpl in H.
eapply Rseq_cv_pos_infty_eq_compat in H; [ | intro; apply Rmult_1_r].
intro M.
destruct (H M) as [N Hcv].
N.
intros.
eapply Rlt_le_trans.
 apply Hcv.
 apply H0.
 INR_solve.
Qed.

Lemma inverse_mean_cv_0 : Rseq_cv inverse_mean 0.
Proof.
unfold inverse_mean.
eapply Rseq_cv_eq_compat.
 2:eapply Rseq_cv_shift_compat_reciprocal.
 2:apply (Cesaro_1 (fun i/ INR (S i))).
 intro n; unfold Rseq_shift; simpl pred; reflexivity.

 apply inverse_cv_0.
Qed.

Lemma Rseq_cv_0_pos_maj_compat : Un Vn, ( n, 0 Un n) → ( n, Un n Vn n) →
  Rseq_cv Vn 0 → Rseq_cv Un 0.
Proof.
intros Un Vn Unpos Unmaj Vncv e epos.
destruct (Vncv e epos) as [N H].
N; intros n nN.
unfold R_dist; rewrite Rminus_0_r; rewrite Rabs_pos_eq; [|apply Unpos].
eapply Rle_lt_trans.
 apply Unmaj.
 pose proof H n nN as J.
 unfold R_dist in J; rewrite Rminus_0_r in J; rewrite Rabs_pos_eq in J.
  apply J.
  eapply Rle_trans; [apply Unpos | apply Unmaj].
Qed.

Lemma half_mean_0 : Un k m, 0 k → (1 m)%nat → ( n, 0 Un n) → ( n, Un n k / INR (S n)) →
  Rseq_cv (fun N/ INR (2 × N + m) × sum_f_R0 Un (pred N)) 0.
Proof.
intros Un k m kpos mpos Unpos Unbound.
apply Rseq_cv_shift_compat; unfold Rseq_shift; simpl pred.
eapply Rseq_cv_0_pos_maj_compat.
 intro.
 rewrite Rmult_comm; apply Rle_mult_inv_pos.
  apply cond_pos_sum; assumption.
  INR_solve.

 intro.
 eapply Rle_trans.
  apply Rmult_le_compat.
   apply Rlt_le; apply Rinv_0_lt_compat; INR_solve.
   apply cond_pos_sum; assumption.
   apply Rlt_le; apply (Rinv_lt_contravar (INR (S n))); INR_solve.
  apply (sum_growing _ (fun nk / INR (S n))); apply Unbound.

  replace (sum_f_R0 (fun n0 : natk / INR (S n0)) n)
    with (sum_f_R0 (fun n0 : nat/ INR (S n0) × k) n)
    by (apply Rseq_sum_ext; intro; field; INR_solve).
  rewrite <- scal_sum.
  rewrite <- Rmult_assoc; rewrite Rmult_comm with _ k; rewrite Rmult_assoc.

 2: replace 0 with (k × 0) by ring.
 2: apply Rseq_cv_mult_compat.
  2: apply Rseq_constant_cv.
  2: apply inverse_mean_cv_0.

 unfold Rseq_mult, Rseq_constant.
 apply (Rmult_le_compat_l k _ _ kpos).
 unfold inverse_mean, Rdiv.
 rewrite Rmult_comm.
 intuition.
Qed.

Lemma bound1'_cv : Rseq_cv bound1' 0.
Proof.
apply Rseq_cv_shift_compat.
unfold bound1', Rseq_shift.
assert (Rseq_cv
      (fun N : nat
       / INR (2 × N + 1) ×
       sum_f_R0 (fun n0 : nat ⇒ 2 / INR (2 × n0 + 1)) (pred N)) 0).
 apply (half_mean_0 _ 2).
  fourier.

  omega.

  intro; unfold Rdiv; apply Rle_mult_inv_pos; [fourier | INR_solve].

  intro; unfold Rdiv.
  apply Rmult_le_compat_l; [fourier | ].
  apply Rle_Rinv; INR_solve.

 intros e epos; destruct (H e epos) as [N J]; N; intros n nN.
 simpl pred.
 apply J; omega.
Qed.

Lemma bound2'_cv : Rseq_cv bound2' 0.
Proof.
apply Rseq_cv_shift_compat.
unfold bound1', Rseq_shift.
assert (Rseq_cv
      (fun N : nat
       / INR (2 × N + 3) ×
       sum_f_R0 (fun n0 : nat ⇒ 2 / INR (2 × n0 + 3)) (pred N)) 0).
 apply (half_mean_0 _ 2).
  fourier.

  omega.

  intro; unfold Rdiv; apply Rle_mult_inv_pos; [fourier | INR_solve].

  intro; unfold Rdiv.
  apply Rmult_le_compat_l; [fourier | ].
  apply Rle_Rinv; INR_solve.

 intros e epos; destruct (H e epos) as [N J]; N; intros n nN.
 simpl pred.
 apply J; omega.
Qed.

Lemma Rsum_switch_index : Un N, sum_f_R0 (fun nUn (N - n)%nat) N = sum_f_R0 Un N.
Proof.
intros Un N.
induction N.
 trivial.

 rewrite decomp_sum by omega; simpl.
 rewrite IHN.
 ring.
Qed.

Lemma bound1c_cv : Rseq_cv bound1c 0.
Proof.
apply Rseq_cv_shift_compat.
unfold bound1', Rseq_shift.
assert (Rseq_cv
      (fun N : nat
       / INR (2 × N + 1) ×
       sum_f_R0 (fun n0 : nat/ INR (S n0)) (pred N)) 0).
 apply (half_mean_0 _ 1).
  fourier.

  omega.

  intro; apply Rlt_le; apply Rinv_0_lt_compat; INR_solve.

  intro; unfold Rdiv; rewrite Rmult_1_l; auto with ×.

 intros e epos; destruct (H e epos) as [N J]; N; intros n nN.
 simpl pred.
 unfold bound1c.
 replace (sum_f_R0 (fun n0 : nat/ INR (S n - S n0 + 1)) (pred (S n)))
   with (sum_f_R0 (fun n0 : nat/ INR (S n0)) (pred (S n)))
   by (rewrite <- Rsum_switch_index; apply Rseq_sum_ext; intro; inject; omega).
 apply J; omega.
Qed.

Lemma bound2c_cv : Rseq_cv bound2c 0.
Proof.
apply Rseq_cv_shift_compat.
unfold bound1', Rseq_shift.
assert (Rseq_cv
      (fun N : nat
       / INR (2 × N + 3) ×
       sum_f_R0 (fun n0 : nat/ INR (S n0)) (pred N)) 0).
 apply (half_mean_0 _ 1).
  fourier.

  omega.

  intro; apply Rlt_le; apply Rinv_0_lt_compat; INR_solve.

  intro; unfold Rdiv; rewrite Rmult_1_l; apply Rle_Rinv; INR_solve.

 intros e epos; destruct (H e epos) as [N J]; N; intros n nN.
 simpl pred.
 unfold bound2c.
 replace (sum_f_R0 (fun n0 : nat/ INR (S n - S n0 + 1)) (pred (S n)))
   with (sum_f_R0 (fun n0 : nat/ INR (S n0)) (pred (S n)))
   by (rewrite <- Rsum_switch_index; apply Rseq_sum_ext; intro; inject; omega).
 apply J; omega.
Qed.

Lemma bound1_cv : Rseq_cv bound1 0.
Proof.
replace 0 with (0 + 0) by ring.
eapply Rseq_cv_eq_compat.
 2:apply Rseq_cv_plus_compat; [apply bound1'_cv | apply bound1c_cv].
 intro; unfold Rseq_plus, bound1', bound1c, bound1.
 rewrite <- Rmult_plus_distr_l.
 inject.
 rewrite <- sum_plus.
 apply Rseq_sum_ext; intro; trivial.
Qed.

Lemma bound2_cv : Rseq_cv bound2 0.
Proof.
replace 0 with (0 + 0) by ring.
eapply Rseq_cv_eq_compat.
 2:apply Rseq_cv_plus_compat; [apply bound2'_cv | apply bound2c_cv].
 intro; unfold Rseq_plus, bound2', bound2c, bound2.
 rewrite <- Rmult_plus_distr_l.
 inject.
 rewrite <- sum_plus.
 apply Rseq_sum_ext; intro; trivial.
Qed.

Lemma abound_cv : Rseq_cv abound 0.
Proof.
replace 0 with (0 + 0) by ring.
eapply Rseq_cv_asymptotic_eq_compat.
 2:apply Rseq_cv_plus_compat; [apply bound1_cv | apply bound2_cv].
  (S O).
 intros n Hb.
  assert (H : n', n = S n').
    (pred n); apply S_pred with O; apply Hb.
  destruct H; subst.
  unfold Rseq_plus.
  symmetry; apply bound_eq.
Qed.

Final result about sums

Lemma An_squared_Bn_cv : Rseq_cv (An × An - Bn) 0.
Proof.
intros e epos.
destruct (abound_cv e epos) as [N H].
(S N); intros n nN.
unfold R_dist; rewrite Rminus_0_r.
unfold Rseq_minus, Rseq_mult, Rseq_abs.
eapply Rle_lt_trans.
 apply An_squared_Bn_maj.
 omega.
 assert (nN' : (n N)%nat) by omega.
 pose proof (H n nN') as T.
 unfold R_dist in T; rewrite Rminus_0_r in T.
 eapply Rle_lt_trans.
  2: apply T.
  apply RRle_abs.
Qed.

Bn converges to pi²/4


Lemma Bn_cv : Rseq_cv Bn (PI ^ 2 / 4).
Proof.
replace (PI ^ 2 / 4) with (PI ^ 2 / 4 - 0) by field.
apply Rseq_cv_eq_compat with (An × An - (An × An - Bn))%Rseq.
 intro; unfold Rseq_minus, Rseq_mult; ring.

 apply Rseq_cv_minus_compat.
  apply An_squared_cv.
  apply An_squared_Bn_cv.
Qed.

Linking sums on nat and sums on Z


Lemma bnz_bntg : n, bntg n = bnz (Z_of_nat n).
Proof.
intro n.
unfold bntg, bnz.
destruct n.
 simpl; field.

 rewrite <- INR_IZR_INZ.
 field.
 INR_solve.
Qed.

Lemma bnz_bntg_neg : n, bntg_neg n = bnz (- Z_of_nat n).
Proof.
intro n.
unfold bntg_neg, bnz.
destruct n.
 simpl; field.

 rewrite Ropp_Ropp_IZR.
 rewrite <- INR_IZR_INZ.
 field.
 rewrite plus_1_S.
 replace (2 × - (1 + INR n) + 1) with (- (1 + 2 × INR n)) by ring.
 apply Ropp_neq_0_compat.
 repeat INR_solve.
Qed.

Lemma bisum_bnz_bntg : (sum_f_R0 bntg + (sum_f_R0 bntg_neg - 1))%Rseq == bisum bnz.
Proof.
intro n.
induction n.
 compute; field.

 simpl bisum.
 rewrite <- IHn.
 unfold Rseq_minus.
 unfold Rseq_plus.
 unfold Rseq_constant.
 repeat rewrite tech5.
 repeat rewrite bnz_bntg_neg.
 repeat rewrite bnz_bntg.
 replace (Zneg (P_of_succ_nat n)) with (- Z_of_nat (S n))%Z by trivial.
 replace (Zpos (P_of_succ_nat n)) with (Z_of_nat (S n))%Z by trivial.
 ring.
Qed.

Definition sumbntg := let (l, _) := Rser_cv_bntg in l.

Lemma Sum_bntg : Rser_cv bntg sumbntg.
Proof.
unfold sumbntg.
destruct Rser_cv_bntg; assumption.
Qed.

Lemma bntg_shift_neg_compat : Rseq_shift bntg_neg == bntg.
intro n.
unfold Rseq_shift.
unfold bntg.
unfold bntg_neg.
rewrite S_INR.
simpl pow.
field; split.
 INR_solve.
 replace (-2 × (INR n + 1) + 1) with (- (2 × (INR n) + 1)) by field.
 apply Ropp_neq_0_compat.
 INR_solve.
Qed.

Lemma Sum_bntg_neg : Rser_cv bntg_neg (sumbntg + 1).
Proof.
apply Rser_cv_shift_rev2.
eapply Rser_cv_ext.
 apply bntg_shift_neg_compat.
 replace (sumbntg + 1 - bntg_neg 0) with sumbntg by (compute; field).
 apply Sum_bntg.
Qed.

Lemma Sum_bnz : Rseq_cv Bn (2 × sumbntg).
Proof.
eapply Rseq_cv_eq_compat; [symmetry; apply bisum_bnz_bntg | ].
replace (2 × sumbntg) with (sumbntg + ((sumbntg + 1) - 1)) by field.
apply Rseq_cv_plus_compat; [apply Sum_bntg | ].
apply Rseq_cv_minus_compat; [ | apply Rseq_constant_cv].
apply Sum_bntg_neg.
Qed.

Lemma sumbntg_val : sumbntg = PI ^ 2 / 8.
Proof.
apply Rmult_eq_reg_l with 2.
 replace (2 × (PI ^ 2 / 8)) with (PI ^ 2 / 4) by field.
 apply (Rseq_cv_unique _ _ _ Sum_bnz Bn_cv).
 assert(0 < 2) by fourier; auto with ×.
Qed.

Lemma odd_zeta : Rser_cv bntg (PI ^ 2 / 8).
Proof.
rewrite <- sumbntg_val.
apply Sum_bntg.
Qed.

Linking even terms of the 1/n² series to the series itself


Lemma odd_zeta_evens : Rser_cv (evens (Rseq_shift Rseq_square_inv)) (PI ^ 2 / 8).
apply Rser_cv_ext with bntg.
 intro n.
 unfold Rseq_shift, evens, Rseq_square_inv, bntg.
 replace (INR (S (2 × n))) with (2 × INR n + 1); [reflexivity | ].
 replace (S n) with (1 + n)%nat by reflexivity.
 INR_solve.
 do 2 (try rewrite <- plus_INR; try rewrite <- mult_INR).
 inject; omega.

 apply odd_zeta.
Qed.

Definition zeta2 := let (l, _) := Rser_cv_square_inv in l.

Lemma zeta2_half : Rser_cv (odds (Rseq_shift (Rseq_square_inv))) (zeta2 / 4).
Proof.
replace (zeta2 / 4) with (/4 × zeta2) by field.
assert (REW : a, (/4 × (4 × a))%Rseq == a).
 intros a n; unfold Rseq_mult, Rseq_inv; field.
 unfold Rseq_constant.
 apply Rgt_not_eq ; fourier.

 eapply Rser_cv_ext.
  symmetry ; apply REW.

  apply (Rser_cv_scal_compat_l _ _ (/ 4)).
  eapply Rser_cv_ext.
   2:unfold zeta2.
   2:destruct Rser_cv_square_inv as [l H].
   2:apply H.

   intro n.
   unfold Rseq_mult, odds, Rseq_shift, Rseq_square_inv, Rseq_constant.
   replace (S (S (2 × n))) with (mult 2 (S n)) by omega.
   replace (INR (2 × (S n))) with (2 × INR (S n)) by (rewrite mult_INR; trivial).
   unfold Rseq_square_inv_s.
   field.
   apply not_0_INR; omega.
Qed.

Final result with free variables

Lemma zeta2_val : zeta2 = PI ^ 2 / 6.
Proof.
apply Rmult_eq_reg_l with (3 / 4);
 [ | intro H; apply (Rmult_eq_compat_l 4) in H; field_simplify in H; fourier].
replace (3 / 4 × zeta2) with (zeta2 - zeta2 / 4) by field.
replace (3 / 4 × (PI ^ 2 / 6)) with (PI ^ 2 / 8) by field.
eapply Rser_cv_unique.
 apply Rser_cv_minus_compat.
  unfold zeta2.
  destruct Rser_cv_square_inv as [x H].
  apply H.

  2:apply remove_odds.
   apply zeta2_half.

   apply Rser_cv_square_inv.

 apply odd_zeta_evens.
Qed.

Coercion INR : nat >-> R.

Final theorem


Theorem zeta2_pi_2_6 : Rser_cv (fun n ⇒ 1 / (n + 1) ^ 2) (PI ^ 2 / 6).
Proof.
rewrite <- zeta2_val.
unfold zeta2.
eapply Rser_cv_ext.
 2:destruct Rser_cv_square_inv as [l H].
 2:apply H.

 intro n; unfold Rseq_shift, Rseq_square_inv_s.
 rewrite plus_1_S.
 field.
 INR_solve.
Qed.