Library Lebesgue.sum_Rbar_nonneg

This file is part of the Coq Numerical Analysis library
Copyright (C) Aubry, Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for the finite summation of extended real numbers.

Used logic axioms

Usage

This module may be used through the import of Lebesgue.Lebesgue_p, or Lebesgue.Lebesgue_p_wDep, where it is exported.

From Requisite Require Import stdlib_wR.
From Coq Require Import FinFun List Permutation.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import list_compl Rbar_compl.

Local Open Scope R_scope.
Local Open Scope list_scope.

Section Nonneg_fun.

Context {A:Type}.

Definition nonneg : (A Rbar) Prop :=
  fun f x, Rbar_le 0 (f x).

Lemma nonneg_ext :
   f g, ( x, f x = g x) nonneg f nonneg g.
Proof.
intros f g H Hf x.
now rewrite <- H.
Qed.

Lemma nonneg_constant :
   a, Rbar_le 0 a nonneg (fun _a).
Proof.
now intros.
Qed.

Lemma nonneg_0 : nonneg (fun _ ⇒ 0).
Proof.
intros _; apply Rbar_le_refl.
Qed.

Lemma nonneg_charac : E, nonneg (charac E).
Proof.
intros E x; apply charac_ge_0.
Qed.

Lemma nonneg_plus:
   (f g : A Rbar),
    nonneg f nonneg g
    nonneg (fun xRbar_plus (f x) (g x)).
Proof.
  intros f g H1 H2.
  intros x.
  generalize (H1 x); generalize (H2 x).
  case (f x); case (g x); try easy.
  simpl; intros; now apply Rplus_le_le_0_compat.
Qed.

Lemma nonneg_plus_R :
   f g : A R,
    nonneg f nonneg g nonneg (fun xf x + g x).
Proof.
intros f g Hf Hg.
apply nonneg_ext with (fun xRbar_plus (f x) (g x)); try easy.
now apply nonneg_plus.
Qed.

Lemma nonneg_mult :
   f g,
    nonneg f nonneg g
    nonneg (fun xRbar_mult (f x) (g x)).
Proof.
intros f g H1 H2.
intros x.
generalize (H1 x); generalize (H2 x).
case (f x); case (g x); try easy.
simpl; intros; now apply Rmult_le_pos.
intros r _ Hr; simpl in Hr.
unfold Rbar_mult, Rbar_mult'.
case (Rle_dec 0 r); intros L.
2: contradict L; easy.
case (Rle_lt_or_eq_dec 0 r L); try easy.
intros _; apply Rbar_le_refl.
intros r Hr _; simpl in Hr.
unfold Rbar_mult, Rbar_mult'.
case (Rle_dec 0 r); intros L.
2: contradict L; easy.
case (Rle_lt_or_eq_dec 0 r L); try easy.
intros _; apply Rbar_le_refl.
Qed.

Lemma nonneg_mult_R :
   f g : A R,
    nonneg f nonneg g nonneg (fun xf x × g x).
Proof.
intros f g Hf Hg.
apply nonneg_ext with (fun xRbar_mult (f x) (g x)); try easy.
now apply nonneg_mult.
Qed.

Lemma nonneg_scal : (f : A Rbar) l ,
  nonneg f Rbar_le 0 l
  nonneg (fun xRbar_mult l (f x)).
Proof.
intros f l H1 H2.
now apply nonneg_mult.
Qed.

Lemma nonneg_scal_R :
   a (f : A R), 0 a nonneg f nonneg (fun xa × f x).
Proof.
intros.
apply nonneg_ext with (fun xRbar_mult a (f x)); try easy.
now apply nonneg_scal.
Qed.

Lemma nonneg_scal_charac :
   a E, 0 a nonneg (fun xa × charac E x).
Proof.
intros a E Ha.
apply nonneg_ext with (fun xRbar_mult a (charac E x)); try now simpl.
apply nonneg_scal; try now simpl.
apply nonneg_charac.
Qed.

Lemma nonneg_Sup_seq :
   f : nat A Rbar,
    ( n, nonneg (f n))
    nonneg (fun xSup_seq (fun nf n x)).
Proof.
intros f Hf x; trans (f 0%nat x).
apply Hf.
apply (Sup_seq_ub (fun nf n x)).
Qed.

Lemma nonneg_Inf_seq :
   f : nat A Rbar,
    ( n, nonneg (f n))
    nonneg (fun xInf_seq (fun nf n x)).
Proof.
intros f Hf x.
apply (Inf_seq_glb (fun nf n x)).
intros; apply Hf.
Qed.

Lemma nonneg_Lim_seq_Rbar :
   (f : nat A Rbar),
    ( n, nonneg (f n))
    nonneg (fun xLim_seq_Rbar (fun n : natf n x)).
Proof.
intros f H.
unfold Lim_seq_Rbar.
rewrite @fun_ext with (g:=fun x
      Rbar_mult (/ 2)
        (Rbar_plus (LimSup_seq_Rbar (fun nf n x)) (LimInf_seq_Rbar (fun nf n x)))).
2: intros x; apply sym_eq, Rbar_mult_inv_is_div_pos.
apply nonneg_scal.
2: simpl; auto with real.
apply nonneg_plus.
intros x.
apply Rbar_le_trans with (2:=LimSup_LimInf_seq_Rbar_le _).
apply Rbar_le_trans with (2:=Sup_seq_ub _ 0%nat).
rewrite Inf_opp_sup.
assert (T: Rbar_opp 0 = 0).
simpl; f_equal; ring.
rewrite <- T; apply Rbar_opp_le.
apply Sup_seq_lub.
intros n; rewrite <- T; apply Rbar_opp_le.
apply H.
unfold LimInf_seq_Rbar.
intros x.
apply Rbar_le_trans with (2:=Sup_seq_ub _ 0%nat).
rewrite Inf_opp_sup.
assert (T: Rbar_opp 0 = 0).
simpl; f_equal; ring.
rewrite <- T; apply Rbar_opp_le.
apply Sup_seq_lub.
intros n; rewrite <- T; apply Rbar_opp_le.
apply H.
Qed.

Fixpoint nonneg_l (l : list Rbar) : Prop :=
  match l with
  | nilTrue
  | a :: l'Rbar_le 0 a nonneg_l l'
  end.

Lemma nonneg_l_In :
   (l : list Rbar), nonneg_l l x, In x l Rbar_le 0 x.
Proof.
intros l; induction l.
intros _ x H; contradict H.
intros (H1,H2) x Hx.
inversion Hx.
rewrite <- H; easy.
apply IHl; easy.
Qed.

Lemma In_nonneg_l : l, ( x, In x l Rbar_le 0 x) nonneg_l l.
Proof.
intros l; induction l.
easy.
intros H; split.
apply H.
apply in_eq.
apply IHl.
intros x Hx.
apply H.
now apply in_cons.
Qed.

