Library Lebesgue.simple_fun

This file is part of the Coq Numerical Analysis 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.

Brief description

Support for Lebesgue integration of simple functions.

Description

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.

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 List Sorted.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Flocq Require Import Core.

From Subsets Require Import Subsets_wDep.
From Lebesgue Require Import list_compl sort_compl.
From Lebesgue Require Import R_compl Rbar_compl sum_Rbar_nonneg.
From Lebesgue Require Import sigma_algebra sigma_algebra_R_Rbar.
From Lebesgue Require Import measurable_fun.
From Lebesgue Require Import measure.

Local Open Scope R_scope.

Section finite_vals_def.

Context {E : Type}.

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

Definition finite_vals_canonic : (E R) list R Prop :=
  fun f l
    (LocallySorted Rlt l)
    ( x, In x l y, f y = x)
    ( y, In (f y) l).

Lemma finite_vals_canonic_not_nil :
   f l, inhabited E finite_vals_canonic f l l nil.
Proof.
intros f l [ x ] (V1,(V2,V3)) V4.
rewrite V4 in V3.
specialize (V3 x).
apply (in_nil V3).
Qed.

Lemma finite_vals_canonic_nil :
   f l, ¬ inhabited E finite_vals_canonic f l l = nil.
Proof.
intros f l; case l; try easy.
clear l; intros a l H1 H2.
exfalso; apply H1.
destruct H2 as (_,(Y1,_)).
destruct (Y1 a); try easy.
apply in_eq.
Qed.

