simplify lemmas and clarify presentation by introducing two definitions

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -10,13 +10,14 @@
   + lemma `negligible_null_set`
   + lemma `measure_null_setP`
   + lemma `null_setU`
-  + definition `null_set_dominates`
+  + definition `null_dominates`
   + lemma `null_dominates_trans`
-  + lemma `measure_null_dominatesP`
-  + lemma `measure_charge_dominatesP`
+  + lemma `content_null_dominatesP`
 
 - in `charge.v`:
+  + definition `charge_dominates`
   + lemma `charge_null_dominatesP`
+  + lemma `content_charge_dominatesP`
 
 ### Changed
 
@@ -47,6 +48,9 @@
   + 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
 
 ### Misc

theories/charge.v

@@ -65,6 +65,7 @@ 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            *)
+(*  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     *)
@@ -433,7 +434,7 @@ Lemma dominates_cscalel d (T : measurableType d) (R : realType)
   (nu : {charge set T -> \bar R})
   (c : R) : nu `<< mu -> cscale c nu `<< mu.
 Proof.
-move=> /measure_null_dominatesP numu; apply/measure_null_dominatesP => E mE.
+move=> /content_null_dominatesP numu; apply/content_null_dominatesP => E mE.
 by move/(numu _ mE) => E0; apply/eqP; rewrite mule_eq0 eqe E0/= eqxx orbT.
 Qed.
 
