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 t ⇒ Rabs (f t)))).
Proof.
intros f; split.
intros (H1,(H2,H3)); split; try easy.
assert (H4: measurable_fun_Rbar gen (fun x : E ⇒ Finite (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 x ⇒ Rbar_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 : E ⇒ Rabs (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 t ⇒ real (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:E→R),
(∀ 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 t ⇒ real (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 t ⇒ f 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 t ⇒ f 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:(E→Rbar)->Prop) ⇒
(∀ f g, ae mu (fun t ⇒ f t = g t) → P f → P g).
End LInt_Rbar.