simple_fun.v

(**
This file is part of the Elfic library

Copyright (C) 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.
*)

(* References to pen-and-paper statements are from RR-9386-v2,
 https://hal.inria.fr/hal-03105815v2/

 This file refers mostly to Section 13.2 (pp. 149-162).

 Some proof paths may differ. *)

From Coq Require Import ClassicalDescription.
From Coq Require Import PropExtensionality FunctionalExtensionality.
From Coq Require Import Lia Reals Lra List Sorted.
From Coquelicot Require Import Coquelicot.
From Flocq Require Import Core.

Require Import list_compl sort_compl.
Require Import Rbar_compl sum_Rbar_nonneg.
Require Import Subset Subset_charac.
Require Import sigma_algebra sigma_algebra_R_Rbar.
Require Import measurable_fun.
Require Import measure.


Section finite_vals_def.

Context {E : Type}.
Hypothesis Einhab : inhabited E.

Definition finite_vals : (E -> R) -> list R -> Prop :=
  fun f l => forall y, In (f y) l.

Definition finite_vals_canonic : (E -> R) -> list R -> Prop :=
  fun f l =>
    (LocallySorted Rlt l) /\
    (forall x, In x l -> exists y, f y = x) /\
    (forall y, In (f y) l).

Lemma finite_vals_canonic_not_nil :
  forall f l, finite_vals_canonic f l -> l <> nil.
Proof.
intros f l (V1,(V2,V3)) V4.
rewrite V4 in V3.
inversion Einhab as [ x ].
specialize (V3 x).
apply (in_nil V3).
Qed.

Lemma finite_vals_canonic_unique :
  forall f l1 l2,
    finite_vals_canonic f l1 ->
    finite_vals_canonic f l2 ->
    l1 = l2.
Proof.
intros f l1 l2 (U1,(V1,W1)) (U2,(V2,W2)).
apply Sorted_In_eq_eq; try assumption.
intros x; split.
intros H1; destruct (V1 x H1) as (y,Hy).
rewrite <- Hy; apply W2.
intros H2; destruct (V2 x H2) as (y,Hy).
rewrite <- Hy; apply W1.
Qed.

Lemma In_finite_vals_nonneg :
  forall (f : E -> R) l a,
    nonneg f -> finite_vals_canonic f l ->
    In a l ->
    Rbar_le 0 a.
