Change the definition of flow_cc

The two definitions are proved equivalent, the older one was more
"computational" but this one is closer from the mathematical
definition.

cumulative_curves.v

@@ -62,13 +62,114 @@ apply: (@le_trans _ _ (f 0%:nng)) => //.
 by apply: ereal_sup_ub; exists 0%:nng.
 Qed.
 
+Lemma left_cont_closure_le_Fup (f : Fup) : (left_cont_closure f <= f :> F)%O.
+Proof.
+rewrite -[X in (_ <= X)%O]non_decr_closure_Fup.
+apply/leFP => t; rewrite le_maxl non_decr_closure_Fup; apply/andP; split=> //.
+apply: ub_ereal_sup => _ [y /= Hy <-]; exact/ndFP'.
+Qed.
+
+Definition left_continuous_at (f : F) x :=
+  forall eps : {posnum R}, exists eta : {posnum R},
+  forall y, x%:nngnum - eta%:num <= y%:nngnum <= x%:nngnum ->
+    (f x - eps%:num%:E < f y <= f x)%dE.
+
+Definition left_continuous f := forall x, left_continuous_at f x.
+
+Lemma left_cont_closureP (f : Fup) :
+  reflect
+    (f 0%:nng = 0%:E /\ left_continuous f)
+    ((f <= left_cont_closure f :> F)%O && `[< forall x, f x \is a fin_num >]).
+Proof.
+set b := _ && _.
+case Eb: b; [apply: ReflectT|apply: ReflectF].
+{ move: Eb => /andP[flec /asboolP Ff] {b}.
+  have f0 : f 0%:nng = 0%:E.
+  { apply/le_anti; rewrite Fplus_ge0 andbT.
+    move: flec => /leFP/(_ 0%:nng) Eb; apply: (le_trans Eb).
+    by rewrite left_cont_closure0. }
+  split=> // x eps.
+  have [| Hx] := leP x%:nngnum 0.
+  { rewrite le_eqVlt nngnum_lt0 orbF => /eqP /val_inj -> /=.
+    exists 1%:pos => y /andP[_].
+    rewrite le_eqVlt nngnum_lt0 orbF => /eqP /val_inj ->.
+    rewrite f0 lexx andbT.
+    by rewrite ltEereal /= add0r oppr_lt0. }
+  have: left_cont_closure f x = f x.
+  { by apply/le_anti/andP; split; apply/leFP;
+      [exact/left_cont_closure_le_Fup|]. }
+  rewrite left_cont_closure_ereal_sup //.
+  set S := [set f u | u in _].
+  move=> H.
+  have /(ub_ereal_sup_adherent eps) : ereal_sup S \is a fin_num by rewrite H.
+  move=> -[_ [[xl /= Hxl <-]] Hxl'].
+  have Hxmxl : 0 < x%:nngnum - xl%:nngnum; [by rewrite subr_gt0|].
+  exists (PosNum Hxmxl) => y; rewrite /= subKr => /andP[Hy Hy'].
+  apply/andP; split; [|exact/ndFP].
+  apply: (@lt_le_trans _ _ (f xl)); [|exact/ndFP].
+  move: Hxl'; apply: le_lt_trans.
+  by rewrite H. }
+rewrite not_andP.
+move: Eb => /negbT; rewrite negb_and.
+case EF: asbool.
+2:{ move: EF => /existsp_asboolPn[x nFfx] _; right=> /(_ x 1%:pos)[eta /(_ x)].
+  rewrite lexx andbT ler_subl_addl ler_addr posnum_ge0 => /(_ erefl).
+  by case: (f x) nFfx. }
+move: EF => /asboolP EF; rewrite orbF => /negP Nflec.
+have [x] : exists x, (left_cont_closure f x < f x)%E.
+{ rewrite not_existsP => H; apply/Nflec/leFP => x.
+  rewrite leNgt; exact/negP. }
+have [| Hx] := leP x%:nngnum 0.
+{ rewrite le_eqVlt nngnum_lt0 orbF => /eqP /val_inj -> /=.
+  rewrite left_cont_closure0 => f0; left=> f0'.
+  by move: f0; rewrite f0' lt_irreflexive. }
+rewrite left_cont_closure_ereal_sup//.
+set S := [set f u | u in _] => H; right.
+rewrite -existsNP; exists x.
+pose fxmsS := fine (f x - ereal_sup S).
+have FsS : ereal_sup S \is a fin_num.
+{ case Es: ereal_sup => //.
+  { by exfalso; move: H; apply/negP; rewrite -leNgt Es lee_pinfty. }
+  exfalso; move: Es; rewrite ereal_sup_ninfty => /(_ (f 0%:nng)) /= H'.
+  by move: (EF 0%:nng); rewrite H'//; exists 0%:nng. }
+have PfxmsS : 0 < fxmsS.
+{ rewrite /fxmsS; case: (f x) (EF x) H => // fx _.
+  by case: ereal_sup FsS => s //= _; rewrite lte_fin subr_gt0. }
+rewrite -existsNP; exists (PosNum PfxmsS).
+rewrite -forallNP => eta.
+rewrite -existsNP; exists (insubd 0%:nng (x%:nngnum - eta%:num)).
+rewrite not_implyP; split.
+{ have [Hxmeta | Hxmeta] := leP 0 (x%:nngnum - eta%:num).
+  { by rewrite insubdK// lexx /= ler_subl_addr ler_addl. }
+  rewrite /insubd insubF /=; [|by apply/negP/negP; rewrite -ltNge].
+  by rewrite ltW//=. }
+apply/negP; rewrite negb_and; apply/orP; left; rewrite -leNgt /=.
+have -> : (f x + (- fxmsS)%:E = ereal_sup S)%dE.
+{ rewrite /fxmsS; case: (f x) (EF x) => // fx _.
+  by case: ereal_sup FsS => s //; rewrite -dsubEFin /= subKr. }
+apply: ereal_sup_ub; eexists=> [|//] /=.
+have [Hxmeta | Hxmeta] := leP 0 (x%:nngnum - eta%:num).
+{ by rewrite ltEsub insubdK//= ltr_subl_addr ltr_addl. }
+by rewrite /insubd insubF /=; [|apply/negP/negP; rewrite -ltNge].
+Qed.
+
 Record flow_cc := {
   flow_cc_val :> Fup;
-  _ : (flow_cc_val <= left_cont_closure flow_cc_val :> F)%O
-      && `[< forall t, flow_cc_val t \is a fin_num >]
+  _ : `[< flow_cc_val 0%:nng = 0%:E
+        /\ left_continuous flow_cc_val
+        /\ forall x, flow_cc_val x \is a fin_num >]
 }.
 Arguments Build_flow_cc : clear implicits.
 
+Program Definition Build_flow_cc' (f : Fup)
+        (Hf : (f <= left_cont_closure f :> F)%O
+              && `[< forall t, f t \is a fin_num >]) := Build_flow_cc f _.
+Next Obligation.
+apply/asboolP; rewrite andA; split; [exact/left_cont_closureP|].
+by move: Hf => /andP[_ /asboolP].
+Qed.
+Arguments Build_flow_cc' : clear implicits.
+
 Canonical flow_cc_subtype := [subType for flow_cc_val].
 Definition flow_cc_eqMixin := [eqMixin of flow_cc by <:].
 Canonical flow_cc_eqType := EqType flow_cc flow_cc_eqMixin.
