Add and move references to RR-9386.

Lebesgue/Subset_system.v

@@ -77,7 +77,8 @@ Inductive Sigma_ring : (U -> Prop) -> Prop :=
   | Sigma_ring_Union_seq : Union_seq Sigma_ring.
 
 (* Sigma_algebra is the sigma-algebra generated by gen,
- ie the smallest sigma-algebra containing gen. *)
+ ie the smallest sigma-algebra containing gen.
+ From Definitions 474 p. 84 and 482 p. 85 (v2) *)
 Inductive Sigma_algebra : (U -> Prop) -> Prop :=
   | Sigma_algebra_Gen : Incl gen Sigma_algebra
   | Sigma_algebra_wEmpty : wEmpty Sigma_algebra
@@ -532,6 +533,7 @@ Proof.
 intros; apply Ext_equiv; split; now apply Lsyst_lub_alt.
 Qed.
 
+(* Lemma 501 p. 87 (v2) *)
 Lemma Sigma_algebra_ext :
   Incl gen0 (Sigma_algebra gen1) ->
   Incl gen1 (Sigma_algebra gen0) ->
@@ -1624,6 +1626,7 @@ apply Sigma_algebra_Compl.
 apply Sigma_algebra_Union.
 Qed.
 
+(* From Lemma 475 p. 84 (v2) *)
 Lemma Sigma_algebra_wFull :
   wFull (Sigma_algebra gen).
 Proof.
@@ -1696,6 +1699,7 @@ Proof.
 rewrite <- Sigma_algebra_is_Algebra; apply Algebra_Union_disj_finite.
 Qed.
 
+(* From Lemma 475 p. 84 (v2) *)
 Lemma Sigma_algebra_Inter_seq :
   Inter_seq (Sigma_algebra gen).
 Proof.
@@ -1722,6 +1726,7 @@ Proof.
 apply Union_seq_disj, Sigma_algebra_Union_seq.
 Qed.
 
+(* From Lemma 502 p. 87 (v2) *)
 Lemma Sigma_algebra_gen_remove :
   forall A, Sigma_algebra gen A ->
     Incl (Sigma_algebra (add gen A)) (Sigma_algebra gen).

Lebesgue/measurable.v

@@ -39,7 +39,6 @@ Section measurable_Facts.
 Context {E : Type}. (* Universe. *)
 Variable genE : (E -> Prop) -> Prop. (* Generator. *)
 
-(* From Definitions 474 p. 84 and 482 p. 85 *)
 Definition measurable : (E -> Prop) -> Prop := Sigma_algebra genE.
 
 Definition measurable_finite : (nat -> E -> Prop) -> nat -> Prop :=
@@ -73,7 +72,6 @@ Proof.
 apply Sigma_algebra_wEmpty.
 Qed.
 
-(* From Lemma 475 p. 84 *)
 Lemma measurable_full : measurable fullset. (* wFull measurable. *)
 Proof.
 apply Sigma_algebra_wFull.
@@ -133,7 +131,6 @@ Proof.
 apply Sigma_algebra_Union_seq.
 Qed.
 
-(* From Lemma 475 p. 84 *)
 Lemma measurable_inter_seq :
   forall A, measurable_seq A -> measurable (inter_seq A).
   (* Inter_seq measurable. *)
@@ -155,7 +152,7 @@ intros A N HA n Hn; apply measurable_union_finite.
 intros m Hm; apply HA; lia.
 Qed.
 
-(* From Lemma 480 pp. 84-85 *)
+(* From Lemma 480 pp. 84-85 (v2) *)
 Lemma measurable_DU :
   forall A, measurable_seq A -> measurable_seq (DU A).
 Proof.
@@ -164,11 +161,6 @@ apply measurable_diff; try easy.
 now apply measurable_union_finite.
 Qed.
 
-Lemma measurable_gen : Incl genE measurable.
-Proof.
-apply Sigma_algebra_Gen.
-Qed.
-
 End measurable_Facts.
 
 
@@ -179,6 +171,11 @@ Section measurable_gen_Facts1.
 Context {E : Type}. (* Universe. *)
 Variable genE : (E -> Prop) -> Prop. (* Generator. *)
 
+Lemma measurable_gen : Incl genE (measurable genE).
+Proof.
+apply Sigma_algebra_Gen.
+Qed.
+
 Lemma measurable_gen_idem : is_Sigma_algebra (measurable genE).
 Proof.
 apply Sigma_algebra_idem.