Lemma finite_vals_canonic_unique :
   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 :
   (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 lsort Rle (RemoveUseless f (nodup Req_EM_T l)).

Lemma finite_vals_canonizer :
   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 yx 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.
y; easy.
Qed.

Lemma finite_vals_unique :
   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 :
   f l x, ( 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: y; easy.
apply nodup_In; easy.
Qed.

Lemma canonizer_Sorted :
   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.
y; easy.
Qed.

Lemma finite_vals_sum_eq :
   f l, finite_vals_canonic f l
     y, Finite (f y) =
      sum_Rbar_map l (fun aa × (charac (fun xf x = a) y)).
Proof.
intros f l (Y1,(Y2,Y3)) y.
rewrite sum_Rbar_map_select_eq with
   (P:= fun z:Rz = f y).
2: intros t Ht1 Ht2; f_equal.
2: rewrite charac_is_0; auto with real.
2: unfold compl; now apply not_eq_sym.
replace (select (fun z : Rz = 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 :
   f l A,
    finite_vals_canonic f l nonneg f
     y, Finite (f y × charac A y) =
      sum_Rbar_map l (fun tt × (charac (fun xA 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 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 : Ef x0 = x) y); intros L; rewrite L;
 auto with real.
Qed.

Lemma finite_vals_canonic_cons :
   (f : E R) v1 v2 l,
    nonneg f
    finite_vals_canonic f (v1 :: v2 :: l)
    let g := fun xf x + (v1-v2) × charac (fun tf t = v2) x in
    ( x, f x = v2 g x = v1) ( 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: x, f x = v2 g x = v1).
intros x Hx; unfold g.
rewrite charac_is_1, Hx; try ring; easy.
assert (Z2: 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.
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}.

Variable gen : (E Prop) Prop.

Definition SF_aux : (E R) list R Prop :=
  fun f l
    finite_vals_canonic f l
    ( a, measurable gen (fun xf x = a)).

Definition SF : (E R) Set := fun f{ l | SF_aux f l }.

Definition SFplus : (E R) Prop :=
  fun fnonneg f l, SF_aux f l.

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

End SF_def.

Section SF_Facts.

Context {E : Type}.

Variable gen : (E Prop) Prop.

Lemma SFplus_cons :
   (f : E R) v1 v2 l,
    nonneg f
    SF_aux gen f (v1 :: v2 :: l)
    let g := fun xf x + (v1 - v2) × charac (fun tf 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_SF_def.

Context {E : Type}.

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

Definition af1 : (E R) Rbar Rbar :=
  fun f aRbar_mult a (mu (fun xFinite (f x) = a)).

Lemma nonneg_af1 : 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 : EFinite (f x0) = x) = 0).
transitivity (mu (fun x0 : EFalse)).
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.

Definition LInt_SF : (f : E R), SF gen f Rbar :=
  fun f Hlet l := proj1_sig H in sum_Rbar_map l (af1 f).

Lemma LInt_SF_correct :
   f (H1 H2 : SF gen f), LInt_SF f H1 = LInt_SF f H2.
Proof.
intros f (l1,H1) (l2,H2).
unfold LInt_SF; simpl.
rewrite finite_vals_canonic_unique with f l1 l2; try easy.
apply H1.
apply H2.
Qed.

Lemma LInt_SF_ext :
   f1 (H1 : SF gen f1) f2 (H2 : SF gen f2),
    ( x, f1 x = f2 x)
    LInt_SF f1 H1 = LInt_SF f2 H2.
Proof.
intros f1 H1 f2 H2 J.
assert (f1 = f2).
now apply fun_ext.
generalize H1.
rewrite H.
intros H3.
apply LInt_SF_correct.
Qed.

Lemma LInt_SF_ext_ex :
   f1 (H1 : SF gen f1) f2,
    ( x, f1 x = f2 x)
      (H2 : SF gen f2),
        LInt_SF f1 H1 = LInt_SF f2 H2.
Proof.
intros f1 H1 f2 H3.
assert (T:f1 = f2).
now apply fun_ext.
generalize H1; intros H4.
rewrite T in H1.
H1.
apply LInt_SF_ext; easy.
Qed.

Lemma SF_cst : a, SF gen (fun _a).
Proof.
intros a.
case (excluded_middle_informative (( t:E, True)) ); intros Z.
apply constructive_indefinite_description in Z.
destruct Z as [ t _ ].
(a :: nil).
split.
split.
apply LSorted_cons1.
split.
intros x H.
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.
nil; split; try split; try split.
apply LSorted_nil.
intros; easy.
intros t; contradict Z; easy.
intros b; apply measurable_ext with (2:=measurable_empty gen).
intros t; contradict Z; easy.
Defined.

Lemma LInt_SF_0 : LInt_SF (fun _ ⇒ 0) (SF_cst 0) = 0.
Proof.
unfold SF_cst, LInt_SF, af1, sum_Rbar_map; simpl.
case (excluded_middle_informative ( _ : E, True)); [simpl | easy].
intros (t,Ht); case (constructive_indefinite_description _); simpl.
intros _ _; rewrite Rbar_mult_0_l, Rbar_plus_0_l; easy.
Qed.

Lemma SF_aux_measurable :
   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 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)).
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 :
   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 :
   f (Hf : SF gen f), measurable_fun_Rbar gen f.
Proof.
intros; now apply measurable_fun_R_Rbar, SF_measurable.
Qed.

Lemma SFplus_Mplus :
   (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 :
   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 :
   f (Hf : SF gen f), nonneg f Rbar_le 0 (LInt_SF f Hf).
Proof.
intros f (l,Hl) Hf; unfold LInt_SF.
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 l2flat_map (fun a ⇒ (map (fun xa + x) l2)) l1.

Lemma cartesian_Rplus_correct :
   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.
x1.
split; try easy.
now apply in_map.
Qed.

Lemma SF_plus :
   (f1 : E R) (H1 : SF gen f1) (f2 : E R) (H2 : SF gen f2),
    SF gen (fun xf1 x + f2 x).
Proof.
intros f1 (l1,H1) f2 (l2,H2).
(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 : Rz = a).
now apply SF_aux_measurable with l1.
now apply SF_aux_measurable with l2.
apply measurable_R_eq.
Qed.

Lemma SF_decomp_aux :
   (f g : E R) lf lg y,
    SF_aux gen f lf SF_aux gen g lg
    In y lf
    mu (fun xf x = y) =
      sum_Rbar_map lg (fun zmu (fun xf x = y g x = z)).
Proof.
intros f g lf lg y Hf Hg Hy.
assert (Z: inhabited E).
destruct Hf as ((_,(Y1,_)),_).
destruct (Y1 y Hy) as (t,Ht); easy.
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 xg 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.
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 SF_decomp :
   (f g : E R) lf lg y,
    SF_aux gen f lf SF_aux gen g lg
    mu (fun xf x = y) =
      sum_Rbar_map lg (fun zmu (fun xf 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 SF_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_SF_decomp :
   (f g : E R) lf lg,
    SF_aux gen f lf SF_aux gen g lg
     sum_Rbar_map lf (af1 f) =
      sum_Rbar_map lf (fun a
        Rbar_mult a (sum_Rbar_map lg (fun zmu (fun xf x = a g x = z)))).
Proof.
intros f g lf lg Hf Hg.
f_equal; f_equal; unfold af1.
apply fun_ext.
intros x; f_equal.
rewrite <- SF_decomp with (lf:=lf); try easy.
apply measure_ext.
intros y; split; intros H.
injection H; easy.
rewrite H; easy.
Qed.

Lemma sum_Rbar_map_change_of_variable :
   (f g : E R) lf lg y,
    SF_aux gen f lf SF_aux gen g lg
    sum_Rbar_map lg (fun zRbar_mult (y + z) (mu (fun xf x = y g x = z))) =
      sum_Rbar_map (canonizer (fun xf x + g x) (cartesian_Rplus lf lg))
        (fun tRbar_mult t (mu (fun xf x = y f x + g x = t))).
Proof.
intros f g lf lg y Hf Hg.
pose (A:=fun z xf x = y g x = z).
pose (B:=fun t xf 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 : Ef x + g x)
     (cartesian_Rplus lf lg))
  (fun t : RRbar_mult t (mu (B t)))).
rewrite (sum_Rbar_map_select_eq (fun zRbar_lt 0
     (mu (A z))) (fun z : RRbar_mult (y + z)
      (mu (A z)))).
rewrite (sum_Rbar_map_select_eq
  (fun tRbar_lt 0
     (mu (B t)))
   (fun t : RRbar_mult t
        (mu (B t)))).
pose (lA:=(select (fun z : RRbar_lt 0 (mu (A z)))
     lg)); fold lA.
pose (lB:=(select
     (fun t : RRbar_lt 0 (mu (B t)))
     (canonizer (fun x : Ef x + g x)
        (cartesian_Rplus lf lg)))); fold lB.
pose (tau := fun zy+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 tRbar_mult t (mu (B t)))).
assert (Y1: 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: 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.
intros H1; apply in_map_iff in H1.
destruct H1 as (z,(Hz1,Hz2)).
rewrite <- Hz1; unfold tau.
assert (H: 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.
x; unfold A in H; split; apply H.
apply In_select_P_inv.
apply In_canonizer; try easy.
destruct H as (x,(Hx1,Hx2)).
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.
intros H1.
replace t with (tau (t-y)).
2: unfold tau; ring.
apply in_map.
assert (H: 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 : Ef x + g x)
           (cartesian_Rplus lf lg))) (x:=t); try easy.
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 : Ef x + g x)
           (cartesian_Rplus lf lg))) (x:=t); easy.