@@ -77,24 +178,24 @@ Canonical flow_cc_choiceType := ChoiceType flow_cc flow_cc_choiceMixin.
 
 Lemma flow_cc_le_left_cont_closure (f : flow_cc) :
   (f <= left_cont_closure f :> F)%O.
-Proof. by case: f => f /= /andP[]. Qed.
+Proof.
+case: f => f /=.
+by rewrite andA asbool_and => /andP[/asboolP/left_cont_closureP/andP[]].
+Qed.
 
 Lemma left_cont_closure_flow_cc (f : flow_cc) : left_cont_closure f = f.
 Proof.
-apply/le_anti; rewrite flow_cc_le_left_cont_closure andbT.
-rewrite -[X in (_ <= X)%O]non_decr_closure_Fup.
-apply/leFP => t; rewrite le_maxl non_decr_closure_Fup; apply/andP; split=> //.
-apply: ub_ereal_sup => _ [y /= Hy <-]; exact/ndFP'.
+by apply/le_anti; rewrite left_cont_closure_le_Fup flow_cc_le_left_cont_closure.
 Qed.
 
 Lemma flow_cc_fin (f : flow_cc) t : f t \is a fin_num.
-Proof. by case: f => f /= /andP[_ /asboolP]. Qed.
+Proof. by case: f => f /= /asboolP[_ [_]]; exact. Qed.
 
 Lemma fin_flow_cc_prop (f : flow_cc) :
   { ff : {nonneg R} -> {nonneg R} | forall t, f t = (ff t)%:nngnum%:E }.
 Proof.
 apply: constructive_indefinite_description.
