Make cdf an instance of Cumulative (fix #1572)

CHANGELOG_UNRELEASED.md

@@ -24,6 +24,9 @@
   + definition `irrational`
   + lemmas `irrationalE`, `rationalP` 
 
+- in `constructive_ereal.v`:
+  + lemma `gte_lte_fin_num`
+
 - in `topology_structure.v`:
   + lemmas `denseI`, `dense0`
 
@@ -40,6 +43,19 @@
 - moved from `pi_irrational.v` to `reals.v` and changed
   + definition `rational`
 
+- in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):
+  + lemma `right_continuousW`
+  + record `isCumulative`
+  + definition `Cumulative`
+
+- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
+  + lemma `nondecreasing_right_continuousP` 
+  + definition `CumulativeBounded`
+
+- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:
+  + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
+  + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
+
 ### Renamed
 
 - in `lebesgue_stieltjes_measure.v`:

reals/constructive_ereal.v

@@ -1688,6 +1688,12 @@ Proof. by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed.
 Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x).
 Proof. by move/ltW; exact: le0_fin_numE. Qed.
 
+Lemma gte_lte_fin_num x a b : a < x < b -> x \is a fin_num.
+Proof.
+rewrite fin_numE -ltey -ltNye.
+by move=> /andP[/(le_lt_trans (leNye _))->/=] /lt_le_trans -> //; exact: leey.
+Qed.
+
 Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x).
 Proof.
 split=> [-> // A A0|Ax]; first by rewrite leey.

theories/lebesgue_stieltjes_measure.v

@@ -60,23 +60,24 @@ Reserved Notation "R .-ocitv.-measurable"
 Notation right_continuous f :=
   (forall x, f%function @ at_right x --> f%function x).
 
-Lemma right_continuousW (R : numFieldType) (f : R -> R) :
-  continuous f -> right_continuous f.
+Lemma right_continuousW (R : numFieldType) {d} (U : orderNbhsType d)
+  (f : R -> U) : continuous f -> right_continuous f.
 Proof. by move=> cf x; apply: cvg_within_filter; exact/cf. Qed.
 
-HB.mixin Record isCumulative (R : numFieldType) (f : R -> R) := {
-  cumulative_is_nondecreasing : {homo f : x y / x <= y} ;
+HB.mixin Record isCumulative (R : numFieldType) {d} (U : orderNbhsType d)
+  (f : R -> U) := {
+  cumulative_is_nondecreasing : nondecreasing f ;
   cumulative_is_right_continuous : right_continuous f }.
 
 #[short(type=cumulative)]
-HB.structure Definition Cumulative (R : numFieldType) :=
-  { f of isCumulative R f }.
+HB.structure Definition Cumulative
+  (R : numFieldType) {d} (U : orderNbhsType d) := { f of isCumulative R d U f }.
 
-Arguments cumulative_is_nondecreasing {R} _.
-Arguments cumulative_is_right_continuous {R} _.
+Arguments cumulative_is_nondecreasing {R d U} _.
+Arguments cumulative_is_right_continuous {R d U} _.
 
-Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R)
-    (f : cumulative R) :
+Lemma nondecreasing_right_continuousP (R : realFieldType) (a : R) (e : R)
+    (f : cumulative R R) :
   e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e.
 Proof.
 move=> e0; move: (cumulative_is_right_continuous f).
@@ -92,15 +93,15 @@ by rewrite opprB ltrBlDl => fa; exact: ltW.
 Qed.
 
 Section id_is_cumulative.
-Variable R : realType.
+Variable R : realFieldType.
 
 Let id_nd : {homo @idfun R : x y / x <= y}.
 Proof. by []. Qed.
 
 Let id_rc : right_continuous (@idfun R).
 Proof. by apply/right_continuousW => x; exact: cvg_id. Qed.
 
-HB.instance Definition _ := isCumulative.Build R idfun id_nd id_rc.
+HB.instance Definition _ := isCumulative.Build R _ R idfun id_nd id_rc.
 End id_is_cumulative.
 (* /TODO: move? *)
 
@@ -373,22 +374,22 @@ apply/andP; split=> //; apply: contraTneq xbj => ->.
 by rewrite in_itv/= le_gtF// (itvP xabi).
 Qed.
 
-Lemma wlength_ge0 (f : cumulative R) (I : set (ocitv_type R)) :
+Lemma wlength_ge0 (f : cumulative R R) (I : set (ocitv_type R)) :
   (0 <= wlength f I)%E.
 Proof.
 by rewrite -(wlength0 f) le_wlength//; exact: cumulative_is_nondecreasing.
 Qed.
 
 #[local] Hint Extern 0 (0%:E <= wlength _ _) => solve[apply: wlength_ge0] : core.
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   isContent.Build _ _ R (wlength f)
     (wlength_ge0 f)
     (wlength_semi_additive f).
 
 Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core.
 
-Lemma cumulative_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0
+Lemma cumulative_content_sub_fsum (f : cumulative R R) (D : {fset nat}) a0 b0
     (a b : nat -> R) : (forall i, i \in D -> a i <= b i) ->
     `]a0, b0] `<=` \big[setU/set0]_(i <- D) `]a i, b i]%classic ->
   f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)).