intros x; apply Y2.
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 : Rz = 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 LInt_SFp_plus :
   (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_SF (fun xf1 x + f2 x) H3 =
      Rbar_plus (LInt_SF f1 H1) (LInt_SF f2 H2).
Proof.
intros f1 (l1,H1) f2 (l2,H2) P1 P2 H3.
unfold LInt_SF; simpl.
apply sym_eq.
rewrite Rbar_plus_comm.
rewrite LInt_SF_decomp with f1 f2 l1 l2; try assumption.
rewrite LInt_SF_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 : Ef2 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 : Ef1 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 xsum_Rbar_map l2
        (fun zRbar_mult (Rbar_plus z x)
              (mu (fun x0 : Ef2 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 x0f1 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_SF_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 : Ef1 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.

Lemma SF_scal :
   (f : E R) (H : SF gen f) a, SF gen (fun xa × f x).
Proof.
intros f (l, H) a.
(canonizer (fun x : Ea*(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 zz = x).
apply SF_aux_measurable with l; easy.
apply measurable_R_eq.
Defined.

Lemma SF_minus :
   (f1 : E R) (H1 : SF gen f1) (f2 : E R) (H2 : SF gen f2),
    SF gen (fun xf1 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 fun_ext.
intros t; ring.
Qed.

Lemma LInt_SFp_scal_aux :
   f l a,
    SF_aux gen f l 0 < a
    map (fun x0a × x0) l = canonizer (fun x0a × f x0) (map (Rmult a) l).
Proof.
intros f l a ((H0,(H1,H2)),H3) H4.
assert (T:finite_vals (fun x0 : ERmult a (f x0)) (map (Rmult a) l)).
intros y; apply in_map; apply H2.
apply finite_vals_canonic_unique with
   (fun xRmult 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 : RRmult (/a) x0)
    (map (fun x0 : RRmult a x0) l)).
now apply in_map.
rewrite map_map.
rewrite <- map_id.
f_equal.
apply fun_ext.
intros y.
field; auto with real.
x0.
rewrite H.
field; auto with real.
Qed.

Lemma LInt_SFp_scal :
   (f : E R) (H : SF gen f) a,
    nonneg f 0 a
    let H' := SF_scal f H a in
    LInt_SF (fun xa × f x) H' = Rbar_mult a (LInt_SF f H).
Proof.
intros f (l,H) a J1 J2 H'.
case (Rle_lt_or_eq_dec _ _ J2).
intros J3.
unfold LInt_SF.
simpl.
rewrite sum_Rbar_map_Rbar_mult.
2: intros y Hy; now apply nonneg_af1.
replace (canonizer (fun x : Ea*(f x))
     (map (Rmult a) l)) with
  (map (fun xa×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.
intros J3; rewrite <- J3 at 1.
rewrite Rbar_mult_0_l.
rewrite <- LInt_SF_0.
apply LInt_SF_ext.
intros t; rewrite <- J3; ring.
Qed.

Lemma LInt_SFp_monotone :
   (f g : E R) (Hf : SF gen f) (Hg : SF gen g),
    nonneg f nonneg g
    ( x, f x g x)
    Rbar_le (LInt_SF f Hf) (LInt_SF g Hg).
Proof.
intros f g Hf Hg H1 H2 Hfg.
pose (h':= fun xg x + (-1)*f x).
pose (h:= fun xf x + h' x).
assert (Y1: x, h x = g x).
intros ; unfold h, h'; ring.
assert (Hh' : SF gen h').
apply SF_plus; try easy.
now apply SF_scal.
assert (Zh' : nonneg (fun x : Eh' x)).
intros x; unfold h'.
simpl; apply Rplus_le_reg_l with (f x).
ring_simplify; easy.
replace (LInt_SF g Hg) with
  (LInt_SF h (SF_plus f Hf h' Hh')).
unfold h; rewrite LInt_SFp_plus; try easy.
rewrite <- (Rbar_plus_0_r (LInt_SF f Hf)) at 1.
apply Rbar_plus_le_compat_l.
apply LInt_SFp_pos; easy.
apply sym_eq, LInt_SF_ext; easy.
Qed.

Lemma LInt_SFp_continuous :
   (f : E R) (Hf : SF gen f),
    nonneg f
    LInt_SF f Hf =
      Rbar_lub (fun x
         (g : E R), (Hg : SF gen g),
          nonneg g
          ( z, g z f z)
          LInt_SF g Hg = x).
Proof.
intros f Hf Zf.
apply sym_eq, Rbar_is_lub_unique.
split.
unfold Rbar_is_upper_bound;
 intros x (g,(Hg1,(Hg2,(Hg3,Hg4)))).
rewrite <- Hg4.
apply LInt_SFp_monotone; assumption.
intros x; unfold Rbar_is_upper_bound.
intros H; apply H.
f; Hf; split; try easy.
Qed.

Lemma SF_charac : A, measurable gen A SF gen (charac A).
Proof.
intros A HA.
(canonizer (charac A) (0::1::nil)).
split.
apply finite_vals_canonizer.
intros x.
case (charac_or A x); intros H; rewrite H.
apply in_eq.
apply in_cons, in_eq.
intros a.
apply (measurable_fun_charac_R gen A HA (fun zz = a)).
apply measurable_R_eq.
Defined.

Lemma LInt_SF_charac :
   A (HA : measurable gen A),
    LInt_SF (charac A) (SF_charac A HA) = mu A.
Proof.
intros A HA.
unfold LInt_SF; simpl.
rewrite canonizer_Sorted; try easy.
unfold RemoveUseless; simpl.
case (in_dec _ _); case (in_dec _ _); intros Y1 Y2;
  unfold sum_Rbar_map; simpl; unfold af1.
rewrite Rbar_mult_0_l, Rbar_plus_0_l.
rewrite Rbar_mult_1_l, Rbar_plus_0_r.
apply measure_ext.
intros x; split; intros H.
apply charac_1.
injection H; easy.
f_equal; apply charac_is_1; easy.
rewrite Rbar_mult_0_l, Rbar_plus_0_l.
rewrite <- meas_emptyset with gen mu.
apply measure_ext.
intros x; split; try easy.
intros Hx; apply Y1.
x.
now apply charac_is_1.
rewrite Rbar_mult_1_l, Rbar_plus_0_r.
apply measure_ext.
intros x; split; intros H.
apply charac_1.
injection H; easy.
f_equal; apply charac_is_1; easy.
rewrite <- meas_emptyset with gen mu.
apply measure_ext.
intros x; split; try easy.
intros Hx; apply Y1.
x.
now apply charac_is_1.
intros y.
case (charac_or A y); intros Hy.
rewrite Hy; apply in_eq.
rewrite Hy; apply in_cons, in_eq.
apply LSorted_consn.
apply LSorted_cons1.
apply Rlt_0_1.
Qed.

Lemma Lint_SFp_skip_0 :
   (f : E R) (Hf : SF gen f) l,
    nonneg_l (map Finite l) finite_vals f (0 :: l) NoDup l
    LInt_SF f Hf = sum_Rbar_map l (af1 f).
Proof.
intros f (lf,((Y1,(Y2,Y3)),Y4)) l Hl H1 H2; simpl.
unfold LInt_SF; simpl.
apply trans_eq with (sum_Rbar_map (sort Rle l)
  (fun a : Raf1 f (Finite a))).
apply sum_Rbar_map_ext_l; try easy.
apply Sorted_In_eq_eq.
intros x; split; intros Hx;
  generalize (In_select_P _ _ _ Hx);
  generalize (In_select_In _ _ _ Hx); intros M1 M2.
apply In_select_P_inv; try easy.
apply Permutation.Permutation_in with l.
apply corr_sort.
destruct (Y2 x M1) as (y,Hy); rewrite <- Hy.
specialize (H1 y).
case (in_inv H1); try easy.
intros K; contradict M2.
unfold af1; rewrite <- Hy, <- K.
apply Rbar_mult_0_l.
apply In_select_P_inv; try easy.
case (excluded_middle_informative ( y, f y = x)).
intros (y,Hy); rewrite <- Hy.
apply Y3.
intros K.
assert (K': y, f y x).
apply not_ex_not_all.
intros (z,Hz); apply K.
z.
case (Req_dec (f z) x); auto with real.
intros L; now contradict Hz.
generalize M2; intros M2'.
contradict M2'; unfold af1.
rewrite measure_ext with gen mu _ (fun _False).
rewrite meas_emptyset; simpl; f_equal; ring.
intros y; split; try easy.
intros M; injection M; apply K'.
apply LocallySorted_select; try assumption.
intros x y z J1 J2; apply Rlt_trans with (1:=J1); easy.
apply LocallySorted_select; try assumption.
intros x y z J1 J2; apply Rlt_trans with (1:=J1); easy.
apply LocallySorted_impl with (Rle) (fun x yx y).
intros a b N; case N; intros N1 N2; auto with real.
now contradict N1.
apply LocallySorted_sort_Rle.
apply LocallySorted_neq.
apply Permutation.Permutation_NoDup with (2:=H2).
apply corr_sort.
apply sym_eq, sum_Rbar_map_Perm_strict.
apply corr_sort.
intros x Hx; unfold af1.
apply Rbar_mult_le_pos_pos_pos.
apply nonneg_l_In with (map Finite l); try easy.
apply in_map; easy.
apply meas_nonneg.
Qed.

Lemma SF_mult_charac :
   (f : E R) (Hf : SF gen f) A,
    measurable gen A
    SF gen (fun xf x × charac A x).
Proof.
intros f (l,(Hl1,Hl2)) A HA.
pose (g:= fun xf x × charac A x); fold g.
(canonizer g (0::l)).
split.
apply finite_vals_canonizer.
intros y; unfold g.
case (charac_or A y); intros Hy.
rewrite Hy, Rmult_0_r.
apply in_eq.
rewrite Hy, Rmult_1_r.
apply in_cons.
apply Hl1.
intros y; unfold g.
apply measurable_ext with (fun x
    (y=0 (¬A x f x = 0))
   
    (y 0 A x (f x = y))).
intros x; case (charac_or A x); intros L; rewrite L;
    try rewrite Rmult_0_l; try rewrite Rmult_1_l.
apply charac_0 in L.
case (Req_dec y 0); intros Hy.
rewrite Rmult_0_r.
split; try easy; intros _; left; split; try easy; now left.
rewrite Rmult_0_r.
split; try easy.
intros T; case T; try easy.
intros T; contradict Hy; easy.
apply charac_1 in L; rewrite Rmult_1_r; split.
intros T; case T; try easy.
intros (Y1,Y2); case Y2; try easy.
intros Y3; rewrite Y1,Y3; easy.
case (Req_dec y 0); intros Hy1 Hy2.
left; split; try easy.
right; rewrite <- Hy1; easy.
right; split; try split; easy.
apply measurable_union; apply measurable_inter;
   try apply measurable_union; try apply measurable_inter;
   try easy; try apply measurable_Prop.
apply measurable_compl_rev; easy.
Defined.

Lemma SF_scal_charac :
   a A, measurable gen A SF gen (fun ta × charac A t).
Proof.
intros a A HA; apply SF_mult_charac; try easy.
apply SF_cst.
Qed.

Lemma SFplus_mult_charac_alt:
   (f : E R) (Hf : SF gen f) A,
    measurable gen A nonneg f
    SF gen (fun y
      sum_Rbar_map (proj1_sig Hf) (fun tt × charac (fun xA x f x = t) y)).
Proof.
intros f Hf A HA P.
assert (T:(fun yreal (sum_Rbar_map (proj1_sig Hf)
        (fun t : R
         Finite
           (t ×
            charac
              (fun x : E
               A x f x = t) y)))) =
   (fun y:E ⇒ (Finite (f y × charac A y)))).
apply fun_ext.
intros x; apply sym_eq; f_equal.
apply finite_vals_charac_sum_eq; try easy.
destruct Hf as (l,Hl); apply Hl.
rewrite T.
apply SF_mult_charac; easy.
Defined.

Lemma LInt_SFp_mult_charac_aux :
   (f : E R) (Hf : SF gen f) A (HA : measurable gen A) (P : nonneg f),
    let H3 := SF_mult_charac f Hf A HA in
    let H4 := SFplus_mult_charac_alt f Hf A HA P in
    LInt_SF (fun xf x × charac A x) H3 =
      LInt_SF (fun y
        sum_Rbar_map (proj1_sig Hf) (fun tt × charac (fun xA x f x = t) y)) H4.
Proof.
intros f Hf A HA P H3 H4.
apply LInt_SF_ext.
intros x.
rewrite <- finite_vals_charac_sum_eq; try easy.
destruct Hf as (l,Hl); apply Hl.
Qed.

Lemma LInt_SFp_mult_charac :
   (f : E R) (Hf : SF gen f) A (HA : measurable gen A),
    nonneg f
    let H3 := SF_mult_charac f Hf A HA in
    LInt_SF (fun xf x × charac A x) H3 =
      sum_Rbar_map (proj1_sig Hf)
         (fun t : RRbar_mult t (mu (fun xA x f x = t))).
Proof.
intros f Hf A HA P H3.
destruct Hf as (l,Hl); simpl.
rewrite Lint_SFp_skip_0 with (l:=l).
apply sum_Rbar_map_ext_f.
intros x Hx; unfold af1.
case (Req_dec x 0); intros Zx.
rewrite Zx, 2!Rbar_mult_0_l; easy.
f_equal.
apply measure_ext.
intros y; split.
intros H1; assert (A y).
apply charac_1.
case (charac_or A y); try easy.
intros T; contradict H1.
rewrite T; rewrite Rmult_0_r.
apply sym_not_eq; simpl; injection; apply Zx.
split; try easy.
injection H1; intros T; rewrite <- T.
rewrite charac_is_1; try easy; ring.
intros (H1,H2); f_equal.
rewrite H2, charac_is_1; try easy; ring.
apply In_nonneg_l.
intros x Hx.
destruct Hl as ((Y1,(Y2,Y4)),Y3).
destruct (Y2 x) as (y,Hy).
apply In_map_Finite; easy.
generalize (P y); intros H; simpl in H.
assert (H0: is_finite x).
clear - Hx.
generalize Hx; case x; try easy.
intros T; rewrite in_map_iff in T.
destruct T as (y,(Hy1,Hy2)); easy.
intros T; rewrite in_map_iff in T.
destruct T as (y,(Hy1,Hy2)); easy.
rewrite <- H0, <- Hy; simpl; easy.
intros y.
case (charac_or A y); intros HAy; rewrite HAy.
rewrite Rmult_0_r; apply in_eq.
rewrite Rmult_1_r; apply in_cons.
apply Hl.
apply LocallySorted_Rlt_NoDup.
apply Hl.
Qed.

End LInt_SF_def.

Section Adap_seq_def.

Context {E : Type}.
Variable gen : (E Prop) Prop.

Definition is_adapted_seq : (E Rbar) (nat E R) Prop :=
  fun f phi
    ( n, nonneg (phi n))
    incr_fun_seq phi

    ( x, is_sup_seq (fun nphi n x) (f x)).

Definition SF_seq : (nat E R) Set := fun phi n, SF gen (phi n).

Lemma is_adapted_seq_is_lim_seq :
   f phi x, is_adapted_seq f phi is_lim_seq (fun nphi n x) (f x).
Proof.
intros f phi x (Y1,(Y2,Y3)).
apply is_sup_incr_is_lim_seq; try easy.
intros n; apply Y2.
Qed.

Lemma is_adapted_seq_nonneg : f phi, is_adapted_seq f phi nonneg f.
Proof.
intros f phi (Y1,(Y2,Y3)); intros x.
apply is_sup_seq_le with (fun _ ⇒ 0) (fun n : natphi n x); try easy.
intros n; apply Y1.
intros eps; split; intros; simpl.
rewrite Rplus_0_l; apply eps.
0%nat; apply Rplus_lt_reg_l with eps; ring_simplify.
apply eps.
Qed.

End Adap_seq_def.

Section Adap_seq_mk.

Notation bpow2 e := (bpow radix2 e).

Context {E: Type}.

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

Variable f : E Rbar.
Hypothesis f_Mplus : Mplus gen f.

Definition mk_adapted_seq : nat E R :=
  fun n xmatch Rbar_le_lt_dec (INR n) (f x) with
    | left _INR n
    | right _round radix2 (FIX_exp (-Z.of_nat n)) Zfloor (f x)
    end.

Lemma mk_adapted_seq_le : n x, Rbar_le (mk_adapted_seq n x) (f x).
Proof with auto with typeclass_instances.
intros n x; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros H; try easy.
case_eq (f x).
intros r Hr; simpl.
apply round_DN_pt...
intros _; easy.
destruct f_Mplus as [Hf _].
intros K; specialize (Hf x).
contradict Hf.
rewrite K; easy.
Qed.

Lemma mk_adapted_seq_ge2 : n x, Rbar_le (mk_adapted_seq n x) (INR n).
Proof with auto with typeclass_instances.
intros n x; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros H.
apply Rbar_le_refl.
simpl; apply Rle_trans with (f x).
apply round_DN_pt...
destruct f_Mplus as [Hf _].
generalize (Hf x), H; case (f x); try easy.
simpl; auto with real.
Qed.

Lemma mk_adapted_seq_nonneg : n, nonneg (mk_adapted_seq n).
Proof with auto with typeclass_instances.
intros n x; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _).
intros _; simpl.
apply pos_INR.
intros _; simpl.
apply round_ge_generic...
apply generic_format_0...
destruct f_Mplus as [Hf _].
specialize (Hf x).
case_eq (f x); simpl; try (intros _; apply Rle_refl).
intros r Hr; rewrite Hr in Hf; easy.
Qed.

Lemma mk_adapted_seq_incr : incr_fun_seq mk_adapted_seq.
Proof with auto with typeclass_instances.
intros x n; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros H1.
case (Rbar_le_lt_dec _ _); intros H2.
apply le_INR; auto with arith.
apply round_ge_generic...
replace (INR n) with (F2R (Float radix2 (Z.of_nat n) 0%Z)).
apply generic_format_F2R.
intros _; unfold FIX_exp, cexp; simpl.
apply Pos2Z.neg_is_nonpos.
unfold F2R; simpl; rewrite Rmult_1_r.
apply sym_eq, INR_IZR_INZ.
generalize H1 H2; case (f x); try easy.
case (Rbar_le_lt_dec _ _); intros H2.
absurd (Rbar_lt (INR n) (INR n)).
apply Rbar_le_not_lt; simpl; apply Rle_refl.
trans (INR (S n)) 1.
change (Rle (INR n) (INR (S n))); apply le_INR; auto with arith.
trans (f x) 1.
apply round_ge_generic...
assert (H:generic_format radix2 (FIX_exp (- Z.of_nat n))
     (round radix2 (FIX_exp (- Z.of_nat n)) Zfloor (f x))).
apply generic_format_round...
generalize H; generalize (round radix2 (FIX_exp (- Z.of_nat n)) Zfloor (f x)).
intros r Hr; rewrite Hr; apply generic_format_F2R.
intros _; unfold cexp, FIX_exp; simpl.
replace (Z.neg (Pos.of_succ_nat n)) with (- Z.of_nat (S n))%Z by easy.
assert (Z.of_nat n Z.of_nat (S n))%Z; lia.
apply round_DN_pt...
Qed.

Lemma mk_adapted_seq_is_sup :
   x, is_sup_seq (fun nmk_adapted_seq n x) (f x).
Proof with auto with typeclass_instances.
intros x.
case_eq (f x); simpl.
intros r Hr eps; split.
intros n.
generalize (mk_adapted_seq_le n x).
rewrite Hr; simpl.
intros Y; apply Rle_lt_trans with (1:=Y).
apply Rplus_lt_reg_l with (-r); ring_simplify; apply eps.
pose (m:=max (Z.abs_nat (up (f x)))
             (1+Z.abs_nat (mag radix2 (pos eps)))).
m.
unfold mk_adapted_seq; simpl.
case (Rbar_le_lt_dec _ _).
intros K; contradict K.
apply Rbar_lt_not_le.
rewrite Hr; simpl.
apply Rlt_le_trans with (IZR (up r)).
apply archimed.
unfold m; rewrite INR_IZR_INZ.
apply IZR_le.
apply Z.le_trans with
   (Z.of_nat (Z.abs_nat (up r))).
rewrite Zabs2Nat.id_abs.
apply Zabs_ind; auto with zarith.
rewrite Hr; apply inj_le.
apply Nat.le_max_l.
intros _; rewrite Hr.
apply Rplus_lt_reg_l with
  (eps-round radix2 (FIX_exp (- Z.of_nat m)) Zfloor r).
apply Rle_lt_trans with
  (-(round radix2 (FIX_exp (- Z.of_nat m)) Zfloor r - r)).
right; ring.
case (Req_dec r 0); intros Zr.
rewrite Zr, 2!round_0...
ring_simplify; apply eps.
apply Rle_lt_trans with (1:=RRle_abs _).
rewrite Rabs_Ropp.
apply Rlt_le_trans with (ulp radix2 (FIX_exp (- Z.of_nat m)) r).
apply error_lt_ulp...
rewrite ulp_FIX.
apply Rle_trans with eps; [idtac|simpl; right; ring].
unfold m; destruct (mag radix2 (pos eps)) as (e,He).
simpl (mag_val _ _ _).
apply Rle_trans with (bpow2 (e-1)).
apply bpow_le.
rewrite Nat2Z.inj_max.
apply Zopp_le_cancel; rewrite Z.opp_involutive.
apply Z.le_trans with (2:=Z.le_max_r _ _).
rewrite Nat2Z.inj_succ.
rewrite Zabs2Nat.id_abs.
apply Zabs_ind; lia.
rewrite <- Rabs_right.
2: apply Rle_ge; left; apply eps.
apply He.
apply Rgt_not_eq, eps.
intros Hr M.
(Z.abs_nat (up M)).
unfold mk_adapted_seq; simpl.
case (Rbar_le_lt_dec _ _).
intros _.
apply Rlt_le_trans with (IZR (up M)).
apply archimed.
rewrite INR_IZR_INZ, Zabs2Nat.id_abs, abs_IZR.
apply RRle_abs.
intros K; contradict K.
rewrite Hr; easy.
destruct f_Mplus as [Hf _].
intros K; specialize (Hf x).
contradict Hf.
rewrite K; easy.
Qed.

Lemma mk_adapted_seq_Sup :
   x, f x = Sup_seq (fun nmk_adapted_seq n x).
Proof with auto with typeclass_instances.
intros x.
apply sym_eq, is_sup_seq_unique.
apply mk_adapted_seq_is_sup.
Qed.

Lemma mk_adapted_seq_Lim :
   x, f x = Lim_seq (fun nmk_adapted_seq n x).
Proof with auto with typeclass_instances.
intros x.
rewrite Lim_seq_incr_Sup_seq.
2: apply mk_adapted_seq_incr.
apply mk_adapted_seq_Sup.
Qed.

Lemma mk_adapted_seq_is_adapted_seq : is_adapted_seq f mk_adapted_seq.
Proof.
split.
intros n x; apply mk_adapted_seq_nonneg.
split.
apply mk_adapted_seq_incr.
apply mk_adapted_seq_is_sup.
Qed.

Lemma mk_adapted_seq_SF_aux :
   n a, measurable gen (fun xmk_adapted_seq n x = a).
Proof with auto with typeclass_instances.
intros n a.
assert (Fn: generic_format radix2 (FIX_exp (- Z.of_nat n)) (INR n)).
replace (INR n) with (F2R (Float radix2 (Z.of_nat n) 0%Z)).
apply generic_format_F2R.
intros _; unfold FIX_exp, cexp; simpl; lia.
unfold F2R; simpl; rewrite Rmult_1_r.
apply sym_eq, INR_IZR_INZ.
case (excluded_middle_informative ( y, mk_adapted_seq n y = a)).
intros K; destruct K as (y,Hy).
assert (Fa: generic_format radix2 (FIX_exp (- Z.of_nat n)) a).
rewrite <- Hy; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros K; try easy.
apply generic_format_round...
generalize (mk_adapted_seq_ge2 n y); rewrite Hy; simpl; intros Ha'.
case (Req_dec a (INR n)); intros Ha.
apply measurable_ext with (fun zRbar_le (INR n) (f z)).
intros z; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros H.
split; easy.
split; intros H1.
absurd (Rbar_le (INR n) (INR n)).
2: apply Rbar_le_refl.
apply Rbar_lt_not_le.
trans (f z) 1.
contradict H1; apply Rlt_not_eq.
rewrite Ha; simpl.
apply Rle_lt_trans with (f z).
apply round_DN_pt...
destruct f_Mplus as [Hf _].
generalize H (Hf z); case (f z); try easy.
destruct f_Mplus as [_ Hf].
apply Hf with (A:= fun xRbar_le (INR n) x).
apply measurable_gen.
(Finite (INR n)); easy.
assert (L: r2:Rbar,
      (z:E),
       (Rbar_le a (f z) Rbar_lt (f z) r2)
              mk_adapted_seq n z = a).
(succ radix2 (FIX_exp (-Z.of_nat n)) a).
intros z; unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros Hz.
split.
intros (Y1,Y2).
assert (Ffz: is_finite (f z)).
destruct f_Mplus as [Hf _].
generalize Y2, (Hf z); case (f z); easy.
rewrite <- Ffz in Hz, Y1, Y2; simpl in Hz, Y1, Y2.
absurd (succ radix2 (FIX_exp (- Z.of_nat n)) a INR n)%R.
apply Rlt_not_le.
apply Rle_lt_trans with (f z); easy.
apply succ_le_lt...
case Ha'; try easy; intros K; now contradict K.
intros K; contradict K; now apply sym_not_eq.
assert (Fz: is_finite (f z)).
destruct f_Mplus as [Hf _].
generalize (Hf z), Hz; case (f z); easy.
rewrite <- Fz; simpl; rewrite <- Fz in Hz; simpl in Hz.
split.
intros (Y1,Y2).
apply round_DN_eq...
intros Y; split.
rewrite <- Y; apply round_DN_pt...
case (generic_format_EM radix2 (FIX_exp (- Z.of_nat n)) (f z)).
intros K; rewrite <- Y; rewrite round_generic...
case (Req_dec (f z) 0); intros L.
rewrite L, succ_0, ulp_FIX.
apply bpow_gt_0.
apply succ_gt_id; easy.
intros K.
rewrite <- Y; rewrite succ_DN_eq_UP...
assert (L: f z round radix2 (FIX_exp (- Z.of_nat n)) Zceil (f z)).
apply round_UP_pt...
case L; try easy.
intros K'; contradict K.
rewrite K'; apply generic_format_round...

destruct L as (r2,Hr2).
apply measurable_ext with
   (fun xRbar_le a (f x) Rbar_lt (f x) r2).
apply Hr2.
destruct f_Mplus as [_ Hf].
apply Hf with (A:= fun xRbar_le a x Rbar_lt x r2).
apply measurable_inter.
apply measurable_gen.
(Finite a); easy.
apply measurable_compl.
eapply measurable_ext.
2: apply measurable_gen.
2: r2; easy.
intros x; split; intros L.
now apply Rbar_le_not_lt.
now apply Rbar_not_lt_le.
intros H.
apply measurable_ext with (fun _False).
2: apply measurable_empty.
intros x; split; try easy.
intros K; apply H; x; easy.
Qed.

Lemma mk_adapted_seq_SF : SF_seq gen mk_adapted_seq.
Proof with auto with typeclass_instances.
assert (C1: N, { l | i,
    (i N)%nat In i l} ) .
induction N.
(0%nat::nil).
intros i Hi.
replace i with 0%nat; try lia.
apply in_eq.
destruct IHN as (l,Hl).
(S N ::l).
intros i Hi.
destruct (ifflr (Nat.lt_eq_cases i (S N))) as [iltSn | ->]; try easy.
now apply in_cons, Hl; lia.
now simpl; left.
intros n.
assert (C: { l | i,
   (i n×Nat.pow 2 n)%nat
        In (INR i/bpow2 (Z.of_nat n)) l }).
destruct (C1 (n×Nat.pow 2 n)%nat) as (l1,Hl1).
(map (fun jINR j / bpow2 (Z.of_nat n)) l1).
intros i Hi.
apply (in_map (fun j : natINR j / bpow2 (Z.of_nat n))
       l1 i).
apply Hl1; easy.
destruct C as (l,Hl).
(canonizer (mk_adapted_seq n) l).
split.
apply finite_vals_canonizer.
intros x.
unfold mk_adapted_seq.
case (Rbar_le_lt_dec _ _); intros H1.
replace (INR n) with
  (INR (n × 2 ^ n) / bpow2 (Z.of_nat n)).
apply Hl; auto.
rewrite mult_INR; rewrite pow_INR.
rewrite pow_powerRZ, bpow_powerRZ.
unfold Rdiv; rewrite Rmult_assoc, Rinv_r.
ring.
apply Rgt_not_eq, powerRZ_lt.
simpl; apply Rlt_0_2.
assert (Hl': i : Z,
     (0 IZR i INR n × bpow2 (Z.of_nat n))%R
     In
       (IZR i / bpow2 (Z.of_nat n)) l).
intros i H.
replace (IZR i) with (INR (Z.abs_nat i)).
apply Hl.
apply Nat2Z.inj_le.
rewrite Zabs2Nat.id_abs.
rewrite Z.abs_eq.
apply le_IZR.
apply Rle_trans with (1:=proj2 H).
rewrite <- INR_IZR_INZ, mult_INR.
right; f_equal.
rewrite pow_INR.
rewrite pow_powerRZ, bpow_powerRZ; easy.
apply le_IZR; apply H.
rewrite INR_IZR_INZ.
rewrite Zabs2Nat.id_abs.
rewrite Z.abs_eq; try easy.
apply le_IZR; apply H.

pose (rnd:=(round radix2 (FIX_exp (-Z.of_nat n)) Zfloor
     (real (f x)))); fold rnd.
assert (Frnd:generic_format radix2 (FIX_exp (-Z.of_nat n))
          rnd).
apply generic_format_round...
rewrite Frnd; unfold F2R; simpl.
unfold cexp, FIX_exp at 2; simpl.
rewrite bpow_opp.
apply Hl'.
split; apply Rmult_le_reg_r with
  (bpow2 (cexp radix2 (FIX_exp (- Z.of_nat n)) rnd));
   try rewrite <- Frnd; try apply bpow_gt_0.
rewrite Rmult_0_l.
apply round_ge_generic...
apply generic_format_0...
destruct f_Mplus as [Hf _].
generalize (Hf x); case (f x); simpl; try easy.
unfold cexp, FIX_exp; simpl.
rewrite Rmult_assoc, <- bpow_plus.
ring_simplify (Z.of_nat n + - Z.of_nat n)%Z.
simpl; rewrite Rmult_1_r.
unfold rnd; apply round_le_generic...
replace (INR n) with (F2R (Float radix2 (Z.of_nat n) 0%Z)).
apply generic_format_F2R.
intros _; unfold FIX_exp, cexp; simpl; lia.
unfold F2R; simpl; rewrite Rmult_1_r.
apply sym_eq, INR_IZR_INZ.
destruct f_Mplus as [Hf _].
generalize H1, (Hf x); case (f x); simpl; try easy; auto with real.
intros a.
apply mk_adapted_seq_SF_aux.
Qed.

Lemma mk_adapted_seq_Mplus : Mplus_seq gen mk_adapted_seq.
Proof.
intros n.
apply SFplus_Mplus.
apply mk_adapted_seq_nonneg.
apply mk_adapted_seq_SF.
Qed.

End Adap_seq_mk.

Section LIntSF_Dirac.

Context {E : Type}.

Context {gen : (E Prop) Prop}.

Lemma LInt_SF_Dirac :
   (f : E R) (Hf : SF gen f) a,
    LInt_SF (Dirac_measure gen a) f Hf = f a.
Proof.
intros f [l [Hf1 Hf2]] a; unfold LInt_SF, af1; simpl.
rewrite (finite_vals_sum_eq _ l); try easy.
apply sum_Rbar_map_ext_f; intros; repeat f_equal.
apply subset_ext; intros t; apply Rbar_finite_eq.
Qed.

End LIntSF_Dirac.