-case: f => f /= /andP[_ /asboolP finf].
+case: f => f /= /asboolP[_ [_ finf]].
 have nngfine : forall t, 0 <= fine (f t).
 { by move=> t; case: (f t) (Fplus_ge0 f t). }
 exists (fun t => Nonneg.NngNum _ (nngfine t)) => t /=.
@@ -110,38 +211,13 @@ Lemma fin_flow_ccE (f : flow_cc) : forall t : {nonneg R}, (f%:fcc t)%:nngnum%:E
 Proof. by move=> t; rewrite /fin_flow_cc; case: (fin_flow_cc_prop f). Qed.
 
 Lemma flow_cc0 (f : flow_cc) : f 0%:nng = 0%:E.
-Proof. by rewrite -left_cont_closure_flow_cc left_cont_closure0. Qed.
+Proof. by case: f => f /= /asboolP[]. Qed.
 
-Lemma flow_cc_left_cont (f : flow_cc) x :
-  forall eps : {posnum R}, exists eta : {posnum R}, forall y,
-    x%:nngnum - eta%:num <= y%:nngnum <= x%:nngnum ->
-    (f x - eps%:num%:E < f y <= f x)%dE.
-Proof.
-move=> eps.
-case: (leP x%:nngnum 0) => [| Hx].
-{ rewrite le_eqVlt nngnum_lt0 orbF => /eqP /val_inj -> /=.
-  exists 1%:pos => y /andP[_].
-  rewrite le_eqVlt nngnum_lt0 orbF => /eqP /val_inj ->.
-  rewrite flow_cc0 lexx andbT.
-  by rewrite ltEereal /= add0r oppr_lt0. }
-move: (erefl (f x)); rewrite -[in LHS]left_cont_closure_flow_cc.
-rewrite left_cont_closure_ereal_sup //.
-set S := [set f u | u in _].
-rewrite -fin_flow_ccE => H.
-have /(ub_ereal_sup_adherent eps) : ereal_sup S \is a fin_num by rewrite H.
-move=> -[_ [[xl /= Hxl <-]] Hxl'].
-have Hxmxl : 0 < x%:nngnum - xl%:nngnum; [by rewrite subr_gt0|].
-exists (PosNum Hxmxl) => y; rewrite /= subKr => /andP[Hy Hy'].
-apply/andP; split.
-2:{ by rewrite fin_flow_ccE; apply/ndFP => //; rewrite non_decr_closure_Fup. }
-apply: (@lt_le_trans _ _ (f xl)).
-2:{ by apply/ndFP => //; rewrite non_decr_closure_Fup. }
-move: Hxl'; apply: le_lt_trans.
-by rewrite -daddEFin H -addEFin.
-Qed.
+Lemma flow_cc_left_cont (f : flow_cc) : left_continuous f.
+Proof. by case: f => f /= /asboolP[_ []]. Qed.
 
 Program Definition flow_cc_plus (f g : flow_cc) : flow_cc :=
-  Build_flow_cc (Fup_plus f g) _.
+  Build_flow_cc' (Fup_plus f g) _.
 Next Obligation.
 apply/andP; split.
 { apply/leFP => t.
@@ -199,7 +275,7 @@ apply/andP; split.
 by apply/asboolP => t; rewrite /F_plus -!fin_flow_ccE -daddEFin.
 Qed.
 
-Program Definition flow_cc_0 := Build_flow_cc Fup_0 _.
+Program Definition flow_cc_0 := Build_flow_cc' Fup_0 _.
 Next Obligation.
 apply/andP; split.
 { apply/leFP => t; exact: left_cont_closure_ge0. }