wip integral

theories/classical_sets.v

@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
-From mathcomp Require Import ssralg matrix.
+From mathcomp Require Import fintype bigop ssralg matrix.
 Require Import boolp.
 
 (******************************************************************************)
@@ -332,6 +332,9 @@ Proof. by rewrite predeqE => ?; split=> [[]|[]]. Qed.
 Lemma setIT {A} (X : set A) : X `&` setT = X.
 Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
 
+Lemma setTI {A} (X : set A) : setT `&` X = X.
+Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
+
 Lemma setI0 {A} (X : set A) : X `&` set0 = set0.
 Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
 
@@ -361,10 +364,16 @@ Lemma setUC A : commutative (@setU A).
 Proof. move=> p q; rewrite /setU predeqE => a; tauto. Qed.
 
 Lemma set0U T (X : set T) : set0 `|` X = X.
-Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|right]. Qed.
+Proof. by rewrite predeqE => t; split; [case|right]. Qed.
 
 Lemma setU0 T (X : set T) : X `|` set0 = X.
-Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|left]. Qed.
+Proof. by rewrite predeqE => t; split; [case|left]. Qed.
+
+Lemma setTU T (X : set T) : setT `|` X = setT.
+Proof. by rewrite predeqE => t; split; [case|left]. Qed.
+
+Lemma setUT T (X : set T) : X `|` setT = setT.
+Proof. by rewrite predeqE => t; split; [case|right]. Qed.
 
 Lemma setU_eq0 T (X Y : set T) : (X `|` Y = set0) = ((X = set0) /\ (Y = set0)).
 Proof. by rewrite -!subset0 subUset. Qed.
@@ -377,6 +386,26 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa].
 by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di.
 Qed.
 
