integral of constant function (#781)

* integral of constant function

* generalize le_integral_abse

* comment from mca meeting, lt0e, ltry, etc.

* comments for reviews and other minor fixes

Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -113,6 +113,10 @@
     `cvgPpinfty_lt_near` and `cvgPninfty_lt_near`
 - in `classical_sets.v`:
   + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F`
+- in `lebesgue_integral.v`:
+  + lemma `integral_cstNy`
+  + lemma `ae_eq0`
+  + lemma `integral_cst`
 
 - in `fsbig.v`:
   + lemma `fsbig_setU_set1`
@@ -129,7 +133,7 @@
   + new definition `inv_fun`.
   + new lemmas `ler_ltP`, and `real_ltr_distlC`.
 - in file `constructive_ereal.v`,
-  + new lemmas `real_ltey`, `real_ltNye`, `real_leey`, `real_leNye`,
+  + new lemmas `real_ltry`, `real_ltNyr`, `real_leey`, `real_leNye`,
     `fin_real`, `addNye`, `addeNy`, `gt0_muley`, `lt0_muley`, `gt0_muleNy`, and
     `lt0_muleNy`.
   + new lemmas `daddNye`, and `daddeNy`.
@@ -201,6 +205,10 @@
   + new lemmas `dfwithin`, `dfwithout`, and `dfwithP`.
 - in `measure.v`:
   + lemma `measurable_fun_bool`
+- in `constructive_ereal.v`:
+  + lemma `lt0e`
+- in `lebesgue_integral.v`:
+  + lemma `le_integral_comp_abse`
 
   + new lemma `dfwith_projK`
 - in file `topology.v`,
@@ -243,6 +251,8 @@
   + definition `fimfunE` now uses fsbig
 - in `sequence.v`:
   + `nneseries_pinfty` generalized to `eseries_pinfty`
+- in `lebesgue_integral.v`:
+  + implicits of `ae_eq_integral`
 
 - moved from `mathcomp_extra.v` to `classical_sets.v`: `pred_oappE`, and
     `pred_oapp_set`.
@@ -304,6 +314,10 @@
   + `seqDUE` -> `seqDU_seqD`
 - file `theories/mathcomp_extra.v` moved to `classical/mathcomp_extra.v`
 - `theories/set_interval.v` -> `theories/real_interval.v`
+- in `lebesgue_integral.v`:
+  + `integral_cst_pinfty` -> `integral_csty`
+  + `sintegral_cst` -> `sintegral_EFin_cst`
+  + `integral_cst` -> `integral_cstr`
 
 - in file `constructive_ereal.v`,
   + `esum_ninftyP` -> `esum_eqNyP`
@@ -352,6 +366,9 @@
   + `app_cvg_locally` -> `cvg_ball`
 - in file `topology.v`,
   + `prod_topo_apply_continuous` -> `proj_continuous`
+- in `constructive_ereal.v`:
+  + `ltey` -> `ltry`
+  + `ltNye` -> `ltNyr`
 
 ### Generalized
 
@@ -411,6 +428,8 @@
   + `prod_topo_apply` -> `proj`
 - in `lebesgue_integral.v`:
   + `integral_sum` -> `integral_nneseries`
+- in `constructive_ereal.v`:
+  + `ltey`, `ltNye`
 
 ### Deprecated
 

theories/altreals/realseq.v

@@ -383,8 +383,8 @@ Lemma ncvg_gt (u : nat -> R) (l1 l2 : \bar R) :
     exists K, forall n, (K <= n)%N -> (l1 < (u n)%:E)%E.
 Proof.
 case: l1 l2 => [l1||] [l2||] //=; first last.
-+ by move=> _ _; exists 0%N => ? ?; exact: ltNye.
-+ by move=> _ _; exists 0%N => ? ?; exact: ltNye.
++ by move=> _ _; exists 0%N => ? ?; exact: ltNyr.
++ by move=> _ _; exists 0%N => ? ?; exact: ltNyr.
 + by move=> _ /(_ (NPInf l1)) [K cv]; exists K => n /cv.
 move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)).
 case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //.
@@ -548,4 +548,3 @@ Qed.
 End LimOp.
 
 (* -------------------------------------------------------------------- *)
-

theories/altreals/realsum.v

@@ -180,7 +180,7 @@ case: (pselect (has_sup E)); last first.
   move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=.
   case/(_ M): h=> x [K -> lt_MuK]; exists K=> n le_Kn; rewrite inE.
   by apply/(lt_le_trans lt_MuK)/mono_u.
-move=> supE; exists (sup E)%:E => //; first exact: ltNye.
+move=> supE; exists (sup E)%:E => //; first exact: ltNyr.
 elim/nbh_finW=>e /= gt0_e.
 case: (sup_adherent gt0_e supE)=> x [K ->] lt_uK.
 exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.