nondecreasing functions have a countable number of discontinuities

Co-authored-by: IshiguroYoshihiro <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -30,6 +30,16 @@
 - in `classical_sets.v`:
   + lemmas `xsectionE`, `ysectionE`
 
+- in `mathcomp_extra.v`:
+  + lemma `ltr_sum`
+
+- in `classical_sets.v`:
+  + lemma `itv_sub_in2`
+
+- in `realfun.v`:
+  + definition `discontinuity`
+  + lemmas `nondecreasing_fun_sum_le`, `discontinuty_countable`
+
 ### Changed
 
 - in `lebesgue_integrale.v`
@@ -68,6 +78,9 @@
   + lemmas `nneseries_ge0`, `is_cvg_nneseries_cond`, `is_cvg_npeseries_cond`,
     `is_cvg_nneseries`, `is_cvg_npeseries`, `nneseries_ge0`, `npeseries_le0`,
     `lee_nneseries`
+
+- in `cardinality.v`:
+  + lemma `infinite_set_fset`
 
 ### Deprecated
 

classical/cardinality.v

@@ -1002,23 +1002,29 @@ move=> /finite_setP[m Am]; rewrite (card_fset_set Am).
 by rewrite (card_le_eqr Am) card_le_II.
 Qed.
 
-Lemma infinite_set_fset {T : choiceType} (A : set T) (n : nat) :
+Lemma infinite_set_fset {T : choiceType} (A : set T) n :
   infinite_set A ->
-    exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N.
+    exists B : {fset T}, [/\ [set` B] `<=` A, B != fset0 & (#|` B| >= n)%N].
 Proof.
 elim/choicePpointed: T => T in A *; first by rewrite emptyE.
-move=> /infiniteP/ppcard_leP[f]; exists (fset_set [set f i | i in `I_n]).
-  rewrite fset_setK//; last exact: finite_image.
-  by apply: subset_trans (fun_image_sub f); apply: image_subset.
-rewrite fset_set_image// card_imfset//= fset_set_II/=.
-by rewrite card_imfset//= ?size_enum_ord//; apply: val_inj.
+move=> /infiniteP/ppcard_leP[f]; exists (fset_set [set f i | i in `I_n.+1]).
+rewrite fset_setK//; last exact: finite_image.
+split.
+- by apply: subset_trans (fun_image_sub f); exact: image_subset.
+- apply/eqP => /fsetP /(_ (f ord0)) => /(_ n).
+  rewrite !inE -falseE => <-.
+  rewrite in_fset_set//; last exact: finite_image.
+  by rewrite inE/=; exists 0.
+- rewrite fset_set_image// card_imfset//= fset_set_II/=.
+  by rewrite card_imfset//= ?size_enum_ord//; exact: val_inj.
 Qed.
 
 Lemma infinite_set_fsetP {T : choiceType} (A : set T) :
   infinite_set A <->
    forall n, exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N.
 Proof.
-split; first by move=> ? ?; apply: infinite_set_fset.
+split.
+  by move=> + n => /infinite_set_fset => /(_ n)[B [? ? ?]]; exists B.
 elim/choicePpointed: T => T in A *.
   move=> /(_ 1%N)[B _]; rewrite cardfs_gt0 => /fset0Pn[x xB].
   by have: [set` B] x by []; rewrite emptyE.

classical/classical_sets.v

@@ -465,6 +465,11 @@ Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed.
 
 #[global] Hint Resolve nat_nonempty : core.
 
+Lemma itv_sub_in2 d (T : porderType d) (P : T -> T -> Prop) (i j : interval T) :
+  [set` j] `<=` [set` i] ->
+  {in i &, forall x y, P x y} -> {in j &, forall x y, P x y}.
+Proof. by move=> ji + x y xj yj; apply; exact: ji. Qed.
+
 Lemma preimage_itv T d (rT : porderType d) (f : T -> rT) (i : interval rT) (x : T) :
   ((f @^-1` [set` i]) x) = (f x \in i).
 Proof. by rewrite inE. Qed.

classical/mathcomp_extra.v

@@ -588,3 +588,13 @@ rewrite mulr_ile1 ?andbT//.
   by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[].
 by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT.
 Qed.
+
+(* TODO: move to ssrnum *)
+Lemma ltr_sum {R : numDomainType} I (r : seq I) (F G : I -> R) :
+  (0 < size r)%N -> (forall i, F i < G i) ->
+  \sum_(i <- r) F i < \sum_(i <- r) G i.
+Proof.
+elim: r => // h [|a t] ih ? FG.
+  by rewrite !big_cons !big_nil !addr0.
+by rewrite [ltLHS]big_cons [ltRHS]big_cons ltrD// ih.
+Qed.

theories/lebesgue_measure.v

@@ -2824,7 +2824,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
 have finite_set_F i : finite_set (F i).
   apply: contrapT.
   pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
-  move/(infinite_set_fset M) => [/= C] CsubFi McardC.
+  move/(infinite_set_fset M) => [/= C [CsubFi _ McardC]].
   have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
             mu (\bigcup_(j in [set` C]) closure (B j)).
     rewrite (measure_bigcup _ [set` C])//; last 2 first.
@@ -3185,7 +3185,7 @@ have {}Hc : mu (\bigcup_(k in G) closure (B k) `\`
   by rewrite lteBlDr-?lteBlDl//; exact: muGSfin.
 have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num).
   pose M := `|ceil (fine (mu O) / r%:num)|.+1.
-  apply: contrapT => /infinite_set_fset /= /(_ M)[G0 G0G'r] MG0.
+  apply: contrapT => /infinite_set_fset /= /(_ M)[G0 [G0G'r _ MG0]].
   have : mu O < mu (\bigcup_(k in bigB G r%:num) closure (B k)).
     apply: (@lt_le_trans _ _ (mu (\bigcup_(k in [set` G0]) closure (B k)))).
       rewrite bigcup_fset measure_fbigsetU//=; last 2 first.

theories/measure.v

@@ -2286,7 +2286,7 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A ->
   \esum_(i in A) \d_ i A = +oo :> \bar R.
 Proof.
 move=> infA; apply/eqyP => r r0.
-have [B BA Br] := infinite_set_fset `|ceil r| infA.
+have [B [BA B0 Br]] := infinite_set_fset `|ceil r| infA.
 apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E).
   by rewrite lee_fin natr_absz gtr0_norm -?ceil_gt0// ceil_ge.
 move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.