Lemma Permutation_nonneg_l :
   l l', Permutation l l' nonneg_l l nonneg_l l'.
Proof.
intros l l' H1 H2.
apply In_nonneg_l.
intros x Hx.
apply nonneg_l_In with l.
easy.
apply Permutation_in with l'; easy.
Qed.

Lemma nonneg_l_app1 : l l', nonneg_l (l ++ l') nonneg_l l.
Proof.
intros l l' H.
apply In_nonneg_l.
intros x Hx.
apply nonneg_l_In with (l++l');try easy.
apply in_or_app;now left.
Qed.

Lemma nonneg_l_app2 : l l', nonneg_l (l ++ l') nonneg_l l'.
Proof.
intros l l' H.
apply In_nonneg_l.
intros x Hx.
apply nonneg_l_In with (l++l');try easy.
apply in_or_app;now right.
Qed.

Lemma nonneg_map :
   (f : A Rbar) l, nonneg f nonneg_l (map f l).
Proof.
intros f l H.
apply In_nonneg_l.
intros x Hx.
destruct ((proj1 (in_map_iff f l x)) Hx) as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply H.
Qed.

End Nonneg_fun.

Section sum_on_Rbar.


Fixpoint sum_Rbar (n : nat) (f : nat Rbar) : Rbar :=
  match n with
  | 0 ⇒ f 0%nat
  | S nRbar_plus (f (S n)) (sum_Rbar n f)
  end.

Lemma sum_Rbar_R :
   (u : nat R) n, sum_Rbar n u = sum_f_R0 u n.
Proof.
intros u n; induction n; simpl; try easy.
rewrite IHn; apply Rbar_plus_comm.
Qed.

Lemma sum_Rbar_ext :
   n f1 f2,
    ( i, (i n)%nat f1 i = f2 i)
    sum_Rbar n f1 = sum_Rbar n f2.
Proof.
induction n.
intros f1 f2 H; simpl.
apply H; auto with arith.
intros f1 f2 H; simpl.
rewrite (IHn f1 f2).
rewrite H; try easy; auto with arith.
intros i Hi; apply H.
auto with arith.
Qed.

Lemma sum_Rbar_is_finite :
   n f,
    ( i, (i n)%nat is_finite (f i))
    is_finite (sum_Rbar n f).
Proof.
intros n f Hf.
induction n.
simpl; now apply (Hf 0%nat).
simpl; unfold is_finite.
rewrite Rbar_plus_real.
rewrite <- Rbar_finite_plus; f_equal.
1,3: now apply (Hf (S n)).
1,2: apply IHn; intros i Hi; apply Hf; lia.
Qed.

Lemma sum_Rbar_ge_0 :
   f n,
    ( i, (i n)%nat Rbar_le 0 (f i))
    Rbar_le 0 (sum_Rbar n f).
Proof.
intros f; induction n.
intros H.
simpl (sum_Rbar 0 f).
apply H; auto with arith.
intros H.
simpl (sum_Rbar _ _).
replace (Finite 0) with (Rbar_plus 0 0).
apply Rbar_plus_le_compat.
apply H; auto with arith.
apply IHn.
intros i Hi; apply H; auto with arith.
simpl; f_equal; ring.
Qed.

Lemma sum_Rbar_ge_0_alt :
   {A : Type} (f : A Rbar) n u,
    nonneg f
    Rbar_le 0 (sum_Rbar n (fun i ⇒ (f (u i)))).
Proof.
intros A f n u H.
apply sum_Rbar_ge_0.
intros i Hi; apply H.
Qed.

Lemma sum_Rbar_end :
   f n,
    ( i, (i S n)%nat Rbar_le 0 (f i))
    sum_Rbar (S n) f = Rbar_plus (f 0%nat) (sum_Rbar n (fun if (S i))).
Proof.
intros f; induction n.
intros H; simpl.
apply Rbar_plus_comm.
intros H.
simpl (sum_Rbar (S n) _).
rewrite Rbar_plus_comm.
rewrite Rbar_plus_assoc.
rewrite (Rbar_plus_comm _ (f 0%nat)).
rewrite <- IHn.
generalize (S n); intros m; now simpl.
intros; apply H; auto with arith.
apply H; auto with arith.
apply sum_Rbar_ge_0.
intros; apply H; auto with arith.
apply H; auto with arith.
Qed.

Lemma sum_Rbar_0 : u n, ( n, u n = Finite 0) sum_Rbar n u = 0.
Proof.
intros f n Hfn.
induction n; simpl; try easy.
now rewrite IHn, Rbar_plus_0_r.
Qed.

Lemma sum_Rbar_one :
   f n i,
    ( j, (j n)%nat j i f j = Finite 0)
    (i n)%nat
    sum_Rbar n f = f i.
Proof.
intros f n i.
induction n.
intros Hj0 Hjn.
simpl.
destruct (eq_nat_dec i 0) as [H|H].
rewrite H; reflexivity.
lia.
intros H1 H2.
destruct (eq_nat_dec (S n) i) as [H|H].
rewrite <- H.
simpl.
rewrite <- Rbar_plus_0_r.
f_equal.
cut ( j, (j n)%nat f j = 0).
intros H0.
transitivity (sum_Rbar n (fun _ ⇒ 0)).
apply sum_Rbar_ext; try easy.
apply sum_Rbar_0; easy.
intros j H0.
apply H1; lia.
cut (i n)%nat; try lia.
cut (( j : nat, (j n)%nat j i f j = 0)); try auto.
intros H3 H4.
specialize (IHn H3 H4).
simpl.
rewrite IHn.
rewrite (H1 (S n) (Nat.le_refl (S n)) H).
now rewrite Rbar_plus_0_l.
Qed.

Lemma sum_Rbar_nondecreasing :
   f,
    nonneg f
     n, Rbar_le (sum_Rbar n f) (sum_Rbar (S n) f).
Proof.
intros f Hf n.
simpl; rewrite <- Rbar_plus_0_l at 1.
apply Rbar_plus_le_compat_r.
apply Hf.
Qed.

Lemma Sup_seq_sum_Rbar_stable :
   f N,
    nonneg f
    ( n, (N < n)%nat f n = 0)
    Sup_seq (fun nsum_Rbar n f) = sum_Rbar N f.
Proof.
intros f N Hf H.
apply Sup_seq_stable with (f:= fun isum_Rbar i f).
intros n; simpl.
rewrite <- (Rbar_plus_0_l (sum_Rbar n f)) at 1.
apply Rbar_plus_le_compat_r.
apply Hf.
intros n Hn; simpl.
rewrite H; auto with arith.
now rewrite Rbar_plus_0_l.
Qed.

Lemma Sup_seq_sum_Rbar_singl :
   f n0,
    nonneg f
    ( n, n n0 f n = 0)
    Sup_seq (fun nsum_Rbar n f) = f n0.
Proof.
intros u n0 Hu Hun.
assert (H : n, (n < n0)%nat sum_Rbar n u = 0).
intros n Hn.
induction n; simpl.
apply Hun; lia.
rewrite IHn, Rbar_plus_0_r.
apply Hun, Nat.lt_neq; assumption.
apply Nat.lt_trans with (S n); lia.
rewrite Sup_seq_sum_Rbar_stable with _ n0; try assumption.
2: intros n Hn; now apply Hun, not_eq_sym, Nat.lt_neq.
case_eq n0; simpl.
intros Hn0; try auto.
intros n Hn0.
rewrite H, Rbar_plus_0_r; [auto | lia].
Qed.

Lemma sum_Rbar_le :
   n (u1 u2 : nat Rbar),
    ( i, (i n)%nat Rbar_le (u1 i) (u2 i))
    Rbar_le (sum_Rbar n u1) (sum_Rbar n u2).
Proof.
intros n u1 u2 H; induction n; simpl.
apply H; lia.
apply Rbar_plus_le_compat.
apply H; lia.
apply IHn; intros i Hi.
apply H; lia.
Qed.

Lemma sum_Rbar_le_n :
   n1 n2 (u : nat Rbar),
    nonneg u (n1 n2)%nat
    Rbar_le (sum_Rbar n1 u) (sum_Rbar n2 u).
Proof.
intros n1 n2 u Hu Hn; induction n2.
rewrite Nat.le_0_r in Hn; rewrite Hn; apply Rbar_le_refl.
case (le_lt_eq_dec n1 (S n2)); try easy; clear Hn; intros Hn.
trans (sum_Rbar n2 u).
apply IHn2; lia.
now apply sum_Rbar_nondecreasing.
rewrite Hn; apply Rbar_le_refl.
Qed.

Lemma sum_Rbar_p_infty :
   (u : nat Rbar) n,
    ( i, (i n)%nat Rbar_le 0 (u i))
    ( i, (i n)%nat u i = p_infty)
    sum_Rbar n u = p_infty.
Proof.
intros u n Hu [i [Hi Hui]]; induction n; simpl.
rewrite Nat.le_0_r in Hi.
now rewrite Hi in Hui.
case (Nat.eq_dec i (S n)); intros Hi'.
rewrite Hi' in Hui; rewrite Hui.
rewrite Rbar_plus_comm; apply Rbar_plus_pos_pinfty.
apply sum_Rbar_ge_0; intros j Hj; apply Hu; lia.
destruct (ifflr (Nat.lt_gt_cases _ _ )Hi') as [Hi'' | Hi''].
apply Nat.lt_succ_r in Hi''.
rewrite IHn; try easy.
now apply Rbar_plus_pos_pinfty, Hu.
intros j Hj; apply Hu; lia.
lia.
contradict Hi''; lia.
Qed.

Lemma sum_Rbar_end_alt :
   (u : nat Rbar) n,
    nonneg u
    sum_Rbar (S n) u =
      Rbar_plus (u 0%nat) (sum_Rbar n (fun iu (S i))).
Proof.
intros; apply sum_Rbar_end; now intros.
Qed.

Lemma sum_Rbar_plus :
   n (u1 u2 : nat Rbar),
    nonneg u1 nonneg u2
    sum_Rbar n (fun pRbar_plus (u1 p) (u2 p)) =
      Rbar_plus (sum_Rbar n u1) (sum_Rbar n u2).
Proof.
induction n; intros u1 u2 H1 H2.
now simpl.
repeat rewrite sum_Rbar_end_alt; try easy.
2: intros i; now apply Rbar_plus_le_0.
rewrite IHn.
2,3: now intros i.
repeat rewrite Rbar_plus_assoc; try easy.
apply Rbar_plus_eq_compat_l.
repeat rewrite <- Rbar_plus_assoc; try easy.
apply Rbar_plus_eq_compat_r, Rbar_plus_comm.
6,7: apply Rbar_plus_le_0; try easy.
all: now apply sum_Rbar_ge_0_alt.
Qed.

Lemma sum_Rbar_scal_l :
   n (u : nat Rbar) a,
    nonneg u Rbar_le 0 a
    sum_Rbar n (fun pRbar_mult a (u p)) =
      Rbar_mult a (sum_Rbar n u).
Proof.
intros n u a Hu Ha; induction n.
now simpl.
simpl; rewrite IHn; try easy.
symmetry.
apply Rbar_mult_plus_distr_l; try easy.
now apply sum_Rbar_ge_0_alt.
Qed.

Lemma sum_Rbar_stable :
   (u : nat Rbar) n p,
    nonneg u
    ( q, (n < q)%nat u q = 0)
    (n p)%nat
    sum_Rbar p u = sum_Rbar n u.
Proof.
intros u n p Hu1 Hu2 H.
repeat rewrite <- Sup_seq_sum_Rbar_stable; try easy.
intros q Hq; apply Hu2; lia.
Qed.

End sum_on_Rbar.

Section Geometrical_series.

Lemma sum_Rbar_geom :
   n r, r 1 sum_Rbar n (pow r) = (1 - r ^ S n) / (1 - r).
Proof.
intros; rewrite sum_Rbar_R, Rbar_finite_eq.
now apply tech3.
Qed.

Lemma series_geom :
   r, Rabs r < 1
    Lim_seq_Rbar (fun nsum_Rbar n (pow r)) = / (1 - r).
Proof.
intros r H.
rewrite Lim_seq_Rbar_ext with (v := fun n(1 - r ^ S n) / (1 - r)).
2: intros; now apply sum_Rbar_geom, Rlt_not_eq, Rabs_lt_between.
rewrite Lim_seq_Rbar_R.
unfold Rdiv.
rewrite Lim_seq_scal_r with (a := / (1 - r)) (u := fun n ⇒ (1 - r ^ S n)).
rewrite <- Rbar_mult_1_l.
assert (H' : 0 < (/ (1 - r))).
apply Rinv_0_lt_compat.
apply Rlt_0_minus.
now apply Rabs_lt_between.
do 2 rewrite Rbar_mult_pos_eq_Rbar_mult with (Hr := H').
apply Rbar_mult_pos_eq.
rewrite Lim_seq_incr_1 with (u := fun n ⇒ 1 - r ^ n).
unfold Rminus.
rewrite Lim_seq_plus with (v := fun n- r ^ n).
2: apply ex_lim_seq_const.
2: {
  apply ex_lim_seq_ext with (u := fun n ⇒ 0 - r ^ n) (v := fun n- r ^ n).
    intros; field.
  apply ex_lim_seq_minus with (u := fun n ⇒ 0) (v := fun nr ^ n).
    apply ex_lim_seq_const.
    now apply ex_lim_seq_geom.
  now rewrite Lim_seq_const, Lim_seq_geom. }
rewrite Lim_seq_const, <- Rbar_plus_0_r.
apply Rbar_plus_eq_compat_l.
rewrite Lim_seq_opp; apply Rbar_opp_eq.
rewrite Rbar_opp_involutive, Lim_seq_geom; try easy.
rewrite Rbar_finite_opp; apply Rbar_finite_eq; lra.
now rewrite Lim_seq_const, Lim_seq_opp, Lim_seq_geom.
Qed.

Lemma series_geom_half_alt :
  Sup_seq (fun nsum_Rbar n (pow (/ 2))) = 2.
Proof.
rewrite Sup_seq_ext with (v := fun n(1 - (/ 2) ^ S n) / (1 - / 2)).
2: intros; apply sum_Rbar_geom; lra.
assert (H : 0 < 1 - / 2) by lra.
rewrite Sup_seq_ext with
    (v := fun nRbar_mult (/ (1 - / 2)) (1 - (/ 2) ^ S n)).
rewrite Sup_seq_scal_l; try lra.
apply Rbar_mult_eq_reg_l with (r := 1 - / 2); try lra.
rewrite Rbar_mult_assoc.
assert (Rbar_mult (1 - / 2) (/ (1 - / 2)) = 1).
apply Rbar_finite_eq ; lra.
rewrite H0.
rewrite Rbar_mult_1_l.
rewrite <- Lim_seq_incr_Sup_seq.
rewrite Lim_seq_minus.
rewrite Lim_seq_const, Lim_seq_incr_1, Lim_seq_geom, Rbar_finite_minus.
simpl; apply Rbar_finite_eq; lra.
apply Rabs_lt_between; split; lra.
apply ex_lim_seq_const.
apply ex_lim_seq_decr.
intros n; induction n; try lra.
simpl; rewrite <- Rmult_1_l; apply Rmult_le_compat_r; try lra.
rewrite <- Rmult_0_r with (r := /2); apply Rmult_le_compat_l; try lra.
rewrite <- Rmult_0_r with (r := /2); apply Rmult_le_compat_l; try lra.
apply pow_le; lra.
rewrite Lim_seq_const, Lim_seq_incr_1, Lim_seq_geom; try easy.
apply Rabs_lt_between; split; lra.
intros; simpl.
apply Rplus_le_compat_l with (r := 1),
    Ropp_le_contravar, Rmult_le_compat_l; try lra.
rewrite <- Rmult_1_l; apply Rmult_le_compat_r; try lra.
apply pow_le; lra.
intros; rewrite Rbar_finite_mult.
now rewrite Rmult_comm with (r1 := / (1 - / 2)).
Qed.

Lemma series_geom_half :
  Sup_seq (fun nsum_Rbar n (fun p(/ 2) ^ S p)) = 1.
Proof.
simpl.
rewrite Sup_seq_ext with
    (v := fun nRbar_mult (/ 2) (sum_Rbar n (pow (/ 2)))).
simpl; rewrite Sup_seq_scal_l; try lra.
rewrite series_geom_half_alt; simpl.
apply Rbar_finite_eq; field.
intros n; rewrite <- sum_Rbar_scal_l.
    apply sum_Rbar_ext; intros i Hi; now simpl.
    intros p; simpl; apply pow_le; lra.
    simpl; lra.
Qed.

End Geometrical_series.

Section sum_in_Rbar_l.

Definition sum_Rbar_l : list Rbar Rbar :=
  fun lfold_right Rbar_plus (Finite 0) l.

Lemma sum_Rbar_l_ge_0 : l, nonneg_l l Rbar_le 0 (sum_Rbar_l l).
Proof.
intros l.
induction l; intros Hl.
apply Rle_refl.
rewrite <- (Rbar_plus_0_l 0).
apply Rbar_plus_le_compat.
apply Hl.
apply IHl, Hl.
Qed.

Lemma sum_Rbar_l_sum_Rbar :
   l,
    nonneg_l l
    sum_Rbar_l l = sum_Rbar (length l - 1) (fun inth i l 0).
Proof.
intros l; case l.
intros H; now simpl.
clear l; intros a l.
replace (length (a::l)-1)%nat with (length l).
2: auto with arith.
generalize a; clear a.
induction l.
intros a H1; unfold sum_Rbar_l; simpl.
apply Rbar_plus_0_r.
intros a0 H1.
simpl (length _).
rewrite sum_Rbar_end.
apply trans_eq with (Rbar_plus a0 (sum_Rbar_l (a :: l))).
easy.
rewrite IHl.
easy.
apply H1.
intros i Hi.
change (nth i (a::l) 0) with (nth (S i) (a0::a::l) 0).
apply nonneg_l_In with (a0::a::l).
apply H1.
apply nth_In.
simpl; auto with arith.
Qed.

Lemma sum_Rbar_l_concat :
   l1 l2,
    nonneg_l l1 nonneg_l l2
    sum_Rbar_l (l1 ++ l2) = Rbar_plus (sum_Rbar_l l1) (sum_Rbar_l l2).
Proof.
intros l1 l2; unfold sum_Rbar_l.
induction l1.
intros _ _ ; simpl.
rewrite Rbar_plus_0_l; easy.
intros H1 H2; simpl.
rewrite IHl1; try easy.
apply sym_eq, Rbar_plus_assoc.
apply H1.
apply sum_Rbar_l_ge_0, H1.
apply sum_Rbar_l_ge_0, H2.
apply H1.
Qed.

Lemma sum_Rbar_l_Prop: (P:RbarProp),
    P 0
    ( x y, P x P y P (Rbar_plus x y))
     l, ( i, In i l P i)
         P (sum_Rbar_l l).
Proof.
  intros P H0 H1 l H2.
  induction l.
  simpl; auto.
  simpl.
  apply H1.
  apply H2.
  apply in_eq.
  apply IHl.
  intros i Hi.
  apply H2.
  simpl.
  right.
  assumption.
Qed.

Lemma sum_Rbar_l_is_finite :
   l,
    ( x, In x l is_finite x)
    is_finite (sum_Rbar_l l).
Proof.
intros l Hl.
apply sum_Rbar_l_Prop; try easy.
intros x y Hx Hy; unfold is_finite.
rewrite Rbar_plus_real; try easy.
rewrite <- Rbar_finite_plus; now f_equal.
Qed.

Lemma sum_Rbar_l_mult :
   a l,
    nonneg_l l
    Rbar_mult a (sum_Rbar_l l) = sum_Rbar_l (map (fun xRbar_mult a x) l).
Proof.
intros a; induction l.
intros H; simpl; apply Rbar_mult_0_r.
intros H; simpl.
rewrite <- IHl.
apply Rbar_mult_plus_distr_l.
apply H.
apply sum_Rbar_l_ge_0, H.
apply H.
Qed.

Lemma Rbar_plus_sum_Rbar_l :
   {A:Type} (f g : A Rbar) l,
    ( x, In x l Rbar_le 0 (f x))
    ( x, In x l Rbar_le 0 (g x))
    Rbar_plus (sum_Rbar_l (map f l)) (sum_Rbar_l (map g l)) =
      sum_Rbar_l (map (fun xRbar_plus (f x) (g x)) l).
Proof.
intros A f g; induction l.
intros _ _; simpl; f_equal; ring.
intros H1 H2.
assert (K1: Rbar_le 0 (sum_Rbar_l (map f l))).
apply sum_Rbar_l_ge_0; apply In_nonneg_l.
intros x Hx; apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)); rewrite <- Hy1.
now apply H1, in_cons.
assert (K2: Rbar_le 0 (sum_Rbar_l (map g l))).
apply sum_Rbar_l_ge_0; apply In_nonneg_l.
intros x Hx; apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)); rewrite <- Hy1.
now apply H2, in_cons.
simpl; rewrite <- IHl.
rewrite 2!Rbar_plus_assoc; try assumption;
    try apply H1; try apply H2; try apply in_eq.
