mv charge to measure and lebesgue_integral (#1953)

* mv charge to measure and lebesgue_integral

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -107,13 +107,21 @@
   + instance of `SubLModule` on  `{linear_continuous _ -> _ }`
   + instance of `LinearContinuous` on the null function
   + notations `{linear_continuous _ -> _ | _ }` and `{linear_continuous _ -> _ }`
-  + definitions `lcfun`, `lcfun_key, `lcfunP`
+  + definitions `lcfun`, `lcfun_key`, `lcfunP`
   + lemmas `lcfun_eqP`, `null_fun_continuous`, `fun_cvgD`,
    `fun_cvgN`, `fun_cvgZ`, `fun_cvgZr`
   + lemmas `lcfun_continuous` and `lcfun_linear`
+
+- new files `signed_measure.v` and `radon_nikodym.v`
+  + with the contents of `charge.v` (deprecated)
 
 ### Changed
 
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definition `preimage_set_system`
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+    `preimage_set_system_id`
+
 - moved from `topology_structure.v` to `filter.v`:
   + lemma `continuous_comp` (and generalized)
 
@@ -122,6 +130,50 @@
   + `funeposneg` renamed to `funeposBneg` and direction of the equality changed
   + `funeD_posD` renamed to `funeDB` and direction of the equality changed
 
+- in `constructive_ereal.v`:
+  + lemmas `EFin_semi_additive` and `dEFin_semi_additive` turned into `Let`s
+
+- moved from `charge.v` to `signed_measure.v`:
+  + mixin `isAdditiveCharge`, structure `AdditiveCharge`
+  + mixin `isSemiSigmaAdditive`, structure `Charge`
+  + factory `isCharge`
+  + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`,
+    `charge_semi_additive2`, `chargeU`, `chargeDI`, `charge_partition`
+  + definitions `measure_of_charge`, `charge_of_finite_measure`
+  + lemma `chargeD`
+  + definitions `crestr`, `crestr0`, `czero`, `cscale`
+  + lemmas `dominates_cscalel`, `dominates_cscaler`
+  + definition `copp`
+  + lemma `cscaleN1`
+  + definition `cadd`
+  + lemmas `dominates_cadd`, `dominates_pushforward`
+  + definitions `positive_set`, `negative_set`
+  + lemmas `negative_set_charge_le0`, `negative_set0`,
+    `positive_negative0`, `bigcup_negative_set`, `negative_setU`,
+    `hahn_decomposition_lemma`
+  + definition `hahn_decomposition`
+  + theorem `Hahn_decomposition`
+  + lemmas `Hahn_decomposition_uniq`, `cjordan_posE`, `cjordan_negE`
+  + definitions `jordan_pos`, `jordan_neg`
+  + lemmas `jordan_posE`, `jordan_negE`, `jordan_decomp`, `jordan_pos_dominates`,
+    `jordan_neg_dominates`
+  + definition `charge_variation`, `charge_dominates`
+  + lemmas `abse_charge_variation`, `null_charge_dominatesP`,
+    `content_charge_dominatesP`, `charge_variation_continuous`
+
+- moved from `charge.v` to `radon_nikodym.v`:
+  + definition `induced_charge`
+  + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`,
+    `integral_normr_continuous`
+  + definitions `approxRN`, `int_approxRN`, `sup_int_approxRN`
+  + lemmas `sup_int_approxRN_ge0`, `radon_nikodym_finite`,
+    `radon_nikodym_sigma_finite`, `change_of_variables`, `integrableM`,
+    `chain_rule`
+  + definition `Radon_Nikodym`
+  + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`,
+    `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
+    `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
+
 ### Renamed
 
 - in `tvs.v`:
@@ -193,6 +245,8 @@
 
 ### Deprecated
 
+- file `charge.v` (use `measure.v` and/or `lebesgue_integral.v`)
+
 ### Removed
 
 - file `signed.v`

_CoqProject

@@ -104,6 +104,7 @@ theories/measure_theory/probability_measure.v
 theories/measure_theory/measure_negligible.v
 theories/measure_theory/measure_extension.v
 theories/measure_theory/measurable_function.v
+theories/measure_theory/signed_measure.v
 theories/measure_theory/measure.v
 
 theories/measurable_realfun.v
@@ -123,6 +124,7 @@ theories/lebesgue_integral_theory/lebesgue_Rintegral.v
 theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
 theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
 theories/lebesgue_integral_theory/lebesgue_integral.v
+theories/lebesgue_integral_theory/radon_nikodym.v
 theories/lebesgue_integral_theory/giry.v
 
 theories/ftc.v

reals/constructive_ereal.v

@@ -931,8 +931,9 @@ Proof. by case: x => //=; rewrite oppr0. Qed.
 
 Lemma EFinD r r' : (r + r')%:E = r%:E + r'%:E. Proof. by []. Qed.
 
