From 6b466dc75219ddb8f0ef4fdf22dd34c675bc77f9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Wed, 16 Mar 2022 20:14:49 +0100
Subject: [PATCH] Add Image/Preimage. WIP: add facts about Image/Preimage.
---
Lebesgue/measurable.v | 67 +++++++++++++++++++++++++++++++++++++++++--
1 file changed, 65 insertions(+), 2 deletions(-)
diff --git a/Lebesgue/measurable.v b/Lebesgue/measurable.v
index 74a631ea..261c0ceb 100644
--- a/Lebesgue/measurable.v
+++ b/Lebesgue/measurable.v
@@ -171,7 +171,7 @@ Qed.
End measurable_Facts.
-Section measurable_gen_Facts.
+Section measurable_gen_Facts1.
(** Properties of the "generation" of measurability. *)
@@ -237,7 +237,70 @@ Proof.
apply Sigma_algebra_gen_add_eq.
Qed.
-End measurable_gen_Facts.
+End measurable_gen_Facts1.
+
+
+Section measurable_gen_Image_Def.
+
+Context {E F : Type}. (* Universes. *)
+
+Variable f : E -> F.
+Variable PE : (E -> Prop) -> Prop. (* Subset system. *)
+Variable PF : (F -> Prop) -> Prop. (* Subset system. *)
+
+Definition Image : (F -> Prop) -> Prop := fun B => PE (preimage f B).
+
+Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
+
+End measurable_gen_Image_Def.
+
+
+Section measurable_gen_Facts2.
+
+Context {E F : Type}. (* Universes. *)
+Variable genE : (E -> Prop) -> Prop. (* Generator. *)
+Variable genF : (F -> Prop) -> Prop. (* Generator. *)
+
+Variable f : E -> F.
+
+Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE)).
+Proof.
+apply Sigma_algebra_equiv; repeat split.
+apply measurable_empty.
+intros B HB; apply measurable_compl; easy.
+intros B HB; apply measurable_union_seq; easy.
+Qed.
+
+Lemma is_Sigma_algebra_Preimage :
+ is_Sigma_algebra (Preimage f (measurable genF)).
+Proof.
+apply Sigma_algebra_equiv; repeat split.
+(* *)
+exists emptyset; split.
+apply measurable_empty.
+symmetry; apply preimage_emptyset.
+(* *)
+intros A [B HB]; exists (compl B); split.
+apply measurable_compl; easy.
+rewrite preimage_compl; f_equal; easy.
+(* *)
+intros A HA.
+unfold image in HA.
+destruct (ClassicalChoice.choice
+ (fun n Bn => measurable genF Bn /\ A n = preimage f Bn) HA) as [B HB].
+exists (union_seq B); split.
+apply measurable_union_seq; intros n; apply HB.
+rewrite preimage_union_seq; f_equal.
+apply subset_seq_ext.
+intros n; rewrite (proj2 (HB n)); easy.
+Qed.
+
+Lemma measurable_gen_Preimage :
+ measurable (Preimage f genF) = Preimage f (measurable genF).
+Proof.
+Admitted.
+
+End measurable_gen_Facts2.
Section measurable_correct.
--
GitLab