Library Lebesgue.LInt

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
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.
This file is still WIP...

From Requisite Require Import stdlib_wR.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Lebesgue Require Import Bochner_wDep.

Local Open Scope R_scope.

Section LInt_def.

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


Definition nonneg_part :=
  fun (f : E Rbar) (x : E) ⇒ Rbar_max 0 (f x).

Definition nonpos_part :=
  fun (f : E Rbar) (x : E) ⇒ Rbar_max 0 (Rbar_opp (f x)).

Lemma sum_nonneg_nonpos_part :
   f x, f x = Rbar_minus (nonneg_part f x) (nonpos_part f x).
Proof.
intros f x.
case (Rbar_le_lt_dec 0 (f x)); intros H.
unfold nonneg_part, nonpos_part.
rewrite Rbar_max_right; try easy.
rewrite Rbar_max_left; try easy.
unfold Rbar_minus; simpl.
now rewrite Ropp_0, Rbar_plus_0_r.
replace (Finite 0) with (Rbar_opp 0).
apply Rbar_opp_le; easy.
simpl; f_equal; ring.
unfold nonneg_part, nonpos_part.
rewrite Rbar_max_left.
2: apply Rbar_lt_le; easy.
rewrite Rbar_max_right.
unfold Rbar_minus; rewrite Rbar_plus_0_l.
rewrite Rbar_opp_involutive; easy.
replace (Finite 0) with (Rbar_opp 0).
apply Rbar_opp_le; try easy.
apply Rbar_lt_le; easy.
simpl; f_equal; ring.
Qed.

Lemma nonneg_nonneg_part :
   f, nonneg (nonneg_part f).
Proof.
intros f x; unfold nonneg_part.
case (f x); simpl; try easy.
intros t; apply Rmax_l.
Qed.

Lemma nonneg_nonpos_part :
   f, nonneg (nonpos_part f).
Proof.
intros f x; unfold nonpos_part.
case (f x); simpl; try easy.
intros t; apply Rmax_l.
Qed.

Lemma sum_nonneg_nonpos_part_abs :
   f x, Rbar_abs (f x) = Rbar_plus (nonneg_part f x) (nonpos_part f x).
Proof.
intros f x.
case (Rbar_le_lt_dec 0 (f x)); intros H.
unfold nonneg_part, nonpos_part.
rewrite Rbar_max_right; try easy.
rewrite Rbar_max_left; try easy.
rewrite Rbar_plus_0_r.
apply Rbar_abs_pos; easy.
replace (Finite 0) with (Rbar_opp 0).
apply Rbar_opp_le; easy.
simpl; f_equal; ring.
unfold nonneg_part, nonpos_part.
rewrite Rbar_max_left.
2: apply Rbar_lt_le; easy.
rewrite Rbar_max_right.
unfold Rbar_minus; rewrite Rbar_plus_0_l.
apply Rbar_abs_neg.
apply Rbar_lt_le; easy.
replace (Finite 0) with (Rbar_opp 0).
apply Rbar_opp_le; try easy.
apply Rbar_lt_le; easy.
simpl; f_equal; ring.
Qed.

Definition ex_LInt : (E R) Prop := fun f
  let f_p := nonneg_part f in
  let f_m := nonpos_part f in
     measurable_fun gen gen_R f
     is_finite (LInt_p mu f_p) is_finite (LInt_p mu f_m).

Definition LInt : (E R) R :=
  fun f
  let f_p := nonneg_part f in
  let f_m := nonpos_part f in
    ((LInt_p mu f_p)-(LInt_p mu f_m))%R.


Lemma LInt_ext : f g,
    ( x, f x = g x)
      LInt f = LInt g.
Proof.
intros f g H.
unfold LInt, nonneg_part, nonpos_part; f_equal; f_equal.
apply LInt_p_ext; intros x; rewrite H; easy.
apply LInt_p_ext; intros x; rewrite H; easy.
Qed.