-Lemma EFin_semi_additive : @semi_additive _ (\bar R) EFin. Proof. by split. Qed.
-HB.instance Definition _ := GRing.isSemiAdditive.Build R (\bar R) EFin
+Let EFin_semi_additive : @nmod_morphism _ (\bar R) EFin. Proof. by split. Qed.
+
+HB.instance Definition _ := GRing.isNmodMorphism.Build R (\bar R) EFin
   EFin_semi_additive.
 
 Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E. Proof. by []. Qed.
@@ -1583,10 +1584,11 @@ Proof. by []. Qed.
 
 Lemma dEFinE (r : R) : dEFin r = r%:E. Proof. by []. Qed.
 
-Lemma dEFin_semi_additive : @semi_additive _ (\bar^d R) dEFin.
+Let dEFin_semi_additive : @nmod_morphism _ (\bar^d R) dEFin.
 Proof. by split. Qed.
+
 #[export]
-HB.instance Definition _ := GRing.isSemiAdditive.Build R (\bar^d R) dEFin
+HB.instance Definition _ := GRing.isNmodMorphism.Build R (\bar^d R) dEFin
   dEFin_semi_additive.
 
 Lemma dEFinB (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.

reals/reals.v

@@ -470,7 +470,7 @@ Lemma RfloorE x : Rfloor x = (Num.floor x)%:~R.
 Proof. by []. Qed.
 
 Lemma mem_rg1_floor x : (range1 (Num.floor x)%:~R) x.
-Proof. by rewrite /range1 /mkset -intrD1 floor_le_tmp floorD1_gt. Qed.
+Proof. by rewrite /range1 /mkset -intrD1 floor_le floorD1_gt. Qed.
 
 Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
 Proof. exact: mem_rg1_floor. Qed.
@@ -510,7 +510,7 @@ Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}.
 Proof. by move=> x y /Num.Theory.le_floor; rewrite ler_int. Qed.
 
 Lemma Rfloor_ge_int x (i : int) : (i%:~R <= x)= (i%:~R <= Rfloor x).
-Proof. by rewrite ler_int floor_ge_int_tmp. Qed.
+Proof. by rewrite ler_int floor_ge_int. Qed.
 
 Lemma Rfloor_lt_int x (i : int) : (x < i%:~R) = (Rfloor x < i%:~R).
 Proof. by rewrite ltr_int -floor_lt_int. Qed.
@@ -544,10 +544,10 @@ Lemma Rceil_ge x : x <= Rceil x.
 Proof. by rewrite Num.Theory.ceil_ge ?num_real. Qed.
 
 Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.
-Proof. by move=> x y ?; rewrite /Rceil ler_int le_ceil_tmp. Qed.
+Proof. by move=> x y ?; rewrite /Rceil ler_int le_ceil. Qed.
 
 Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x.
-Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) le_ceil_tmp. Qed.
+Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) le_ceil. Qed.
 
 Lemma RceilE x : Rceil x = (Num.ceil x)%:~R.
 Proof. by []. Qed.

theories/Make

@@ -71,6 +71,7 @@ measure_theory/probability_measure.v
 measure_theory/measure_negligible.v
 measure_theory/measure_extension.v
 measure_theory/measurable_function.v
+measure_theory/signed_measure.v
 measure_theory/measure.v
 
 measurable_realfun.v
@@ -89,6 +90,7 @@ lebesgue_integral_theory/lebesgue_integral_under.v
 lebesgue_integral_theory/lebesgue_Rintegral.v
 lebesgue_integral_theory/lebesgue_integral_fubini.v
 lebesgue_integral_theory/lebesgue_integral_differentiation.v
+lebesgue_integral_theory/radon_nikodym.v
 lebesgue_integral_theory/lebesgue_integral.v
 lebesgue_integral_theory/giry.v
 

theories/all_analysis.v

@@ -19,7 +19,6 @@ From mathcomp Require Export hoelder.
 From mathcomp Require Export probability.
 From mathcomp Require Export lebesgue_stieltjes_measure.
 From mathcomp Require Export convex.
-From mathcomp Require Export charge.
 From mathcomp Require Export kernel.
 From mathcomp Require Export pi_irrational.
 From mathcomp Require Export gauss_integral.