f_equal.
rewrite Rbar_plus_comm; rewrite Rbar_plus_assoc;
   try assumption; try apply H2; try apply in_eq.
f_equal; apply Rbar_plus_comm.
apply Rbar_plus_le_0; easy.
apply Rbar_plus_le_0; try easy.
apply H2, in_eq.
intros x Hx; apply H1, in_cons; easy.
intros x Hx; apply H2, in_cons; easy.
Qed.

Lemma sum_Rbar_l_switch :
   {A : Type} (G : A A Rbar) l1 l2,
    ( x1 x2, In x1 l1 In x2 l2 Rbar_le 0 (G x1 x2))
    sum_Rbar_l (map (fun x1sum_Rbar_l (map (fun x2G x1 x2) l2)) l1) =
      sum_Rbar_l (map (fun x2sum_Rbar_l (map (fun x1G x1 x2) l1)) l2).
Proof.
intros G; induction l1.
intros l2 _; simpl.
induction l2; simpl; try easy.
rewrite <- IHl2; simpl.
f_equal; ring.
intros l2 HG; simpl.
rewrite IHl1.
clear IHl1; induction l2.
simpl; f_equal; ring.
simpl.
rewrite <- IHl2.
rewrite <- 2!Rbar_plus_assoc; try easy.
f_equal.
rewrite 2!Rbar_plus_assoc; try easy.
f_equal.
now rewrite Rbar_plus_comm.
apply HG; apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
now apply in_cons.
apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
apply in_eq.
now apply in_cons.
apply HG; apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
apply in_eq.
now apply in_cons.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
now apply in_cons.
apply in_eq.
apply Rbar_plus_le_0.
apply HG; apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
now apply in_cons.
apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
apply in_eq.
now apply in_cons.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros z Hz.
apply in_map_iff in Hz.
destruct Hz as (t,(Ht1,Ht2)).
rewrite <- Ht1; apply HG; now apply in_cons.
apply Rbar_plus_le_0.
apply HG; apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
apply in_eq.
now apply in_cons.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply HG.
now apply in_cons.
apply in_eq.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx.
apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros z Hz.
apply in_map_iff in Hz.
destruct Hz as (t,(Ht1,Ht2)).
rewrite <- Ht1; apply HG; now apply in_cons.
intros x y Hx Hy; apply HG; try easy.
apply in_cons; easy.
intros x y Hx Hy; apply HG; try easy.
apply in_cons; easy.
Qed.

