simple_fun.v

intros f g Hf Hg Zf Zg Hfg.
pose (h':= fun x => g x + (-1)*f x).
pose (h:= fun x => f x + h' x).
assert (Y1: forall 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 : E => h' x)).
intros x; unfold h'.
simpl; apply Rplus_le_reg_l with (f x).
ring_simplify; easy.
replace (LInt_SFp g Hg) with
  (LInt_SFp h (SF_plus f Hf h' Hh')).
unfold h; rewrite LInt_SFp_plus; try easy.
rewrite <- (Rbar_plus_0_r (LInt_SFp f Hf)) at 1.
apply Rbar_plus_le_compat_l.
apply LInt_SFp_pos; easy.
apply sym_eq, LInt_SFp_ext; easy.
Qed.

(* Lemma 782 p. 160 *)
Lemma LInt_SFp_continuous :
  forall (f : E -> R) (Hf : SF gen f),
    nonneg f ->
    LInt_SFp f Hf =
      Rbar_lub (fun x =>
        exists (g : E -> R), exists (Hg : SF gen g),
          nonneg g /\
          (forall z, g z <= f z) /\
          LInt_SFp 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.
exists f; exists Hf; split; try easy.
split; try easy.
intros; apply Rle_refl.
Qed.

Lemma SF_charac : forall A, measurable gen A -> SF gen (charac A).
Proof.
intros A HA.
exists (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 z => z = a)).
apply measurable_R_eq.
Defined.

(* Lemma 771 p. 156 *)
Lemma LInt_SFp_charac :
  forall A (HA : measurable gen A),
    LInt_SFp (charac A) (SF_charac A HA) = mu A.
Proof.
intros A HA.
unfold LInt_SFp; simpl.
rewrite canonizer_Sorted; try easy.
unfold RemoveUseless; simpl.
case (excluded_middle_informative _); case (excluded_middle_informative _); 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.
exists 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.
exists 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 780 p. 160 *)
Lemma Lint_SFp_eq_other_list :
  forall (f : E -> R) (Hf : SF gen f) l,
    nonneg_l (map Finite l) -> finite_vals f (0 :: l) -> NoDup l ->
    LInt_SFp f Hf = sum_Rbar_map l (af1 f).
Proof.
intros f (lf,((Y1,(Y2,Y3)),Y4)) l Hl H1 H2; simpl.
unfold LInt_SFp; simpl.
apply trans_eq with (sum_Rbar_map (sort Rle l)
  (fun a : R => af1 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 (exists y, f y = x)).
intros (y,Hy); rewrite <- Hy.
apply Y3.
intros K.
assert (K':forall y, f y <> x).
apply not_ex_not_all.
intros (z,Hz); apply K.
exists 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 y => x <> 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 :
  forall (f : E -> R) (Hf : SF gen f) A,
    measurable gen A ->
    SF gen (fun x => f x * charac A x).
Proof.
intros f (l,(Hl1,Hl2)) A HA.
pose (g:= fun x => f x * charac A x); fold g.
exists (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 :
  forall (x : E) a A, measurable gen A -> SF gen (fun t => a * charac A t).
Proof.
intros x a A HA; apply SF_mult_charac; try easy.
apply (SF_cst x).
Qed.

Lemma SF_mult_charac_alt:
  forall (f : E -> R) (Hf : SF gen f) A,
    measurable gen A -> nonneg f ->
    SF gen (fun y =>
      sum_Rbar_map (proj1_sig Hf) (fun t => t * charac (fun x => A x /\ f x = t) y)).
Proof.
intros f Hf A HA P.
assert (T:(fun y => real (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 functional_extensionality.
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 :
  forall (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 := SF_mult_charac_alt f Hf A HA P in
    LInt_SFp (fun x => f x * charac A x) H3 =
      LInt_SFp (fun y =>
        sum_Rbar_map (proj1_sig Hf) (fun t => t * charac (fun x => A x /\ f x = t) y)) H4.
Proof.
intros f Hf A HA P H3 H4.
apply LInt_SFp_ext; try easy.
intros x; simpl; apply Rmult_le_pos.
apply P.
case (charac_or A x); intros L; rewrite L; auto with real.
intros x.
rewrite <- finite_vals_charac_sum_eq; try easy.
destruct Hf as (l,Hl); apply Hl.
Qed.

Lemma LInt_SFp_mult_charac :
  forall (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_SFp (fun x => f x * charac A x) H3 =
      sum_Rbar_map (proj1_sig Hf)
         (fun t : R => Rbar_mult t (mu (fun x => A x /\ f x = t))).
Proof.
intros f Hf A HA P H3.
destruct Hf as (l,Hl); simpl.
rewrite Lint_SFp_eq_other_list 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_SFp_def.


Section Adap_seq_def.

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

(* From Definition 798 p. 166 *)
Definition is_adapted_seq : (E -> Rbar) -> (nat -> E -> R) -> Prop :=
  fun f phi =>
    (forall n, nonneg (phi n)) /\
    incr_fun_seq phi /\
(*    (forall x n, phi n x <= phi (S n) x) /\*)
    (forall x, is_sup_seq (fun n => phi n x) (f x)).

(* From Definition 798 p. 166 *)
Definition SF_seq : (nat -> E -> R) -> Set := fun phi => forall n, SF gen (phi n).

Lemma is_adapted_seq_is_lim_seq :
  forall f phi x, is_adapted_seq f phi -> is_lim_seq (fun n => phi 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 : forall 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 : nat => phi n x); try easy.
intros n; apply Y1.
intros eps; split; intros; simpl.
rewrite Rplus_0_l; apply eps.
exists 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.

(* From Lemma 799 pp. 166-167 *)
Definition mk_adapted_seq : nat -> E -> R :=
  fun n x => match 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.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_le : forall 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 : forall 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 : forall 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.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_incr : incr_fun_seq mk_adapted_seq.
(*  forall x n, mk_adapted_seq n x <= mk_adapted_seq (S n) x.*)
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.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_is_sup :
  forall x, is_sup_seq (fun n => mk_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)))).
exists 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.
exists (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.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_Sup :
  forall x, f x = Sup_seq (fun n => mk_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.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_Lim :
  forall x, f x = Lim_seq (fun n => mk_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.

(* From Lemma 799 pp. 166-167 *)
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.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_SF_aux :
  forall n a, measurable gen (fun x => mk_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 (exists y, mk_adapted_seq n y = a)).
(* non vide *)
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.
(* . a = n *)
apply measurable_ext with (fun z => Rbar_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 x => Rbar_le (INR n) x).
apply measurable_gen.
exists (Finite (INR n)); easy.
(* . a < n *)
assert (L: exists r2:Rbar,
     forall (z:E),
       (Rbar_le a (f z) /\ Rbar_lt (f z) r2)
             <-> mk_adapted_seq n z = a).
(* 2 cas non fusionnables
   sinon r2 = p_infty mais < infty marche pas *)
exists (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).
(* a < n <= f z < succ a : impossible *)
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 x =>  Rbar_le a (f x)/\ Rbar_lt (f x) r2).
apply Hr2.
destruct f_Mplus as [_ Hf].
apply Hf with (A:= fun x => Rbar_le a x /\ Rbar_lt x r2).
apply measurable_inter.
apply measurable_gen.
exists (Finite a); easy.
apply measurable_compl.
eapply measurable_ext.
2: apply measurable_gen.
2: exists 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; exists x; easy.
Qed.

(* From Lemma 799 pp. 166-167 *)
Lemma mk_adapted_seq_SF : SF_seq gen mk_adapted_seq.
Proof with auto with typeclass_instances.
assert (C1: forall N, { l | forall i,
    (i <= N)%nat -> In i l} ) .
induction N.
exists (0%nat::nil).
intros i Hi.
replace i with 0%nat; try lia.
apply in_eq.
destruct IHN as (l,Hl).
exists (S N ::l).
intros i Hi.
case (le_lt_or_eq i (S N)); try easy.
intros Hi'; apply in_cons.
apply Hl; lia.
intros Hi'; rewrite Hi'; apply in_eq.
(* *)
intros n.
assert (C: { l | forall 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).
exists (map (fun j => INR j / bpow2 (Z.of_nat n)) l1).
intros i Hi.
apply (in_map (fun j : nat => INR j / bpow2 (Z.of_nat n))
       l1 i).
apply Hl1; easy.
(*  *)
destruct C as (l,Hl).
exists (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':forall 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.
intros _ ; apply Rle_refl.
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}.
Hypothesis Einhab : inhabited E.

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

(* Lemma 787 p. 162 *)
Lemma LInt_SFp_Dirac :
  forall (f : E -> R) (Hf : SF gen f) a, (* nonneg not necessary. *)
    LInt_SFp (Dirac_measure gen a) f Hf = f a.
Proof.
intros f [l [Hf1 Hf2]] a; unfold LInt_SFp, 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.