Lemma ex_LInt_equiv_abs :
    f,
    (ex_LInt f)
       (measurable_fun gen gen_R f
          is_finite (LInt_p mu (fun tRabs (f t)))).
Proof.
intros f; split.
intros (H1,(H2,H3)); split; try easy.
assert (H4: measurable_fun_Rbar gen (fun x : EFinite (f x))).
apply measurable_fun_composition with (2:=measurable_fun_Finite); easy.
erewrite LInt_p_ext.
2: intros x; apply trans_eq with (Rbar_abs (f x)); [easy|idtac].
2: rewrite (sum_nonneg_nonpos_part_abs f x); easy.
rewrite LInt_p_plus; try easy.
rewrite <- H2, <- H3; easy.
split.
apply nonneg_nonneg_part.
apply measurable_fun_fp; easy.
split.
apply nonneg_nonpos_part.
apply measurable_fun_fm; easy.
intros (H1,H2); split; try easy; split.
eapply Rbar_bounded_is_finite.
apply LInt_p_nonneg; try easy.
apply nonneg_nonneg_part.
2: easy.
2: exact H2.
apply LInt_p_monotone; try easy.
intros x; replace (Finite (Rabs (f x))) with (Rbar_abs (f x)) by easy.
rewrite (sum_nonneg_nonpos_part_abs f x).
rewrite <- (Rbar_plus_0_r (nonneg_part f x)) at 1.
apply Rbar_plus_le_compat_l.
apply nonneg_nonpos_part.
eapply Rbar_bounded_is_finite.
apply LInt_p_nonneg; try easy.
apply nonneg_nonpos_part.
2: easy.
2: exact H2.
apply LInt_p_monotone; try easy.
intros x; replace (Finite (Rabs (f x))) with (Rbar_abs (f x)) by easy.
rewrite (sum_nonneg_nonpos_part_abs f x).
rewrite <- (Rbar_plus_0_l (nonpos_part f x)) at 1.
apply Rbar_plus_le_compat_r.
apply nonneg_nonneg_part.
Qed.

LInk with Bif

Lemma Bif_measurable : (f : E R),
         bf : Bif mu f,
          measurable_fun_R gen f.
Proof.
intros f bf.
generalize (measurable_Bif bf).
unfold fun_Bif, measurable_fun_R.
intros H A HA.
apply H.
apply measurable_R_equiv_oo; easy.
Qed.