Lemma sum_Rbar_l_map_select_eq :
   {A : Type} P (f : A Rbar) l,
    ( y, In y l ¬P y f y = 0)
    sum_Rbar_l (map f l) = sum_Rbar_l (map f (select P l)).
Proof.
intros E P f l; induction l.
simpl; easy.
intros H; simpl.
case (in_dec P a); intros H2.
simpl; rewrite <- IHl; try easy.
intros y Hy1 Hy2; apply H; try easy.
now apply in_cons.
rewrite (H a); try easy.
rewrite Rbar_plus_0_l.
apply IHl.
intros y Hy1 Hy2; apply H; try easy.
now apply in_cons.
apply in_eq.
Qed.

Lemma sum_Rbar_l_Perm :
   l1 l2,
    Permutation l1 l2 nonneg_l l1
    sum_Rbar_l l1 = sum_Rbar_l l2.
Proof.
generalize (Permutation_ind
  (fun l1 l2nonneg_l l1 sum_Rbar_l l1 = sum_Rbar_l l2)).
intros T; apply T; clear T; try easy.
intros x l1 l2 H1 H2 H3; simpl.
rewrite H2; try easy.
now inversion H3.
intros x y l H; simpl.
rewrite <- 2!Rbar_plus_assoc.
now rewrite (Rbar_plus_comm x y).
inversion H; now inversion H1.
now inversion H.
apply sum_Rbar_l_ge_0.
inversion H; now inversion H1.
now inversion H.
inversion H; now inversion H1.
apply sum_Rbar_l_ge_0.
inversion H; now inversion H1.
intros l1 l2 l3 H1 H2 H3 H4 H5.
rewrite H2; try easy.
apply H4.
apply Permutation_nonneg_l with l1; easy.
Qed.