@@ -406,7 +407,7 @@ rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in leRHS]big_seq.
 by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab.
 Qed.
 
-Lemma wlength_sigma_subadditive (f : cumulative R) :
+Lemma wlength_sigma_subadditive (f : cumulative R R) :
   measurable_subset_sigma_subadditive (wlength f).
 Proof.
 move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-].
@@ -475,7 +476,7 @@ rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX.
 by rewrite AE leeD2l// lee_fin lerBlDl natrX De.
 Qed.
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   Content_SigmaSubAdditive_isMeasure.Build _ _ _
     (wlength f) (wlength_sigma_subadditive f).
 
@@ -490,17 +491,18 @@ move=> k; split => //; rewrite wlength_itv /= -EFinB.
 by case: ifP; rewrite ltey.
 Qed.
 
-Definition lebesgue_stieltjes_measure (f : cumulative R) :=
+Definition lebesgue_stieltjes_measure (f : cumulative R R) :=
   measure_extension (wlength f).
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   Measure.on (lebesgue_stieltjes_measure f).
 
-Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
+Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R R) :
   sigma_finite setT (lebesgue_stieltjes_measure f).
 Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed.
 
-HB.instance Definition _ (f : cumulative R) := @Measure_isSigmaFinite.Build _ _ _
-  (lebesgue_stieltjes_measure f) (sigmaT_finite_lebesgue_stieltjes_measure f).
+HB.instance Definition _ (f : cumulative R R) :=
+  @Measure_isSigmaFinite.Build _ _ _ (lebesgue_stieltjes_measure f)
+    (sigmaT_finite_lebesgue_stieltjes_measure f).
 
 End wlength_extension.
 Arguments lebesgue_stieltjes_measure {R}.
@@ -512,7 +514,7 @@ Section lebesgue_stieltjes_measure.
 Variable R : realType.
 Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R).
 
-Lemma lebesgue_stieltjes_measure_unique (f : cumulative R)
+Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R)
     (mu : {measure set gitvs -> \bar R}) :
     (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) ->
   forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X.
@@ -527,17 +529,17 @@ End lebesgue_stieltjes_measure.
 Section completed_lebesgue_stieltjes_measure.
 Context {R : realType}.
 
-Definition completed_lebesgue_stieltjes_measure (f : cumulative R) :=
+Definition completed_lebesgue_stieltjes_measure (f : cumulative R R) :=
   @completed_measure_extension _ _ _ (wlength f).
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   Measure.on (@completed_lebesgue_stieltjes_measure f).
 
-Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R) :
+Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R R) :
   sigma_finite setT (@completed_lebesgue_stieltjes_measure f).
 Proof. exact/completed_measure_extension_sigma_finite/wlength_sigma_finite. Qed.
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   @Measure_isSigmaFinite.Build _ _ _
     (@completed_lebesgue_stieltjes_measure f)
     (sigmaT_finite_completed_lebesgue_stieltjes_measure f).