+Lemma setIDl T : left_distributive (@setI T) (@setU T).
+Proof.
+move=> X Y Z; rewrite predeqE => t; split.
+  by move=> [[Xt|Yt] Zt]; [left|right].
+by move=> [[Xt Zt]|[Yt Zt]]; split => //; [left|right].
+Qed.
+
+Lemma setIDr T : right_distributive (@setI T) (@setU T).
+Proof. by move=> X Y Z; rewrite ![X `&` _]setIC setIDl. Qed.
+
+Lemma setUDl T : left_distributive (@setU T) (@setI T).
+Proof.
+move=> X Y Z; rewrite predeqE => t; split.
+  by move=> [[Xt Yt]|Zt]; split; by [left|right].
+by move=> [[Xt|Zt] [Yt|Zt']]; by [left|right].
+Qed.
+
+Lemma setUDr T : right_distributive (@setU T) (@setI T).
+Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUDl. Qed.
+
 Definition is_prop {A} (X : set A) := forall x y, X x -> X y -> x = y.
 Definition is_fun {A B} (f : A -> B -> Prop) := all (is_prop \o f).
 Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).
@@ -428,6 +457,40 @@ Lemma fun_of_rel_uniq {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a
   is_prop (f a) -> forall b, f a b ->  fun_of_rel f0 f a = b.
 Proof. by move=> fa_prop b /xget_prop xgeteq; rewrite /fun_of_rel xgeteq. Qed.
 
+
+Section SetMonoids.
+Variable (T : Type).
+
+Import Monoid.
+Canonical setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
+Canonical setU_comoid := ComLaw (@setUC T).
+Canonical setU_mul_monoid := MulLaw (@setTU T) (@setUT T).
+Canonical setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).
+Canonical setI_comoid := ComLaw (@setIC T).
+Canonical setI_mul_monoid := MulLaw (@set0I T) (@setI0 T).
+Canonical setU_add_monoid := AddLaw (@setUDl T) (@setUDr T).
+Canonical setI_add_monoid := AddLaw (@setIDl T) (@setIDr T).
+
+End SetMonoids.
+
+Lemma bigcup_ord T n (A : nat -> set T) :
+ \big[setU/set0]_(i < n) A i = \bigcup_(i in [set k | (k < n)%N]) A i.
+Proof.
+elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE; split => -[].
+rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
+  by move=> [A0|[i AS]]; [exists 0%N|exists i.+1].
+by move=> [[|i] Ai]; [left|right; exists i].
+Qed.
+
+Lemma bigcap_ord T n (A : nat -> set T) :
+ \big[setI/setT]_(i < n) A i = \bigcap_(i in [set k | (k < n)%N]) A i.
+Proof.
+elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE.
+rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
+  by move=> [A0 AS] [|i]// /AS.
+by move=> AP; split => [|i i_lt]; apply: AP.
+Qed.
+
 Module Pointed.
 
 Definition point_of (T : Type) := T.

theories/integral.v

@@ -426,73 +426,68 @@ Canonical ereal_topologicalType := TopologicalType _ ereal_topologicalMixin.
 
 End ereal_topologicalType.
 
-Lemma hausdorff_ereal (R : numFieldType) : hausdorff (ereal_topologicalType R).
+Lemma ereal_hausdorff (R : numFieldType) : hausdorff (ereal_topologicalType R).
 Proof.
 rewrite open_hausdorff.
 move=> -[x| |] // [y| |] //=.
 Admitted.
+Hint Resolve ereal_hausdorff.
 
 Section additivity.
 Variables (R : numFieldType) (X : Type) (mx : set X -> {ereal R}).
+Definition additive2 := forall A B, A `&` B = set0 -> mx (A `|` B) = (mx A + mx B)%E.
 Definition additive := forall A, triviset A -> forall n,
-  mx (\bigcup_(i in (fun k => (k <= n)%N)) A i) = (\sum_(i < n.+1) mx (A i))%E.
+  mx (\big[setU/set0]_(i < n.+1) A i) = (\sum_(i < n.+1) mx (A i))%E.
 Definition sigma_additive := forall A, triviset A ->
-  mx (\bigcup_n A n) = lim (fun n => (\sum_(i < n.+1) mx (A i))%E).
+  (fun n => (\sum_(i < n.+1) mx (A i))%E) --> mx (\bigcup_n A n).
 End additivity.
 
-Lemma additive2 (R : numFieldType) X (mx : set X -> {ereal R}) :
-  additive mx -> forall A B, A `&` B = set0 -> mx (A `|` B) = (mx A + mx B)%E.
+Lemma additive2P (R : numFieldType) X (mx : set X -> {ereal R}) :
+  additive mx <-> additive2 mx.
 Proof.
-move=> amx A B AB.
-set C := fun n => if n isn't n'.+1 then A else if n' is O then B else set0.
-rewrite (_ : _ `|` _ = \bigcup_(i in (fun k => (k <= 1)%N)) C i); last first.
-  rewrite funeqE => x; rewrite propeqE; split.
-  move=> -[Ax|Bx]; by [exists O | exists 1%nat].
-  move=> -[[/= _ ?|[|]]]; [by left | by right|by case].
-rewrite amx; last first.
-  move=> [[//|[_|_ _] /=]|].
-  by rewrite setIC.
-  by rewrite set0I.
-  move=> [|] /=; last by move=> *; rewrite setI0.
-  by move=> [//|[//|/= *]]; rewrite set0I.
-by rewrite 2!big_ord_recl /= big_ord0 adde0.
+split => [amx A B AB|a2mx A ATI n].
+  set C := fun n => if n isn't n'.+1 then A else if n' is O then B else set0.
+  have CTI : triviset C by move=> [|[|i]] [|[|j]]; rewrite ?set0I ?setI0// setIC.
+  by have := amx _ CTI 1%N; rewrite !big_ord_recl !big_ord0 adde0/= setU0.
+elim: n => [|n IHn] in A ATI *;
+  rewrite big_ord_recl [in RHS]big_ord_recl ?big_ord0 ?setU0 ?adde0//=.
+rewrite a2mx ?(IHn (fun i => A (bump 0 i)))//.
+  by move=> j i neq_ji; apply: ATI.
+by rewrite big_distrr /= big1// => i _; apply: ATI.
 Qed.
 
 Lemma sigma_additive_implies_additive (R : numFieldType) X (mx : set X -> {ereal R}) :
   mx set0 = 0%:E -> sigma_additive mx -> additive mx.
 Proof.
-move=> mx0 samx B Bset n; set B' := fun i => if (i <= n)%nat then B i else set0.
-transitivity (mx (\bigcup_i B' i)).
-  congr mx; rewrite funeqE => x; rewrite propeqE; split.
-  by move=> -[j jn] ?; exists j => //; rewrite /B' jn.
-  by move=> -[j _]; rewrite /B'; case: ifPn => // jn Bj; exists j.
-rewrite samx; last first.
-  move=> j i ij; rewrite /B' funeqE => x; rewrite propeqE; split => //.
-  move=> -[]; case : ifPn => // ni Bi; case: ifPn => // jn Bj.
-  by rewrite -(Bset j i).
-transitivity (\sum_(i < n.+1) mx (B' i))%E; last first.
-  by apply eq_bigr => i _; rewrite /B' -ltnS ltn_ord.
-apply/flim_lim; first exact/hausdorff_ereal.
-(*apply/(@flim_map_lim _ [normedModType R of R^o]).
-move=> /= s [e e0 es]; exists n.+1 => // m nm; apply es => /=.
-rewrite (_ : _ - _ = 0) ?normr0 //; apply/eqP; rewrite subr_eq0; apply/eqP.
-rewrite -(@big_mkord _ _ _ m.+1 xpredT (fun i => mx (B' i))).
-rewrite -(@subnKC n.+1 m.+1) 1?ltnW // /index_iota subn0 iota_add big_cat.
-rewrite -[in X in _ = X + _](subn0 n.+1) -/(index_iota 0 n.+1).
-rewrite big_mkord /= add0n [X in _ = _ + X]big1_seq ?addr0; last first.
-  move=> /= i; rewrite mem_iota subnKC; last exact/ltnW.
-  by move=> /andP[ni im]; rewrite /B' leqNgt ni /= mx0.
-by apply eq_bigr => i _; rewrite /B' -ltnS ltn_ord.
-Qed.*)
-Admitted.
+move=> mx0 samx; apply/additive2P => A B AB_eq0.
+set C := fun i => if (i == 0)%N then A else if (i == 1)%N then B else set0.
+have CTI : triviset C by move=> [|[|i]] [|[|j]]; rewrite ?setI0 ?set0I// setIC.
+have -> : A `|` B = \bigcup_i C i.
+  rewrite predeqE => x; split.
+    by case=> [Ax|Bx]; by [exists 0%N|exists 1%N].
+  by case=> [[|[|n]]]//; by [left|right].
+have /flim_unique := samx C CTI; apply => //.
+apply: flim_fconst; exists 2%N => // -[|n] _//.
+by rewrite !big_ord_recl/= big1 ?adde0.
+Qed.
 
 Section properties_of_measures.
 Variables (R : numFieldType) (X : measurableType) (mx : set X -> {ereal R}).
 Axiom measurable0 : mx set0 = 0%:E.
 Axiom measurable_ge0 : forall x, (0%:E <= mx x)%E.
 Axiom measurable_sigma_additive : sigma_additive mx.
+Hint Resolve measurable0 measurable_ge0 measurable_sigma_additive.
+
+Lemma measurable_additive : additive mx.
+Proof. exact: sigma_additive_implies_additive. Qed.
+Hint Resolve measurable_additive.
+
+Lemma measurable_additive2 : additive2 mx.
+Proof. exact/additive2P. Qed.
+
 End properties_of_measures.
 
+
 Lemma lee_addl (R : numDomainType) (x y : {ereal R}) : (0%:E <= y)%E ->  (x <= x + y)%E.
 Proof.
 by move: x y => -[ x [y| |]//= | [| |]// | [| | ]//]; rewrite !lee_fin ler_addl.
@@ -517,13 +512,9 @@ Proof.
 move=> A B AB; have {1}-> : B = A `|` (B `\` A).
   rewrite funeqE => x; rewrite propeqE.
   have [Ax|Ax] := pselect (A x).
-  split=> [Bx|]; by [left | move=> -[/AB //|] []].
-  split=> [Bx|]; by [right| move=> -[//|] []].
-rewrite additive2 // ?lee_addl //.
-exact: measurable_ge0.
-apply sigma_additive_implies_additive.
-exact: measurable0.
-exact: measurable_sigma_additive.
+    split=> [Bx|]; by [left | move=> -[/AB //|] []].
+  by split=> [Bx|]; by [right| move=> -[//|] []].
+rewrite measurable_additive2 ?lee_addl ?measurable_ge0//.
 rewrite setDE setICA (_ : _ `&` ~` _ = set0) ?setI0 //.
 by rewrite funeqE => x; rewrite propeqE; split => // -[].
 Qed.
@@ -563,16 +554,14 @@ have AB : \bigcup_(n in setT) A n = \bigcup_(n in setT) B n.
   rewrite funeqE => x; rewrite propeqE; split.
   by move=> -[n _]; rewrite AE => -[n' _] ?; exists n'.
   by move=> -[n _ ?]; exists n => //; rewrite AE; exists n.
-rewrite AB measurable_sigma_additive; last by move=> i j; exact: Binter.
+rewrite AB -(flim_lim _ (@measurable_sigma_additive _ _ _ _ _))//.
 rewrite (_ : (fun n => \sum_(i < n.+1) mx (B i))%E = mx \o A) //.
-rewrite funeqE => n; rewrite -sigma_additive_implies_additive // -?AE //.
-exact: measurable0.
-exact: measurable_sigma_additive.
+by rewrite funeqE => n; rewrite -measurable_additive// bigcup_ord -AE.
 Qed.
 
 (* measure satisfies Boole's inequality *)
 Lemma bool_le (A : nat -> set X) : forall n,
-  (mx (\bigcup_(i in (fun k => (k <= n)%N)) A i) <= \sum_(i < n.+1) mx (A i))%E.
+  (mx (\bigcup_(i in [set k | (k <= n)%N]) A i) <= \sum_(i < n.+1) mx (A i))%E.
 Proof.
 elim => [|n ih].
   rewrite big_ord_recl big_ord0 adde0 (_ : bigsetU _ _ = A O) //.
@@ -587,10 +576,7 @@ have -> : C = B `|` (A n.+1 `&` ~` B).
     by move=> jn Aj; left; exists j.
   move=> -[[j jn Aj]|]; first by exists j => //; rewrite ltnW.
   by move=> [An1 _]; exists n.+1.
-rewrite additive2; last 2 first.
-  apply sigma_additive_implies_additive.
-  exact: measurable0.
-  exact: measurable_sigma_additive.
+rewrite measurable_additive2; last first.
   rewrite setIC -setIA (_ : ~` _ `&` _ = set0) ?setI0 //.
   by rewrite funeqE => x; rewrite propeqE; split => // -[].
 rewrite (@le_trans _ _ (mx B + mx (A n.+1))%E) // ?lee_add2l //.

theories/topology.v

@@ -1030,6 +1030,14 @@ move=> eq_fg P /=; apply: filterS2 eq_fg => x eq_fg [y [fxy Py]].
 by exists y; rewrite -eq_fg.
 Qed.
 
+Lemma flim_near_const (T U : Type) (f : T -> U) (F : set (set T)) (G : set (set U)) :
+  Filter F -> ProperFilter G ->
+  (\forall y \near G, \forall x \near F, f x = y) -> f @ F --> G.
+Proof.
+move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G).
+by apply: filter_app fFG; near=> y => /=; apply: filterS => x /= ->; near: y.
+Grab Existential Variables. all: by end_near. Qed.
+
 (** ** Specific filters *)
 
 Section at_point.
@@ -1497,6 +1505,21 @@ Qed.
 Arguments cst_continuous {T T'} k F {FF}.
 Hint Resolve cst_continuous : core.
 
+Lemma flim_fconst (T : Type) (U : topologicalType)
+  (f : T -> U) (F : set (set T)) (l : U) :
+  Filter F ->
+  (\forall x \near F, f x = l) -> f @ F --> l.
+Proof.
+move=> FF fFl P /=; rewrite !near_simpl => Pl.
+by apply: filterS fFl => _ ->; apply: locally_singleton.
+Qed.
+
+Lemma flim_const (T : Type) (U : topologicalType) (F : set (set T)) {FF : Filter F}
+  (x : U) : (fun _ : T => x) @ F --> x.
+Proof. by apply: flim_fconst; near=> x0.
+Grab Existential Variables. all: end_near. Qed.
+Arguments flim_const {T U F FF} x.
+
 (** ** Topology defined by a filter *)
 
 Section TopologyOfFilter.
@@ -2665,21 +2688,13 @@ Lemma flimi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y :
   forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z].
 Proof. by move/flimi_ballP. Qed.
 
-Lemma flim_const {T} {F : set (set T)}
-   {FF : Filter F} (a : M) : a @[_ --> F] --> a.
-Proof.
-move=> P /locallyP[_ /posnumP[eps] subP]; rewrite !near_simpl /=.
-by apply: filterE=> ?; apply/subP/ballxx.
-Qed.
-
 Definition ball_set (A : set M) e := \bigcup_(p in A) ball p e.
 Canonical set_filter_source :=
   @Filtered.Source Prop _ M (fun A => locally_ ball_set A).
 
 End pseudoMetricType_numDomainType.
 Hint Resolve locally_ball : core.
 Hint Resolve close_refl : core.
-Arguments flim_const {R M T F FF} a.
 Arguments close_lim {T} F1 F2 {FF2} _.
 
 Section pseudoMetricType_numFieldType.