Definition sum_Rbar_map : {A : Type}, list A (A Rbar) Rbar :=
  fun A l fsum_Rbar_l (map f l).

Lemma sum_Rbar_map_cons :
   {A : Type} a l (f : A Rbar),
    sum_Rbar_map (a :: l) f = Rbar_plus (f a) (sum_Rbar_map l f).
Proof.
intros A a l f; unfold sum_Rbar_map; now simpl.
Qed.

Lemma sum_Rbar_map_ext_f :
   {A : Type} l (f1 f2 : A Rbar),
    ( x, In x l f1 x = f2 x)
    sum_Rbar_map l f1 = sum_Rbar_map l f2.
Proof.
intros A l f1 f2; induction l.
easy.
intros H; rewrite 2!sum_Rbar_map_cons.
rewrite H.
rewrite IHl; try easy.
intros x Hx; apply H; now apply in_cons.
apply in_eq.
Qed.


Lemma sum_Rbar_map_sum_Rbar :
   {A : Type} a0 (f : A Rbar) l,
    (l nil f a0 = 0)
    ( x, In x l Rbar_le 0 (f x))
    sum_Rbar_map l f = sum_Rbar (length l - 1) (fun if (nth i l a0)).
Proof.
intros A a0 f l H1 H2.
case_eq l.
intros H3; unfold sum_Rbar_map; simpl.
case H1; easy.
intros a l' H3; rewrite <- H3.
unfold sum_Rbar_map.
rewrite sum_Rbar_l_sum_Rbar.
rewrite length_map.
apply sum_Rbar_ext.
intros i Hi.
rewrite map_nth_alt with (da:=a0); auto with arith.
assert (0 < length l)%nat; auto with zarith.
rewrite H3; simpl; auto with arith.
apply In_nonneg_l.
intros x Hx; apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; now apply H2.
Qed.