Proof.
intros f l a H (Y1,(Y2,Y3)) H'.
destruct (Y2 a H') as (y,Hy).
rewrite <- Hy; apply H.
Qed.

Definition canonizer : (E -> R) -> list R -> list R :=
  fun f l => sort Rle (RemoveUseless f (nodup Req_EM_T l)).

Lemma finite_vals_canonizer :
  forall f l, finite_vals f l -> finite_vals_canonic f (canonizer f l).
Proof.
unfold finite_vals, canonizer.
intros f l H.
pose (l1 := nodup Req_EM_T l); fold l1.
pose (l2 := RemoveUseless f l1); fold l2.
pose (l3 := sort Rle l2); fold l3.
split.
(* *)
apply LocallySorted_impl with Rle (fun x y => x <> y).
intros a b Z1 Z2; case Z1; [easy|intros Z3; easy].
apply LocallySorted_sort_Rle.
apply LocallySorted_neq.
apply Permutation.Permutation_NoDup with l2.
apply corr_sort.
apply NoDup_select.
apply NoDup_nodup.
(* *)
split.
(* *)
intros x Hx.
assert (H0: In x l2).
apply Permutation.Permutation_in with l3; auto.
apply Permutation.Permutation_sym.
apply corr_sort.
apply In_select_P with (1:=H0).
(* *)
intros y.
cut (In (f y) l2).
intros H1; apply Permutation.Permutation_in with l2; auto.
apply corr_sort.
assert (In (f y) l1).
apply nodup_In, H.
apply In_select_P_inv; try easy.
exists y; easy.
Qed.

Lemma finite_vals_unique :
  forall f l1 l2,
    finite_vals f l1 ->
    finite_vals f l2 ->
    canonizer f l1 = canonizer f l2.
Proof.
intros f l1 l2 H1 H2.
apply finite_vals_canonic_unique with f.
now apply finite_vals_canonizer.
now apply finite_vals_canonizer.
Qed.

Lemma In_canonizer :
  forall f l x, (exists y, f y = x) -> In x l -> In x (canonizer f l).
Proof.
intros f l x (y,Hy) Hx.
unfold canonizer.
apply Permutation.Permutation_in with
  (RemoveUseless f (nodup Req_EM_T l)).
apply corr_sort.
apply In_select_P_inv.
2: exists y; easy.
apply nodup_In; easy.
Qed.

Lemma canonizer_Sorted :
  forall f l,
    finite_vals f l ->
    LocallySorted Rlt l ->
    canonizer f l = RemoveUseless f l.
Proof.
intros f l H1 H2.
apply finite_vals_canonic_unique with f.
now apply finite_vals_canonizer.
split.
apply LocallySorted_select; try easy.
intros; apply Rlt_trans with y; easy.
split.
intros y Hy.
apply In_select_P with (1:=Hy).
intros y; apply In_select_P_inv.
apply H1.
exists y; easy.
Qed.

Lemma finite_vals_sum_eq :
  forall f l, finite_vals_canonic f l ->
    forall y, Finite (f y) =
      sum_Rbar_map l (fun a => a * (charac (fun x => f x = a) y)).
Proof.
intros f l (Y1,(Y2,Y3)) y.
rewrite sum_Rbar_map_select_eq with
   (P:= fun z:R => z = f y).
2: intros t Ht1 Ht2; f_equal.
2: rewrite charac_is_0; auto with real.
2: unfold Subset.compl; now apply not_eq_sym.
replace (select (fun z : R => z = f y) l)
    with (f y::nil).
unfold sum_Rbar_map; simpl.
rewrite Rplus_0_r; rewrite charac_is_1; try easy.
f_equal; ring.
apply Sorted_In_eq_eq.
intros x; split; intros K.
inversion K.
apply In_select_P_inv; try easy.
rewrite <- H; apply Y3.
contradict H; apply in_nil.
generalize (In_select_P _ _ _ K); intros J1.
rewrite J1; apply in_eq.
apply LSorted_cons1.
apply LocallySorted_select; try assumption.
intros a b c H1 H2; apply Rlt_trans with (1:=H1); easy.
Qed.

Lemma finite_vals_charac_sum_eq :
  forall f l A,
    finite_vals_canonic f l -> nonneg f ->
    forall y, Finite (f y * charac A y) =
      sum_Rbar_map l (fun t => t * (charac (fun x => A x /\ f x = t) y)).
Proof.
intros f l A Hl Hf y.
apply trans_eq with
  (Rbar_mult (Finite (f y)) (charac A y)).
easy.
rewrite finite_vals_sum_eq with f l y; try easy.
rewrite Rbar_mult_comm, sum_Rbar_map_Rbar_mult.
apply sum_Rbar_map_ext_f.
intros x Hx; simpl; f_equal.
generalize (charac_inter A); intros H; unfold Subset.inter in H.
rewrite H; ring.
intros x Hx; simpl.
apply Rmult_le_pos.
destruct Hl as (Y1,(Y2,Y3)); destruct (Y2 x Hx) as (t,Ht).
rewrite <- Ht; apply Hf.
case (charac_or (fun x0 : E => f x0 = x) y); intros L; rewrite L;
 auto with real.
Qed.

(* Given a function f and its associated canonical list l, the next lemma
 builds a new function g canonically associated to l deprived from some item v.
 This means that on the (nonempty) subset {f = v}, g must take one of the remaining
 values. Thus, the initial list must contain at least two values. *)
Lemma finite_vals_canonic_cons :
  forall (f : E -> R) v1 v2 l,
    nonneg f ->
    finite_vals_canonic f (v1 :: v2 :: l) ->
    let g := fun x => f x + (v1-v2) * charac (fun t => f t = v2) x in
    (forall x, f x = v2 -> g x = v1) /\ (forall x, f x <> v2 -> g x = f x) /\
    nonneg g /\ finite_vals_canonic g (v1 :: l).
Proof.
intros f v1 v2 l H1 H2 g.
assert (Z1: forall x, f x = v2 -> g x = v1).
intros x Hx; unfold g.
rewrite charac_is_1, Hx; try ring; easy.
assert (Z2: forall x, f x <> v2 -> g x = f x).
intros x Hx; unfold g.
rewrite charac_is_0; try ring; easy.
split; try easy.
split; try easy.
split.
intros x.
case (Req_dec (f x) v2); intros Hx.
rewrite (Z1 _ Hx).
apply In_finite_vals_nonneg with f (v1 :: v2 :: l); try apply in_eq; easy.
rewrite (Z2 _ Hx); easy.
(* *)
destruct H2 as (Y1,(Y2,Y3)).
split.
apply (LocallySorted_cons2 _ v1 v2); try apply Rlt_trans; easy.
split.
intros x Hx.
destruct (Y2 x) as (y,Hy).
case (in_inv Hx); intros Hx2.
rewrite Hx2; apply in_eq.
apply in_cons, in_cons; easy.
exists y.
rewrite <- Hy.
apply Z2.
rewrite Hy.
case (in_inv Hx); intros Hx2.
rewrite <- Hx2.
apply Rlt_not_eq.
inversion Y1; easy.
apply Rgt_not_eq, Rlt_gt.
apply LocallySorted_extends with (l); try easy.
apply Rlt_trans.
inversion Y1; easy.
(* *)
intros y; case (Req_dec (f y) v2); intros H.
rewrite (Z1 _ H); apply in_eq.
rewrite (Z2 _ H).
specialize (Y3 y).
case (in_inv Y3); intros Y4.
rewrite <- Y4; apply in_eq.
case (in_inv Y4); intros Y5.
contradict H; easy.
apply in_cons; easy.
Qed.

End finite_vals_def.


Section SF_def.

Context {E : Type}.
Hypothesis Einhab : inhabited E.

Variable gen : (E -> Prop) -> Prop.

(* From Lemma 752 p. 149 *)
Definition SF_aux : (E -> R) -> list R -> Prop :=
  fun f l =>
    finite_vals_canonic f l /\
    (forall a, measurable gen (fun x => f x = a)).

(* From Lemma 752 p. 149 *)
Definition SF : (E -> R) -> Set := fun f => { l | SF_aux f l }.

Definition SFplus : (E -> R) -> Prop :=
  fun f => nonneg f /\ exists l, SF_aux f l.

Definition SFplus_seq : (nat -> E -> R) -> Prop :=
  fun f => forall n, SFplus (f n).

End SF_def.


Section SF_Facts.

Context {E : Type}.
Hypothesis Einhab : inhabited E.

Variable gen : (E -> Prop) -> Prop.

Lemma SF_aux_cons :
  forall (f : E -> R) v1 v2 l,
    nonneg f ->
    SF_aux gen f (v1 :: v2 :: l) ->
    let g := fun x => f x + (v1 - v2) * charac (fun t => f t = v2) x in
    nonneg g /\ SF_aux gen g (v1 :: l).
Proof.
intros f v1 v2 l Hf1 [Hf2 Hf3] g.
generalize (finite_vals_canonic_cons f v1 v2 l Hf1); fold g;
    intros [Hg1 [Hg2 [Hg3 Hg4]]]; try apply Hf2.
split; try easy.
split; try easy.
intros a.
apply measurable_ext with (fun x => (f x = v2 /\ v1 = a) \/
    (f x <> v2 /\ f x = a)).
intros x; case (Req_dec (f x) v2); intros H.
rewrite (Hg1 x H).
split; try tauto.
rewrite (Hg2 x H).
split; try tauto.
apply measurable_union; apply measurable_inter; try apply Hf3.
apply measurable_Prop.
apply measurable_compl_rev, Hf3.
Qed.

End SF_Facts.


Section LInt_SFp_def.

Context {E : Type}.
Hypothesis Einhab : inhabited E.

Context {gen : (E -> Prop) -> Prop}.
Variable mu : measure gen.

(* From Lemma 770 p. 156 *)
Definition af1 : (E -> R) -> Rbar -> Rbar :=
  fun f a => Rbar_mult a (mu (fun x => Finite (f x) = a)).

Lemma nonneg_af1 : forall f : E -> R, nonneg f -> nonneg (af1 f).
Proof.
intros f Hf x.
destruct (Rbar_le_lt_dec 0 x).
apply Rbar_mult_le_pos_pos_pos; try easy.
apply meas_nonneg.
unfold af1.
assert (H : mu (fun x0 : E => Finite (f x0) = x) = 0).
transitivity (mu (fun x0 : E => False)).
apply sym_eq, measure_ext.
intros s.
split; try easy; intros H0.
unfold nonneg in Hf.
specialize (Hf s).
rewrite <- H0 in r.
apply Rbar_le_not_lt in Hf.
case (Hf r).
apply meas_emptyset.
rewrite H.
rewrite Rbar_mult_0_r.
apply Rbar_le_refl.
Qed.

(* Lemma 770 p. 156 *)
Definition LInt_SFp : forall (f : E -> R), SF gen f -> Rbar :=
  fun f H => let l := proj1_sig H in sum_Rbar_map l (af1 f).

Lemma LInt_SFp_correct :
  forall f (H1 H2 : SF gen f), nonneg f -> LInt_SFp f H1 = LInt_SFp f H2.
Proof.
intros f (l1,H1) (l2,H2) H.
unfold LInt_SFp; simpl.
rewrite finite_vals_canonic_unique with f l1 l2; try easy.
apply H1.
apply H2.
Qed.

Lemma LInt_SFp_ext :
  forall f1 (H1 : SF gen f1) f2 (H2 : SF gen f2),
    nonneg f1 ->
    (forall x, f1 x = f2 x) ->
    LInt_SFp f1 H1 = LInt_SFp f2 H2.
Proof.
intros f1 H1 f2 H2 H0 J.
assert (f1 = f2).
now apply functional_extensionality.
generalize H1.
rewrite H.
intros H3.
apply LInt_SFp_correct; try easy.
now rewrite <- H.
Qed.

Lemma SF_cst : forall (x : E) a, SF gen (fun _ => a).
Proof.
intros t a; exists (a :: nil).
split.
split.
apply LSorted_cons1.
split.
intros x H.
exists t.
now inversion H.
intros _; apply in_eq.
intros y; try easy.
case (Req_dec a y); intros Hy.
apply measurable_ext with (fun _ => True); try easy.
apply measurable_full.
apply measurable_ext with (fun _ => False); try easy.
apply measurable_empty.
Defined.

Lemma LInt_SFp_0 : forall x, LInt_SFp (fun _ => 0) (SF_cst x 0) = 0.
Proof.
intros x; unfold SF_cst, LInt_SFp; simpl.
unfold af1, sum_Rbar_map; simpl.
rewrite Rbar_mult_0_l.
apply Rbar_plus_0_l.
Qed.

(* Lemma 759 p. 153 *)
Lemma SF_aux_measurable :
  forall f l, SF_aux gen f l -> measurable_fun gen gen_R f.
Proof.
intros f l H A HA.
apply measurable_ext with
   (fun x => exists n, (n < length l)%nat /\ A (nth n l 0) /\ f x = nth n l 0).
intros x; split.
intros (n,(Hn1,(Hn2,Hn3))).
rewrite Hn3; easy.
intros H1.
destruct H as ((_,(H2,H3)),_).
specialize (H3 x).
destruct (In_nth l (f x) 0 H3) as (m,(Hm1,Hm2)).
exists m; split; auto; split; auto.
rewrite Hm2; auto.
apply measurable_union_finite_alt.
intros n Hn.
apply measurable_inter.
case (excluded_middle_informative (A (nth n l 0))); intros T.
apply measurable_ext with (fun _ => True).
intros _; split; easy.
apply measurable_full.
apply measurable_ext with (fun _ => False).
intros _; split; easy.
apply measurable_empty.
apply H.
Qed.

Lemma SF_measurable :
  forall f (Hf : SF gen f), measurable_fun_R gen f.
Proof.
intros f [l Hf]; now apply SF_aux_measurable with l.
Qed.

Lemma SF_measurable_Rbar :
  forall f (Hf : SF gen f), measurable_fun_Rbar gen f.
Proof.
intros; now apply measurable_fun_R_Rbar, SF_measurable.
Qed.

Lemma SFplus_Mplus :
  forall (f : E -> R), nonneg f -> SF gen f -> Mplus gen f.
Proof.
intros f Hf1 Hf2; split; try easy.
now apply SF_measurable_Rbar.
Qed.

Lemma SF_nonneg_In_ge_0 :
  forall f l x, SF_aux gen f l -> nonneg f ->  In x l -> 0 <= x.
Proof.
intros f l x ((Y1,(Y2,Y3)),H1) H2 H3.
destruct (Y2 x H3) as (y,Hy).
rewrite <- Hy; apply H2.
Qed.

Lemma LInt_SFp_pos :
  forall f (Hf : SF gen f), nonneg f -> Rbar_le 0 (LInt_SFp f Hf).
Proof.
intros f (l,Hl) Hf; unfold LInt_SFp.
simpl (proj1_sig _).
apply sum_Rbar_map_ge_0.
intros x Hx; unfold af1.
apply Rbar_mult_le_pos_pos_pos.
apply SF_nonneg_In_ge_0 with f l; easy.
apply meas_nonneg.
Qed.

Definition cartesian_Rplus : list R -> list R -> list R :=
  fun l1 l2 => flat_map (fun a => (map (fun x => a + x) l2)) l1.

Lemma cartesian_Rplus_correct :
  forall l1 l2 x1 x2,
    In x1 l1 -> In x2 l2 ->
    In (x1 + x2) (cartesian_Rplus l1 l2).
Proof.
intros l1 l2 x1 x2 H1 H2; unfold cartesian_Rplus.
apply in_flat_map.
exists x1.
split; try easy.
now apply in_map.
Qed.

(* From Lemma 757 pp. 152-153 *)
Lemma SF_plus :
  forall (f1 : E -> R) (H1 : SF gen f1) (f2 : E -> R) (H2 : SF gen f2),
    SF gen (fun x => f1 x + f2 x).
Proof.
intros f1 (l1,H1) f2 (l2,H2).
exists (canonizer (fun x : E => (f1 x) + (f2 x))
                   (cartesian_Rplus l1 l2)).
split.
apply finite_vals_canonizer.
intros y; apply cartesian_Rplus_correct.
apply H1.
apply H2.
intros a.
apply measurable_fun_plus_R with (A:= fun z : R => z = a).
now apply SF_aux_measurable with l1.
now apply SF_aux_measurable with l2.
apply measurable_R_eq.
Qed.

(* Lemma 775 p. 157 *)
Lemma SFp_decomp_aux :
  forall (f g : E -> R) lf lg y,
    SF_aux gen f lf -> SF_aux gen g lg ->
    In y lf ->
    mu (fun x => f x = y) =
      sum_Rbar_map lg (fun z => mu (fun x => f x = y /\ g x = z)).
Proof.
intros f g lf lg y Hf Hg Hy.
assert (length lg <> 0)%nat.
intros K; cut (lg = nil).
apply finite_vals_canonic_not_nil with g; try easy.
apply Hg.
now apply length_zero_iff_nil.
rewrite measure_decomp_finite with
 (B:= fun n x => g x = nth n lg 0) (N:=(length lg-1)%nat).
apply sym_eq; apply sum_Rbar_map_sum_Rbar with (a0:=0%R).
left; apply finite_vals_canonic_not_nil with g; try easy.
apply Hg.
intros x Hx; apply meas_nonneg.
now apply Hf.
intros n Hn.
apply Hg.
intros x.
destruct (In_nth lg (g x) 0) as (n,(Hn1,Hn2)).
apply Hg.
exists n; split; auto with zarith.
intros n p x Hn Hp H1 H2.
destruct Hg as ((T1,T2),_).
apply LocallySorted_Rlt_inj with lg; auto with zarith.
rewrite <- H1, H2; easy.
Qed.

Lemma SFp_decomp :
  forall (f g : E -> R) lf lg y,
    SF_aux gen f lf -> SF_aux gen g lg ->
    mu (fun x => f x = y) =
      sum_Rbar_map lg (fun z => mu (fun x => f x = y /\ g x = z)).
Proof.
intros f g lf lg y Hf Hg.
case (ListDec.In_decidable Req_dec y lf); intros Hy.
apply SFp_decomp_aux with lf; easy.
apply trans_eq with 0.
rewrite <- meas_emptyset with gen mu.
apply sym_eq, measure_ext.
intros x; split; try easy.
intros H.
apply Hy.
rewrite <- H; apply Hf.
apply trans_eq with (sum_Rbar_map lg (fun _ => 0)).
clear; induction lg.
unfold sum_Rbar_map; now simpl.
rewrite sum_Rbar_map_cons, Rbar_plus_0_l; easy.
apply sum_Rbar_map_ext_f.
intros x Hx.
rewrite <- meas_emptyset with gen mu.
apply measure_ext.
intros z; split; try easy.
intros (Y1,Y2).
apply Hy.
rewrite <- Y1; apply Hf.
Qed.

Lemma LInt_SFp_decomp :
  forall (f g : E -> R) lf lg,
    SF_aux gen f lf -> SF_aux gen g lg ->
    (* LInt_SFp f Hf = *) sum_Rbar_map lf (af1 f) =
      sum_Rbar_map lf (fun a =>
        Rbar_mult a (sum_Rbar_map lg (fun z => mu (fun x => f x = a /\ g x = z)))).
Proof.
intros f g lf lg Hf Hg.
f_equal; f_equal; unfold af1.
apply functional_extensionality.
intros x; f_equal.
rewrite <- SFp_decomp with (lf:=lf); try easy.
apply measure_ext.
intros y; split; intros H.
injection H; easy.
rewrite H; easy.
Qed.

(* Lemma 776 pp. 157-158 *)
Lemma sum_Rbar_map_change_of_variable :
  forall (f g : E -> R) lf lg y,
    SF_aux gen f lf -> SF_aux gen g lg -> (* In y lf -> *)
    sum_Rbar_map lg (fun z => Rbar_mult (y + z) (mu (fun x => f x = y /\ g x = z))) =
      sum_Rbar_map (canonizer (fun x => f x + g x) (cartesian_Rplus lf lg))
        (fun t => (* t = y+z *) Rbar_mult t (mu (fun x => f x = y /\ f x + g x = t))).
Proof.
intros f g lf lg y Hf Hg.
pose (A:=fun z x => f x = y /\ g x = z).
pose (B:=fun t x => f x = y /\ f x + g x = t).
change (sum_Rbar_map lg (fun z : R =>
   Rbar_mult (y + z)
     (mu (A z))) = sum_Rbar_map
  (canonizer (fun x : E => f x + g x)
     (cartesian_Rplus lf lg))
  (fun t : R => Rbar_mult t (mu (B t)))).
rewrite (sum_Rbar_map_select_eq (fun z => Rbar_lt 0
     (mu (A z))) (fun z : R => Rbar_mult (y + z)
      (mu (A z)))).
rewrite (sum_Rbar_map_select_eq
  (fun t => Rbar_lt 0
     (mu (B t)))
   (fun t : R  => Rbar_mult t
        (mu (B t)))).
pose (lA:=(select (fun z : R => Rbar_lt 0 (mu (A z)))
     lg)); fold lA.
pose (lB:=(select
     (fun t : R => Rbar_lt 0 (mu (B t)))
     (canonizer (fun x : E => f x + g x)
        (cartesian_Rplus lf lg)))); fold lB.
pose (tau := fun z => y+z).
apply trans_eq with
  (sum_Rbar_map lA
    (fun z : R =>
      Rbar_mult (tau z) (mu (B (tau z))))).
apply sum_Rbar_map_ext_f.
intros z Hz; f_equal; try easy.
apply measure_ext.
intros x; unfold A, B, tau.
split; intros (T1,T2); split; try easy.
rewrite T1, T2; easy.
apply Rplus_eq_reg_l with (f x).
rewrite T2, T1; easy.
rewrite <- (sum_Rbar_map_map tau
  (fun t => Rbar_mult t (mu (B t)))).
(*  *)
assert (Y1: forall z x,
   (B (y + z) x) <-> A z x).
intros z x; unfold A,B; split; intros (Y1,Y2); split; try easy.
apply Rplus_eq_reg_l with (f x); rewrite Y2, Y1; easy.
rewrite Y1, Y2; easy.
assert (Y2: forall t x,
     A (t - y) x <-> B t x).
intros t x.
replace t with (y+(t-y)) at 2 by ring.
symmetry.
apply Y1.

(* *)
f_equal.
apply Sorted_In_eq_eq.
intros t; split.
(* eq 1 *)
intros H1; apply in_map_iff in H1.
destruct H1 as (z,(Hz1,Hz2)).
rewrite <- Hz1; unfold tau.
assert (H:exists x, g x = z /\ f x = y).
destruct (measure_gt_0_exists gen mu (A z)).
apply In_select_P with (l:=lg) (x:=z); try easy.
exists x; unfold A in H; split; apply H.
apply In_select_P_inv.
apply In_canonizer; try easy.
destruct H as (x,(Hx1,Hx2)).
exists x; rewrite Hx1, Hx2; easy.
apply cartesian_Rplus_correct.
destruct H as (x,(Hx1,Hx2)).
rewrite <- Hx2; apply Hf.
destruct H as (x,(Hx1,Hx2)).
rewrite <- Hx1; apply Hg.
rewrite measure_ext with gen mu (B (y+z)) (A z).
apply In_select_P with (l:=lg) (x:=z); easy.
intros x; apply Y1.
(* eq 2 *)
intros H1.
replace t with (tau (t-y)).
2: unfold tau; ring.
apply in_map.
assert (H:exists x, f x + g x = t /\ f x = y).
destruct (measure_gt_0_exists gen mu (B t)).
apply In_select_P with (l:=(canonizer (fun x : E => f x + g x)
           (cartesian_Rplus lf lg))) (x:=t); try easy.
exists x; unfold B in H; split; apply H.
apply In_select_P_inv.
destruct H as (x,(Hx1,Hx2)).
replace (t-y) with (g x).
apply Hg.
apply Rplus_eq_reg_l with (f x); rewrite Hx1, Hx2; ring.
rewrite measure_ext with gen mu (A (t-y)) (B t).
apply In_select_P with (l:=(canonizer (fun x : E => f x + g x)
           (cartesian_Rplus lf lg))) (x:=t); easy.
intros x; apply Y2.
(* sort *)
apply LocallySorted_map.
intros u v H; unfold tau.
apply Rplus_lt_compat_l; easy.
apply LocallySorted_select.
intros u v w R1 R2; apply Rlt_trans with v; auto with real.
apply Hg.
apply LocallySorted_select.
intros u v w R1 R2; apply Rlt_trans with v; auto with real.
apply finite_vals_canonizer.
intros q; apply cartesian_Rplus_correct.
apply Hf.
apply Hg.
(* *)
intros t Ht1 Ht2.
rewrite measure_le_0_eq_0.
apply Rbar_mult_0_r.
apply measurable_inter.
apply Hf.
generalize (measurable_fun_plus_R gen f g).
intros T; apply T with (A:= fun z : R => z = t).
now apply SF_aux_measurable with lf.
now apply SF_aux_measurable with lg.
apply measurable_R_eq.
apply Rbar_not_lt_le; easy.
(* *)
intros t Ht1 Ht2.
rewrite measure_le_0_eq_0.
apply Rbar_mult_0_r.
apply measurable_inter.
apply Hf.
apply Hg.
apply Rbar_not_lt_le; easy.
Qed.

(* Lemma 778 pp. 158-159 *)
Lemma LInt_SFp_plus :
  forall (f1 : E -> R) (H1 : SF gen f1) (f2 : E -> R) (H2 : SF gen f2),
    nonneg f1 -> nonneg f2 ->
    let H3 := SF_plus f1 H1 f2 H2 in
    LInt_SFp (fun x => f1 x + f2 x) H3  =
      Rbar_plus (LInt_SFp f1 H1) (LInt_SFp f2 H2).
Proof.
intros f1 (l1,H1) f2 (l2,H2) P1 P2 H3.
unfold LInt_SFp; simpl.
apply sym_eq.
rewrite Rbar_plus_comm.
rewrite LInt_SFp_decomp with f1 f2 l1 l2; try assumption.
rewrite LInt_SFp_decomp with f2 f1 l2 l1; try assumption.
apply trans_eq with (Rbar_plus
  (sum_Rbar_map l2
     (fun a : R =>
        (sum_Rbar_map l1 (fun z : R =>
           Rbar_mult a (mu (fun x : E => f2 x = a /\ f1 x = z))))))
  (sum_Rbar_map l1
     (fun a : R =>
        (sum_Rbar_map l2 (fun z : R =>
           Rbar_mult a (mu (fun x : E => f1 x = a /\ f2 x = z)))))) ).
f_equal.
apply sum_Rbar_map_ext_f.
intros x Hx; apply sum_Rbar_map_Rbar_mult.
intros y Hy; apply meas_nonneg.
apply sum_Rbar_map_ext_f.
intros x Hx; apply sum_Rbar_map_Rbar_mult.
intros y Hy; apply meas_nonneg.
rewrite sum_Rbar_map_switch.
rewrite Rbar_plus_sum_Rbar_map.
apply trans_eq with
  (sum_Rbar_map l1 (fun x => sum_Rbar_map l2
        (fun z => Rbar_mult (Rbar_plus z x)
              (mu (fun x0 : E => f2 x0 = z /\ f1 x0 = x))))).
apply sum_Rbar_map_ext_f.
intros x Hx.
rewrite Rbar_plus_sum_Rbar_map.
apply sum_Rbar_map_ext_f.
intros y Hy.
rewrite Rbar_mult_plus_distr_r.
f_equal; f_equal.
apply measure_ext.
intros z; split; intros (J1,J2); split; easy.
apply SF_nonneg_In_ge_0 with f2 l2; easy.
apply SF_nonneg_In_ge_0 with f1 l1; easy.
intros z Hz.
apply Rbar_mult_le_pos_pos_pos.
apply SF_nonneg_In_ge_0 with f2 l2; easy.
apply meas_nonneg.
intros z Hz.
apply Rbar_mult_le_pos_pos_pos.
apply SF_nonneg_In_ge_0 with f1 l1; easy.
apply meas_nonneg.
2: intros z Hz.
2: apply sum_Rbar_map_ge_0.
2: intros w Hw; apply Rbar_mult_le_pos_pos_pos.
2: apply SF_nonneg_In_ge_0 with f2 l2; easy.
2: apply meas_nonneg.
2: intros z Hz.
2: apply sum_Rbar_map_ge_0.
2: intros w Hw; apply Rbar_mult_le_pos_pos_pos.
2: apply SF_nonneg_In_ge_0 with f1 l1; easy.
2: apply meas_nonneg.
2: intros x y Hx Hy; apply Rbar_mult_le_pos_pos_pos.
2: apply SF_nonneg_In_ge_0 with f2 l2; easy.
2: apply meas_nonneg.
apply trans_eq with
(sum_Rbar_map l1
  (fun x : R =>
     sum_Rbar_map (canonizer (fun x => ((f1 x)+(f2 x)))
                  (cartesian_Rplus l1 l2))
    (fun t =>
       Rbar_mult t (mu (fun x0 => f1 x0 = x /\ (f1 x0)+(f2 x0) = t))))).
apply sum_Rbar_map_ext_f.
intros x Hx.
rewrite <- sum_Rbar_map_change_of_variable; try easy.
apply sum_Rbar_map_ext_f.
intros z Hz; f_equal.
simpl; rewrite Rplus_comm; easy.
apply measure_ext.
intros w; split; intros (Y1,Y2); easy.
(* *)
rewrite LInt_SFp_decomp
  with (g:=f1) (lg:=l1); try easy.
apply sym_eq; apply trans_eq with
 (sum_Rbar_map (proj1_sig H3)
  (fun a : R =>
     sum_Rbar_map l1
        (fun z : R =>
         Rbar_mult a (mu
           (fun x : E =>
             (f1 x)+(f2 x) = a /\ f1 x = z))))).
apply sum_Rbar_map_ext_f.
intros w Hw.
apply sum_Rbar_map_Rbar_mult.
intros x _; apply meas_nonneg.
rewrite sum_Rbar_map_switch.
apply sum_Rbar_map_ext_f.
intros x Hx.
replace (canonizer (fun x0 : E => (f1 x0)+(f2 x0))
     (cartesian_Rplus l1 l2))
   with (proj1_sig H3).
apply sum_Rbar_map_ext_f.
intros x0 Hx0.
f_equal.
apply measure_ext.
intros z; split; intros (Y1,Y2); easy.
apply finite_vals_canonic_unique with
 (fun x => (f1 x)+(f2 x)); try easy.
destruct H3; destruct s; simpl; easy.
apply finite_vals_canonizer.
intros w.
apply cartesian_Rplus_correct.
apply H1.
apply H2.
intros x y Hx Hy.
apply Rbar_mult_le_pos_pos_pos.
apply SF_nonneg_In_ge_0 with (fun x : E => f1 x + f2 x) (proj1_sig H3); try easy.
destruct H3; destruct s; simpl; easy.
intros w; simpl; apply Rplus_le_le_0_compat.
apply P1.
apply P2.
apply meas_nonneg.
destruct H3; destruct s; simpl; easy.
Qed.

(* From Lemma 757 pp. 152-153 *)
Lemma SF_scal :
  forall (f : E -> R) (H : SF gen f) a, SF gen (fun x => a * f x).
Proof.
intros f (l, H) a.
exists (canonizer (fun x : E => a*(f x))
                  (map (Rmult a) l)).
split.
apply finite_vals_canonizer.
intros y; apply in_map.
apply H.
intros x.
apply measurable_fun_scal_R with (A := fun z => z = x).
apply SF_aux_measurable with l; easy.
apply measurable_R_eq.
Defined.

Lemma SF_minus :
  forall (f1 : E -> R) (H1 : SF gen f1) (f2 : E -> R) (H2 : SF gen f2),
    SF gen (fun x => f1 x - f2 x).
Proof.
intros f1 H1 f2 H2; unfold Rminus.
apply SF_plus; try easy.
replace (fun x => -f2 x) with (fun x => (-1*f2 x)).
apply SF_scal; easy.
apply functional_extensionality.
intros t; ring.
Qed.

Lemma LInt_SFp_scal_aux :
  forall f l a,
    SF_aux gen f l -> 0 < a ->
    map (fun x0 => a * x0) l = canonizer (fun x0 => a * f x0) (map (Rmult a) l).
Proof.
intros f l a ((H0,(H1,H2)),H3) H4.
assert (T:finite_vals (fun x0 : E => Rmult a (f x0)) (map (Rmult a) l)).
intros y; apply in_map; apply H2.
apply finite_vals_canonic_unique with
   (fun x => Rmult a (f x)); try assumption.
2: apply finite_vals_canonizer; auto.
split.
apply LocallySorted_map; try assumption.
intros x y; now apply Rmult_lt_compat_l.
split; try assumption.
intros x H5.
destruct (H1 (Rmult (/a) x)).
replace l with (map (fun x0 : R => Rmult (/a) x0)
    (map (fun x0 : R => Rmult a x0) l)).
now apply in_map.
rewrite map_map.
rewrite <- map_id.
f_equal.
apply functional_extensionality.
intros y.
field; auto with real.
exists x0.
rewrite H.
field; auto with real.
Qed.

(* From Lemma 779 pp. 159-160 *)
Lemma LInt_SFp_scal :
  forall (f : E -> R) (H : SF gen f) a,
    nonneg f -> 0 <= a ->
    let H' := SF_scal f H a in
    LInt_SFp (fun x => a * f x) H' = Rbar_mult a (LInt_SFp f H).
Proof.
intros f (l,H) a J1 J2 H'.
case (Rle_lt_or_eq_dec _ _ J2).
   (* a finite and > 0 *)
intros J3.
unfold LInt_SFp.
simpl.
rewrite sum_Rbar_map_Rbar_mult.
2: intros y Hy; now apply nonneg_af1.
replace (canonizer (fun x : E => a*(f x))
     (map (Rmult a) l)) with
  (map (fun x => a*x) l).
rewrite sum_Rbar_map_map.
apply sum_Rbar_map_ext_f.
intros y Hy; unfold af1.
rewrite Rbar_mult_assoc.
f_equal.
apply sym_eq, measure_ext.
intros z; split; intros H1; f_equal.
injection H1; intros H1'; now rewrite H1'.
apply Rmult_eq_reg_l with a.
now injection H1.
now apply Rgt_not_eq.
apply LInt_SFp_scal_aux; easy.
 (* a = 0 *)
intros J3; rewrite <- J3 at 1.
rewrite Rbar_mult_0_l.
destruct Einhab.
rewrite <- (LInt_SFp_0 X).
apply LInt_SFp_ext; try easy.
intros y.
rewrite <- J3, Rmult_0_l.
apply Rbar_le_refl.
intros y; rewrite <- J3; apply Rmult_0_l.
Qed.

(* Lemma 781 p. 160 *)
Lemma LInt_SFp_monotone :
  forall (f g : E -> R) (Hf : SF gen f) (Hg : SF gen g),
    nonneg f -> nonneg g ->
    (forall x, f x <= g x) ->
    Rbar_le (LInt_SFp f Hf) (LInt_SFp g Hg).
Proof.