LInt_p.v

  forall f g, Mplus gen f -> Mplus gen g ->
    ae_eq mu f g ->
    LInt_p mu f = LInt_p mu g.
Proof.
intros.
apply LInt_p_ae_compat with (fun x y => x = y); try easy.
clear; intros.
apply LInt_p_ext; easy.
Qed.

(* Lemma 809 p. 170 *)
Lemma LInt_p_ae_le_compat :
  forall f g, Mplus gen f -> Mplus gen g ->
    ae mu (fun x => Rbar_le (f x) (g x)) ->
    Rbar_le (LInt_p mu f) (LInt_p mu g).
Proof.
intros.
apply LInt_p_ae_compat with Rbar_le; try easy.
apply Rbar_le_refl.
clear; intros.
now apply LInt_p_monotone.
Qed.

(* Lemma 811 p. 170 *)
Lemma LInt_p_ae_finite :
  forall f, Mplus gen f ->
    is_finite (LInt_p mu f) ->
    ae mu (fun x => is_finite (f x)).
Proof.
intros f [H1 H2] H3.
pose (A:=(fun x : E => f x = p_infty)).
assert (Y1: measurable gen A).
apply H2 with (A:=fun y => y = p_infty).
apply measurable_Rbar_eq.
exists A; split; try split; try easy.
unfold A; intros x; generalize (H1 x); case (f x); try easy.
intros r _ K; now contradict K.
case (Rbar_eq_dec (mu A) 0); try easy.
intros H4; absurd (LInt_p mu f=p_infty).
rewrite <- H3; easy.
rewrite LInt_p_decomp with f A; try easy.
replace (LInt_p mu (fun x : E => Rbar_mult (f x) (charac A x))) with p_infty.
(* *)
apply Rbar_plus_pos_pinfty.
apply LInt_p_nonneg; try easy.
intros y; apply Rbar_mult_le_pos_pos_pos; try easy.
apply nonneg_charac.
(* *)
rewrite LInt_p_when_charac with (f':=fun _ => p_infty); try easy.
rewrite LInt_p_scal; try easy.
rewrite LInt_p_charac; try easy.
apply sym_eq, Rbar_mult_lt_pos_pinfty.
case (Rbar_le_lt_or_eq_dec _ _ (meas_nonneg gen mu A)); try easy.
intros K; contradict K; apply sym_not_eq; easy.
now apply Mplus_charac.
Qed.

Lemma LInt_p_minus :
  forall f g, Mplus gen f -> Mplus gen g ->
    (forall x, Rbar_le (g x) (f x)) ->
    is_finite (LInt_p mu g) ->
    LInt_p mu (fun x => Rbar_minus (f x) (g x)) =
      Rbar_minus (LInt_p mu f) (LInt_p mu g).
Proof.
intros f g Hf Hg H H'.
assert (Y1: nonneg (fun x : E => Rbar_minus (f x) (g x))).
intros t.
case_eq (g t).
intros r Hr; apply Rbar_plus_le_reg_r with (Finite r); try easy.
rewrite <- Rbar_plus_minus_r; try easy.
rewrite Rbar_plus_0_l.
rewrite <- Hr; apply H.
intros Ht.
replace (f t) with (p_infty); simpl.
apply Rle_refl.
generalize (H t); rewrite Ht.
case (f t); easy.
intros Ht; absurd (Rbar_le 0 (g t)).
rewrite Ht; simpl; easy.
apply Hg.
(* *)
assert (Y2: measurable_fun_Rbar gen (fun x : E => Rbar_minus (f x) (g x))).
apply measurable_fun_plus_alt; try apply Hf.
apply measurable_fun_opp; apply Hg.
(* *)
apply Rbar_plus_eq_reg_r with (LInt_p mu g); try easy.
rewrite <- Rbar_plus_minus_r; try easy.
rewrite <- LInt_p_plus; try easy.
apply LInt_p_ae_eq_compat; try easy.
split.
intros t; apply Rbar_plus_le_0; try apply Y1; apply Hg.
apply measurable_fun_plus_alt; now try apply Hg.
eapply ae_imply.
2: apply (LInt_p_ae_finite g); try easy.
intros t Ht; simpl in Ht.
rewrite <- Rbar_plus_minus_r; easy.
Qed.

Lemma Rbar_le_abs_LInt_p_aux :
  forall a b c d,
    is_finite c -> is_finite d -> (Rbar_le 0 a) -> (Rbar_le 0 b) ->
    Rbar_minus (Rbar_plus a b) (Rbar_plus c d) =
      Rbar_plus (Rbar_minus a c) (Rbar_minus b d).
Proof.
intros a b c d H1 H2; rewrite <- H1; rewrite <- H2.
case a; case b; simpl; try easy.
intros; f_equal; ring.
Qed.

Lemma Rbar_le_LInt_p_charac :
  forall f A, nonneg f ->
    Rbar_le (LInt_p mu (fun x => Rbar_mult (f x) (charac A x))) (LInt_p mu f).
Proof.
intros f A Hf.
apply LInt_p_monotone.
intros x.
case (charac_or A x); intros T; rewrite T.
rewrite Rbar_mult_0_r; apply Hf.
rewrite Rbar_mult_1_r; apply Rbar_le_refl.
Qed.

Lemma Rbar_le_abs_LInt_p :
  forall f g, Mplus gen f -> Mplus gen g ->
    is_finite (LInt_p mu f) -> is_finite (LInt_p mu g) ->
    Rbar_le (Rbar_abs (Rbar_minus (LInt_p mu f) (LInt_p mu g)))
      (LInt_p mu (fun x => Rbar_abs (Rbar_minus (f x) (g x)))).
Proof.
intros f g [H1 H2] [H4 H5] H3 H6.
assert (Y1: measurable_fun_Rbar gen (fun x => Rbar_minus (f x) (g x))).
unfold Rbar_minus; apply measurable_fun_plus_alt; try easy.
apply measurable_fun_opp; easy.
pose (A:= fun x => Rbar_le (g x) (f x)).
assert (HA: measurable gen A).
apply measurable_ext with (fun x => Rbar_le 0 (Rbar_minus (f x) (g x))).
unfold A; intros t; split.
2: apply Rbar_minus_le_0.
case_eq (g t).
intros r Hr T; apply Rbar_plus_le_reg_r with (-r); try easy.
simpl (Rbar_plus r (-r)); ring_simplify (r+-r)%R.
apply Rbar_le_trans with (1:=T).
apply Rbar_eq_le; easy.
case (f t); simpl; try easy.
case (f t); simpl; try easy.
apply Y1.
apply measurable_gen.
exists (Finite 0); easy.
assert (Y2: is_finite
  (LInt_p mu (fun x : E => Rbar_mult (g x) (charac A x)))).
cut (Rbar_le 0 (LInt_p mu (fun x : E => Rbar_mult (g x) (charac A x)))).
cut (Rbar_le (LInt_p mu (fun x : E => Rbar_mult (g x) (charac A x))) (LInt_p mu g)).
rewrite <- H6.
case (LInt_p mu (fun x : E => Rbar_mult (g x) (charac A x))); easy.
apply Rbar_le_LInt_p_charac; easy.
apply LInt_p_nonneg; try easy.
apply nonneg_mult; try easy.
apply nonneg_charac.
(* *)
rewrite (LInt_p_decomp f A); try easy.
rewrite (LInt_p_decomp g A); try easy.
apply Rbar_le_trans with
  (Rbar_abs (Rbar_minus
     (LInt_p mu (fun x => Rbar_mult (Rbar_abs (Rbar_minus (f x) (g x))) (charac A x)))
     (LInt_p mu (fun x => Rbar_mult (Rbar_abs (Rbar_minus (f x) (g x))) (charac (fun t => ~A t) x))))).
apply Rbar_eq_le; f_equal.
rewrite Rbar_le_abs_LInt_p_aux; try easy.
unfold Rbar_minus at 3; f_equal.
rewrite <- LInt_p_minus; try easy.
apply LInt_p_ext.
intros x; case (charac_or A x); intros Hx; rewrite Hx.
rewrite 3!Rbar_mult_0_r; unfold Rbar_minus; rewrite Rbar_plus_0_l.
simpl; f_equal; ring.
rewrite 3!Rbar_mult_1_r.
apply charac_1 in Hx.
apply sym_eq, Rbar_abs_pos.
apply Rbar_minus_le_0, Hx.
split.
apply nonneg_mult; try easy.
apply nonneg_charac.
apply measurable_fun_mult; try easy.
apply measurable_fun_charac; easy.
split.
apply nonneg_mult; try easy.
apply nonneg_charac.
apply measurable_fun_mult; try easy.
apply measurable_fun_charac; easy.
intros x; case (charac_or A x); intros Hx; rewrite Hx.
rewrite 2!Rbar_mult_0_r; apply Rbar_le_refl.
rewrite 2!Rbar_mult_1_r.
apply charac_1 in Hx; apply Hx.
rewrite <- Rbar_opp_minus; f_equal.
rewrite <- LInt_p_minus; try easy.
apply LInt_p_ext.
intros x; case (charac_or (fun t => ~A t) x); intros Hx; rewrite Hx.
rewrite 3!Rbar_mult_0_r; unfold Rbar_minus; rewrite Rbar_plus_0_l.
simpl; f_equal; ring.
rewrite 3!Rbar_mult_1_r.
apply charac_1 in Hx.
rewrite <- Rbar_opp_minus.
apply sym_eq, Rbar_abs_neg.
rewrite <- Rbar_opp_minus.
replace (Finite 0) with (Rbar_opp 0).
apply Rbar_opp_le.
apply Rbar_minus_le_0.
apply Rbar_lt_le.
apply Rbar_not_le_lt; easy.
simpl; f_equal; ring.
split.
apply nonneg_mult; try easy.
apply nonneg_charac.
apply measurable_fun_mult; try easy.
apply measurable_fun_charac; try easy.
apply measurable_compl_rev; easy.
split.
apply nonneg_mult; try easy.
apply nonneg_charac.
apply measurable_fun_mult; try easy.
apply measurable_fun_charac; try easy.
apply measurable_compl_rev; easy.
intros x; case (charac_or (fun t => ~A t) x); intros Hx; rewrite Hx.
rewrite 2!Rbar_mult_0_r; apply Rbar_le_refl.
rewrite 2!Rbar_mult_1_r.
apply charac_1 in Hx; unfold A in Hx.
apply Rbar_lt_le.
apply Rbar_not_le_lt; easy.
cut (Rbar_le 0 (LInt_p mu (fun x : E => Rbar_mult (f x) (charac (fun t => ~A t) x)))).
cut (Rbar_le (LInt_p mu (fun x : E => Rbar_mult (f x) (charac (fun t => ~A t) x))) (LInt_p mu f)).
rewrite <- H3.
case (LInt_p mu (fun x : E => Rbar_mult (f x) (charac (fun t => ~A t) x))); easy.
apply Rbar_le_LInt_p_charac; easy.
apply LInt_p_nonneg; try easy.
apply nonneg_mult; try easy.
apply nonneg_charac.
cut (Rbar_le 0 (LInt_p mu (fun x : E => Rbar_mult (g x) (charac (fun t => ~A t) x)))).
cut (Rbar_le (LInt_p mu (fun x : E => Rbar_mult (g x) (charac (fun t => ~A t) x))) (LInt_p mu g)).
rewrite <- H6.
case (LInt_p mu (fun x : E => Rbar_mult (g x) (charac (fun t => ~A t) x))); easy.
apply Rbar_le_LInt_p_charac; easy.
apply LInt_p_nonneg; try easy.
apply nonneg_mult; try easy.
apply nonneg_charac.
apply LInt_p_nonneg; try easy.
apply nonneg_mult; try easy.
apply nonneg_charac.
apply LInt_p_nonneg; try easy.
apply nonneg_mult; try easy.
apply nonneg_charac.
unfold Rbar_minus at 1.
apply Rbar_le_trans with (1:=Rbar_abs_triang _ _).
rewrite Rbar_abs_opp.
rewrite 2!Rbar_abs_pos.
rewrite <- LInt_p_decomp; try easy.
apply Rbar_le_refl.
split.
intros t; apply Rbar_abs_ge_0.
apply measurable_fun_abs; easy.
apply LInt_p_nonneg; try easy.
intros t; apply Rbar_mult_le_pos_pos_pos.
apply Rbar_abs_ge_0.
apply nonneg_charac.
apply LInt_p_nonneg; try easy.
intros t; apply Rbar_mult_le_pos_pos_pos.
apply Rbar_abs_ge_0.
apply nonneg_charac.
Qed.

Lemma LInt_p_dominated_convergence :
  forall (f : nat -> E -> Rbar) g, Mplus_seq gen f -> Mplus gen g ->
    (forall x, ex_lim_seq_Rbar (fun n => f n x)) ->
    (forall n x, Rbar_le (f n x) (g x)) ->
    is_finite (LInt_p mu g) ->
    let lim_f := fun x => Lim_seq_Rbar (fun n => f n x) in
    Mplus gen lim_f /\
    is_finite (LInt_p mu lim_f) /\
    LInt_p mu lim_f = Lim_seq_Rbar (fun n => LInt_p mu (f n)) /\
    ex_lim_seq_Rbar (fun n => LInt_p mu (f n)).
Proof.
intros f g H1 H4 H3 H6 H7 lim_f.

assert (H: Mplus gen lim_f).
split.
(* . *)
intros x; unfold lim_f; rewrite ex_lim_seq_Rbar_LimInf; try easy.
unfold LimInf_seq_Rbar.
apply Rbar_le_trans with (2:= Sup_seq_ub _ 0%nat).
rewrite Inf_eq_glb.
apply Rbar_glb_correct; intros y (n,Hn).
rewrite Hn; apply H1.
(* . *)
eapply measurable_fun_ext.
intros t; apply sym_eq, ex_lim_seq_Rbar_LimSup; easy.
apply measurable_fun_LimSup_seq_Rbar; intros n; apply (H1 n).

pose (e := fun n x => Rbar_abs (Rbar_minus (f n x) (lim_f x))).
pose (k:= fun m x => Rbar_minus (Rbar_mult 2 (g x)) (e m x)).

assert (Ye1: forall n, nonneg (e n)).
intros n x; unfold e; apply Rbar_abs_ge_0.

assert (Ye2: forall n, measurable_fun_Rbar gen (e n)).
intros n; unfold e; apply measurable_fun_abs.
unfold Rbar_minus; apply measurable_fun_plus_alt; try apply (H1 n).
apply measurable_fun_opp; apply H.

assert (Yh1: nonneg (fun x => Rbar_mult 2 (g x))).
intros t; apply Rbar_mult_le_pos_pos_pos; try apply H4.
simpl; auto with real.

assert (Yh2: measurable_fun_Rbar gen (fun x => Rbar_mult 2 (g x))).
apply measurable_fun_scal; apply H4.

assert (Y: forall n x, Rbar_le (e n x) (Rbar_mult 2 (g x))).
intros n x; unfold e, Rbar_minus.
apply Rbar_le_trans with (1:= Rbar_abs_triang _ _).
rewrite Rbar_abs_opp.
rewrite 2!Rbar_abs_pos; try apply (H1 n); try apply H.
apply Rbar_le_trans with (Rbar_plus (g x) (g x)).
apply Rbar_plus_le_compat.
apply H6.
unfold lim_f; rewrite ex_lim_seq_Rbar_LimSup; try easy.
unfold LimSup_seq_Rbar.
apply Rbar_le_trans with (1:= Inf_seq_minor _ 0%nat).
apply Sup_seq_lub.
intros m; apply H6.
apply Rbar_eq_le; unfold Rbar_mult, Rbar_mult'.
case Rle_dec.
2: intros T; contradict T; auto with real.
intros H8; case (Rle_lt_or_eq_dec 0 2 H8).
2: intros T; contradict T; auto with real.
case (g x); simpl; try easy.
intros r _; f_equal; ring.

assert (Yk1: forall n, nonneg (k n)).
intros n x; unfold k.
apply Rbar_minus_le_0; easy.

assert (Yk2: forall n, measurable_fun_Rbar gen (k n)).
intros n; unfold k.
unfold Rbar_minus; apply measurable_fun_plus_alt; try easy.
apply measurable_fun_opp; easy.

(* First step *)
assert (K1:
  LimSup_seq_Rbar (fun n => LInt_p mu (fun x => Rbar_abs (Rbar_minus (f n x) (lim_f x)))) = 0).
erewrite LimSup_seq_Rbar_ext.
2: intros n; rewrite (LInt_p_ext mu _ (fun x => e n x)); easy.
apply Rbar_le_antisym.
apply Rbar_opp_le.
simpl (Rbar_opp 0); rewrite Ropp_0.
apply Rbar_plus_le_reg_l with (Rbar_mult 2 (LInt_p mu g)).
rewrite <- H7; simpl; easy.
rewrite Rbar_plus_0_r.
apply Rbar_le_trans with
  (LInt_p mu (fun x => LimInf_seq_Rbar (fun n => k n x))).
apply Rbar_eq_le.
rewrite <- LInt_p_scal; try easy.
apply LInt_p_ae_eq_compat; try easy.
split.
intros t; unfold LimInf_seq_Rbar.
apply Rbar_le_trans with (2:= Sup_seq_ub _ 0%nat).
rewrite Inf_eq_glb.
apply Rbar_glb_correct; intros y (n,Hn).
rewrite Hn; apply Yk1.
apply measurable_fun_LimInf_seq_Rbar; easy.
apply ae_eq_sym; unfold ae_eq, ae_rel.
apply ae_imply with (fun x : E => is_finite (g x)).
intros x Hx.
unfold k; rewrite LimInf_seq_Rbar_minus_compat_l.
replace (LimSup_seq_Rbar (fun n : nat => e n x)) with (Finite 0).
unfold Rbar_minus; simpl (Rbar_opp 0); rewrite Ropp_0.
apply Rbar_plus_0_r.
(* *)
apply sym_eq, LimSup_seq_Rbar_abs_minus; try easy.
destruct H as [H _].
generalize (H x); unfold lim_f.
cut (Rbar_le (Lim_seq_Rbar (fun n : nat => f n x)) (g x)).
rewrite <- Hx.
case ((Lim_seq_Rbar (fun n : nat => f n x))); easy.
rewrite ex_lim_seq_Rbar_LimSup; try easy.
unfold LimSup_seq_Rbar.
apply Rbar_le_trans with (1:= Inf_seq_minor _ 0%nat).
apply Sup_seq_lub.
intros n; rewrite plus_0_r; easy.
rewrite <- Hx; easy.
apply LInt_p_ae_finite; try easy.
simpl; auto with real.
eapply Rbar_le_trans.
apply Fatou_lemma; try easy.
erewrite LimInf_seq_Rbar_ext.
2: intros m.
2: unfold k; apply LInt_p_minus; try easy.
rewrite LimInf_seq_Rbar_minus_compat_l.
rewrite LInt_p_scal; try easy.
apply Rbar_le_refl.
simpl; auto with real.
rewrite LInt_p_scal; try easy.
rewrite <- H7; easy.
simpl; auto with real.
cut (Rbar_le 0 (LInt_p mu (e m))).
cut (Rbar_le  (LInt_p mu (e m))  (Rbar_mult 2 (LInt_p mu g))).
rewrite <- H7.
case (LInt_p mu (e m)); easy.
rewrite <- LInt_p_scal; try easy.
apply LInt_p_monotone; try easy.
simpl; auto with real.
apply LInt_p_nonneg; try easy.
unfold LimSup_seq_Rbar; rewrite Inf_eq_glb.
apply Rbar_glb_correct.
intros x (n,Hn); rewrite Hn.
apply Rbar_le_trans with (2:=Sup_seq_ub _ 0%nat).
apply LInt_p_nonneg; try easy.

(* Second step *)
assert (K6: is_finite (LInt_p mu lim_f)).
cut (Rbar_le 0 (LInt_p mu lim_f)).
2: apply LInt_p_nonneg; now try apply H.
cut (Rbar_le  (LInt_p mu lim_f) (LInt_p mu g)).
rewrite <- H7.
case (LInt_p mu lim_f); easy.
apply LInt_p_monotone; try easy.
intros t.
unfold lim_f; rewrite ex_lim_seq_Rbar_LimSup; try easy.
unfold LimSup_seq_Rbar.
apply Rbar_le_trans with (1:=Inf_seq_minor _ 0%nat).
apply Sup_seq_lub.
intros n; apply H6.

assert (K2:
 LimSup_seq_Rbar (fun n => Rbar_abs (Rbar_minus (LInt_p mu (f n)) (LInt_p mu lim_f))) = 0).
apply Rbar_le_antisym.
2: unfold LimSup_seq_Rbar; rewrite Inf_eq_glb.
2: apply Rbar_glb_correct; intros y (n,Hn); rewrite Hn.
2: apply Rbar_le_trans with (2:= Sup_seq_ub _ 0%nat).
2: apply Rbar_abs_ge_0.
rewrite <- K1.
apply LimSup_seq_Rbar_le; intros n.
apply Rbar_le_abs_LInt_p; try easy.
cut (Rbar_le 0 (LInt_p mu (f n))).
2: apply LInt_p_nonneg; now try apply (H1 n).
cut (Rbar_le  (LInt_p mu (f n)) (LInt_p mu g)).
rewrite <- H7.
case (LInt_p mu (f n)); easy.
apply LInt_p_monotone; try easy.

(* third step *)
assert (K3:
  ex_lim_seq_Rbar (fun n => Rbar_abs (Rbar_minus (LInt_p mu (f n)) (LInt_p mu lim_f))) /\
       Lim_seq_Rbar (fun n => Rbar_abs (Rbar_minus (LInt_p mu (f n)) (LInt_p mu lim_f))) = 0).
assert (H9: LimInf_seq_Rbar (fun n => Rbar_abs (Rbar_minus (LInt_p mu (f n)) (LInt_p mu lim_f))) = 0).
apply Rbar_le_antisym.
rewrite <- K2.
apply LimSup_LimInf_seq_Rbar_le.
unfold LimInf_seq_Rbar.
apply Rbar_le_trans with (2:= Sup_seq_ub _ 0%nat).
rewrite Inf_eq_glb.
apply Rbar_glb_correct; intros y (n,Hn).
rewrite Hn; apply Rbar_abs_ge_0.
assert (H10 : ex_lim_seq_Rbar
  (fun n : nat => Rbar_abs (Rbar_minus (LInt_p mu (f n)) (LInt_p mu lim_f)))).
apply LimInfSup_ex_lim_seq_Rbar; try easy.
rewrite K2, H9; apply Rbar_le_refl.
split; try easy.
rewrite ex_lim_seq_Rbar_LimSup; try easy.

(* *)
generalize (ex_lim_seq_Rbar_minus _ _  K6 (proj1 K3) (proj2 K3)); easy.
Qed.

End LInt_p_plus_def.


Section LInt_p_mu_ext.

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

Context {genE : (E -> Prop) -> Prop}.
Variable mu1 mu2 : measure genE.

Lemma LInt_p_mu_ext :
  (forall A, measurable genE A -> mu1 A = mu2 A) ->
  forall f, LInt_p mu1 f = LInt_p mu2 f.
Proof.
intros H f; unfold LInt_p.
apply Rbar_le_antisym;
  apply Rbar_lub_subset; intros x (g,(Hg, (Hg1,(Hg2,Hg3))));
  exists g; exists Hg; split; try easy; split; try easy;
  rewrite <- Hg3; unfold LInt_SFp ;
  apply sum_Rbar_map_ext_f; intros t Ht ;
  unfold af1; rewrite H; try easy ;
  destruct Hg as (l,(Hl1,Hl2)) ;
  apply measurable_ext with (2:=(Hl2 t)) ;
  intros u; apply iff_sym, Rbar_finite_eq.
Qed.

End LInt_p_mu_ext.


Section LInt_p_chg_meas.

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

Context {genE : (E -> Prop) -> Prop}.
Context {genF : (F -> Prop) -> Prop}.

Variable h : E -> F.
Hypothesis Mh : measurable_fun genE genF h.

Variable mu : measure genE.

Definition meas_image_meas : (F -> Prop) -> Rbar :=
  fun B => mu (fun x => B (h x)).

Lemma meas_image_emptyset : meas_image_meas emptyset = 0.
Proof.
unfold meas_image_meas; now rewrite meas_emptyset.
Qed.

Lemma meas_image_nonneg : nonneg meas_image_meas.
Proof.
intros B; apply meas_nonneg.
Qed.

Lemma meas_image_sigma_additivity :
  forall B,
    (forall n, measurable genF (B n)) ->
    (forall n m x, B n x -> B m x -> n = m) ->
    meas_image_meas (fun x => exists n, B n x) =
      Sup_seq (fun n => sum_Rbar n (fun m => meas_image_meas (B m))).
Proof.
intros B HB1 HB2; apply meas_sigma_additivity.
intros n; specialize (Mh (B n) (HB1 n)); easy.
intros n m x; now apply HB2.
Qed.

Definition meas_image : measure genF :=
  mk_measure genF meas_image_meas
    meas_image_emptyset meas_image_nonneg meas_image_sigma_additivity.

Lemma LInt_p_change_meas :
  forall f, Mplus genF f ->
    LInt_p meas_image f = LInt_p mu (fun x => f (h x)).
Proof.
intros f Hf.
apply Mp_correct in Hf; try easy.
induction Hf as [ | a f Ha Hf | f g Hf IHHf Hg IHHg | f Hf1 Hf2].
(* *)
rewrite LInt_p_charac; try easy; simpl; unfold meas_image_meas.
rewrite <- LInt_p_charac; auto.
(* *)
apply Mp_correct in Hf; try easy.
rewrite 2!LInt_p_scal; try now f_equal.
now apply (Mplus_composition _ genF).
(* *)
apply Mp_correct in Hf; apply Mp_correct in Hg; try easy.
rewrite 2!LInt_p_plus; try now f_equal.
1,2: now apply (Mplus_composition _ genF).
(* *)
rewrite 2!Beppo_Levi; try easy.
now apply Sup_seq_ext.
1,2: intros n; specialize (Hf2 n); apply Mp_correct in Hf2; try easy.
now apply (Mplus_composition _ genF).
Qed.

End LInt_p_chg_meas.


Section LInt_p_Dirac.

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

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

(* Lemma 822 p. 174 *)
Lemma LInt_p_Dirac :
  forall (f : E -> Rbar) a, Mplus genE f ->
    LInt_p (Dirac_measure genE a) f = f a.
Proof.
intros f a Hf.
rewrite <- LInt_p_with_mk_adapted_seq; try easy.
rewrite Sup_seq_ext with (v := fun n => mk_adapted_seq f n a).
now rewrite <- (mk_adapted_seq_Sup _ Hf).
intros.
assert (Hphi : SF genE (mk_adapted_seq f n)) by now apply mk_adapted_seq_SF.
rewrite (LInt_p_SFp_eq Einhab _ _ Hphi); try easy.
apply LInt_SFp_Dirac.
now apply (mk_adapted_seq_nonneg _ Hf).
Qed.

End LInt_p_Dirac.