Lemma sum_Rbar_map_select_eq :
   {A : Type} P (f : A Rbar) l,
    ( y, In y l ¬P y f y = 0)
    sum_Rbar_map l f = sum_Rbar_map (select P l) f.
Proof.
intros A P f l; induction l.
simpl; easy.
intros H; simpl; rewrite sum_Rbar_map_cons.
case (in_dec P a); intros H2.
rewrite sum_Rbar_map_cons; rewrite <- IHl; try easy.
intros y Hy1 Hy2; apply H; try easy.
now apply in_cons.
rewrite (H a); try easy.
rewrite Rbar_plus_0_l.
apply IHl.
intros y Hy1 Hy2; apply H; try easy.
now apply in_cons.
apply in_eq.
Qed.

Lemma sum_Rbar_map_switch :
   {A : Type} (G : A A Rbar) l1 l2,
    ( x y, In x l1 In y l2 Rbar_le 0 (G x y))
    sum_Rbar_map l1 (fun xsum_Rbar_map l2 (fun yG x y)) =
      sum_Rbar_map l2 (fun ysum_Rbar_map l1 (fun xG x y)).
Proof.
intros G l1 l2; unfold sum_Rbar_map.
apply sum_Rbar_l_switch.
Qed.

Lemma sum_Rbar_map_ge_0 :
   {A : Type} (f : A Rbar) l,
    ( x, In x l Rbar_le 0 (f x))
    Rbar_le 0 (sum_Rbar_map l f).
Proof.
intros A f l H.
apply sum_Rbar_l_ge_0.
apply In_nonneg_l.
intros x Hx; apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; now apply H.
Qed.

Lemma sum_Rbar_map_le_0 : {E: Type},
     (f:ER) l, ( i, In i l Rbar_le (f i) 0)
         Rbar_le (sum_Rbar_map l (fun if i)) 0.
Proof.
  intros E f l Hl.
  induction l; simpl.
  apply Rle_refl.
  rewrite <- (Rbar_plus_0_l 0).
  apply Rbar_plus_le_compat.
  apply Hl.
  simpl.
  left.
  reflexivity.
  apply IHl.
  intros i Hi.
  apply Hl.
  simpl.
  right.
  assumption.
Qed.

Lemma sum_Rbar_map_map :
   {A B : Type} (f : A B) g l,
    sum_Rbar_map (map f l) g = sum_Rbar_map l (fun xg (f x)).
Proof.
intros A B f g l; unfold sum_Rbar_map.
now rewrite map_map.
Qed.

Lemma sum_Rbar_map_is_finite :
   {E : Type} (f : E Rbar) l,
    ( x, In x l is_finite (f x))
    is_finite (sum_Rbar_map l f).
Proof.
intros E f l H.
apply sum_Rbar_l_is_finite; intros y Hy.
apply in_map_inv in Hy; destruct Hy as [x [Hx1 Hx2]].
rewrite Hx2; now apply H.
Qed.

Lemma sum_Rbar_map_Rbar_mult :
   {A : Type} (f : A Rbar) a l,
    ( x, In x l Rbar_le 0 (f x))
    Rbar_mult a (sum_Rbar_map l f) = sum_Rbar_map l (fun xRbar_mult a (f x)).
Proof.
intros A f a l.
rewrite <- sum_Rbar_map_map with (g:= fun xRbar_mult a x).
unfold sum_Rbar_map at 1.
intros H.
cut (nonneg_l (map f l)).
generalize (map f l).
clear H l; intros l; induction l.
intros _; simpl; unfold sum_Rbar_map; simpl.
apply Rbar_mult_0_r.
intros H; rewrite sum_Rbar_map_cons.
rewrite <- IHl.
simpl.
apply Rbar_mult_plus_distr_l.
apply H.
apply sum_Rbar_l_ge_0, H.
apply H.
apply In_nonneg_l.
intros x Hx; apply in_map_iff in Hx.
destruct Hx as (y,(Hy1,Hy2)).
rewrite <- Hy1; apply H; easy.
Qed.

Lemma Rbar_plus_sum_Rbar_map :
   {A : Type} (f g : A Rbar) l,
    ( x, In x l Rbar_le 0 (f x))
    ( x, In x l Rbar_le 0 (g x))
    Rbar_plus (sum_Rbar_map l f) (sum_Rbar_map l g) =
      sum_Rbar_map l (fun xRbar_plus (f x) (g x)).
Proof.
intros.
now apply Rbar_plus_sum_Rbar_l.
Qed.

Lemma sum_Rbar_map_concat :
   {A : Type} l1 l2 (f : A Rbar),
    nonneg f
    sum_Rbar_map (l1 ++ l2) f = Rbar_plus (sum_Rbar_map l1 f) (sum_Rbar_map l2 f).
Proof.
intros A l1 l2 f Hf.
unfold sum_Rbar_map; rewrite map_app.
apply sum_Rbar_l_concat.
apply nonneg_map; easy.
apply nonneg_map; easy.
Qed.

Lemma sum_Rbar_map_Perm :
   {A : Type} l1 l2 (f : A Rbar),
    Permutation l1 l2 nonneg f
    sum_Rbar_map l1 f = sum_Rbar_map l2 f.
Proof.
intros A l1 l2 f H1 H2.
apply sum_Rbar_l_Perm.
apply Permutation_map; easy.
apply nonneg_map; easy.
Qed.

Lemma sum_Rbar_map_Perm_strict :
   {A : Type} l1 l2 (f : A Rbar),
    Permutation l1 l2
    ( x, In x l1 Rbar_le 0 (f x))
    sum_Rbar_map l1 f = sum_Rbar_map l2 f.
Proof.
intros A l1 l2 f H1 H2.
apply sum_Rbar_l_Perm.
apply Permutation_map; easy.
apply In_nonneg_l.
intros y Hy.
apply in_map_iff in Hy.
destruct Hy as (z,(Hz1,Hz2)).
rewrite <- Hz1; apply H2; easy.
Qed.

Lemma sum_Rbar_map_ext_l :
   {A : Type} l1 l2 (f : A Rbar),
    select (fun x ⇒ (f x 0)) l1 = select (fun xf x 0) l2
    sum_Rbar_map l1 f = sum_Rbar_map l2 f.
