Require Import Reals utils.RealAdd.
Require Import Coquelicot.Hierarchy.
Require Import Morphisms Equivalence.
Require Import Lra.
Require Import utils.Utils.
Require Import List.
(* For const *)
Require Export Program.Basics.
Require Import Coquelicot.Coquelicot.

Set Bullet Behavior "Strict Subproofs".

Local Open Scope R.
Section rels.
  Context {Ts:Type}.

  Definition rv_le :=
    pointwise_relation Ts Rle.

  Global Instance rv_le_pre : PreOrder rv_le.
  Proof.
    unfold rv_le.
    constructor; intros.
    - intros ??; lra.
    - intros ??????.
      eapply Rle_trans; eauto.
  Qed.

  Global Instance rv_le_part : PartialOrder rv_eq rv_le.
  Proof.
    intros ??.
    split; intros eqq.
    - repeat red.
      repeat red in eqq.
      split; intros ?; rewrite eqq; lra.
    - destruct eqq as [le1 le2].
      intros y.
      specialize (le1 y).
      specialize (le2 y).
      lra.
  Qed.

  Definition Rbar_rv_le := pointwise_relation Ts Rbar_le.

  Global Instance Rbar_rv_le_pre : PreOrder Rbar_rv_le.
  Proof.
    unfold Rbar_rv_le.
    constructor; intros.
    - intros ??; apply Rbar_le_refl.
    - intros ??????.
      eapply Rbar_le_trans; eauto.
  Qed.

  Global Instance Rbar_rv_le_part : PartialOrder rv_eq Rbar_rv_le.
  Proof.
    intros ??.
    split; intros eqq.
    - repeat red.
      repeat red in eqq.
      split; intros ?; rewrite eqq; apply Rbar_le_refl.
    - destruct eqq as [le1 le2].
      intros y.
      specialize (le1 y).
      specialize (le2 y).
      now apply Rbar_le_antisym.
  Qed.

End rels.

