lemma about sums of non-negative terms over general sets of indices

theories/cardinality.v

@@ -57,6 +57,9 @@ Qed.
 Lemma preimage_set0 T U (f : T -> U) : f @^-1` set0 = set0.
 Proof. by rewrite predeqE. Qed.
 
+Lemma preimageK T U (f : T -> U) (A : set U) : f @` (f @^-1` A) `<=` A.
+Proof. by move=> u [t]; rewrite /preimage => Aft <-{u}. Qed.
+
 Lemma in_inj_comp (A B C : Type) (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) :
   {in P &, injective f} -> {in Q &, injective h} -> (forall x, Q x -> P (h x)) ->
   {in Q &, injective (f \o h)}.
@@ -504,18 +507,6 @@ Qed.
 
 Definition set_finite T (A : set T) := exists n, A #= `I_n.
 
-Lemma set_finite_countable (T : pointedType) (A : set T) :
-  set_finite A -> countable A.
-Proof.
-by move=> [n /card_eqP[f Anf]]; exists f; split => //; exact: (inj_of_bij Anf).
-Qed.
-
-Lemma set_finite0 (T : pointedType) : set_finite (@set0 T).
-Proof.
-exists O; apply/card_eqP; exists (fun=> point); split => //; last by move=> ? [].
-by move=> x y; rewrite in_setE.
-Qed.
-
 Lemma set_finite_seq (T : pointedType) (s : seq T) :
   set_finite [set i | i \in s].
 Proof.
@@ -529,6 +520,68 @@ exists (size (undup s)); apply/card_eqP; exists (index^~ (undup s)); split.
   by rewrite index_uniq //; exact: undup_uniq.
 Qed.
 
+From mathcomp Require finmap.
+
+Section fset_classical_set.
+Import finmap.
+
+Lemma set_finite_fset (T : pointedType) (S : {fset T}%fset) :
+  set_finite [set x | x \in S].
+Proof. exact: set_finite_seq. Qed.
+
+Lemma eq_set0_fset0 (T : choiceType) (S : {fset T}%fset) :
+  ([set x | x \in S] == set0) = (S == fset0).
+Proof.
+apply/eqP/eqP=> [|->]; rewrite predeqE //.
+by move=> S0; apply/fsetP => t; apply/negbTE/negP=> /(proj1 (S0 t)).
+Qed.
+
+Lemma fset0_set0 (T : choiceType) : [set x | x \in fset0] = @set0 T.
+Proof. by rewrite predeqE. Qed.
+
+End fset_classical_set.
+
+Section set_finite_maximum.
+
+Lemma image_maximum n (f : nat -> nat) :
+  (exists i, i <= n /\ (forall j, j <= n -> f j <= f i))%N.
+Proof.
+elim: n => [|n [j [jn1 nfj]]]; first by exists 0%N; split => //; case.
+have [fn1fj|fjfn1] := leP (f n.+1) (f j).
+  exists j; split=> [|i]; first by rewrite (leq_trans jn1).
+  by rewrite leq_eqVlt => /orP[/eqP -> //|]; rewrite ltnS; apply nfj.
+have fmax : (forall i, i <= n -> f n.+1 > f j /\ f j >= f i)%N.
+  by move=> i ni; split => //; exact: nfj ni.
+exists n.+1; split => // k; rewrite leq_eqVlt ltnS => /orP[/eqP-> //|].
+by move/fmax => [_ /leq_trans]; apply; exact/ltnW.
+Qed.
+
+Lemma set_finite_maximum (A : set nat) : set_finite A -> A !=set0 ->
+  (exists i, A i /\ forall j, A j -> j <= i)%nat.
+Proof.
+case => -[|n /card_eqP[f]]; first by rewrite II0 => /card_eq0 -> [].
+move/set_bijective_inverse => -[f1 bij_f1] A0.
+have [i [ni H]] := image_maximum n f1.
+exists (f1 i); split; first by apply (sub_of_bij bij_f1); exists i.
+move=> j Aj.
+have [/= k [kn1 ->]] := (sur_of_bij bij_f1) _ Aj.
+by apply H; rewrite -ltnS.
+Qed.
+
+End set_finite_maximum.
+
+Lemma set_finite_countable (T : pointedType) (A : set T) :
+  set_finite A -> countable A.
+Proof.
+by move=> [n /card_eqP[f Anf]]; exists f; split => //; exact: (inj_of_bij Anf).
+Qed.
+
+Lemma set_finite0 (T : pointedType) : set_finite (@set0 T).
+Proof.
+exists O; apply/card_eqP; exists (fun=> point); split => //; last by move=> ? [].
+by move=> x y; rewrite in_setE.
+Qed.
+
 Section set_finite_bijection.
 
 Lemma set_bijective_U1 (T : pointedType) n (f g : nat -> T) (A : set T) :
@@ -772,6 +825,12 @@ have AfA : A #= f @` A by apply/card_eqP; exists f.
 by split => //; exists f.
 Qed.
 
+Corollary set_finite_preimage (T U : pointedType) (B : set U) (f : T -> U) :
+  {in (f @^-1` B) &, injective f} -> set_finite B -> set_finite (f @^-1` B).
+Proof.
+by move=> fi fB; case: (injective_set_finite fi (@preimageK _ _ _ _) fB).
+Qed.
+
 Corollary surjective_set_finite
   (T U : pointedType) (A : set T) (B : set U) (f : T -> U) :
   surjective A B f -> set_finite A ->
@@ -1106,37 +1165,6 @@ Qed.
 
 Section infinite_nat.
 
-Let image_maximum n (f : nat -> nat) :
-  (exists i, i <= n /\ (forall j, j <= n -> f j <= f i))%N.
-Proof.
-elim: n => [|n [j [jn1 nfj]]]; first by exists 0%N; split => //; case.
-have [fn1fj|fjfn1] := leP (f n.+1) (f j).
-  exists j; split=> [|i]; first by rewrite (leq_trans jn1).
-  by rewrite leq_eqVlt => /orP[/eqP[->//]|]; rewrite ltnS; apply nfj.
-have fmax : (forall i, i <= n -> f n.+1 > f j /\ f j >= f i)%N.
-  by move=> i ni; split => //; exact: nfj ni.
-exists n.+1; split => // k; rewrite leq_eqVlt ltnS => /orP[/eqP-> //|].
-by move/fmax => [_ /leq_trans]; apply; exact/ltnW.
-Qed.
-
-Let set_finite_maximum (A : set nat) : set_finite A -> A !=set0 ->
-  (exists i, A i /\ forall j, A j -> j <= i)%nat.
-Proof.
-case => -[|n].
-  by rewrite II0 => /card_eq0 -> [].
-move/card_eqP => -[/= f].
-move/set_bijective_inverse => -[f1 bij_f1] A0.
-have [i [ni H]] := image_maximum n f1.
-exists (f1 i).
-split.
-apply (sub_of_bij bij_f1).
-by exists i.
-move=> j Aj.
-have [/= k [kn1 ->]] := (sur_of_bij bij_f1) _ Aj.
-apply H.
-by rewrite -ltnS.
-Qed.
-
 Lemma infinite_nat : ~ set_finite (@setT nat).
 Proof.
 case=> n /card_eq_sym/card_eqP [/= g].

theories/ereal.v

@@ -380,9 +380,12 @@ Qed.
 Lemma adde_ge0 x y : 0%:E <= x -> 0%:E <= y -> 0%:E <= x + y.
 Proof. by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed.
 
-Lemma sume_ge0 T (u_ : T -> {ereal R}) : (forall n, 0%:E <= u_ n) -> forall l,
-  0%:E <= \sum_(i <- l) u_ i.
-Proof. by move=> ?; elim => [|? ? ?]; rewrite ?big_nil// big_cons adde_ge0. Qed.
+Lemma sume_ge0 T (u_ : T -> {ereal R}) (P : pred T) : (forall n, 0%:E <= u_ n) ->
+  forall l, 0%:E <= \sum_(i <- l | P i) u_ i.
+Proof.
+move=> ?; elim => [|? ? ?]; rewrite ?big_nil// big_cons.
+by case: ifPn => _; rewrite ?adde_ge0.
+Qed.
 
 End ERealArithTh_numDomainType.
 Arguments is_real {R}.

theories/measure_wip.v

@@ -23,6 +23,7 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+(* TODO: PR *)
 Lemma lee_adde (R : realFieldType) (a b : {ereal R}) :
   (forall e : {posnum R}, (a <= b + e%:num%:E)%E) -> (a <= b)%E.
 Proof.
@@ -389,89 +390,118 @@ Lemma ereal_limD (R : realType) (f g : nat -> {ereal R}) :
   cvg f -> cvg g -> ~~ adde_undef (lim f) (lim g) ->
   (lim (f \+ g) = lim f + lim g)%E.
 Proof. by move=> cf cg fg; apply/cvg_lim => //; apply ereal_cvgD. Qed.
+(* end TODO: PR *)
 
-(* *)
-
-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.
+(* TODO: move *)
+(* NB: could be more general (s2 need not be uniq )*)
+Lemma ler_sum_cond (R : realFieldType) (T : choiceType) (s1 s2 : seq T)
+  (a : T -> {ereal R}) : (forall x, 0%:E <= a x)%E -> {subset s1 <= s2} ->
+  uniq s1 -> uniq s2 -> (\sum_(i <- s1) a i <= \sum_(i <- s2) a i)%E.
+Proof.
+move=> a0 s12 us1 us2; rewrite (@bigID _ _ _ _ s2 [pred x | x \in s1]) /=.
+set lhs := (X in (X <= _)%E). set rhs := (X in (_ <= X + _)%E).
+suff -> : (lhs = rhs)%E by rewrite lee_addl // sume_ge0.
+rewrite {}/lhs {}/rhs -[RHS]big_filter; apply/perm_big.
+apply: (uniq_perm us1 (filter_uniq _ us2)) => t.
+by rewrite mem_filter; apply/idP/idP => [ts1|/andP[]//]; rewrite s12 // andbT.
+Qed.
 
 From mathcomp Require Import finmap.
 
-Definition isum (R : realFieldType) (T : choiceType) (S : set T) (a : T -> {ereal R}) :=
+(* sum of non-negative terms over general sets of indices *)
+Definition isum (R : realFieldType) (T : choiceType) (S : set T)
+    (a : T -> {ereal R}) :=
   if pselect (S !=set0) is left _ then
-    ereal_sup [set (\sum_(i <- enum_fset F) a i)%E |
-               F in (fun x => F != fset0 /\ [set i | i \in x] `<=` S)]
+    ereal_sup [set (\sum_(i <- F) a i)%E |
+               F in [set F | F != fset0 /\ [set i | i \in F] `<=` S]]
   else 0%:E.
 
 Lemma isum0 (R : realFieldType) (T : choiceType) (a : T -> {ereal R}) :
   isum set0 a = 0%:E.
 Proof. by rewrite /isum; case: pselect => // -[]. Qed.
 
-Lemma isum_countable (R : realType) (T : choiceType) (S : set T)
-  (a : T -> {ereal R}) (e : nat -> T) :
-  (forall n, 0%:E <= a n)%E ->
+Lemma isum_fset (R : realType) (T : choiceType) (S : {fset T})
+    (a : T -> {ereal R}) : (forall i, 0%:E <= a i)%E ->
+  isum [set x | x \in S] a = (\sum_(i <- S) a i)%E.
+Proof.
+move=> a0; rewrite /isum; case: pselect => [S0|]; last first.
+  move/set0P/negP/negPn; rewrite eq_set0_fset0 => /eqP ->.
+  by rewrite big_seq_fset0.
+apply/eqP; rewrite eq_le; apply/andP; split.
+  by apply ub_ereal_sup => /= x -[F [F0 FS] <-{x}]; rewrite /set1 ler_sum_cond.
+apply ereal_sup_ub; exists S; split => //.
+by move/set0P : S0; apply: contra => /eqP ->; rewrite fset0_set0.
+Qed.
+
+Lemma isum_countable (R : realType) (T : pointedType) (S : set T)
+  (a : T -> {ereal R}) (e : nat -> T) : (forall n, 0%:E <= a n)%E ->
   S #= @setT nat ->
   enumeration S e ->
   injective e ->
   isum S a = lim (fun n => (\sum_(i < n) a (e i))%E).
 Proof.
-move=> a0 ST [Se SeT] ie.
-rewrite /isum.
-case: pselect => [S0|]; last first.
+move=> a0 ST [Se SeT] ie; rewrite /isum; case: pselect => [S0|]; last first.
   move/set0P/negP/negPn/eqP => S0; move: SeT.
-  rewrite S0 => /esym/image_set0_set0.
-  by rewrite predeqE => /(_ 1%N) [] /(_ I).
+  by rewrite S0 => /esym/image_set0_set0; rewrite predeqE => /(_ 1%N) [] /(_ I).
 apply/eqP; rewrite eq_le; apply/andP; split; last first.
   apply: ereal_lim_le.
     by apply: (@is_cvg_ereal_nneg_series _ (a \o e)) => n; exact: a0.
   near=> N.
   have N0 : (0 < N)%nat by near: N; exists 1%N.
   have [N' NN'] : exists N', N = N'.+1 by exists N.-1; rewrite prednK.
-  have -> : (\sum_(i < N) a (e i) = \sum_(i <- [fset i | i in 'I_N]%fset) a (e i))%E.
+  have -> : (\sum_(i < N) a (e i) =
+      \sum_(i <- [fset i | i in 'I_N]%fset) a (e i))%E.
     by rewrite big_imfset //= big_enum.
   apply: ereal_sup_ub.
   exists (e @` [fset (nat_of_ord i) | i in 'I_N'.+1])%fset.
     split.
       apply/fset0Pn; exists (e (@ord0 N)).
-      apply/imfsetP => /=; exists 0%N => //.
-      by apply/imfsetP; exists ord0 => //.
+      by apply/imfsetP => /=; exists 0%N => //; apply/imfsetP; exists ord0.
      move=> t /imfsetP[k /= /imfsetP[/= j _ ->{k} ->{t}]].
      by rewrite SeT; exists j.
   rewrite big_imfset /=; last first.
-    move=> x y /imfsetP[/= x' _ xx' /imfsetP[/= y' _ yy']].
-    exact: ie.
+    by move=> x y /imfsetP[/= x' _ xx' /imfsetP[/= y' _ yy']]; exact: ie.
   rewrite big_imfset /=; last by move=> x y _ _; apply ord_inj.
   by rewrite big_imfset /= // NN'.
-apply ereal_lim_ge.
-  by apply: (@is_cvg_ereal_nneg_series _ (a \o e)) => n; exact: a0.
-near=> n.
 apply: ub_ereal_sup => x [/= F [F0 FS] <-{x}].
 have [N FNS] : exists N, (F `<=` [fset (e (nat_of_ord i)) | i in 'I_N])%fset.
   have [N H] : exists N, forall x, x \in F -> forall i, e i = x -> (i <= N)%N.
-    admit.
-  exists N.+1.
-  apply/fsubsetP => x Fx.
-  apply/imfsetP => /=.
-  admit.
-have H1 : (\sum_(i <- F) a i <= \sum_(i < N) (a (e i)))%E.
-admit.
-have H2 : (\sum_(i < N) (a (e i)) <= lim (fun n => \sum_(i < n) a (e i)))%E.
-  admit.
-apply: (le_trans H1).
-apply: (le_trans H2).
-Admitted.
+    have eF0 : e @^-1` (fun x => x \in F) !=set0.
+      case/fset0Pn : F0 => t Ft; have [i [_ tei]] := Se _ (FS _ Ft).
+      by exists i; rewrite /preimage -tei.
+    have feF : set_finite (e @^-1` (fun x => x \in F)).
+      by apply set_finite_preimage;
+        [move=> ? ? ? ?; exact: ie|exact: set_finite_fset].
+    have [i []] := set_finite_maximum feF eF0.
+    by rewrite /preimage => eiF K; exists i => t tF j ejt; apply K; rewrite ejt.
+  exists N.+1;apply/fsubsetP => x Fx; apply/imfsetP => /=.
+  have [j [_ xej]] := Se _ (FS _ Fx).
+  by exists (inord j) => //; rewrite xej inordK // ltnS (H _ Fx).
+apply ereal_lim_ge.
+  by apply: (@is_cvg_ereal_nneg_series _ (a \o e)) => n; exact: a0.
+near=> n.
+rewrite -big_image /= ler_sum_cond => //; last first.
+  by rewrite map_inj_uniq //; [exact: enum_uniq | move=> i j /ie /ord_inj].
+move=> x xF; apply/mapP.
+have Nn : (N <= n)%N by near: n; exists N.
+move/fsubsetP : FNS => /(_ _ xF)/imfsetP[/= j _ xej].
+by exists (widen_ord Nn j) => //; rewrite mem_enum.
+Grab Existential Variables. all: end_near. Qed.
 
-Lemma isum_isum (R : realType) (T : choiceType)
-  (I : set T) (K : set nat) (J : nat -> set T) (a : T -> {ereal R}) :
+Lemma isum_isum (R : realType) (T : choiceType) (I : set T) (K : set nat)
+    (J : nat -> set T) (a : T -> {ereal R}) :
   I = \bigcup_(k in K) (J k) ->
   K !=set0 ->
   (forall k, J k !=set0) ->
   triviset J ->
-  isum I (fun i => a i) = isum K (fun k => isum (J k) (fun i => a i)).
+  isum I a = isum K (fun k => isum (J k) a).
 Proof.
 Admitted.
 
+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.
+
 Module OuterMeasure.
 
 Section ClassDef.
@@ -701,16 +731,22 @@ have H1(*TODO: rename*) : (mu_ext (\bigcup_n A n) <= muB)%E.
       rewrite /mu_ext.
       apply ereal_inf_lb.
       have [enu [enuenu injenu]] : exists e : nat -> nat * nat, enumeration (@setT (nat * nat)) e /\ injective e.
-        admit.
+        have /countable_enumeration [|[f ef]] := countable_prod_nat.
+          by rewrite predeqE => /(_ (O%N, 0%N)) [] /(_ I).
+        by exists (enum_wo_rep infinite_prod_nat ef); split;
+         [exact: enumeration_enum_wo_rep | exact: injective_enum_wo_rep].
       exists (fun x => let i := enu x in B i.1 i.2).
         split.
-          admit.
+          move=> i.
+          move: (BA (enu i).1) => -[].
+          by rewrite /measurable_cover => -[] /(_ (enu i).2).
+        move/subset_trans : AB; apply.
         admit.
       have : forall ab : nat * nat, (0%:E <= mu (B ab.1 ab.2))%E.
         move=> ab.
         apply: measure_ge0.
         by move: (BA ab.1) => [] [] /(_ ab.2).
-      move/(@isum_countable R [choiceType of nat * nat] setT (fun ab => mu (B ab.1 ab.2)) enu).
+      move/(@isum_countable R _ setT (fun ab => mu (B ab.1 ab.2)) enu).
       by move/(_ countably_infinite_prod_nat enuenu injenu).
     move/le_trans; apply.
     rewrite le_eqVlt; apply/orP; left; apply/eqP.
@@ -722,24 +758,24 @@ have H1(*TODO: rename*) : (mu_ext (\bigcup_n A n) <= muB)%E.
       admit.
     have H4 : triviset (fun (i : nat) (y : nat * nat) => exists2 j : nat, setT j & (i, j) = y).
       admit.
-    rewrite (@isum_isum R [choiceType of nat * nat] setT setT (fun i => [set (i, j) | j in @setT nat]) (fun ab => mu (B ab.1 ab.2)) H1 H2 H3 H4).
+    rewrite (@isum_isum R _ setT setT (fun i => [set (i, j) | j in @setT nat]) (fun ab => mu (B ab.1 ab.2)) H1 H2 H3 H4).
     have [enu [enuenu injenu]] : exists e : nat -> nat, enumeration (@setT nat) e /\ injective e.
       admit.
-    rewrite (@isum_countable R [choiceType of nat] setT (fun k : nat_choiceType => isum (fun y : nat * nat => exists2 j : nat, setT j & (k, j) = y) (fun i : [choiceType of nat * nat] => mu (B i.1 i.2))) enu) //; last 2 first.
-      admit.
+    rewrite (@isum_countable R _ setT (fun k : nat_choiceType => isum (fun y : nat * nat => exists2 j : nat, setT j & (k, j) = y) (fun i => mu (B i.1 i.2))) enu) //; last 2 first.
       admit.
+      by apply/card_eqP; exists id; split => // x _; exists x. (* TODO: lemma? *)
     congr (lim _).
     rewrite funeqE => /= i.
     apply: eq_bigr=> j _.
-    have [enu' [enuenu' injenu']] : exists e : nat -> nat * nat, enumeration ((fun y : nat * nat => exists2 j0 : nat, setT j0 & (enu j, j0) = y)) e /\ injective e.
+    have [enu' [enuenu' injenu']] : exists e : nat -> nat * nat, enumeration ((fun y => exists2 j0 : nat, setT j0 & (enu j, j0) = y)) e /\ injective e.
       admit.
-    rewrite (@isum_countable R [choiceType of nat * nat] (fun y : nat * nat => exists2 j0 : nat, setT j0 & (enu j, j0) = y) (fun i0 : nat * nat => mu (B i0.1 i0.2)) enu') //; last 2 first.
+    rewrite (@isum_countable R [pointedType of nat * nat] (fun y => exists2 j0 : nat, setT j0 & (enu j, j0) = y) (fun i0 : nat * nat => mu (B i0.1 i0.2)) enu') //; last 2 first.
       admit.
       admit.
     congr (lim _).
     rewrite funeqE => /= k.
     admit.
-  by apply/le_trans.
+  exact/le_trans.
 apply: (le_trans H1) => {H1}.
 rewrite {}/muB /=.
 apply lee_lim.