@@ -516,8 +517,8 @@ Lemma dominates_cadd d (T : measurableType d) (R : realType)
   nu0 `<< mu -> nu1 `<< mu ->
   cadd nu0 nu1 `<< mu.
 Proof.
-move=> /measure_null_dominatesP nu0mu.
-move=> /measure_null_dominatesP nu1mu A nA A0 mA0 A0A.
+move=> /content_null_dominatesP nu0mu.
+move=> /content_null_dominatesP nu1mu A nA A0 mA0 A0A.
 by have muA0 := nA _ mA0 A0A; rewrite /cadd nu0mu// nu1mu// adde0.
 Qed.
 
@@ -563,19 +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.
-move=> /measure_null_dominatesP numu; apply/measure_null_dominatesP => A mA.
+move=> /content_null_dominatesP numu; apply/content_null_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.
@@ -1022,8 +1019,8 @@ Qed.
 Lemma jordan_pos_dominates (mu : {measure set T -> \bar R}) :
   nu `<< mu -> jordan_pos `<< mu.
 Proof.
-move=> /measure_null_dominatesP nu_mu.
-apply/measure_null_dominatesP => A mA muA0.
+move=> /content_null_dominatesP nu_mu.
+apply/content_null_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.
@@ -1034,8 +1031,8 @@ Qed.
 Lemma jordan_neg_dominates (mu : {measure set T -> \bar R}) :
   nu `<< mu -> jordan_neg `<< mu.
 Proof.
-move=> /measure_null_dominatesP nu_mu.
-apply/measure_null_dominatesP => A mA muA0.
+move=> /content_null_dominatesP nu_mu.
+apply/content_null_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.
@@ -1085,9 +1082,14 @@ HB.instance Definition _ := isCharge.Build _ _ _ mu
 
 End charge_variation.
 
+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).
 
@@ -1099,34 +1101,44 @@ rewrite (jordan_decomp nuPN mA) /cadd/= cscaleN1 /charge_variation.
 by rewrite (le_trans (lee_abs_sub _ _))// !gee0_abs.
 Qed.
 
-Lemma dominates_charge_variation (mu : {measure set T -> \bar R}) :
+Lemma __deprecated__dominates_charge_variation (mu : {measure set T -> \bar R}) :
   nu `<< mu -> charge_variation nuPN `<< mu.
 Proof.
-move=> /[dup]numu /measure_null_dominatesP nu0mu0.
-apply/measure_null_dominatesP => A mA muA0; rewrite /charge_variation/=.
-have /measure_null_dominatesP ->// := jordan_pos_dominates nuPN numu.
+move=> /[dup]numu /content_null_dominatesP nu0mu0.
+apply/content_null_dominatesP => A mA muA0; rewrite /charge_variation/=.
+have /content_null_dominatesP ->// := jordan_pos_dominates nuPN numu.
 rewrite add0e.
-by have /measure_null_dominatesP -> := jordan_neg_dominates nuPN numu.
+by have /content_null_dominatesP -> := jordan_neg_dominates nuPN numu.
 Qed.
 
 Lemma charge_null_dominatesP (mu : {measure set T -> \bar R}) :
-  nu `<< mu <->
-  (forall A, measurable A -> mu A = 0 -> charge_variation nuPN A = 0).
+  nu `<< mu <-> charge_dominates mu nuPN.
 Proof.
 split => [|numu].
-- move/dominates_charge_variation/measure_null_dominatesP => + Am A A0.
-  exact.
-- apply/measure_null_dominatesP => A mA /numu => /(_ mA) nuA0.
+- move=> /[dup]numu /content_null_dominatesP nu0mu0.
+  move=> A mA muA0; rewrite /charge_variation/=.
+  have /content_null_dominatesP ->// := jordan_pos_dominates nuPN numu.
+  rewrite add0e.
+  by have /content_null_dominatesP -> := jordan_neg_dominates nuPN numu.
+- apply/content_null_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/content_null_dominatesP/charge_null_dominatesP.
+- by move/charge_null_dominatesP/content_null_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=> /[dup]nudommu /measure_null_dominatesP numu.
+move=> /[dup]nudommu /content_null_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].
@@ -1153,8 +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.
-have /measure_null_dominatesP/[apply]/[apply] :=
-  dominates_charge_variation nudommu.
+move/charge_null_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).
@@ -1171,27 +1182,9 @@ have /(_ _ _)/cvg_lim <-// := lim_sup_set_cvg (charge_variation nuPN) F.
 by rewrite -ge0_fin_numE// fin_num_measure//; exact: bigcup_measurable.
 Qed.
 
-Lemma measure_charge_dominatesP (mu : {measure set T -> \bar R}) :
-  (forall A, measurable A -> mu A = 0 -> nu A = 0)
-  <->
-  (forall A, measurable A -> mu A = 0 -> charge_variation nuPN A = 0).
-Proof.
-split.
-  move/measure_null_dominatesP => numu.
-  move=> A mA muA0.
-  apply/eqP; rewrite eq_le measure_ge0 andbT.
-  rewrite /charge_variation.
-  rewrite adde_le0//.
-    by have /measure_null_dominatesP->// := jordan_pos_dominates nuPN numu.
-  by have /measure_null_dominatesP->// := jordan_neg_dominates nuPN numu.
-move=> H A mA muA0.
-apply/eqP.
-rewrite -abse_eq0 eq_le abse_ge0 andbT.
-have <- := H _ mA muA0.
-exact: abse_charge_variation.
-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_charge d (T : measurableType d) {R : realType}
     (mu : {measure set T -> \bar R}) (f : T -> \bar R)
@@ -1261,7 +1254,7 @@ Proof. exact: integrable_abse. Qed.
 
 Lemma dominates_induced : induced_charge intnf `<< mu.
 Proof.
-apply/measure_null_dominatesP => /= A mA muA.
+apply/content_null_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.
@@ -1769,7 +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/measure_null_dominatesP in nu_mu.
+  move/content_null_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.
@@ -1864,8 +1857,8 @@ 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.
-  apply/measure_null_dominatesP => S mS mu_kS0.
-  move/measure_null_dominatesP : nu_mu; apply => //.
+  apply/content_null_dominatesP => S mS mu_kS0.
+  move/content_null_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].

theories/measure_theory/measure_negligible.v

@@ -32,6 +32,8 @@ From mathcomp Require Import measurable_structure measure_function.
 (*              mu-.null_set == (measure-theoretic) null sets                 *)
 (*                 m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or      *)
 (*                              m2 dominates m1                               *)