Section defs.
  Context {Ts:Type}.

  Section funs.

    (* const is defined in Program.Basics *)

    Definition EventIndicator {P : Ts->Prop} (dec:forall x, {P x} + {~ P x}) : Ts -> R
      := fun omega => if dec omega then 1 else 0.

    Definition rvplus (rv_X1 rv_X2 : Ts -> R) :=
      (fun omega =>  (rv_X1 omega) + (rv_X2 omega)).

    Definition rvsum (Xn : nat -> Ts -> R) (n : nat) :=
      (fun omega => sum_n (fun n0 => Xn n0 omega) n).

    Definition rvscale (c:R) (rv_X : Ts -> R) :=
      fun omega => c * (rv_X omega).

    Definition rvopp (rv_X : Ts -> R) := rvscale (-1) rv_X.

    Definition rvminus (rv_X1 rv_X2 : Ts -> R) :=
      rvplus rv_X1 (rvopp rv_X2).

    Definition rvmult (rv_X1 rv_X2 : Ts -> R) := 
      fun omega => (rv_X1 omega) * (rv_X2 omega).

    Definition rvsqr (rv_X : Ts -> R) := fun omega => Rsqr (rv_X omega).
    Definition rvsqrt (rv_X : Ts -> R) := fun omega => sqrt (rv_X omega).    

    Definition rvpow (rv_X : Ts -> R) (n:nat) := fun omega => pow (rv_X omega) n.

    Definition rvpower (rv_X1 rv_X2 : Ts -> R) := fun omega => power (rv_X1 omega) (rv_X2 omega).

    Definition rvabs  (rv_X : Ts -> R) := fun omega => Rabs (rv_X omega).

    Definition rvsign (rv_X : Ts -> R) := fun omega => sign(rv_X omega).

    Lemma rvabs_pos (rv_X : Ts -> R) :
      rv_le (const 0) (rvabs rv_X).
    Proof.
      intro x.
      unfold const, rvabs.
      apply Rabs_pos.
    Qed.

    Definition rvchoice (c:Ts -> bool) (rv_X1 rv_X2 : Ts -> R)
      := fun omega => if c omega then  rv_X1 omega else rv_X2 omega.

    Definition Rbar_rvchoice (c:Ts -> bool) (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => if c omega then  rv_X1 omega else rv_X2 omega.

    Definition bvmin_choice (rv_X1 rv_X2:Ts -> R) : Ts -> bool
      := fun omega => if Rle_dec (rv_X1 omega) (rv_X2 omega) then true else false.

    Definition Rbar_bvmin_choice (rv_X1 rv_X2:Ts -> Rbar) : Ts -> bool
      := fun omega => if Rbar_le_dec (rv_X1 omega) (rv_X2 omega) then true else false.

    Definition bvmax_choice (rv_X1 rv_X2:Ts -> R) : Ts -> bool
      := fun omega => if Rle_dec (rv_X1 omega) (rv_X2 omega) then false else true.

    Definition Rbar_bvmax_choice (rv_X1 rv_X2:Ts -> Rbar) : Ts -> bool
      := fun omega => if Rbar_le_dec (rv_X1 omega) (rv_X2 omega) then false else true.

    Definition rvmax  (rv_X1 rv_X2 : Ts -> R)
      := fun omega => Rmax (rv_X1 omega) (rv_X2 omega).

    Definition Rbar_rvmax  (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => Rbar_max (rv_X1 omega) (rv_X2 omega).

    Definition rvmin  (rv_X1 rv_X2 : Ts -> R)
      := fun omega => Rmin (rv_X1 omega) (rv_X2 omega). 

    Definition Rbar_rvmin  (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => Rbar_min (rv_X1 omega) (rv_X2 omega). 

    Definition rvmaxlist (X : nat -> Ts -> R) (N : nat) : Ts -> R :=
      fun (omega : Ts) => Rmax_list_map (List.seq 0 (S N)) (fun n => X n omega).

    Program Definition pos_fun_part {Ts:Type} (f : Ts -> R) : (Ts -> nonnegreal) :=
      fun x => mknonnegreal (Rmax (f x) 0) _.
    Next Obligation.
      apply Rmax_r.
    Defined.
    
    Program Definition neg_fun_part {Ts:Type} (f : Ts -> R) : (Ts -> nonnegreal) :=
      fun x => mknonnegreal (Rmax (- f x) 0) _.
    Next Obligation.
      apply Rmax_r.
    Defined.

    Definition rvclip {Ts:Type} (f : Ts -> R) (c : nonnegreal) : Ts -> R
      := fun x => if Rgt_dec (f x) c then c else
                    (if Rlt_dec (f x) (-c) then (-c) else f x).

    Lemma rvclip_le_c (rv_X : Ts -> R) (c : nonnegreal) :
      rv_le (rvclip rv_X c) (const c).
    Proof.
      intro x0.
      unfold rvclip, const.
      assert (0 <= c) by apply (cond_nonneg c).
      match_destr; [lra |].
      match_destr; lra.
    Qed.
    
    Lemma rvclip_negc_le (rv_X : Ts -> R) (c : nonnegreal) :
      rv_le (const (-c)) (rvclip rv_X c).
    Proof.
      intro x0.
      unfold rvclip, const.
      assert (0 <= c) by apply (cond_nonneg c).
      match_destr; [lra |].
      match_destr; lra.
    Qed.

    Lemma rvclip_abs_bounded rv_X c :
      forall omega : Ts, Rabs ((rvclip rv_X c) omega) <= c.
    Proof.
      intros.
      assert (0 <= c) by apply (cond_nonneg c).
      unfold rvclip.
      match_destr.
      rewrite Rabs_pos_eq; lra.
      match_destr.
      rewrite Rabs_Ropp.
      rewrite Rabs_pos_eq; lra.      
      apply Rabs_le.
      lra.
    Qed.

    Lemma rvclip_abs_le_c (rv_X : Ts -> R) (c : nonnegreal) :
      rv_le (rvabs (rvclip rv_X c)) (const c).
    Proof.
      intro x.
      unfold rvabs, const.
      apply rvclip_abs_bounded.
    Qed.

  End funs.

  Section eqs.
    Existing Instance rv_eq_equiv.

    Global Instance rvplus_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvplus.
    Proof.
      unfold rv_eq, rvplus, pointwise_relation.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvscale_proper : Proper (eq ==> rv_eq ==> rv_eq ) rvscale.
    Proof.
      unfold rv_eq, rvopp, Proper, rvscale, respectful, pointwise_relation.
      intros ??? x y eqq z.
      subst.
      now rewrite eqq.
    Qed.

    Global Instance rvopp_proper : Proper (rv_eq ==> rv_eq ) rvopp.
    Proof.
      unfold rv_eq, rvopp, Proper, rvscale, respectful, pointwise_relation.
      intros x y eqq z.
      now rewrite eqq.
    Qed.

    Global Instance rvminus_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvminus.
    Proof.
      unfold rv_eq, rvminus, rvplus, rvopp, rvscale, pointwise_relation.
      intros ???????.
      now rewrite H, H0.
    Qed.
    
    Global Instance rvmult_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvmult.
    Proof.
      unfold rv_eq, rvmult.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvsqr_proper : Proper (rv_eq ==> rv_eq) rvsqr.
    Proof.
      unfold rv_eq, rvsqr, Proper, respectful, pointwise_relation.
      intros x y eqq z.
      unfold Rsqr.
      rewrite eqq.
      trivial.
    Qed.

    Global Instance rvpow_proper : Proper (rv_eq ==> eq ==> rv_eq) rvpow.
    Proof.
      unfold rv_eq, rvpow, Proper, respectful, pointwise_relation.
      intros x y eqq z ???.
      subst.
      rewrite eqq.
      trivial.
    Qed.

    Global Instance rvpower_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvpower.
    Proof.
      unfold rv_eq, rvpower, Proper, respectful, pointwise_relation.
      intros x y eqq1 z ? eqq2 ?.
      subst.
      now rewrite eqq1, eqq2.
    Qed.

    Global Instance rvabs_proper : Proper (rv_eq ==> rv_eq) rvabs.
    Proof.
      unfold rv_eq, rvabs, Proper, respectful, pointwise_relation.
      intros x y eqq z.
      unfold Rabs.
      rewrite eqq.
      trivial.
    Qed.

    Global Instance rvmax_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvmax.
    Proof.
      unfold rv_eq, rvmax.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvmin_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvmin.
    Proof.
      unfold rv_eq, rvmin.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance Rbar_rvmax_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) Rbar_rvmax.
    Proof.
      unfold rv_eq, Rbar_rvmax.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance Rbar_rvmin_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) Rbar_rvmin.
    Proof.
      unfold rv_eq, Rbar_rvmin.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvsign_proper : Proper (rv_eq ==> rv_eq) rvsign.
    Proof.
      unfold rvsign.
      intros ????.
      now rewrite H.
    Qed.

    Local Open Scope equiv_scope.
    Lemma rv_pos_neg_id (rv_X:Ts->R) : rv_X === rvplus (pos_fun_part rv_X) (rvopp (neg_fun_part rv_X)).
    Proof.
      intros x.
      unfold rvplus, rvopp, pos_fun_part, neg_fun_part, rvscale; simpl.
      unfold Rmax, Rmin.
      repeat match_destr; lra.
    Qed.

    Lemma rv_pos_neg_abs (rv_X:Ts->R) : rvabs rv_X === rvplus (pos_fun_part rv_X) (neg_fun_part rv_X).
    Proof.
      intros x.
      unfold rvplus, rvabs, pos_fun_part, neg_fun_part; simpl.
      unfold Rabs, Rmax, Rmin.
      repeat match_destr; lra.
    Qed.

    Lemma rvmult_assoc
          (rv_X1 rv_X2 rv_X3 : Ts -> R) :
      (rvmult (rvmult rv_X1 rv_X2) rv_X3) === (rvmult rv_X1 (rvmult rv_X2 rv_X3)).
    Proof.
      intros x.
      unfold rvmult.
      lra.
    Qed.

    Lemma rvmult_comm
          (rv_X1 rv_X2 : Ts -> R) :
      (rvmult rv_X1 rv_X2)  === (rvmult rv_X2 rv_X1).
    Proof.
      intros x.
      unfold rvmult.
      lra.
    Qed.

    Lemma rvmult_rvadd_distr
          (rv_X1 rv_X2 rv_X3 : Ts -> R) :
      (rvmult rv_X1 (rvplus rv_X2 rv_X3)) ===  
                                          (rvplus (rvmult rv_X1 rv_X2) (rvmult rv_X1 rv_X3)).
    Proof.
      intros x.
      unfold rvmult, rvplus.
      lra.
    Qed.

    Lemma rvsum_distr_r {n} (X : nat -> Ts -> R) (f : Ts -> R) :
      rv_eq (rvsum (fun j => rvmult (X j) f) n) (rvmult (rvsum X n) f).
    Proof.
      intro x; unfold rvsum, rvmult.
      induction n.
      - rewrite sum_O.
        now rewrite sum_O.
      - rewrite sum_Sn.
        rewrite sum_Sn.
        unfold plus; simpl.
        rewrite IHn.
        lra.
    Qed.

    Lemma pos_fun_part_le rv_X : rv_le (fun x : Ts => pos_fun_part rv_X x) (rvabs rv_X).
    Proof.
      intros ?.
      unfold rvabs, pos_fun_part, Rabs, Rmax; simpl.
      repeat match_destr; lra.
    Qed.

    Lemma neg_fun_part_le rv_X : rv_le (fun x : Ts => (neg_fun_part rv_X x)) (rvabs rv_X).
    Proof.
      intros ?.
      unfold rvabs, rvopp, rvscale, neg_fun_part, Rabs, Rmax; simpl.
      repeat match_destr; lra.
    Qed.

    Lemma rv_le_pos_fun_part rv_X1 rv_X2 :
      rv_le rv_X1 rv_X2 ->
      rv_le (fun x : Ts => pos_fun_part rv_X1 x) (fun x : Ts => pos_fun_part rv_X2 x).
    Proof.
      intros le12 a.
      simpl.
      now apply Rle_max_compat_r.
    Qed.

    Lemma rv_le_neg_fun_part rv_X1 rv_X2 :
      rv_le rv_X1 rv_X2 ->
      rv_le (fun x : Ts => neg_fun_part rv_X2 x) (fun x : Ts => neg_fun_part rv_X1 x).
    Proof.
      intros le12 a.
      simpl.
      replace 0 with (- 0) by lra.
      repeat rewrite Rcomplements.Rmax_opp_Rmin.
      apply Ropp_le_contravar.
      now apply Rle_min_compat_r.
    Qed.
    
    Lemma rvmax_unfold (f g:Ts->R) :
      rvmax f g === rvscale (/2) (rvplus (rvplus f g) (rvabs (rvminus f g))).
    Proof.
      intro x.
      unfold rvmax, rvminus, rvscale, rvabs, rvopp, rvscale, rvplus.
      unfold Rmax, Rabs.
      repeat match_destr; lra.
    Qed.

    Lemma rvmin_unfold (f g:Ts->R) :
      rvmin f g === rvscale (/2) (rvminus (rvplus f g) (rvabs (rvminus f g))).
    Proof.
      intro x.
      unfold rvmin, rvminus, rvscale, rvabs, rvopp, rvscale, rvplus.
      unfold Rmin, Rabs.
      repeat match_destr; try lra.
    Qed.

    Lemma rvmult_unfold (f g:Ts->R) :
      rvmult f g === rvscale (1/4) (rvminus (rvsqr (rvplus f g))
                                            (rvsqr (rvminus f g))).
    Proof.
      intros x.
      unfold rvmult, rvminus, rvplus,rvsqr, rvopp, rvscale.
      replace (1 / 4 * ((f x + g x)² + -1 * (f x + -1 * g x)²)) with ((f x)*(g x)) by (unfold Rsqr; lra).
      intuition.
    Qed.

    Lemma rvsqr_unfold (f:Ts->R) :
      rvsqr f === rvpow f 2.
    Proof.
      intros x.
      unfold rvpow, rvsqr, Rsqr; simpl.
      lra.
    Qed.

    Lemma rvsqr_rvsign_nonzero (f : Ts -> R):
      (forall omega, 0 <> f omega) -> rvsqr (rvsign f) === const 1.
    Proof.
      intros H omega.
      unfold rvsqr,rvsign,const.
      destruct (Rle_dec (f omega) 0).
      + destruct r as [H1 | H2].
        -- generalize (sign_eq_m1 _ H1); intros; (rewrite H0).
           unfold Rsqr; lra.
        -- rewrite H2. specialize (H omega). congruence.
      + apply Rnot_le_gt in n.
        generalize (sign_eq_1 _ n); intros; rewrite H0.
        unfold Rsqr; lra.
    Qed.

    Lemma rvpower_abs2_unfold (f:Ts->R) :
      rvpower (rvabs f) (const 2) === rvsqr f.
    Proof.
      intros x.
      apply power_abs2_sqr.
    Qed.

    Lemma rvpower_abs_scale c (X:Ts->R) n :
      rvpower (rvscale (Rabs c) (rvabs X)) (const n) === rvscale (power (Rabs c) n) (rvpower (rvabs X) (const n)).
    Proof.
      intros x.
      unfold rvpower, rvscale.
      rewrite power_mult_distr; trivial.
      - apply Rabs_pos.
      - apply rvabs_pos.
    Qed.

    Lemma rv_abs_abs (rv_X:Ts->R) :
      rv_eq (rvabs (rvabs rv_X)) (rvabs rv_X).
    Proof.
      intros a.
      unfold rvabs.
      now rewrite Rabs_Rabsolu.
    Qed.
    
    Lemma rvpowabs_choice_le c (rv_X1 rv_X2 : Ts -> R) p :
      rv_le (rvpower (rvabs (rvchoice c rv_X1 rv_X2)) (const p))
            (rvplus (rvpower (rvabs rv_X1) (const p)) (rvpower (rvabs rv_X2) (const p))).
    Proof.
      intros a.
      unfold rvpower, rvabs, rvchoice, rvplus, const; simpl.
      match_destr.
      - assert (0 <= power (Rabs (rv_X2 a)) p) by apply power_nonneg.
        lra.
      - assert (0 <= power (Rabs (rv_X1 a)) p) by apply power_nonneg.
        lra.
    Qed.
    
    Lemma pos_fun_part_unfold (f : Ts->R) :
      (fun x => nonneg (pos_fun_part f x)) === rvmax f (const 0).
    Proof.
      intros x.
      reflexivity.
    Qed.

    Lemma neg_fun_part_unfold (f : Ts->R) :
      (fun x => nonneg (neg_fun_part f x)) === rvmax (rvopp f) (const 0).
    Proof.
      intros x.
      unfold neg_fun_part, rvopp, const, rvscale, rvmax; simpl.
      f_equal.
      lra.
    Qed.

    Lemma rvmin_choice (rv_X1 rv_X2 : Ts -> R)
      : rvmin rv_X1 rv_X2 === rvchoice (bvmin_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold rvmin, rvchoice, bvmin_choice, Rmin.
      match_destr.
    Qed.

    Lemma Rbar_rvmin_choice (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rvmin rv_X1 rv_X2 === Rbar_rvchoice (Rbar_bvmin_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold Rbar_rvmin, Rbar_rvchoice, Rbar_bvmin_choice, Rbar_min, Rmin.
      destruct (Rbar_le_dec (rv_X1 a) (rv_X2 a))
      ; destruct (rv_X1 a)
      ; destruct (rv_X2 a)
      ; simpl; repeat match_destr; simpl in *; trivial; try lra.
    Qed.

    Lemma rvmax_choice (rv_X1 rv_X2 : Ts -> R)
      : rvmax rv_X1 rv_X2 === rvchoice (bvmax_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold rvmax, rvchoice, bvmax_choice, Rmax.
      match_destr.
    Qed.

    Lemma Rbar_rvmax_choice (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rvmax rv_X1 rv_X2 === Rbar_rvchoice (Rbar_bvmax_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold Rbar_rvmax, Rbar_rvchoice, Rbar_bvmax_choice, Rbar_max, Rmax.
      destruct (Rbar_le_dec (rv_X1 a) (rv_X2 a))
      ; destruct (rv_X1 a)
      ; destruct (rv_X2 a)
      ; simpl; repeat match_destr; simpl in *; trivial; try lra.
    Qed.

    Lemma rvchoice_le_max (c:Ts->bool) (rv_X1 rv_X2 : Ts -> R)
      : rv_le (rvchoice c rv_X1 rv_X2) (rvmax rv_X1 rv_X2).
    Proof.
      intros a.
      unfold rvchoice, rvmax, Rmax.
      repeat match_destr; lra.
    Qed.

    Lemma Rbar_rvchoice_le_max (c:Ts->bool) (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rv_le (Rbar_rvchoice c rv_X1 rv_X2) (Rbar_rvmax rv_X1 rv_X2).
    Proof.
      intros a.
      unfold Rbar_rvchoice, Rbar_rvmax, Rbar_max, Rmax.
      repeat match_destr; trivial; try lra
      ; try apply Rbar_le_refl.
      apply Rbar_not_le_lt in n.
      now apply Rbar_lt_le.
    Qed.

    Lemma rvchoice_le_min (c:Ts->bool) (rv_X1 rv_X2 : Ts -> R)
      : rv_le (rvmin rv_X1 rv_X2) (rvchoice c rv_X1 rv_X2).
    Proof.
      intros a.
      unfold rvchoice, rvmin, Rmin.
      repeat match_destr; lra.
    Qed.

    Lemma Rbar_rvchoice_le_min (c:Ts->bool) (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rv_le (Rbar_rvmin rv_X1 rv_X2) (Rbar_rvchoice c rv_X1 rv_X2).
    Proof.
      intros a.
      unfold Rbar_rvchoice, Rbar_rvmin, Rbar_min, Rmin.
      repeat match_destr; simpl in *; trivial; try lra
      ; try apply Rbar_le_refl.
    Qed.

    Lemma rvminus_self (x:Ts->R) : rv_eq (rvminus x x) (const 0).
    Proof.
      intros a.
      unfold rvminus, rvplus, rvopp, rvscale, const.
      lra.
    Qed.

    Lemma rvminus_unfold (x y : Ts -> R)
      : rv_eq (rvminus x y)  (fun a => x a - y a).
    Proof.
      unfold rvminus, rvplus, rvopp, rvscale.
      intros a.
      lra.
    Qed.

    Lemma rvabs_rvminus_sym (x y : Ts -> R) :
      rv_eq (rvabs (rvminus x y)) (rvabs (rvminus y x)).
    Proof.
      repeat rewrite rvminus_unfold.
      unfold rvabs.
      intros a.
      apply Rabs_minus_sym.
    Qed.

    Lemma rvabs_pow1 (x:Ts->R) : rv_eq (rvpower (rvabs x) (const 1)) (rvabs x).
    Proof.
      intros a.
      unfold rvpower, rvabs, const.
      apply power_1.
      apply Rabs_pos.
    Qed.

    Lemma rv_abs_scale_eq (c:R) (rv_X:Ts->R) :
      rv_eq (rvabs (rvscale c rv_X)) (rvscale (Rabs c) (rvabs rv_X)).
    Proof.
      intros a.
      unfold rvabs, rvscale.
      apply Rabs_mult.
    Qed.
    
    Lemma rv_abs_const_eq (c:R)  :
      rv_eq (Ts:=Ts) (rvabs (const c)) (const (Rabs c)).
    Proof.
      intros a.
      reflexivity.
    Qed.
    
    Lemma rvpow_mult_distr (x y:Ts->R) n :
      rv_eq (rvpow (rvmult x y) n) (rvmult (rvpow x n) (rvpow y n)).
    Proof.
      intros a.
      unfold rvpow, rvmult.
      apply Rpow_mult_distr.
    Qed.

    Lemma rvpow_scale c (X:Ts->R) n :
      rv_eq (rvpow (rvscale c X) n) (rvscale (pow c n) (rvpow X n)).
    Proof.
      intros x.
      unfold rvpow, rvscale.
      apply Rpow_mult_distr.
    Qed.

    Lemma rvpow_const c n :
      rv_eq (Ts:=Ts) (rvpow (const c) n) (const (pow c n)).
    Proof.
      intros x.
      reflexivity.
    Qed.

    Lemma rvpower_const b e :
      rv_eq (Ts:=Ts) (rvpower (const b) (const e)) (const (power b e)).
    Proof.
      reflexivity.
    Qed.

    Lemma fold_right_rvplus c (l:list (Ts->R)) (a:Ts) :
      fold_right rvplus (const c) l a =
      fold_right Rplus c (map (fun x => x a) l).
    Proof.
      unfold rvplus, const.
      induction l; simpl; trivial.
      now rewrite IHl.
  Qed.

      Lemma rvabs_bound (rv_X : Ts -> R) :
    rv_le (rvabs rv_X) (rvplus (rvsqr rv_X) (const 1)).
  Proof.
    assert (forall x, 0 <= (rvsqr (rvplus (rvabs rv_X) (const (-1)))) x) by (intros; apply Rle_0_sqr).

    assert (rv_eq (rvsqr (rvplus (rvabs rv_X) (const (-1))))
                  (rvplus 
                     (rvplus (rvsqr (rvabs rv_X)) (rvscale (-2) (rvabs rv_X)))
                     (const 1))).
    {
      intro x.
      unfold rvsqr, rvplus, rvscale, rvabs, const, Rsqr.
      now ring_simplify.
    }
    intros x.
    specialize (H x).
    rewrite H0 in H.
    unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, rvabs, const in *.
    rewrite Rsqr_abs.
    unfold Rsqr in *.
    apply Rplus_le_compat_l with (r := 2 * Rabs (rv_X x)) in H.
    ring_simplify in H.
    generalize (Rabs_pos (rv_X x)); intros.
    lra.
  Qed.

  Lemma rvabs_sqr (rv_X : Ts -> R) :
    rv_eq (rvabs (rvsqr rv_X)) (rvsqr rv_X).
    Proof.
      intro x.
      unfold rvabs, rvsqr.
      apply Rabs_pos_eq.
      apply Rle_0_sqr.
    Qed.
      
  Lemma rvsqr_abs (rv_X : Ts -> R) :
    rv_eq (rvsqr (rvabs rv_X)) (rvsqr rv_X).
    Proof.
      intro x.
      unfold rvabs, rvsqr.
      now rewrite <- Rsqr_abs.
    Qed.

    Lemma rvmult_abs (rv_X1 rv_X2 : Ts -> R):
      rv_eq (rvabs (rvmult rv_X1 rv_X2)) (rvmult (rvabs rv_X1) (rvabs rv_X2)).
    Proof.
      intro x.
      unfold rvmult, rvabs.
      apply Rabs_mult.
    Qed.
    
    Lemma rvprod_bound (rv_X1 rv_X2 : Ts->R) :
      rv_le (rvscale 2 (rvmult rv_X1 rv_X2))
            (rvplus (rvsqr rv_X1) (rvsqr rv_X2)).
    Proof.
      assert (forall x, 0 <= (rvsqr (rvminus rv_X1 rv_X2)) x) by (intros; apply Rle_0_sqr).
      assert (rv_eq (rvsqr (rvminus rv_X1 rv_X2)) 
                  (rvplus (rvplus (rvsqr rv_X1) (rvopp (rvscale 2 (rvmult rv_X1 rv_X2))))
                          (rvsqr rv_X2))).
    { 
      intro x.
      unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr.
      now ring_simplify.
    }
    intros x; specialize (H x).
    rewrite H0 in H; clear H0.
    unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr in *.
    lra.
  Qed.  
  
  Lemma rvprod_abs_bound (rv_X1 rv_X2 : Ts->R) :
    rv_le (rvscale 2 (rvabs (rvmult rv_X1 rv_X2)))
                          (rvplus (rvsqr rv_X1) (rvsqr rv_X2)).
  Proof.
    generalize (rvprod_bound (rvabs rv_X1) (rvabs rv_X2)); intros.
    do 2 rewrite rvsqr_abs in H.
    now rewrite rvmult_abs.
  Qed.

  Lemma rvsum_sqr_bound (rv_X1 rv_X2 : Ts->R) :
    rv_le (rvsqr (rvplus rv_X1 rv_X2)) 
                          (rvscale 2 (rvplus (rvsqr rv_X1) (rvsqr rv_X2))).
  Proof.
    assert (forall x, 0 <= (rvsqr (rvminus rv_X1 rv_X2)) x) by (intros; apply Rle_0_sqr).
    assert (rv_eq (rvsqr (rvminus rv_X1 rv_X2)) 
                  (rvplus (rvplus (rvsqr rv_X1) (rvopp (rvscale 2 (rvmult rv_X1 rv_X2))))
                          (rvsqr rv_X2))).
    { 
      intro x.
      unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr.
      now ring_simplify.
    }
    intros x; specialize (H x).
    rewrite H0 in H; clear H0.
    unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr in *.
    apply Rplus_le_compat_l with (r:= ((rv_X1 x + rv_X2 x) * (rv_X1 x + rv_X2 x))) in H.
    ring_simplify in H.
    ring_simplify.
    apply H.
  Qed.    

  Lemma rvsqr_eq (x:Ts->R): rv_eq (rvsqr x) (rvmult x x).
  Proof.
    intros ?.
    reflexivity.
  Qed.

  Lemma rvprod_abs1_bound (rv_X1 rv_X2 : Ts->R) :
    rv_le (rvabs (rvmult rv_X1 rv_X2))
                          (rvplus (rvsqr rv_X1) (rvsqr rv_X2)).
  Proof.
    generalize (rvprod_abs_bound rv_X1 rv_X2).
    unfold rv_le, rvscale, rvabs, rvmult, rvsqr, Rsqr; intros H x.
    specialize (H x).
    assert (Rabs (rv_X1 x * rv_X2 x) <= 2 * Rabs (rv_X1 x * rv_X2 x)).
    apply Rplus_le_reg_l with (r := - Rabs(rv_X1 x * rv_X2 x)).
    ring_simplify.
    apply Rabs_pos.
    lra.
  Qed.

    Lemma Rbar_Rabs_lim_sum_le0 (f : nat -> Ts -> R) (x : Ts) :
    is_finite (Lim_seq (sum_n (fun n=> Rabs (f n x)))) ->
    Rbar_le
      (Rbar_abs (Lim_seq (fun n => (rvsum f) n x)))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    intros.
    apply series_abs_bounded in H.
    generalize H; intros HH.
    generalize (ex_series_Rabs (fun n => (f n x)) H); intros.
    generalize (Series_Rabs (fun n => (f n x)) H); intros.
    unfold rvsum, rvabs.
    apply ex_series_Lim_seq in H.
    apply ex_series_Lim_seq in H0.
    replace (Lim_seq
               (fun n : nat => sum_n (fun n0 : nat => f n0 x) n))
      with (Finite ( Series (fun n : nat => f n x))).
    replace (Lim_seq
          (fun n : nat =>
             sum_n (fun n0 : nat => Rabs (f n0 x)) n))
      with (Finite (Series (fun n : nat => Rabs (f n x)))).
    simpl.
    apply Rge_le.
    rewrite Rabs_right.
    apply Rle_ge, H1.
    apply Rle_ge, Series_nonneg; trivial.
    intros.
    apply Rabs_pos.
  Qed.

  Lemma Rabs_lim_sum_le0 (f : nat -> Ts -> R) (x : Ts) :
    is_finite (Lim_seq (sum_n (fun n=> Rabs (f n x)))) ->
    Rbar_le
      (Rbar_abs (Finite (real (Lim_seq (fun n => (rvsum f) n x)))))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    intros.
    apply series_abs_bounded in H.
    generalize H; intros HH.
    generalize (ex_series_Rabs (fun n => (f n x)) H); intros.
    generalize (Series_Rabs (fun n => (f n x)) H); intros.
    unfold rvsum, rvabs.
    apply ex_series_Lim_seq in H.
    apply ex_series_Lim_seq in H0.
    replace (Lim_seq
               (fun n : nat => sum_n (fun n0 : nat => f n0 x) n))
      with (Finite ( Series (fun n : nat => f n x))).
    replace (Lim_seq
          (fun n : nat =>
             sum_n (fun n0 : nat => Rabs (f n0 x)) n))
      with (Finite (Series (fun n : nat => Rabs (f n x)))).
    simpl.
    apply Rge_le.
    rewrite Rabs_right.
    apply Rle_ge, H1.
    apply Rle_ge, Series_nonneg; trivial.
    intros.
    apply Rabs_pos.
  Qed.

    Lemma Rbar_Rabs_lim_sum_le (f : nat -> Ts -> R) (x : Ts) :
    Rbar_le
      (Rbar_abs (Lim_seq (fun n => (rvsum f) n x)))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    case_eq (Lim_seq
          (fun n : nat =>
           rvsum (fun n0 : nat => rvabs (f n0)) n x)); intros.
    - rewrite <- H.
      apply Rbar_Rabs_lim_sum_le0.
      unfold rvsum, rvabs in H.
      replace  (Lim_seq (sum_n (fun n : nat => Rabs (f n x))))
        with
           (Lim_seq
              (fun n : nat =>
                 sum_n (fun n0 : nat => Rabs (f n0 x)) n)).
      now rewrite H.
      apply Lim_seq_ext.
      intros; trivial.
    - destruct (Lim_seq (fun n : nat => rvsum f n x)); now simpl.
    - assert (Rbar_le 0 (Lim_seq
        (fun n : nat =>
         rvsum (fun n0 : nat => rvabs (f n0)) n x))).
      + apply Lim_seq_pos.
        intros.
        unfold rvsum, rvabs.
        apply sum_n_nneg.
        intros.
        apply Rabs_pos.
      + rewrite H in H0.
        now simpl in H0.
  Qed.


  Lemma Rabs_lim_sum_le (f : nat -> Ts -> R) (x : Ts) :
    Rbar_le
      (Rbar_abs (Finite (real (Lim_seq (fun n => (rvsum f) n x)))))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    case_eq (Lim_seq
          (fun n : nat =>
           rvsum (fun n0 : nat => rvabs (f n0)) n x)); intros.
    - rewrite <- H.
      apply Rabs_lim_sum_le0.
      unfold rvsum, rvabs in H.
      replace  (Lim_seq (sum_n (fun n : nat => Rabs (f n x))))
        with
           (Lim_seq
              (fun n : nat =>
                 sum_n (fun n0 : nat => Rabs (f n0 x)) n)).
      now rewrite H.
      apply Lim_seq_ext.
      intros; trivial.
    - destruct (Lim_seq (fun n : nat => rvsum f n x)); now simpl.
    - assert (Rbar_le 0 (Lim_seq
        (fun n : nat =>
         rvsum (fun n0 : nat => rvabs (f n0)) n x))).
      + apply Lim_seq_pos.
        intros.
        unfold rvsum, rvabs.
        apply sum_n_nneg.
        intros.
        apply Rabs_pos.
      + rewrite H in H0.
        now simpl in H0.
  Qed.

  End eqs.
End defs.

Ltac rv_unfold := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax, 
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvminus,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult in *.

Ltac rv_unfold'_in_star := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax, 
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult in *; repeat rewrite rvminus_unfold in *.

Tactic Notation "rv_unfold'" "in" "*" := rv_unfold'_in_star.

Ltac rv_unfold'_goal := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax, 
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult; repeat rewrite rvminus_unfold.

Tactic Notation "rv_unfold'" := rv_unfold'_goal.

Ltac rv_unfold'_in_hyp H := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax, 
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult in H; repeat rewrite rvminus_unfold in H.

Tactic Notation "rv_unfold'" "in" hyp(H) := rv_unfold'_in_hyp H.
