WIP: measurable subspace.

Lebesgue/Subset_system_base.v

@@ -14,6 +14,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
+From Coq Require Import ClassicalChoice.
 From Coq Require Import Arith Lia.
 
 Require Import logic_compl nat_compl.
@@ -185,6 +186,22 @@ Definition Union_disj : Prop :=
 End Base_Def.
 
 
+Section Trace_Def.
+
+Context {U : Type}. (* Universe. *)
+
+Variable P : (U -> Prop) -> Prop. (* Subset system. *)
+Variable V : U -> Prop. (* Subset. *)
+
+(* Definition 226 p. 40 (v3) *)
+(* Next definition is not satisfactory!
+ We need a subset of the power set of V, not U... *)
+Definition Trace : (U -> Prop) -> Prop :=
+  fun A => exists B, P B /\ A = inter B V.
+
+End Trace_Def.
+
+
 Section Prod_Def.
 
 Context {U1 U2 : Type}. (* Universes. *)
@@ -427,6 +444,29 @@ Global Hint Resolve -> Union_Inter_equiv : base_facts.
 (*Print HintDb base_facts.*)
 
 
+Section Trace_Facts1.
+
+Context {U : Type}. (* Universe. *)
+
+Variable P : (U -> Prop) -> Prop. (* Subset system. *)
+Variable V : U -> Prop. (* Subset. *)
+
+Lemma Trace_wEmpty : wEmpty P -> wEmpty (Trace P V).
+Proof.
+intros HP; exists emptyset; split; try easy.
+rewrite inter_empty_l; easy.
+Qed.
+
+(* The above definition of Trace does not allow to prove next lemma... *)
+Lemma Trace_Compl : Compl P -> Compl (Trace P V).
+Proof.
+intros HP A [B [HB HA]]; exists (compl B); rewrite HA; split; try auto.
+(* rewrite compl_inter. is wrong! the left compl is actually in V! *)
+Abort.
+
+End Trace_Facts1.
+
+
 Section Prod_Facts.
 
 Context {U1 U2 : Type}. (* Universes. *)
@@ -1232,6 +1272,26 @@ End Seq_Facts2.
 *)
 
 
+Section Trace_Facts2.
+
+Context {U : Type}. (* Universe. *)
+
+Variable P : (U -> Prop) -> Prop. (* Subset system. *)
+Variable V : U -> Prop. (* Subset. *)
+
+Lemma Trace_Union_seq : Union_seq P -> Union_seq (Trace P V).
+Proof.
+intros HP A HA.
+destruct (choice (fun n Bn => P Bn /\ A n = inter Bn V) HA) as [B HB].
+exists (union_seq B); split.
+apply HP; intros; apply HB.
+rewrite distrib_inter_union_seq_r; f_equal.
+apply subset_seq_ext; intros n; rewrite (proj2 (HB n)); easy.
+Qed.
+
+End Trace_Facts2.
+
+
 Section Any_Def.
 
 (** Uncountable operations. *)

Lebesgue/measurable.v

@@ -379,6 +379,27 @@ Qed.
 End measurable_gen_Image_Facts3.
 
 
+Section measurable_subspace.
+
+Context {E : Type}. (* Universe. *)
+
+Variable P : (E -> Prop) -> Prop. (* Subset system. *)
+
+Lemma measurable_subspace :
+  forall F, is_Sigma_algebra P -> is_Sigma_algebra (Trace P F).
+Proof.
+intros F; rewrite 2!Sigma_algebra_equiv; intros HP; repeat split.
+(* *)
+apply Trace_wEmpty; easy.
+(* *)
+
+
+
+Admitted.
+
+End measurable_subspace.
+
+
 Section Cartesian_product_def.
 
 Context {E1 E2 : Type}. (* Universes. *)