+(*   content_dominates mu nu == forall A, measurable A ->                     *)
+(*                              mu A = 0 -> nu A = 0                          *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -384,26 +386,30 @@ Section absolute_continuity.
 Context d (T : semiRingOfSetsType d) (R : realType).
 Implicit Types m : set T -> \bar R.
 
-Definition null_set_dominates m1 m2 := m2.-null_set `<=` m1.-null_set.
+Definition null_dominates m2 m1 := m2.-null_set `<=` m1.-null_set.
 
 End absolute_continuity.
-Notation "m1 `<< m2" := (null_set_dominates m1 m2).
+Notation "m1 `<< m2" := (null_dominates m2 m1).
 
 Section null_dominates_lemmas.
 Context d (T : semiRingOfSetsType d) (R : realType).
 Implicit Types m : set T -> \bar R.
 
 Lemma null_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3.
-Proof. by move=> m12 m23 A /m23/m12. Qed.
+Proof. by move=> m12 m23 A /m23 /m12. Qed.
 
 End null_dominates_lemmas.
 
+Definition content_dominates {d} {T : measurableType d} {R : realType}
+    (mu : {content set T -> \bar R}) (nu : set T -> \bar R) :=
+  forall A, measurable A -> mu A = 0 -> nu A = 0.
+
 Section content_null_dominates_lemmas.
-Context d (T : measurableType d) (R : realType) (U : Type).
-Implicit Types (mu : {content set T -> \bar R}) (f g : T -> U).
+Context d (T : measurableType d) (R : realType).
+Implicit Types (mu : {content set T -> \bar R}).
 
-Lemma measure_null_dominatesP (nu : set T -> \bar R) mu :
-  nu `<< mu <-> (forall A, measurable A -> mu A = 0 -> nu A = 0).
+Lemma content_null_dominatesP (nu : set T -> \bar R) mu :
+  nu `<< mu <-> content_dominates mu nu.
 Proof.
 split.
 - by move=> dom A mA muA0; apply: (dom A) => //; exact/measure_null_setP.
@@ -419,7 +425,7 @@ Implicit Types (nu mu : {measure set T -> \bar R}) (f g : T -> U).
 Lemma null_dominates_ae_eq nu mu f g E : measurable E ->
   nu `<< mu -> ae_eq mu E f g -> ae_eq nu E f g.
 Proof.
-move=> mE /measure_null_dominatesP m21 [A [*]]; exists A; split => //.
+move=> mE /content_null_dominatesP m21 [A [*]]; exists A; split => //.
 exact: m21.
 Qed.
 

theories/probability.v

@@ -1575,7 +1575,7 @@ HB.instance Definition _ := @Measure_isProbability.Build _ _ R
 
 Lemma dominates_uniform_prob : uniform_prob ab `<< mu.
 Proof.
-apply/measure_null_dominatesP.
+apply/content_null_dominatesP.
 move=> A mA muA0; rewrite /uniform_prob integral_uniform_pdf.
 apply/eqP; rewrite eq_le; apply/andP; split; last first.
   apply: integral_ge0 => x [Ax /=]; rewrite in_itv /= => xab.
@@ -1878,7 +1878,7 @@ HB.instance Definition _ :=
 
 Lemma normal_prob_dominates : normal_prob `<< mu.
 Proof.
-apply/measure_null_dominatesP=> A mA muA0; rewrite /normal_prob /normal_pdf.
+apply/content_null_dominatesP=> A mA muA0; rewrite /normal_prob /normal_pdf.
 have [s0|s0] := eqVneq sigma 0.
   apply: null_set_integral => //=; apply: (integrableS measurableT) => //=.
   exact: integrable_indic_itv.
@@ -2654,7 +2654,7 @@ Qed.
 
 Lemma beta_prob_dom : beta_prob `<< mu.
 Proof.
-apply/measure_null_dominatesP => A mA muA0; rewrite /beta_prob /mscale/=.
+apply/content_null_dominatesP => A mA muA0; rewrite /beta_prob /mscale/=.
 apply/eqP; rewrite mule_eq0 eqe invr_eq0 gt_eqF/= ?beta_fun_gt0//; apply/eqP.
 rewrite /beta_num integral_XMonemX_restrict.
 apply/eqP; rewrite eq_le; apply/andP; split; last first.