rebase

theories/lebesgue_measure.v

@@ -2206,106 +2206,6 @@ Qed.
 
 End egorov.
 
-(* PRs in progress *)
-Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N :
-  (\sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i)%E.
-Proof. by congr (lim _); apply: eq_fun => n /=; apply: big_nat_widenl. Qed.
-
-Lemma eseries_mkcondl {R : numFieldType} (f : nat -> \bar R) P Q :
-  (\sum_(i <oo | P i && Q i) f i = \sum_(i <oo | Q i) if P i then f i else 0)%E.
-Proof. by congr (lim _); apply/funext => n; rewrite big_mkcondl. Qed.
-
-Lemma eseries_mkcondr {R : numFieldType} (f : nat -> \bar R) P Q :
-  (\sum_(i <oo | P i && Q i) f i = \sum_(i <oo | P i) if Q i then f i else 0)%E.
-Proof. by congr (lim _); apply/funext => n; rewrite big_mkcondr. Qed.
-
-Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} :
-  (forall i, P i -> f i = g i) ->
-  (\sum_(N <= i <oo | P i) f i = \sum_(N <= i <oo | P i) g i)%E.
-Proof. by move=> efg; congr (lim _); apply/funext => n; exact: eq_bigr. Qed.
-
-Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N :
-  (forall i, P i -> 0 <= f i)%E ->
-  ((\sum_(N <= i <oo | P i) (x%:E * f i) = x%:E * \sum_(N <= i <oo | P i) f i))%E.
-Proof.
-move=> f0; rewrite -limeMl//; last exact: is_cvg_nneseries.
-by congr (lim _); apply/funext => /= n; rewrite ge0_sume_distrr.
-Qed.
-
-Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) N :
-  (forall i, P i -> 0 <= u i)%E ->
-  (forall n, P n -> u n <= v n)%E ->
-  (\sum_(N <= i <oo | P i) u i <= \sum_(N <= i <oo | P i) v i)%E.
-Proof.
-move=> u0 Puv; apply: lee_lim.
-- by apply: is_cvg_ereal_nneg_natsum_cond => n ? /u0; exact.
-- apply: is_cvg_ereal_nneg_natsum_cond => n _ Pn.
-  by rewrite (le_trans _ (Puv _ Pn))// u0.
-- by near=> n; apply: lee_sum => k; exact: Puv.
-Unshelve. all: by end_near. Qed.
-
-Lemma bigcup_bigcup_new (I : Type) T1 T2 (F : I -> set T1) (G : T1 -> set T2) :
-  \bigcup_(i in \bigcup_n F n) G i = \bigcup_n \bigcup_(i in F n) G i.
-Proof.
-apply/seteqP; split.
-  by move=> x [n [m _ D'mn] h]; exists m => //; exists n.
-by move=> x [n _ [m D'nm]] h; exists m => //; exists n.
-Qed.
-
-Lemma closed_bigcup (T : topologicalType) (I : choiceType) (A : set I)
-    (F : I -> set T) :
-    finite_set A -> (forall i, A i -> closed (F i)) ->
-  closed (\bigcup_(i in A) F i).
-Proof.
-move=> finA cF; rewrite -bigsetU_fset_set//; apply: closed_bigsetU => i.
-by rewrite in_fset_set// inE; exact: cF.
-Qed.
-
-Lemma lee_addgt0Pr {R : realFieldType} (x y : \bar R) :
-  reflect (forall e, (0 < e)%R -> (x <= y + e%:E)%E) (x <= y)%E.
-Proof.
-apply/(iffP idP) => [|].
-- move: x y => [x| |] [y| |]//.
-  + by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_paddr// ltW.
-  + by move=> _ e e0; rewrite leNye.
-- move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//.
-  + by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
-  + by move: xy => /(_ _ lte01).
-  + by move: xy => /(_ _ lte01).
-  + by move: xy => /(_ _ lte01).
-Qed.
-(* /PRs in progress *)
-
-(* TODO: move to measure.v once the eseries_cond PR is merged *)
-Lemma measure_sigma_sub_additive_tail d (R : realType) (T : semiRingOfSetsType d)
-  (mu : {measure set T -> \bar R}) (A : set T) (F : nat -> set T) N :
-    (forall n, measurable (F n)) -> measurable A ->
-    A `<=` \bigcup_(n in ~` `I_N) F n ->
-  (mu A <= \sum_(N <= n <oo) mu (F n))%E.
-Proof.
-move=> mF mA AF; rewrite eseries_cond eseries_mkcondr.
-rewrite (@eq_eseriesr _ _ (fun n => mu (if (N <= n)%N then F n else set0))).
-- apply: measure_sigma_sub_additive => //.
-  + by move=> n; case: ifPn.
-  + move: AF; rewrite bigcup_mkcond.
-    by under eq_bigcupr do rewrite mem_not_I.
-- by move=> o _; rewrite (fun_if mu) measure0.
-Qed.
-
-Lemma outer_measure_sigma_subadditive_tail (T : Type) (R : realType)
-    (mu : {outer_measure set T -> \bar R}) N (F : (set T) ^nat) :
-  (mu (\bigcup_(n in ~` `I_N) (F n)) <= \sum_(N <= i <oo) mu (F i))%E.
-Proof.
-rewrite bigcup_mkcond.
-have := outer_measure_sigma_subadditive mu
-  (fun n => if n \in ~` `I_N then F n else set0).
-move/le_trans; apply.
-rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries.
-- by move=> k _; exact: outer_measure_ge0.
-- move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk.
-  by rewrite mem_not_I (negbTE Nk) outer_measure0.
-Qed.
-
 Definition vitali_cover {R : realType} (E : set R) I
     (B : I -> (R * {posnum R})%type) (D : set I) :=
   forall x, E x -> forall e : R, 0 < e -> exists i,
@@ -2370,7 +2270,7 @@ have EBr2 n : E n -> scale_cball 1 (B n) `<=` (ball (0 : R^o) (r%:num + 2))%R.
   move: rx; rewrite /ball /= !sub0r !normrN => rx.
   rewrite -(subrK x y) (le_lt_trans (ler_norm_add _ _))//.
   rewrite addrC ltr_le_add// -(subrK (B n).1 y) -(addrA (y - _)%R).
-  rewrite (le_trans (ler_norm_add _ _))// (natrD _ 1%N) ler_add//.
+  rewrite (le_trans (ler_norm_add _ _))// (_ : 2 = 1 + 1)%R// ler_add//.
     rewrite (@closed_ballE _ [normedModType R of R^o]) // in Bny.
     by rewrite distrC (le_trans Bny)// VB1//; exact: DV.
   rewrite (@closed_ballE _ [normedModType R of R^o]) // in Bnx.
@@ -2388,7 +2288,7 @@ have finite_set_F i : finite_set (F i).
   move/(infinite_set_fset M) => [/= C] CsubFi McardC.
   have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
             mu (\bigcup_(j in [set` C]) scale_cball 1 (B j)).
-    rewrite (measure_bigcup mu [set` C])//; last 2 first.
+    rewrite (measure_bigcup [the measure _ _ of mu] [set` C])//; last 2 first.
       by move=> ? _; exact: measurable_scale_cball.
       by apply: sub_trivIset tDB; by apply: (subset_trans CsubFi) => x [[]].
     rewrite /= nneseries_esum//= set_mem_set// esum_fset// fsbig_finite//=.
@@ -2429,7 +2329,7 @@ have mur2_fin_num_ : mu (ball (0 : R^o) (r%:num + 2))%R < +oo.
   by rewrite lebesgue_measure_ball// ltry.
 have FE : \sum_(n <oo) \esum_(i in F n) mu (scale_cball 1 (B i)) =
           mu (\bigcup_(i in E) scale_cball 1 (B i)).
-  rewrite E_partition bigcup_bigcup_new; apply/esym.
+  rewrite E_partition bigcup_bigcup; apply/esym.
   transitivity (\sum_(n <oo) mu (\bigcup_(i in F n) scale_cball 1 (B i))).
     apply: measure_semi_bigcup => //.
     - by move=> i; apply: bigcup_measurable => *; exact: measurable_scale_cball.
@@ -2438,7 +2338,7 @@ have FE : \sum_(n <oo) \esum_(i in F n) mu (scale_cball 1 (B i)) =
         apply: disjoint_vitali_collection_partition => //.
         by move=> k -[] /DV /VB1.
       by rewrite -E_partition; apply: sub_trivIset tDB => x [].
-    - rewrite -bigcup_bigcup_new; apply: bigcup_measurable => k _.
+    - rewrite -bigcup_bigcup; apply: bigcup_measurable => k _.
       exact: measurable_scale_cball.
   apply: (@eq_eseriesr _ (fun n => mu (\bigcup_(i in F n) scale_cball 1 (B i)))).
   move=> i _; rewrite bigcup_mkcond measure_semi_bigcup//; last 3 first.
@@ -2447,12 +2347,12 @@ have FE : \sum_(n <oo) \esum_(i in F n) mu (scale_cball 1 (B i)) =
     rewrite -bigcup_mkcond; apply: bigcup_measurable => k _.
     exact: measurable_scale_cball.
   rewrite esum_mkcond//= nneseries_esum// -fun_true//=.
-  by under eq_esum do rewrite (fun_if mu) (measure0 mu).
+  by under eq_esum do rewrite (fun_if mu) (measure0 [the measure _ _ of mu]).
 apply/eqP; rewrite eq_le measure_ge0 andbT.
 apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e.
 have [N F5e] : exists N,
     \sum_(N <= n <oo) \esum_(i in F n) mu (scale_cball 1 (B i)) <
-    5^-1%:E * e%:num%:E.
+    5%:R^-1%:E * e%:num%:E.
   pose f n := \bigcup_(i in F n) scale_cball 1 (B i).
   have foo : \sum_(k <oo) (mu \o f) k < +oo.
     rewrite /f /= [ltLHS](_ : _ =
@@ -2473,7 +2373,7 @@ have [N F5e] : exists N,
   rewrite /f /=.
   move/fine_fcvg => /=.
   move/(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]).
-  have : (0 < 5^-1 * e%:num)%R  by rewrite mulr_gt0// invr_gt0// ltr0n.
+  have : (0 < 5%:R^-1 * e%:num)%R  by rewrite mulr_gt0// invr_gt0// ltr0n.
   move=> /[swap] /[apply].
   rewrite near_map => -[N _]/(_ _ (leqnn N)) h; exists N; move: h.
   rewrite sub0r normrN ger0_norm//; last first.
@@ -2494,7 +2394,7 @@ have closedK : closed K.
   apply: closed_bigcup => //= i iN; apply: closed_bigcup => //.
   by move=> j Fij; exact: (@closed_ball_closed _ [normedModType R of R^o]).
 have ZNF5 : Z r%:num `<=`
-    \bigcup_(i in ~` `I_N) \bigcup_(j in F i) scale_cball 5 (B j).
+    \bigcup_(i in ~` `I_N) \bigcup_(j in F i) scale_cball 5%:R (B j).
   move=> z Zz.
   have Kz : ~ K z.
     rewrite /K => -[n /= nN [m] [[Dm _] _] Bmz].
@@ -2539,7 +2439,7 @@ have ZNF5 : Z r%:num `<=`
     by rewrite (le_trans Biy)// ltW.
   have [j [Ej Bij0 Bij5]] : exists j, [/\ E j,
       scale_cball 1 (B i) `&` scale_cball 1 (B j) !=set0 &
-      scale_cball 1 (B i) `<=` scale_cball 5 (B j)].
+      scale_cball 1 (B i) `<=` scale_cball 5%:R (B j)].
     have [j [Dj Bij0 Bij2 Bij5]] := Dintersect _ Vi.
     exists j; split => //; split => //.
     by move: Bij0; rewrite setIC; exact: subsetI_neq0.
@@ -2551,13 +2451,13 @@ have ZNF5 : Z r%:num `<=`
     exists k => //= kN.
     by apply: BjK => x Bjx; exists k => //; exists j.
   by exists k => //; exists j => //; exact: Bij5.
-have {ZNF5}ZNF5 :
-    mu (Z r%:num) <= \sum_(N <= m <oo) \esum_(i in F m) mu (scale_cball 5 (B i)).
+have {}ZNF5 : mu (Z r%:num) <=
+    \sum_(N <= m <oo) \esum_(i in F m) mu (scale_cball 5%:R (B i)).
   apply: (@le_trans _ _ (mu (\bigcup_(i in ~` `I_N)
-      \bigcup_(j in F i) scale_cball 5 (B j)))).
+      \bigcup_(j in F i) scale_cball 5%:R (B j)))).
     exact: le_outer_measure.
   apply: (@le_trans _ _ (\sum_(N <= i <oo) mu
-                           (\bigcup_(j in F i) scale_cball 5 (B j)))).
+                           (\bigcup_(j in F i) scale_cball 5%:R (B j)))).
     apply: measure_sigma_sub_additive_tail => //.
       move=> n; apply: bigcup_measurable => k _.
       by apply: measurable_closed_ball => //; rewrite mulr_ge0// ler0n.
@@ -2567,22 +2467,21 @@ have {ZNF5}ZNF5 :
   rewrite -[in leRHS](set_mem_set (F n)) -nneseries_esum//.
   rewrite bigcup_mkcond eseries_mkcond.
   rewrite [leRHS](_ : _ = \sum_(i <oo) mu
-      (if i \in F n then (scale_cball 5 (B i)) else set0)); last first.
+      (if i \in F n then (scale_cball 5%:R (B i)) else set0)); last first.
     congr (lim _); apply/funext => x.
     by under [RHS]eq_bigr do rewrite (fun_if mu) measure0.
   apply: measure_sigma_sub_additive => //.
-  + move=> m; case: ifPn => // _; apply: measurable_scale_cball => //.
-    exact: ler0n.
+  + by move=> m; case: ifPn => // _; exact: measurable_scale_cball.
   + apply: bigcup_measurable => k _; case: ifPn => // _.
-    by apply: measurable_scale_cball; exact: ler0n.
+    exact: measurable_scale_cball.
 apply/(le_trans ZNF5)/ltW.
 move: F5e.
-rewrite [in X in X -> _](@lte_pdivl_mull R 5%R e%:num%:E) ?ltr0n//.
+rewrite [in X in X -> _](@lte_pdivl_mull R 5%:R e%:num%:E) ?ltr0n//.
 rewrite -nneseriesZl//; last by move=> *; exact: esum_ge0.
 move/le_lt_trans; apply.
 apply: lee_nneseries => //; first by move=> *; exact: esum_ge0.
 move=> n _.
-rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesrM//.
+rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesZl//.
 apply: lee_nneseries => // m mFn.
 rewrite scale_cball1 lebesgue_measure_closed_ball ?mulr_ge0 ?ler0n//.
 by rewrite lebesgue_measure_closed_ball// -EFinM mulrnAr.

theories/measure.v

@@ -2618,6 +2618,21 @@ Qed.
 
 End more_premeasure_ring_lemmas.
 
+Lemma measure_sigma_sub_additive_tail d (R : realType) (T : semiRingOfSetsType d)
+  (mu : {measure set T -> \bar R}) (A : set T) (F : nat -> set T) N :
+    (forall n, measurable (F n)) -> measurable A ->
+    A `<=` \bigcup_(n in ~` `I_N) F n ->
+  (mu A <= \sum_(N <= n <oo) mu (F n))%E.
+Proof.
+move=> mF mA AF; rewrite eseries_cond eseries_mkcondr.
+rewrite (@eq_eseriesr _ _ (fun n => mu (if (N <= n)%N then F n else set0))).
+- apply: measure_sigma_sub_additive => //.
+  + by move=> n; case: ifPn.
+  + move: AF; rewrite bigcup_mkcond.
+    by under eq_bigcupr do rewrite mem_not_I.
+- by move=> o _; rewrite (fun_if mu) measure0.
+Qed.
+
 Section ring_sigma_content.
 Context d (R : realType) (T : semiRingOfSetsType d)
         (mu : {measure set T -> \bar R}).
@@ -3354,6 +3369,20 @@ Arguments outer_measure_ge0 {R T} _.
 Arguments le_outer_measure {R T} _.
 Arguments outer_measure_sigma_subadditive {R T} _.
 
+Lemma outer_measure_sigma_subadditive_tail (T : Type) (R : realType)
+    (mu : {outer_measure set T -> \bar R}) N (F : (set T) ^nat) :
+  (mu (\bigcup_(n in ~` `I_N) (F n)) <= \sum_(N <= i <oo) mu (F i))%E.
+Proof.
+rewrite bigcup_mkcond.
+have := outer_measure_sigma_subadditive mu
+  (fun n => if n \in ~` `I_N then F n else set0).
+move/le_trans; apply.
+rewrite [in leRHS]eseries_cond [in leRHS]eseries_mkcondr; apply: lee_nneseries.
+- by move=> k _; exact: outer_measure_ge0.
+- move=> k _; rewrite fun_if; case: ifPn => Nk; first by rewrite mem_not_I Nk.
+  by rewrite mem_not_I (negbTE Nk) outer_measure0.
+Qed.
+
 Section outer_measureU.
 Context d (T : semiRingOfSetsType d) (R : realType).
 Variable mu : {outer_measure set T -> \bar R}.

theories/normedtype.v

@@ -5899,7 +5899,7 @@ move/(@nbhs_closedballP R M _ x) => [r xrA].
 have r2k20 : 0 < minr (r%:num / 2) (k / 2) by rewrite lt_minr// !divr_gt0.
 exists (PosNum r2k20) => /=.
   by rewrite lt_minl orbC ltr_pdivr_mulr// ltr_pmulr// ltr1n.
-apply/(subset_trans _ xrA)/(subset_trans _ (subset_closed_ball _)) => //.
+apply/(subset_trans _ xrA)/(subset_trans _ (@subset_closed_ball _ _ _ _)) => //.
 by apply: le_ball; rewrite le_minl; rewrite ler_pdivr_mulr// ler_pmulr// ler1n.
 Qed.