Lebesgue measure and integral

[affeldt-aist]

Merged as #543

A formalization of the Lebesgue measure and integral.

Fixes #368 .

[pi8027]

Here is a patch I propose (context: math-comp/math-comp#732 (comment)):

From 46158eb46e2ab033884151726c6dbbd9233b1e24 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <[email protected]>
Date: Wed, 26 May 2021 14:37:16 +0900
Subject: [PATCH] normrzE

---
 theories/measure_wip.v | 29 +++++++++++------------------
 1 file changed, 11 insertions(+), 18 deletions(-)

diff --git a/theories/measure_wip.v b/theories/measure_wip.v
index 5f94173..e7e507f 100644
--- a/theories/measure_wip.v
+++ b/theories/measure_wip.v
@@ -63,17 +63,8 @@ Definition uncurry {A B C:Type} (f:A -> B -> C)
   (p:A * B) : C := match p with (x, y) => f x y end.
 
 (* NB: PR to MathComp in progress *)
-Lemma gez0_norm (R : numDomainType) (i : int) : 0 <= i -> `|i|%:R = i%:~R :> R.
-Proof. by move/gez0_abs => <-. Qed.
-
-Lemma gtz0_norm (R : numDomainType) (i : int) : 0 < i -> `|i|%:R = i%:~R :> R.
-Proof. by move/gtz0_abs => <-. Qed.
-
-Lemma ltz0_norm (R : numDomainType) (i : int) : i < 0 -> `|i|%:R = - i%:~R :> R.
-Proof.
-move/ltz0_abs/eqP; rewrite -eqr_oppLR => /eqP <-.
-by rewrite abszN absz_id mulrNz opprK.
-Qed.
+Lemma normrzE (R : numDomainType) i : `|i|%:R = `|i|%:~R :> R.
+Proof. by rewrite -abszE. Qed.
 (* END NB: PR to MathComp in progress *)
 
 Section eseries.
@@ -3570,10 +3561,11 @@ exists (set_of_itv \o ccitv).
   rewrite predeqE => /= r; split => // _; have [r0|r0] := leP 0 r.
   - exists (absz (ceil r)) => //; apply/set_of_itv_mem.
     rewrite itv_boundlr/= 2!lte_bnd (le_trans _ r0)/= ?oppr_le0 ?ler0n//.
-    by rewrite gez0_norm ?ceil_ge0 // ler_ceil.
+    by rewrite normrzE ger0_norm ?ceil_ge0 // ler_ceil.
   - exists (absz (floor r)) => //; apply/set_of_itv_mem.
     rewrite itv_boundlr /= 2!lte_bnd (le_trans (ltW r0)) ?ler0n// andbT.
-    by rewrite ler_oppl ltz0_norm ?floor_lt0// ler_oppl opprK ler_floor.
+    rewrite ler_oppl normrzE ltr0_norm ?floor_lt0//.
+    by rewrite mulrNz ler_opp2 ler_floor.
 move=> n; split.
   by exists [fset (ccitv n)]%fset; rewrite ssetE /= big_seq_fset1.
 by rewrite length_itv hlength_itv /=; case: ifPn; rewrite lte_pinfty.
@@ -3965,7 +3957,8 @@ have len_iIN_dvg : forall M, M > 0 -> exists N, (N >= 1)%N /\ (M%:E < length (iI
     have ? : (0 < `|ceil M|)%N by rewrite absz_gt0 gt_eqF // ceil_gt0.
     exists `|ceil M|%N; split=> //; rewrite /iIN ioo set_of_itvE setTI.
     rewrite length_ccitv lte_fin (le_lt_trans (ler_ceil _)) //.
-    by rewrite -gtz0_norm ?ceil_gt0// ltr_nat -addnn -ltn_subLR // subnn.
+    rewrite -[c in c%:~R]gtr0_norm ?ceil_gt0//.
+    by rewrite -normrzE ltr_nat -addnn -add1n leq_add2r.
   rewrite /iIN.
   wlog : i {ij iIN} b r {iroo} / i = Interval -oo%O (BSide b r).
     move=> h; move: iroo => [->|iroo]; first exact: h.
@@ -3978,7 +3971,7 @@ have len_iIN_dvg : forall M, M > 0 -> exists N, (N >= 1)%N /\ (M%:E < length (iI
     rewrite ltr_oppl opprK.
     case: ifPn => [rrM|].
       rewrite meet_l ?(le_trans r0) // lte_fin mulrSr.
-      rewrite gez0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))//.
+      rewrite normrzE ger0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))//.
       rewrite -ltr_subl_addl (@le_lt_trans _ _ (`|r| + M)) // ?ler_addr//.
         by rewrite ler0_norm // addrC.
       rewrite (@lt_le_trans _ _ (`|r| + M + 1)) // ?ltr_addl // ler_add2r.
@@ -3986,7 +3979,7 @@ have len_iIN_dvg : forall M, M > 0 -> exists N, (N >= 1)%N /\ (M%:E < length (iI
     move=> /negP; apply: absurd.
     rewrite -(ler0_norm r0) mulrSr ltr_spaddr //.
     rewrite (@le_trans _ _ (`|r| + M)) // ?ler_addl //; first exact/ltW.
-    by rewrite gez0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))// ler_ceil.
+    by rewrite normrzE (ger0_norm (ceil_ge0 _)) ?addr_ge0 ?ler_ceil // ltW.
   have crM : (0 < `|ceil (`|r| + M)|)%N.
     by rewrite absz_gt0 gt_eqF // ceil_gt0 // -(addr0 0) ler_lt_add.
   exists (`|ceil (`| r | + M)|%N); split => //.
@@ -3994,10 +3987,10 @@ have len_iIN_dvg : forall M, M > 0 -> exists N, (N >= 1)%N /\ (M%:E < length (iI
   rewrite opprK andbT.
   case: ifPn => [_|].
     rewrite meet_l; last first.
-      rewrite gez0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))// gtr0_norm//.
+      rewrite normrzE ger0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))// gtr0_norm//.
       by rewrite (le_trans (ler_ceil _)) // ler_int ceil_le // ler_addl ltW.
     rewrite lte_fin -{1}(add0r M) ltr_le_add //.
-    rewrite gez0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))// gtr0_norm//.
+    rewrite normrzE ger0_norm ?ceil_ge0// ?(addr_ge0 _ (ltW _))// gtr0_norm//.
     by rewrite (le_trans (ler_ceil _)) // ler_int ceil_le // ler_addr ltW.
   move/negP; apply: absurd.
   rewrite -(@ltr_nat R) in crM.
-- 
2.20.1

[affeldt-aist]

@pi8027 I have replayed the proofs in the spirit of your patch. Maybe that's good enough with only one lemma.
I modify the mathcomp PR accordingly. Thanks for your time!