Lebesgue Stieltjes measure

CHANGELOG_UNRELEASED.md

@@ -14,6 +14,26 @@
 - in `measure.v`:
   + lemmas `negligibleI`, `negligible_bigsetU`, `negligible_bigcup`
 
+- in `reals.v`:
+  + lemma `le_inf`
+- in `constructive_ereal.v`:
+  + lemmas `le_er_map`, `er_map_idfun`
+- new `lebesgue_stieltjes_measure.v`:
+  + notation `right_continuous`
+  + lemmas `right_continuousW`, `nondecreasing_right_continuousP`
+  + mixin `isCumulative`, structure `Cumulative`, notation `cumulative`
+  + `idfun` instance of `Cumulative`
+  + `wlength`, `wlength0`, `wlength_singleton`, `wlength_setT`, `wlength_itv`,
+    `wlength_finite_fin_num`, `finite_wlength_itv`, `wlength_itv_bnd`, `wlength_infty_bnd`,
+    `wlength_bnd_infty`, `infinite_wlength_itv`, `wlength_itv_ge0`, `wlength_Rhull`,
+    `le_wlength_itv`, `le_wlength`, `wlength_semi_additive`, `wlength_ge0`,
+    `lebesgue_stieltjes_measure_unique`
+  + content instance of `hlength`
+  + `cumulative_content_sub_fsum`,
+    `wlength_sigma_sub_additive`, `wlength_sigma_finite`
+  + measure instance of `hlength`
+  + definition `lebesgue_stieltjes_measure`
+
 ### Changed
 
 - in `hoelder.v`:
@@ -25,11 +45,30 @@
   + order of parameters changed in `semi_sigma_additive_is_additive`,
     `isMeasure`
 
+- in `lebesgue_measure.v`:
+  + are now prefixed with `LebesgueMeasure`:
+    * `hlength`, `hlength0`, `hlength_singleton`, `hlength_setT`, `hlength_itv`,
+      `hlength_finite_fin_num`, `hlength_infty_bnd`,
+      `hlength_bnd_infty`, `hlength_itv_ge0`, `hlength_Rhull`,
+      `le_hlength_itv`, `le_hlength`, `hlength_ge0`, `hlength_semi_additive`,
+      `hlength_sigma_sub_additive`, `hlength_sigma_finite`, `lebesgue_measure`
+    * `finite_hlengthE` renamed to `finite_hlentgh_itv`
+    * `pinfty_hlength` renamed to `infinite_hlength_itv`
+  + `lebesgue_measure` now defined with `lebesgue_stieltjes_measure`
+  + `lebesgue_measure_itv` does not refer to `hlength` anymore
+- moved from `lebesgue_measure.v` to `lebesgue_stieltjes_measure.v`
+  + notations `_.-ocitv`, `_.-ocitv.-measurable`
+  + definitions `ocitv`, `ocitv_display`
+  + lemmas `is_ocitv`, `ocitv0`, `ocitvP`, `ocitvD`, `ocitvI`
+
 ### Renamed
 
 - in `charge.v`
   + `isCharge` -> `isSemiSigmaAdditive`
 
+- in `ereal.v`:
+  + `le_er_map` -> `le_er_map_in`
+
 ### Generalized
 
 - in `topology.v`:
@@ -39,6 +78,8 @@
 
 ### Removed
 
+- `lebesgue_measure_unique` (generalized to `lebesgue_stieltjes_measure_unique`)
+
 ### Infrastructure
 
 ### Misc

_CoqProject

@@ -32,6 +32,7 @@ theories/nsatz_realtype.v
 theories/esum.v
 theories/real_interval.v
 theories/lebesgue_measure.v
+theories/lebesgue_stieltjes_measure.v
 theories/forms.v
 theories/derive.v
 theories/measure.v

theories/Make

@@ -30,6 +30,7 @@ numfun.v
 lebesgue_integral.v
 hoelder.v
 probability.v
+lebesgue_stieltjes_measure.v
 summability.v
 signed.v
 itv.v

theories/constructive_ereal.v

@@ -123,6 +123,9 @@ Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' :=
   | -oo => -oo
   end.
 
+Lemma er_map_idfun T (x : \bar T) : er_map idfun x = x.
+Proof. by case: x. Qed.
+
 Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.
 
 Section EqEReal.
@@ -356,6 +359,13 @@ Definition lteey := (ltey, leey).
 
 Definition lteNye := (ltNye, leNye).
 
+Lemma le_er_map (f : R -> R) : {homo f : x y / (x <= y)%R} ->
+  {homo er_map f : x y / x <= y}.
+Proof.
+move=> ndf.
+by move=> [r| |] [l| |]//=; rewrite ?leey ?leNye// !lee_fin; exact: ndf.
+Qed.
+
 Lemma le_total_ereal : totalPOrderMixin [porderType of \bar R].
 Proof.
 by move=> [?||][?||]//=; rewrite (ltEereal, leEereal)/= ?num_real ?le_total.

theories/ereal.v

@@ -162,7 +162,7 @@ Section ERealArithTh_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y z u a b : \bar R) (r : R).
 
-Lemma le_er_map (A : set R) (f : R -> R) :
+Lemma le_er_map_in (A : set R) (f : R -> R) :
   {in A &, {homo f : x y / (x <= y)%O}} ->
   {in (EFin @` A)%classic &, {homo er_map f : x y / (x <= y)%E}}.
 Proof.

theories/lebesgue_integral.v

@@ -4869,7 +4869,7 @@ move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
 have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
   by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm.
 rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
-by rewrite lebesgue_measure_itv hlength_itv/= lte_fin gtr_opp// EFinD ltry.
+by rewrite lebesgue_measure_itv/= lte_fin gtr_opp// EFinD ltry.
 Qed.
 
 Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) :
@@ -5571,7 +5571,7 @@ have ball_itv2 r : 0 < r -> ball x r = `[x - r, x + r] `\` [set x + r; x - r].
   rewrite -ball_itvr // setDD setIC; apply/esym/setIidPl.
   by rewrite ballE set_itvcc => ?/=; rewrite in_itv => /andP [/ltW -> /ltW ->].
 have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E.
-  move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv hlength_itv /= lte_fin.
+  move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv/= lte_fin.
   rewrite ler_lt_add // ?rE // -EFinD; congr (_ _).
   by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r.
 move=> oA intf ctsfx Ax.