Lemma Bif_ex_LInt : (f : E R),
         (bf : Bif mu f),
        ex_LInt f.
   Proof.
   intros f bf.
   apply ex_LInt_equiv_abs.
   split.
   apply Bif_measurable; easy.
   generalize bf.
   destruct bf; intros bf.
   destruct (proj2 (ax_lim_l1 (mkposreal _ Rlt_0_1))) as (N,HN).
   simpl in HN; rewrite Rplus_0_l in HN.
   eapply Rbar_bounded_is_finite.
   apply LInt_p_nonneg; try easy.
   intros t; simpl; apply Rabs_pos.
   2: easy.
   eapply LInt_p_monotone.
   intros t.
   replace (Finite (Rabs (f t))) with (Rbar_abs (Finite (f t))) by easy.
   replace (Finite (f t)) with
     (Rbar_plus (Rbar_minus (f t) (seq N t)) (seq N t)).
   2: apply sym_eq, Rbar_plus_minus_r; easy.
   eapply Rbar_le_trans with (1:= Rbar_abs_triang _ _).
   apply Rbar_le_refl.
   rewrite LInt_p_plus; try easy;
      try (intros t; apply Rbar_abs_ge_0).
   assert (T1:is_finite ((LInt_p mu
        (fun x
           Rbar_abs (Rbar_minus (f x) (seq N x)))))).
  apply Rbar_bounded_is_finite with 0 1; try easy.
  apply LInt_p_nonneg; try easy.
  intros t; apply Rbar_abs_ge_0.
  apply Rbar_lt_le.
  replace (LInt_p mu (fun x
        Rbar_abs (Rbar_minus (f x) (seq N x)))) with (LInt_p mu
              (fun x ⇒ ( f - seq N )%fn x)); try easy.
  apply HN; auto with arith.
  apply LInt_p_ext; intros t.
  unfold fun_norm, norm; simpl.
  unfold abs; simpl; f_equal; f_equal.
  unfold fun_plus, fun_scal, opp; simpl.
  unfold plus, scal, mult, one; simpl.
  unfold mult; simpl; ring.
  assert (T2: is_finite ((LInt_p mu (fun xRbar_abs (seq N x))))).
  generalize (integrable_sf_norm (ax_int N)).
  intros K; generalize (Bif_integrable_sf K).
  intros K'; generalize (is_finite_LInt_p_Bif K').
  unfold fun_Bif, fun_norm.
  intros Y.
  erewrite LInt_p_ext.
  apply Y.
  intros x; case (seq N); simpl; intros.
  apply norm_ge_0.
  intros x; simpl; f_equal.
  generalize (fun_sf_norm (seq N) x).
  unfold norm; simpl; easy.
  rewrite <- T1, <- T2; easy.
  split.
  intros x; apply Rbar_abs_ge_0.
  apply measurable_fun_abs.
  apply measurable_fun_plus.
  apply measurable_fun_R_Rbar.
  apply Bif_measurable; easy.
  apply measurable_fun_opp.
  apply measurable_fun_R_Rbar.
  apply Bif_measurable.
  apply (Bif_integrable_sf (ax_int N)); easy.
  intros t; easy.
  split.
  intros x; apply Rbar_abs_ge_0.
  apply measurable_fun_abs.
  apply measurable_fun_R_Rbar.
  apply Bif_measurable.
  apply (Bif_integrable_sf (ax_int N)); easy.
Qed.

Lemma ex_LInt_Bif : (f : E R),
        ex_LInt f Bif mu f.
Proof.
intros f H1.
assert (H2: measurable_fun gen gen_R f
     is_finite
        (LInt_p mu
           (fun t : ERabs (f t)))).
apply ex_LInt_equiv_abs; try easy.
destruct H2 as (H2,H3).
apply R_Bif; try easy.
apply measurable_fun_gen_ext2 with (gen_R); try easy.
intros A HA; apply measurable_R_equiv_oo.
apply measurable_gen; easy.
intros A HA; apply measurable_R_equiv_oo.
apply measurable_gen; easy.
Qed.


Lemma Bif_fp : (f: E R),
      bf : Bif mu f, Bif mu (fun treal (nonneg_part f t)).
Proof.
 intros f bf.
 apply R_Bif; try easy.
 apply measurable_fun_gen_ext2 with (gen_R).
 intros A HA; apply measurable_R_equiv_oo.
 apply measurable_gen; easy.
 intros A HA; apply measurable_R_equiv_oo.
 apply measurable_gen; easy.
 apply measurable_fun_composition with (2:=measurable_fun_real).
 apply measurable_fun_fp.
 apply measurable_fun_R_Rbar.
 apply Bif_measurable; easy.
  erewrite LInt_p_ext.
  generalize (Bif_ex_LInt f bf); intros (H1,(H2,H3)).
  apply H2.
  intros t; unfold fun_norm, norm; simpl.
  unfold abs; simpl.
  rewrite Rabs_pos_eq; try easy.
  apply Rmax_l.
  Qed.

Lemma Bif_ext : (f g:ER),
     ( t:E, f t = g t) Bif mu f Bif mu g.
Proof.
 intros f g H1 H2.
 destruct H2.
 eexists seq; try easy.
 intros x; rewrite <- H1; easy.
 apply is_LimSup_seq_Rbar_ext with (2:=ax_lim_l1).
 intros n; apply LInt_p_ext.
 intros x; unfold fun_norm, fun_plus.
 rewrite H1; easy.