Proof.
intros A l1 l2 f H.
rewrite sum_Rbar_map_select_eq with
   (P:=fun xf x 0).
rewrite sum_Rbar_map_select_eq with
   (P:=fun xf x 0) (l:=l2).
rewrite H; easy.
intros y K1 K2; case (Rbar_eq_dec (f y) 0); easy.
intros y K1 K2; case (Rbar_eq_dec (f y) 0); easy.
Qed.

Lemma sum_Rbar_map_ge :
   {A : Type} l (f1 f2 : A Rbar),
    ( x, In x l Rbar_le (f1 x) (f2 x))
    Rbar_le (sum_Rbar_map l f1) (sum_Rbar_map l f2).
Proof.
intros A l f1 f2 H.
induction l.
simpl.
apply Rle_refl.
do 2 rewrite sum_Rbar_map_cons.
apply Rbar_plus_le_compat.
apply H.
simpl ; now left.
apply IHl.
intros.
apply H.
now apply in_cons.
Qed.

Lemma Sup_seq_sum_Rbar_map :
   {A : Type} l (f : nat A Rbar),
    ( n, nonneg (f n))
    ( a n, In a l Rbar_le (f n a) (f (S n) a))
    Sup_seq (fun nsum_Rbar_map l (f n)) =
      sum_Rbar_map l (fun xSup_seq (fun nf n x)).
Proof.
intros A l f Hf.
induction l.
intros _; apply is_sup_seq_unique.
simpl; intros eps; split.
intros _; rewrite Rplus_0_l; apply eps.
0%nat; rewrite Rminus_0_l.
rewrite <- Ropp_0; apply Ropp_lt_contravar, eps.
intros H.
rewrite sum_Rbar_map_cons.
rewrite <- IHl.
rewrite <- Sup_seq_plus.
apply Sup_seq_ext.
intros n; apply sum_Rbar_map_cons.
intros n; apply H; try easy.
apply in_eq.
intros n.
apply sum_Rbar_map_ge.
intros x Hx; apply H; apply in_cons; easy.
apply ex_Rbar_plus_ge_0.
eapply Rbar_le_trans. 2: apply Sup_seq_ub.
apply (Hf 0%nat).
eapply Rbar_le_trans. 2: apply Sup_seq_ub.
apply sum_Rbar_map_ge_0.
intros y Hy; apply (Hf 0%nat).
intros b n Hb; apply H.
apply in_cons; easy.
Qed.

Lemma sum_Rbar_map_plus: {E: Type} (P:(ERbar)->Prop),
     P (fun t ⇒ 0)
    ( f g, P f P g P (fun tRbar_plus (f t) (g t)))
     (f : R E R) l, ( i, In i l P (f i))
        P (fun tsum_Rbar_map l (fun if i t)).
Proof.
  intros E P H H0 f l H1.
  induction l; simpl; auto.
  apply H0.
  apply H1.
  apply in_eq.
  apply IHl.
  intros i Hi.
  apply H1.
  apply in_cons; assumption.
Qed.

Lemma sum_Rbar_map_le :
   {A : Type} (l1 l2 : list A) (f : A Rbar),
    nonneg f
    incl_dup l1 l2
    Rbar_le (sum_Rbar_map l1 f) (sum_Rbar_map l2 f).
Proof.
intros A l1; induction l1 as [ | a].
intros l2 f Hf _; unfold sum_Rbar_map at 1.
simpl (sum_Rbar_l (map f Datatypes.nil)).
apply sum_Rbar_map_ge_0.
intros x Hx; apply Hf.
intros l2 f Hf (t1,(t2,(H1,H2))).
rewrite sum_Rbar_map_cons.
trans (Rbar_plus (f a) (sum_Rbar_map (t1++t2) f)).
apply Rbar_plus_le_compat_l.
apply IHl1; easy.
rewrite H1.
rewrite 2!sum_Rbar_map_concat; try easy.
rewrite sum_Rbar_map_cons.
rewrite Rbar_plus_comm, Rbar_plus_assoc.
apply Rbar_plus_le_compat_l.
rewrite Rbar_plus_comm; apply Rbar_le_refl.
apply sum_Rbar_map_ge_0; intros x _; apply Hf.
apply sum_Rbar_map_ge_0; intros x _; apply Hf.
apply Hf.
Qed.

Lemma sum_Rbar_sum_Rbar_map :
   (u : nat Rbar) n,
    nonneg u
    sum_Rbar n u = sum_Rbar_map (seq 0 (S n)) u.
Proof.
intros u n Hu.
rewrite sum_Rbar_map_sum_Rbar with (a0:=0%nat).
rewrite length_seq.
replace (S n -1)%nat with n by auto with arith.
apply sum_Rbar_ext; intros i Hi.
rewrite seq_nth; auto with arith.
left; easy.
intros x Hx; apply Hu.
Qed.

Lemma sum_Rbar_perm_le :
   (u : nat Rbar) (phi : nat nat) n,
    nonneg u
    bInjective (S n) phi
    Rbar_le (sum_Rbar n (fun pu (phi p)))
            (sum_Rbar (max_n phi n) u).
Proof.
intros u phi n Hu Hphi.
rewrite sum_Rbar_sum_Rbar_map.
2: intros x; apply Hu.
rewrite <- sum_Rbar_map_map.
rewrite sum_Rbar_sum_Rbar_map; try easy.
apply sum_Rbar_map_le; try easy.
induction n.
simpl (map phi (seq 0 1)).
simpl (max_n phi 0).
case (phi 0)%nat.
nil; nil; simpl; split; try easy.
intros l; (seq 0 (S l)); nil.
split; try easy.
apply nth_eq with 0%nat.
rewrite length_app; simpl.
rewrite 2!length_seq; auto with zarith.
rewrite length_seq.
intros i Hi.
assert (H: (i l i = S l)%nat) by lia.
destruct H.
rewrite app_nth1.
rewrite 2! seq_nth; lia.
rewrite length_seq; lia.
rewrite H, seq_nth; try lia.
rewrite app_nth2; rewrite length_seq; try lia.
replace (S l - S l)%nat with 0%nat by auto with arith.
simpl; lia.
rewrite (seq_app (S (S n)) (S n)); try auto with arith.
rewrite map_app.
replace (S (S n) - S n)%nat with 1%nat by lia.
simpl (map phi (seq (S n) 1)).
rewrite (seq_app (S (max_n phi (S n))) (S (max_n phi n))).
apply incl_dup_end_not_in.
apply IHn; intros p q Hp Hq; apply Hphi; lia.
intros K; apply in_map_iff in K.
destruct K as (m,(Hm1,Hm2)).
apply in_seq in Hm2.
absurd (S n < 0 + S n)%nat; auto with arith.
replace (S n) with m at 1; try apply Hm2.
apply Hphi; lia.
rewrite <- seq_app.
apply in_seq.
split; try auto with arith.
assert (phi (S n) max_n phi (S n))%nat; auto with zarith.
simpl; apply Nat.le_max_l.
all: simpl; apply le_n_S, Nat.le_max_r.
Qed.