@@ -203,7 +200,6 @@ Proof.
 apply Sigma_algebra_lub_alt.
 Qed.
 
-(* Lemma 501 p. 87 *)
 Lemma measurable_gen_ext :
   forall genE',
     Incl genE (measurable genE') -> Incl genE' (measurable genE) ->
@@ -212,7 +208,6 @@ Proof.
 apply Sigma_algebra_ext.
 Qed.
 
-(* From Lemma 502 p. 87 *)
 Lemma measurable_gen_remove :
   forall A, measurable genE A ->
     Incl (measurable (add genE A)) (measurable genE).
@@ -249,8 +244,10 @@ Variable f : E -> F.
 Variable PE : (E -> Prop) -> Prop. (* Subset system. *)
 Variable PF : (F -> Prop) -> Prop. (* Subset system. *)
 
+(* From Lemma 524 p. 93 (v2) *)
 Definition Image : (F -> Prop) -> Prop := fun B => PE (preimage f B).
 
+(* From Lemma 523 p. 93 (v2) *)
 Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
 
 End measurable_gen_Image_Def.
@@ -311,6 +308,7 @@ Variable genF : (F -> Prop) -> Prop. (* Generator. *)
 
 Variable f : E -> F.
 
+(* Lemma 524 p. 93 (v2) *)
 Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE)).
 Proof.
 apply Sigma_algebra_equiv; repeat split.
@@ -319,6 +317,7 @@ intros B HB; apply measurable_compl; easy.
 intros B HB; apply measurable_union_seq; easy.
 Qed.
 
+(* Lemma 523 p. 93 (v2) *)
 Lemma is_Sigma_algebra_Preimage :
   is_Sigma_algebra (Preimage f (measurable genF)).
 Proof.
@@ -354,6 +353,7 @@ Variable genF : (F -> Prop) -> Prop. (* Generator. *)
 
 Variable f : E -> F.
 
+(* Lemma 527 pp. 93-94 (v2) *)
 Lemma measurable_gen_Preimage :
   measurable (Preimage f genF) = Preimage f (measurable genF).
 Proof.
@@ -474,8 +474,10 @@ Section Borel_subsets.
 
 Context {E : UniformSpace}. (* Uniform universe. *)
 
+(* Definition 517 p. 91 (v2) *)
 Definition measurable_Borel := measurable (@open E).
 
+(* From Lemma 518 p. 91 *)
 Lemma measurable_Borel_open : Incl open measurable_Borel.
 Proof.
 intros A HA; now apply measurable_gen.
@@ -515,6 +517,7 @@ Context {E F : UniformSpace}. (* Uniform universes. *)
 
 Let genExF := Gen_Prod (@open E) (@open F).
 
+(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
 Lemma measurable_Borel_prod_incl : Incl (measurable genExF) measurable_Borel.
 Proof.
 apply measurable_gen_monot.
@@ -537,6 +540,7 @@ Let genE1xE2 := Gen_Prod (@open E1) (@open E2).
 Hypothesis HE1 : is_second_countable E1.
 Hypothesis HE2 : is_second_countable E2.
 
+(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
 Lemma measurable_Borel_prod_incl_alt :
   Incl measurable_Borel (measurable genE1xE2).
 Proof.
@@ -554,7 +558,7 @@ apply measurable_Prop.
 apply measurable_prod; apply measurable_gen; easy.
 Qed.
 
-(* From Lem 701 p. 135,136 (RR-9386-v3) (with m := 2 and Y_i := X_i). *)
+(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
 Lemma measurable_Borel_prod_eq : measurable_Borel = measurable genE1xE2.
 Proof.
 intros; apply Ext_equiv; split.
@@ -562,7 +566,7 @@ apply measurable_Borel_prod_incl_alt; easy.
 apply measurable_Borel_prod_incl.
 Qed.
 
-(* From Lem 701 p. 135,136 (RR-9386-v3) (with m := 2 and Y_i := X_i). *)
+(* From Lemma 711 p. 137 (v3) (with m := 2 and Y_i := X_i). *)
 Lemma measurable_Borel_prod_eq_alt :
   measurable_Borel = measurable_Prod (@open E1) (@open E2).
 Proof.