Qed.

Lemma Bif_fm : (f: E R),
      bf : Bif mu f, Bif mu (fun treal (nonpos_part f t)).
Proof.
intros f bf.
assert (Y1 : Bif mu (-f)%fn).
apply Bif_ext with (2:=Bif_scal (-1) bf).
intros t; easy.
apply Bif_ext with (2:=Bif_plus Y1 (Bif_fp f bf)).
intros t; unfold fun_plus, fun_scal, plus; simpl.
unfold scal, opp, one; simpl.
replace (f t) with (real (Finite (f t))) at 1; try easy.
rewrite (sum_nonneg_nonpos_part f t); simpl.
unfold mult; simpl; ring.
Qed.

Lemma BInt_LInt_eq : (f : E R),
         bf : Bif mu f,
          BInt bf = LInt f.
Proof.
 intros f bf; unfold LInt.
 generalize (Bif_fp f bf); intros B1.
 generalize (Bif_fm f bf); intros B2.
 rewrite (BInt_ext _ ((B1-B2)%Bif)).
 2: intros t.
 2: replace (f t) with (real (Finite (f t))) at 1; try easy.
 2: rewrite (sum_nonneg_nonpos_part f t); simpl.
 2: unfold fun_plus, fun_scal, one, scal, plus, opp, mult; simpl.
 2: unfold mult; simpl; ring.
 rewrite BInt_minus.
 generalize (Bif_ex_LInt f bf); intros (T1,(T2,T3)).
 rewrite <- T2, <- T3; simpl.
 unfold plus, Rminus; simpl; f_equal.
 apply BInt_LInt_p_eq.
 unfold fun_Bif; intros t.
 apply Rmax_l.
 unfold opp; simpl; f_equal.
 apply BInt_LInt_p_eq.
 unfold fun_Bif; intros t.
 apply Rmax_l.
 Qed.

Lemma ex_LInt_plus :
    (f g : E R),
      ex_LInt f ex_LInt g
      ex_LInt (fun tf t + g t).
Proof.
intros f g Hf Hg.
generalize (ex_LInt_Bif f Hf); intros bf.
generalize (ex_LInt_Bif g Hg); intros bg.
apply Bif_ex_LInt.
apply Bif_ext with (2:=Bif_plus bf bg); easy.
Qed.

Lemma LInt_plus : (f g : E R),
   ex_LInt f ex_LInt g
   LInt f + LInt g
      = LInt (fun tf t + g t).
Proof.
intros f g Hf Hg.
generalize (ex_LInt_Bif f Hf); intros bf.
generalize (ex_LInt_Bif g Hg); intros bg.
rewrite <- BInt_LInt_eq with f bf.
rewrite <- BInt_LInt_eq with g bg.
apply trans_eq with (plus (BInt bf)%Bif (BInt bg)%Bif).
unfold plus; simpl; easy.
rewrite <- BInt_plus.
rewrite BInt_LInt_eq.
f_equal; apply LInt_ext.
Qed.

EO Link with Bif



End LInt_def.

Section LInt_Rbar.

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

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

Definition ex_LInt_Rbar : (E Rbar) Prop := fun f
  let f_p := nonneg_part f in
  let f_m := nonpos_part f in
     measurable_fun gen gen_Rbar f
     is_finite (LInt_p mu f_p) is_finite (LInt_p mu f_m).

Definition LInt_Rbar : (E Rbar) R :=
  fun f
  let f_p := nonneg_part f in
  let f_m := nonpos_part f in
    (Rbar_minus (LInt_p mu f_p) (LInt_p mu f_m)).


Definition ae_compat := fun (P:(ERbar)->Prop) ⇒
  ( f g, ae mu (fun tf t = g t) P f P g).





End LInt_Rbar.