Lemma sum_Rbar_map_prod :
   {A B : Type} (lA : list A) (lB : list B) (f : A B Rbar),
    ( a, nonneg (f a))
    sum_Rbar_map (list_prod lA lB) (fun abf (fst ab) (snd ab)) =
    sum_Rbar_map lA (fun asum_Rbar_map lB (fun bf a b)).
Proof.
intros A B lA lB f Hf.
induction lA as [ | a]; simpl.
now unfold sum_Rbar_map.
rewrite sum_Rbar_map_concat, sum_Rbar_map_cons.
2: clear a; intros a; apply Hf.
rewrite IHlA.
apply Rbar_plus_eq_compat_r.
now rewrite sum_Rbar_map_map.
Qed.

Lemma double_series_aux1 :
   (u : nat nat Rbar) (phi : nat nat × nat) n m i,
    ( p, nonneg (u p))
    Bijective phi
    ( p q j, (p n)%nat (q m)%nat
      phi j = (p, q) (j i)%nat)
    let u' := fun pqu (fst pq) (snd pq) in
    Rbar_le
      (sum_Rbar n (fun psum_Rbar m (fun qu p q)))
      (sum_Rbar i (fun ju' (phi j))).
Proof.
intros u phi n m i Hu Hphi Hb u'.
repeat rewrite sum_Rbar_sum_Rbar_map.
2: intros j; apply Hu.
2: intros p; apply sum_Rbar_ge_0; intros q _; apply Hu.
replace (sum_Rbar_map (seq 0 (S n)) (fun psum_Rbar m (fun qu p q)))
    with (sum_Rbar_map (seq 0 (S n))
            (fun psum_Rbar_map (seq 0 (S m)) (fun qu p q))).
2: apply sum_Rbar_map_ext_f; intros p _; now rewrite sum_Rbar_sum_Rbar_map.
rewrite <- sum_Rbar_map_prod; try easy.
rewrite <- sum_Rbar_map_map.
apply sum_Rbar_map_le.
intros pq; apply Hu.
now apply incl_dup_prod_seq.
Qed.

Lemma double_series_aux2 :
   (u : nat nat Rbar) (phi : nat nat × nat) n m i,
    ( n, nonneg (u n))
    Bijective phi
    ( j, (j i)%nat
      (fst (phi j) n)%nat (snd (phi j) m)%nat)
    let u' := fun pqu (fst pq) (snd pq) in
    Rbar_le
      (sum_Rbar i (fun ju' (phi j)))
      (sum_Rbar n (fun psum_Rbar m (fun qu p q))).
Proof.
intros u phi n m i Hu Hphi Hb u'.
repeat rewrite sum_Rbar_sum_Rbar_map.
2: intros p; apply sum_Rbar_ge_0; intros q _; apply Hu.
2: intros j; apply Hu.
replace (sum_Rbar_map (seq 0 (S n)) (fun psum_Rbar m (fun qu p q)))
    with (sum_Rbar_map (seq 0 (S n))
            (fun psum_Rbar_map (seq 0 (S m)) (fun qu p q))).
2: apply sum_Rbar_map_ext_f; intros p _; now rewrite sum_Rbar_sum_Rbar_map.
rewrite <- sum_Rbar_map_prod; try easy.
rewrite <- sum_Rbar_map_map.
apply sum_Rbar_map_le.
intros pq; apply Hu.
now apply incl_dup_seq_prod.
Qed.

Lemma Sup_seq_sum_Rbar :
   m (u : nat nat Rbar),
    ( p, nonneg (u p))
    ( p q, Rbar_le (u p q) (u (S p) q))
    Sup_seq (fun nsum_Rbar m (fun qu n q)) =
    sum_Rbar m (fun qSup_seq (fun nu n q)).
Proof.
intros m u Hu1 Hu2; induction m; try easy; simpl.
rewrite Sup_seq_plus; try easy.
apply Rbar_plus_eq_compat_l, IHm.
intros n; apply sum_Rbar_le; intros q _; apply Hu2.
apply ex_Rbar_plus_ge_0; apply Sup_seq_minor_le with (n := 0%nat) (M := 0).
2: apply sum_Rbar_ge_0; intros q _.
all: apply Hu1.
Qed.

Lemma double_series :
   (u : nat nat Rbar) (phi : nat nat × nat),
    ( n, nonneg (u n))
    Bijective phi
    let u' := fun pqu (fst pq) (snd pq) in
    Sup_seq (fun nsum_Rbar n (fun p
        Sup_seq (fun msum_Rbar m (fun qu p q)))) =
    Sup_seq (fun isum_Rbar i (fun ju' (phi j))).
Proof.
intros u phi Hu [psi [HN1 HN2]] u'.
  assert (Hphi : Bijective phi).
   psi; now split.
apply Rbar_le_antisym.
apply Sup_seq_lub; intros n.
rewrite <- Sup_seq_sum_Rbar.
2: intros m p; apply sum_Rbar_ge_0; intros q _; apply Hu.
2: intros p q; apply sum_Rbar_le_n; [apply Hu | lia].
apply Sup_seq_lub; intros m.
pose (i := max_n (fun pmax_n (fun qpsi (p, q)) m) n).
trans (sum_Rbar i (fun ju' (phi j))).
2: apply Sup_seq_ub with (u := fun i'sum_Rbar i' _).
apply double_series_aux1; try easy.
intros p q j Hp Hq Hj; apply f_equal with (f := psi) in Hj; rewrite HN1 in Hj.
rewrite Hj; unfold i.
apply Nat.le_trans with (max_n (fun q'psi (p, q')) m).
now apply max_n_correct with (f := fun q'psi (p, q')).
now apply max_n_correct with (f := fun p'max_n (fun q'psi (p', q')) m).
apply Sup_seq_lub; intros i.
pose (n := max_n (fun jfst (phi j)) i).
pose (m := max_n (fun jsnd (phi j)) i).
trans (sum_Rbar n (fun p
    Sup_seq (fun m'sum_Rbar m' (fun qu p q)))).
2: apply Sup_seq_ub with (u := fun n'sum_Rbar n' _).
trans (sum_Rbar n (fun psum_Rbar m (fun qu p q))).
2: { apply sum_Rbar_le; intros p Hp.
    apply Sup_seq_ub with (u := fun m'sum_Rbar m' _). }
apply double_series_aux2; try easy.
intros j Hj; split.
now apply max_n_correct with (f := fun jfst (phi j)).
now apply max_n_correct with (f := fun jsnd (phi j)).
Qed.

End sum_in_Rbar_l.