\sum^oo_i F notation

CHANGELOG_UNRELEASED.md

@@ -55,6 +55,8 @@
     `caratheodory_measure_sigma_additive`,
     defintions `caratheodory_measure_mixin`, `caratheodory_measure`,
     lemma `caratheodory_measure_complete`
+  + notations `\sum^oo_i F` and `\sum^oo_(i in P) F`
+    + for the definitions `sumoo` and `sumoo_cond`
 
 ### Changed
 

theories/measure.v

@@ -9,6 +9,10 @@ From HB Require Import structures.
 (******************************************************************************)
 (*                            Measure Theory                                  *)
 (*                                                                            *)
+(* Notations for series:                                                      *)
+(* \sum^oo_i F == lim (fun n => \sum_(i < n) F i)                             *)
+(* \sum^oo_(i in P) F == lim (fun n => \sum_(i < n | P i) F i)                *)
+(*                                                                            *)
 (* semiRingOfSetsType == the type of semirings of sets                        *)
 (*     ringOfSetsType == the type of rings of sets                            *)
 (*     measurableType == the type of sigma-algebras                           *)
@@ -55,6 +59,20 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Reserved Notation "mu .-negligible" (at level 2, format "mu .-negligible").
 Reserved Notation "{ 'ae' m , P }" (at level 0, format "{ 'ae'  m ,  P }").
 Reserved Notation "mu .-measurable" (at level 2, format "mu .-measurable").