@@ -605,7 +607,7 @@ HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) :=
   cumulativey : f @ +oo --> r }.
 
 #[short(type=cumulativeBounded)]
-HB.structure Definition CumulativeBounded (R : numFieldType) (l r : R) :=
+HB.structure Definition CumulativeBounded (R : realFieldType) (l r : R) :=
   { f of isCumulativeBounded R l r f & Cumulative R f}.
 
 Arguments cumulativeNy {R l r} s.

theories/normedtype_theory/ereal_normedtype.v

@@ -482,3 +482,37 @@ split=> [|[Py]] [x [xr Px]]; last by exists x; split=> // -[y||]//; apply: Px.
 by split; [|exists x; split=> // y xy]; apply: Px.
 Qed.
 End nbhs_ereal.
+
+Section ereal_OrderNbhs.
+Variable R : realFieldType.
+
+Let ereal_order_nbhsE (x : \bar R) :
+  nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]).
+Proof.
+apply/seteqP; split=> A.
+  rewrite /nbhs/= /ereal_nbhs/=; move: x => [r||].
+  - move=> [e/= e0 reA].
+    exists `](r - e)%:E, (r + e)%:E[ => [|y/=].
+      by rewrite in_itv/= ?lte_fin// ltrBlDr andbb ltrDl; split => //; right.
+    move: y => [y| |]//=; rewrite !in_itv/=; last by rewrite !ltNge/= leey.
+    by rewrite !lte_fin -ltr_distlC => /reA.
+  - case=> M [Mreal MA].
+    exists `]M%:E, +oo[ => [|y/=]; rewrite in_itv/= andbT; last exact: MA.
+    by rewrite ltry; split => //; left.
+  - case=> M [Mreal MA].
+    exists `]-oo, M%:E[ => [|y/=]; rewrite in_itv/=; last exact: MA.
+    by rewrite ltNyr; split => //; left.
+move=> [[ [[]/= r|[]] [[]/= s|[]] ]] [] []// _.
+  - move=> /[dup]/gte_lte_fin_num/fineK <-; rewrite in_itv/=.
+    move=> /andP[rx sx] rsA; apply: (nbhs_interval rx sx) => z rz zs.
+    by apply: rsA =>/=; rewrite in_itv/= rz.
+  - rewrite nbhsE/= => rx rA; exists `]r, +oo[%classic => //.
+    by split; [rewrite set_itvE; exact: open_ereal_gt_ereal | ].
+  - rewrite nbhsE/= => xs ?; exists `]-oo, s[%classic => //.
+    by split; [rewrite set_itvE; exact: open_ereal_lt_ereal | ].
+  - by rewrite set_itvE/= subTset => _ ->; exact: filter_nbhsT.
+Qed.
+
+HB.instance Definition _ := Order_isNbhs.Build _ (\bar R) ereal_order_nbhsE.
+
+End ereal_OrderNbhs.

theories/probability.v

@@ -245,6 +245,9 @@ have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a.
 by rewrite -(cvg_unique _ cdf_ns cdf_na).
 Unshelve. all: by end_near. Qed.
 
+HB.instance Definition _ := isCumulative.Build R _ (\bar R) (cdf X)
+  cdf_nondecreasing cdf_right_continuous.
+
 End cumulative_distribution_function.
 
 Section cdf_of_lebesgue_stieltjes_mesure.

theories/topology_theory/num_topology.v

@@ -131,12 +131,16 @@ HB.instance Definition _ (R : realFieldType) := PseudoPointedMetric.copy R R^o.
 HB.instance Definition _ (R : numClosedFieldType) :=
   PseudoPointedMetric.copy R R^o.
 
+#[export, non_forgetful_inheritance]
+HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
+
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ (R : realFieldType) :=
   Order_isNbhs.Build _ R (@real_order_nbhsE R).
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
+HB.instance Definition _ (R : realType) :=
+  Order_isNbhs.Build _ R (@real_order_nbhsE R).
 
 Module Exports. HB.reexport. End Exports.