fine lemmas (#748)

* changelog and simple lint * linting * typos * unncessary change * notations for rintegral * fixing changelog * use lte_oppl, shorten * fix changelog Co-authored-by: Reynald Affeldt <[email protected]>
math-comp · Sep 23, 2022 · dc56124 · dc56124
1 parent f9a37af
commit dc56124
Show file tree

Hide file tree

Showing 3 changed files with 45 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -5,6 +5,10 @@
 ### Added
 - in `topology.v`:
   + lemmas `continuous_subspaceT`, `subspaceT_continuous`
+- in `constructive_ereal.v`
+  + lemmas `fine_le`, `fine_lt`, `fine_abse`, `abse_fin_num`
+- in `lebesgue_integral.v`
+  + lemmas `integral_fune_lt_pinfty`, `integral_fune_fin_num`
 
 ### Changed
 

diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
@@ -542,6 +542,18 @@ Section ERealArithTh_numDomainType.
 Context {R : numDomainType}.
 Implicit Types (x y z : \bar R) (r : R).
 
+Lemma fine_le : {in fin_num &, {homo @fine R : x y / x <= y >-> (x <= y)%R}}.
+Proof. by move=> [? [?| |]| |]. Qed.
+
+Lemma fine_lt : {in fin_num &, {homo @fine R : x y / x < y >-> (x < y)%R}}.
+Proof. by move=> [? [?| |]| |]. Qed.
+
+Lemma fine_abse : {in fin_num, {morph @fine R : x / `|x| >-> `|x|%R}}.
+Proof. by case. Qed.
+
+Lemma abse_fin_num x : `|x| \is a fin_num <-> x \is a fin_num.
+Proof. by case: x. Qed.
+
 Lemma fine_eq0 x : x \is a fin_num -> (fine x == 0%R) = (x == 0).
 Proof. by move: x => [//| |] /=; rewrite fin_numE. Qed.
 

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -2771,11 +2771,14 @@ Local Open Scope ereal_scope.
 Variables (d : measure_display) (T : measurableType d) (R : realType)
           (mu : {measure set T -> \bar R}).
 
-Definition Rintegral (D : set T) (f : T -> \bar R) :=
-  fine (\int[mu]_(x in D) f x).
+Definition Rintegral (D : set T) (f : T -> R) :=
+  fine (\int[mu]_(x in D) (f x)%:E).
 
 End Rintegral.
 
+Notation "\int [ mu ]_ ( x 'in' D ) f" := (Rintegral mu D (fun x => f)) : ring_scope.
+Notation "\int [ mu ]_ x f" := (Rintegral mu setT (fun x => f)) : ring_scope.
+
 Section integrable.
 Local Open Scope ereal_scope.
 Variables (d : measure_display) (T : measurableType d) (R : realType).
@@ -3780,6 +3783,30 @@ Qed.
 
 End integralB.
 
+Section integrable_fune.
+Variables (d : _) (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
+Local Open Scope ereal_scope.
+
+Lemma integral_fune_lt_pinfty (f : T -> \bar R) :
+  mu.-integrable D f -> \int[mu]_(x in D) f x < +oo.
+Proof.
+move=> intf; rewrite (funeposneg f) integralB//;
+  [|exact: integrable_funepos|exact: integrable_funeneg].
+rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lte_oppl ltNye_eq.
+by rewrite integrable_neg_fin_num.
+Qed.
+
+Lemma integral_fune_fin_num (f : T -> \bar R) :
+  mu.-integrable D f -> \int[mu]_(x in D) f x \is a fin_num.
+Proof.
+move=> h; apply/fin_numPlt; rewrite integral_fune_lt_pinfty// andbC/= -/(- +oo).
+rewrite lte_oppl -integralN; first exact/integral_fune_lt_pinfty/integrableN.
+by rewrite fin_num_adde_def// fin_numN integrable_neg_fin_num.
+Qed.
+
+End integrable_fune.
+
 Section integral_counting.
 Local Open Scope ereal_scope.
 Variables (R : realType).