+Reserved Notation "\sum^oo_ i F"
+  (at level 41, F at level 41, i at level 0,
+           format "'[' \sum^oo_ i '/  '  F ']'").
+Reserved Notation "\sum^oo_ ( i 'in' P ) F"
+  (at level 41, F at level 41, i, P at level 50,
+           format "'[' \sum^oo_ ( i  'in'  P ) '/  '  F ']'").
+
+Definition sumoo {R : numFieldType} (F : (er R)^nat) :=
+  lim (fun n => \sum_(i < n) F i)%E.
+Definition sumoo_cond {R : numFieldType} (P : pred nat) (F : (er R)^nat) :=
+  lim (fun n => \sum_(i < n | P i) F i)%E.
+
+Notation "\sum^oo_ i F" := (sumoo (fun i => F)).
+Notation "\sum^oo_ ( i 'in' P ) F" := (sumoo_cond P (fun i => F)).
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -656,9 +674,9 @@ Variable (mu : {measure set T -> {ereal R}}).
 
 (* 404,p.44 measure satisfies generalized Boole's inequality *)
 Theorem generalized_Boole_inequality (A : (set T) ^nat) :
-  (forall i : nat, measurable (A i)) ->
+  (forall i, measurable (A i)) ->
   (measurable (\bigcup_n A n)) ->
-  (mu (\bigcup_n A n) <= lim (fun n => \sum_(i < n) mu (A i)))%E.
+  (mu (\bigcup_n A n) <= \sum^oo_i (mu (A i)))%E.
 Proof.
 move=> mA mbigcupA; set B := fun n => \big[setU/set0]_(i < n.+1) (A i).
 have AB : \bigcup_k A k = \bigcup_n B n.
@@ -679,7 +697,7 @@ have -> : lim (mu \o B) = ereal_sup ((mu \o B) @` setT).
     by move/nondecreasing_seq_ereal_cvg; apply/(@cvg_lim _ _ (mu \o B @ \oo)) (* bug *).
   move=> n m nm; apply: le_measure => //; try by rewrite inE; apply mB.
   by move: nm; rewrite -ltnS; exact/(@subset_bigsetU _ _ xpredT).
-have BA : forall m, (mu (B m) <= lim (fun n : nat => \sum_(i < n) mu (A i)))%E.
+have BA : forall m, (mu (B m) <= \sum^oo_i (mu (A i)))%E.
   move=> m; rewrite (le_trans (le_mu_bigsetU (measure_additive_measure mu) mA m.+1)) // -/(B m).
   by apply: (@ereal_nneg_series_lim_ge _ (mu \o A) xpredT) => n _; exact: measure_ge0.
 by apply ub_ereal_sup => /= x [n _ <-{x}]; apply BA.
@@ -729,7 +747,7 @@ Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) : type_scope.
 
 Definition sigma_subadditive (R : numFieldType) (T : Type)
   (mu : set T -> {ereal R}) := forall (A : (set T) ^nat),
-  (mu (\bigcup_n (A n)) <= lim (fun n => \sum_(i < n) mu (A i)))%E.
+  (mu (\bigcup_n (A n)) <= \sum^oo_i (mu (A i)))%E.
 
 Module OuterMeasure.
 
@@ -797,15 +815,15 @@ Lemma le_outer_measureIC (R : realFieldType) T
 Proof.
 pose B : (set T) ^nat := bigcup2 (X `&` A) (X `&` ~` A).
 have cvg_mu :
-    (fun n => (\sum_(i < n) mu (B i))%E) --> (mu (B 0%N) + mu (B 1%N))%E.
+    (fun n => \sum_(i < n) mu (B i))%E --> (mu (B 0%N) + mu (B 1%N))%E.
   rewrite -2!cvg_shiftS /=.
   rewrite [X in X --> _](_ : _ = (fun=> mu (B 0%N) + mu (B 1%N)))%E; last first.
     rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _.
     by rewrite /B /bigcup2 /=.
   exact: cvg_cst.
 have := outer_measure_sigma_subadditive mu B.
 suff : \bigcup_n B n = X.
-  by move=> -> /le_trans; apply; rewrite (cvg_lim _ cvg_mu).
+  by move=> -> /le_trans; apply; rewrite /sumoo (cvg_lim _ cvg_mu).
 transitivity (\big[setU/set0]_(i < 2) B i).
   rewrite (bigcup_recl 2) // bigcup_ord [X in _ `|` X](_ : _ = set0) ?setU0 //.
   by rewrite predeqE => t; split => // -[].
@@ -834,7 +852,7 @@ Variables (R : realType) (T : Type)
   (mu : {outer_measure set T -> {ereal R}}).
 
 Lemma outer_measure_bigcup_lim (A : (set T) ^nat)  X :
-  (mu (X `&` \bigcup_k A k) <= lim (fun n => \sum_(k < n) mu (X `&` A k)))%E.
+  (mu (X `&` \bigcup_k A k) <= \sum^oo_k (mu (X `&` A k)))%E.
 Proof.
 apply: (le_trans _ (outer_measure_sigma_subadditive mu (fun n => X `&` A n))).
 by apply/le_outer_measure; rewrite bigcup_distrr.
@@ -861,7 +879,8 @@ have /(lee_add2r (mu (X `&` ~` (A `|` B)))) :
     by move=> [_ ?|[_ ?|//]]; [left|right].
   rewrite (le_trans (outer_measure_sigma_subadditive mu Z)) //.
   suff : ((fun n => \sum_(i < n) mu (Z i)) -->
-    mu (X `&` A) + mu (X `&` B `&` ~` A))%E by move/cvg_lim => ->.
+      mu (X `&` A) + mu (X `&` B `&` ~` A))%E.
+    by rewrite /sumoo => /cvg_lim ->.
   rewrite -(cvg_shiftn 2) /=; set l := (X in _ --> X).
   rewrite [X in X --> _](_ : _ = cst l); first exact: cvg_cst.
   rewrite funeqE => i; rewrite addn2 2!big_ord_recl big1 ?adde0 //.
@@ -950,13 +969,13 @@ Qed.
 
 Lemma caratheodory_lim_lee (A : (set T) ^nat) : (forall n, M (A n)) ->
   trivIset setT A -> forall X,
-  (lim (fun n => \sum_(k < n) mu (X `&` A k)) + mu (X `&` ~` \bigcup_k A k) <=
+  (\sum^oo_k (mu (X `&` A k)) + mu (X `&` ~` \bigcup_k A k) <=
    mu X)%E.
 Proof.
 move=> MA tA X.
 set A' := \bigcup_k A k; set B := fun n => \big[setU/set0]_(k < n) (A k).
 suff : forall n, (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X)%E.
-  move=> XA; rewrite (_ : lim _ = ereal_sup
+  move=> XA; rewrite (_ : \sum^oo__ _ = ereal_sup
       ((fun n => \sum_(k < n) mu (X `&` A k))%E @` setT)); last first.
     apply/cvg_lim => //; apply/nondecreasing_seq_ereal_cvg.
     apply: (@lee_sum_nneg_ord _ (fun n => mu (X `&` A n)) xpredT) => n _.
@@ -1028,16 +1047,15 @@ Proof. by move=> mx; apply outer_measure_ge0. Qed.
 Lemma caratheodory_measure_sigma_additive : @semi_sigma_additive _ U mu.
 Proof.
 move=> A mA tA mbigcupA; set B := \bigcup_k A k.
-suff : forall X, (mu X = lim (fun n : nat => \sum_(k < n) mu (X `&` A k)) +
-             mu (X `&` ~` B))%E.
-  move/(_ B); rewrite setICr outer_measure0 adde0.
+suff : forall X, (mu X = \sum^oo_k (mu (X `&` A k)) + mu (X `&` ~` B))%E.
+  move/(_ B); rewrite setICr outer_measure0 adde0 /sumoo.
   rewrite (_ : (fun n => _) = (fun n => (\sum_(k < n) mu (A k))%E)); last first.
     rewrite funeqE => n; apply eq_bigr => i _; congr (mu _).
     by rewrite setIC; apply/setIidPl => t Ait; exists i.
   move=> ->; have : forall n, xpredT n -> (0%:E <= mu (A n))%E.
     by move=> n _; apply outer_measure_ge0.
-  move/(@is_cvg_ereal_nneg_series _ (mu \o A)) => /cvg_ex[l] H.
-  by move/(@cvg_lim _ (@ereal_hausdorff R)) : (H) => ->.
+  move/(@is_cvg_ereal_nneg_series _ (mu \o A)) => /cvg_ex[l] hl.
+  by move/(@cvg_lim _ (@ereal_hausdorff R)) : (hl) => ->.
 move=> X.
 have mB : mu.-measurable B := caratheodory_measurable_bigcup mA.
 apply/eqP; rewrite eq_le (caratheodory_lim_lee mA tA X) andbT.