define null set and fix the definition of domination of measure/charge (#1760)

* add def of null_set

* null_dominates

---------

Co-authored-by: Reynald Affeldt <[email protected]>

Author: IshiguroYoshihiro

CHANGELOG_UNRELEASED.md

@@ -12,6 +12,20 @@
 
 - in `normed_module.v`:
   + lemma `limit_point_infinite_setP`
+- in `measure_negligible.v`:
+  + definition `null_set` with notation `_.-null_set`
+  + lemma `subset_null_set`
+  + lemma `negligible_null_set`
+  + lemma `measure0_null_setP`
+  + lemma `null_setU`
+  + definition `null_dominates`
+  + lemma `null_dominates_trans`
+  + lemma `null_content_dominatesP`
+
+- in `charge.v`:
+  + definition `charge_dominates`
+  + lemma `charge_null_dominatesP`
+  + lemma `content_charge_dominatesP`
 
 - in `sequences.v`:
   + lemma `increasing_seq_injective`
@@ -22,10 +36,24 @@
 
 ### Changed
 
+- in `charge.v`:
+  + `dominates_cscalel` specialized from
+    `set _ -> \bar _` to `{measure set _ -> \bar _}`
+
+- in `measurable_structure.v`:
+  + the notation ``` `<< ``` is now for `null_set_dominates`,
+    the previous definition can be recovered with the lemma
+    `null_dominatesP`
+
 ### Renamed
 
 - in `probability.v`:
   + `derivable_oo_continuous_bnd_onemXnMr` -> `derivable_oo_LRcontinuous_onemXnMr`
+- in `measure_negligible.v`:
+  + `measure_dominates_ae_eq` -> `null_dominates_ae_eq`
+
+- in `charge.v`:
+  + `induced` -> `induced_charge`
 
 ### Generalized
 
@@ -68,6 +96,12 @@
 - in `sequences.v`:
   + notation `eq_bigsetU_seqD`
     (deprecated since 1.2.0)
+- in `measurable_structure.v`:
+  + definition `measure_dominates` (use `null_set_dominates` instead)
+  + lemma `measure_dominates_trans`
+
+- in `charge.v`:
+  + lemma `dominates_charge_variation` (use `charge_null_dominatesP` instead)
 
 ### Infrastructure
 

theories/charge.v

@@ -65,7 +65,8 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral.
 (*                              decomposition nuPN: hahn_decomposition nu P N *)
 (*     charge_variation nuPN == variation of the charge nu                    *)
 (*                           := jordan_pos nuPN \+ jordan_neg nuPN            *)
-(*              induced intf == charge induced by a function f : T -> \bar R  *)
+(*  charge_dominates mu nuPN := content_dominates mu (charge_variation nuPN)  *)
+(*       induced_charge intf == charge induced by a function f : T -> \bar R  *)
 (*                              R has type realType; T is a measurableType.   *)
 (*                              intf is a proof that f is integrable over     *)
 (*                              [set: T]                                      *)
@@ -429,24 +430,27 @@ HB.instance Definition _ := isCharge.Build _ _ _ cscale
 End charge_scale.
 
 Lemma dominates_cscalel d (T : measurableType d) (R : realType)
-  (mu : set T -> \bar R)
+  (mu : {measure set T -> \bar R})
   (nu : {charge set T -> \bar R})
   (c : R) : nu `<< mu -> cscale c nu `<< mu.
-Proof. by move=> numu E mE /numu; rewrite /cscale => ->//; rewrite mule0. Qed.
+Proof.
+move=> /null_content_dominatesP numu; apply/null_content_dominatesP => E mE.
+by move/(numu _ mE) => E0; apply/eqP; rewrite mule_eq0 eqe E0/= eqxx orbT.
+Qed.
 
 Lemma dominates_cscaler d (T : measurableType d) (R : realType)
   (nu : {charge set T -> \bar R})
   (mu : set T -> \bar R)
   (c : R) : c != 0%R -> mu `<< nu -> mu `<< cscale c nu.
 Proof.
-move=> /negbTE c0 munu E mE /eqP; rewrite /cscale mule_eq0 eqe c0/=.
-by move=> /eqP/munu; exact.
+move=> /negbTE c0 /null_dominates_trans; apply => E nE A mA AE.
+by have /eqP := nE A mA AE; rewrite mule_eq0 eqe c0/= => /eqP.
 Qed.
 
 Section charge_opp.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
-Variables (nu : {charge set T -> \bar R}).
+Variable nu : {charge set T -> \bar R}.
 
 Definition copp := \- nu.
 
@@ -513,7 +517,9 @@ Lemma dominates_cadd d (T : measurableType d) (R : realType)
   nu0 `<< mu -> nu1 `<< mu ->
   cadd nu0 nu1 `<< mu.
 Proof.
-by move=> nu0mu nu1mu A mA A0; rewrite /cadd nu0mu// nu1mu// adde0.
+move=> /null_content_dominatesP nu0mu.
+move=> /null_content_dominatesP nu1mu A nA A0 mA0 A0A.
+by have muA0 := nA _ mA0 A0A; rewrite /cadd nu0mu// nu1mu// adde0.
 Qed.
 
 Section pushforward_charge.
@@ -558,18 +564,15 @@ HB.instance Definition _ := isCharge.Build _ _ _
 
 HB.end.
 
-Section dominates_pushforward.
-
 Lemma dominates_pushforward d d' (T : measurableType d) (T' : measurableType d')
   (R : realType) (mu : {measure set T -> \bar R})
   (nu : {charge set T -> \bar R}) (f : T -> T') (mf : measurable_fun setT f) :
   nu `<< mu -> pushforward nu f `<< pushforward mu f.
 Proof.
-by move=> numu A mA; apply: numu; rewrite -[X in measurable X]setTI; exact: mf.
+move=> /null_content_dominatesP numu; apply/null_content_dominatesP => A mA.
+by apply: numu; rewrite -[X in measurable X]setTI; exact: mf.
 Qed.
 
-End dominates_pushforward.
-
 Section positive_negative_set.
 Context d (T : semiRingOfSetsType d) (R : numDomainType).
 Implicit Types nu : set T -> \bar R.
@@ -1016,7 +1019,9 @@ Qed.
 Lemma jordan_pos_dominates (mu : {measure set T -> \bar R}) :
   nu `<< mu -> jordan_pos `<< mu.
 Proof.
-move=> nu_mu A mA muA0; have := nu_mu A mA muA0.
+move=> /null_content_dominatesP nu_mu.
+apply/null_content_dominatesP => A mA muA0.
+have := nu_mu A mA muA0.
 rewrite jordan_posE// cjordan_posE /crestr0 mem_set// /crestr/=.
 have mAP : measurable (A `&` P) by exact: measurableI.
 suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP) => ->.
@@ -1026,7 +1031,9 @@ Qed.
 Lemma jordan_neg_dominates (mu : {measure set T -> \bar R}) :
   nu `<< mu -> jordan_neg `<< mu.
 Proof.
-move=> nu_mu A mA muA0; have := nu_mu A mA muA0.
+move=> /null_content_dominatesP nu_mu.
+apply/null_content_dominatesP => A mA muA0.
+have := nu_mu A mA muA0.
 rewrite jordan_negE// cjordan_negE /crestr0 mem_set// /crestr/=.
 have mAN : measurable (A `&` N) by exact: measurableI.
 suff : mu (A `&` N) = 0 by move=> /(nu_mu _ mAN) ->; rewrite oppe0.
@@ -1075,35 +1082,64 @@ HB.instance Definition _ := isCharge.Build _ _ _ mu
 
 End charge_variation.
 
-Lemma abse_charge_variation d (T : measurableType d) (R : realType)
-    (nu : {charge set T -> \bar R}) P N (PN : hahn_decomposition nu P N) A :
-  measurable A -> `|nu A| <= charge_variation PN A.
-Proof.
-move=> mA.
-rewrite (jordan_decomp PN mA) /cadd/= cscaleN1 /charge_variation.
-by rewrite (le_trans (lee_abs_sub _ _))// !gee0_abs.
-Qed.
+Definition charge_dominates d (T : measurableType d) {R : realType}
+    (mu : {content set T -> \bar R}) (nu : {charge set T -> \bar R})
+    (P N : set T) (nuPN : hahn_decomposition nu P N) :=
+  content_dominates mu (charge_variation nuPN).
 
 Section charge_variation_continuous.
 Local Open Scope ereal_scope.
-Context {R : realType} d (T : measurableType d).
+Context d (T : measurableType d) {R : realType}.
 Variable nu : {charge set T -> \bar R}.
 Variables (P N : set T) (nuPN : hahn_decomposition nu P N).
 
-Lemma dominates_charge_variation (mu : {measure set T -> \bar R}) :
+Lemma abse_charge_variation A :
+  measurable A -> `|nu A| <= charge_variation nuPN A.
+Proof.
+move=> mA.
+rewrite (jordan_decomp nuPN mA) /cadd/= cscaleN1 /charge_variation.
+by rewrite (le_trans (lee_abs_sub _ _))// !gee0_abs.
+Qed.
+
+Lemma __deprecated__dominates_charge_variation (mu : {measure set T -> \bar R}) :
   nu `<< mu -> charge_variation nuPN `<< mu.
 Proof.
-move=> numu A mA muA0.
-rewrite /charge_variation/= (jordan_pos_dominates nuPN numu)// add0e.
-by rewrite (jordan_neg_dominates nuPN numu).
+move=> /[dup]numu /null_content_dominatesP nu0mu0.
+apply/null_content_dominatesP => A mA muA0; rewrite /charge_variation/=.
+have /null_content_dominatesP ->// := jordan_pos_dominates nuPN numu.
+rewrite add0e.
+by have /null_content_dominatesP -> := jordan_neg_dominates nuPN numu.
+Qed.
+
+Lemma null_charge_dominatesP (mu : {measure set T -> \bar R}) :
+  nu `<< mu <-> charge_dominates mu nuPN.
+Proof.
+split => [|numu].
+- move=> /[dup]numu /null_content_dominatesP nu0mu0.
+  move=> A mA muA0; rewrite /charge_variation/=.
+  have /null_content_dominatesP ->// := jordan_pos_dominates nuPN numu.
+  rewrite add0e.
+  by have /null_content_dominatesP -> := jordan_neg_dominates nuPN numu.
+- apply/null_content_dominatesP => A mA /numu => /(_ mA) nuA0.
+  apply/eqP; rewrite -abse_eq0 eq_le abse_ge0 andbT.
+  by rewrite -nuA0 abse_charge_variation.
+Qed.
+
+Lemma content_charge_dominatesP (mu : {measure set T -> \bar R}) :
+  content_dominates mu nu <-> charge_dominates mu nuPN.
+Proof.
+split.
+- by move/null_content_dominatesP/null_charge_dominatesP.
+- by move/null_charge_dominatesP/null_content_dominatesP.
 Qed.
 
 Lemma charge_variation_continuous (mu : {measure set T -> \bar R}) :
   nu `<< mu -> forall e : R, (0 < e)%R ->
   exists d : R, (0 < d)%R /\
   forall A, measurable A -> mu A < d%:E -> charge_variation nuPN A < e%:E.
 Proof.
-move=> numu; apply/not_forallP => -[e] /not_implyP[e0] /forallNP H.
+move=> /[dup]nudommu /null_content_dominatesP numu.
+apply/not_forallP => -[e] /not_implyP[e0] /forallNP H.
 have {H} : forall n, exists A,
     [/\ measurable A, mu A < (2 ^- n.+1)%:E & charge_variation nuPN A >= e%:E].
   move=> n; have /not_andP[|] := H (2 ^- n.+1); first by rewrite invr_gt0.
@@ -1129,7 +1165,7 @@ have : mu (lim_sup_set F) = 0.
   by move/cvg_lim : h => ->//; rewrite ltry.
 have : measurable (lim_sup_set F).
   by apply: bigcap_measurable => // k _; exact: bigcup_measurable.
-move=> /(dominates_charge_variation numu) /[apply].
+move/null_charge_dominatesP : nudommu => /[apply] /[apply].
 apply/eqP; rewrite neq_lt// ltNge measure_ge0//=.
 suff : charge_variation nuPN (lim_sup_set F) >= e%:E by exact: lt_le_trans.
 have echarge n : e%:E <= charge_variation nuPN (\bigcup_(j >= n) F j).
@@ -1147,12 +1183,17 @@ by rewrite -ge0_fin_numE// fin_num_measure//; exact: bigcup_measurable.
 Qed.
 
 End charge_variation_continuous.
+#[deprecated(since="mathcomp-analysis 1.15.0", note="use `charge_null_dominatesP` instead")]
+Notation dominates_charge_variation := __deprecated__dominates_charge_variation (only parsing).
 
-Definition induced d (T : measurableType d) {R : realType}
+Definition induced_charge d (T : measurableType d) {R : realType}
     (mu : {measure set T -> \bar R}) (f : T -> \bar R)
     (intf : mu.-integrable [set: T] f) :=
   fun A => (\int[mu]_(t in A) f t)%E.
 
+#[deprecated(since="mathcomp-analysis 1.15.0", note="renamed to `induced_charge`")]
+Notation induced := induced_charge (only parsing).
+
 Section induced_charge.
 Context d (T : measurableType d) {R : realType} (mu : {measure set T -> \bar R}).
 Local Open Scope ereal_scope.
@@ -1169,7 +1210,7 @@ Qed.
 Variable f : T -> \bar R.
 Hypothesis intf : mu.-integrable setT f.
 
-Local Notation nu := (induced intf).
+Local Notation nu := (induced_charge intf).
 
 Let nu0 : nu set0 = 0. Proof. by rewrite /nu integral_set0. Qed.
 
@@ -1211,10 +1252,10 @@ Hypothesis intf : mu.-integrable setT f.
 Let intnf : mu.-integrable [set: T] (abse \o f).
 Proof. exact: integrable_abse. Qed.
 
-Lemma dominates_induced : induced intnf `<< mu.
+Lemma dominates_induced : induced_charge intnf `<< mu.
 Proof.
-move=> /= A mA muA.
-rewrite /induced; apply/eqP; rewrite -abse_eq0 eq_le abse_ge0 andbT.
+apply/null_content_dominatesP => /= A mA muA.
+rewrite /induced_charge; apply/eqP; rewrite -abse_eq0 eq_le abse_ge0 andbT.
 rewrite (le_trans (le_abse_integral _ _ _))//=.
   by case/integrableP : intnf => /= + _; exact: measurable_funTS.
 rewrite le_eqVlt; apply/orP; left; apply/eqP.
@@ -1238,7 +1279,7 @@ Lemma integral_normr_continuous (e : R) : (0 < e)%R ->
   exists d : R, (0 < d)%R /\
   forall A, measurable A -> mu A < d%:E -> (\int[mu]_(x in A) `|f x| < e)%R.
 Proof.
-move=> e0; have [P [N pn]] := Hahn_decomposition (induced intnf).
+move=> e0; have [P [N pn]] := Hahn_decomposition (induced_charge intnf).
 have [r [r0 re]] := charge_variation_continuous pn (dominates_induced intf) e0.
 exists r; split => //= A mA Ad.
 have {re} := re _ mA Ad.
@@ -1721,6 +1762,7 @@ pose AP := A `&` P.
 have mAP : measurable AP by exact: measurableI.
 have muAP_gt0 : 0 < mu AP.
   rewrite lt0e measure_ge0// andbT.
+  move/null_content_dominatesP in nu_mu.
   apply/eqP/(contra_not (nu_mu _ mAP))/eqP; rewrite gt_eqF//.
   rewrite (@lt_le_trans _ _ (sigma AP))//.
     rewrite (@lt_le_trans _ _ (sigma A))//; last first.
@@ -1815,7 +1857,9 @@ pose mu_ j : {finite_measure set T -> \bar R} := mfrestr (mE j) (muEoo j).
 have nuEoo i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure.
 pose nu_ j : {finite_measure set T -> \bar R} := mfrestr (mE j) (nuEoo j).
 have nu_mu_ k : nu_ k `<< mu_ k.
-  by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI.
+  apply/null_content_dominatesP => S mS mu_kS0.
+  move/null_content_dominatesP : nu_mu; apply => //.
+  exact: measurableI.
 have [g_] := choice (fun j => radon_nikodym_finite (nu_mu_ j)).
 move=> /all_and3[g_ge0 ig_ int_gE].
 pose f_ j x := if x \in E j then g_ j x else 0.
@@ -2038,11 +2082,11 @@ have mf : measurable_fun E ('d nu '/d mu).
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
 apply: integral_ae_eq => //.
 - apply: (integrableS measurableT) => //; apply: f_integrable.
-  exact: measure_dominates_trans numu mula.
+  exact: null_dominates_trans numu mula.
 - apply: emeasurable_funM => //.
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
 - move=> A AE mA; rewrite change_of_variables//.
-  + by rewrite -!f_integral//; exact: measure_dominates_trans numu mula.
+  + by rewrite -!f_integral//; exact: null_dominates_trans numu mula.
   + exact: f_ge0.
   + exact: measurable_funS mf.
 Qed.
@@ -2204,7 +2248,7 @@ Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la ->
                 ('d nu '/d mu \* 'd (charge_of_finite_measure mu) '/d la).
 Proof.
 have [Pnu [Nnu nuPN]] := Hahn_decomposition nu.
-move=> numu mula; have nula := measure_dominates_trans numu mula.
+move=> numu mula; have nula := null_dominates_trans numu mula.
 apply: integral_ae_eq; [exact: measurableT| |exact: emeasurable_funM|].
 - exact: Radon_Nikodym_integrable.
 - move=> E _ mE.

theories/measure_theory/measurable_structure.v

@@ -114,12 +114,6 @@ From mathcomp Require Import ereal topology normedtype sequences.
 (*                                   and the tnth projections.                *)
 (* ```                                                                        *)
 (*                                                                            *)
-(* ## More measure-theoretic definitions                                      *)
-(*                                                                            *)
-(* ```                                                                        *)
-(*  m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1     *)
-(* ```                                                                        *)
-(*                                                                            *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -144,7 +138,6 @@ Reserved Notation "'<<sr' G '>>'" (format "'<<sr'  G '>>'").
 Reserved Notation "'<<M' G '>>'" (format "'<<M'  G '>>'").
 Reserved Notation "p .-prod" (format "p .-prod").
 Reserved Notation "p .-prod.-measurable" (format "p .-prod.-measurable").
-Reserved Notation "m1 `<< m2" (at level 51).
 
 Inductive measure_display := default_measure_display.
 Declare Scope measure_display_scope.
@@ -1659,18 +1652,3 @@ HB.instance Definition _ := @isMeasurable.Build (measure_tuple_display d)
   (n.-tuple T) (g_sigma_preimage coors) tuple_set0 tuple_setC tuple_bigcup.
 
 End measurable_tuple.
-
-Section absolute_continuity.
-Context d (T : semiRingOfSetsType d) (R : realType).
-Implicit Types m : set T -> \bar R.
-
-Definition measure_dominates m1 m2 :=
-  forall A, measurable A -> m2 A = 0 -> m1 A = 0.
-
-Local Notation "m1 `<< m2" := (measure_dominates m1 m2).
-
-Lemma measure_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3.
-Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed.
-
-End absolute_continuity.
-Notation "m1 `<< m2" := (measure_dominates m1 m2).