WIP: new implementation.

Lebesgue/measurable_fun-new.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** References to pen-and-paper statements are from RR-9386,
+ https://hal.inria.fr/hal-03105815/
+
+ In version 2 (v2), this file refers to Section 9.2 (pp. 93-94).
+ In version 3 (v3), this file refers to Section 9.2 (pp. 130-132).
+
+ Some proof paths may differ. *)
+
+(*From Coquelicot Require Import Coquelicot.*)
+
+Require Import Subset Subset_dec Subset_system_base measurable.
+
+Open Scope nat_scope.
+
+
+Section compl1.
+
+Context {E F : Type}. (* Universes. *)
+
+Variable f : E -> F. (* Function. *)
+Variable AE : E -> Prop. (* Subset. *)
+Variable AF : F -> Prop. (* Subset. *)
+
+Inductive image : F -> Prop := Im : forall x, AE x -> image (f x).
+
+Definition preimage : E -> Prop := fun x => AF (f x).
+
+End compl1.
+
+
+Section compl2.
+
+Context {E F : Type}. (* Universes. *)
+
+Variable f : E -> F. (* Function. *)
+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 AF => PE (preimage f AF).
+
+(* From Lemma 523 p. 93 (v2) *)
+Definition Preimage : (E -> Prop) -> Prop := image (preimage f) PF.
+
+End compl2.
+
+
+Section Measurable_fun_Def.
+
+Context {E F : Type}.
+Variable genE : (E -> Prop) -> Prop.
+Variable genF : (F -> Prop) -> Prop.
+
+(* Definition 522 p. 93 (v2) *)
+Definition measurable_fun : (E -> F) -> Prop :=
+  fun f => Incl (Preimage f (measurable genF)) (measurable genE).
+
+Lemma measurable_fun_ext :
+  forall f g, same_fun f g -> measurable_fun f -> measurable_fun g.
+Proof.
+intros f g H Hf AE HAE; induction HAE as [AF HAF].
+rewrite <- (preimage_ext_fun f); try easy.
+
+
+intros f g H Hf A [B HB]; rewrite (proj2 HB); apply Hf.
+exists B; split; try easy.
+apply preimage_ext_fun; easy.
+Qed.
+
+(* Lemma 526 p. 93 (v2) *)
+Lemma measurable_fun_cst : forall y, measurable_fun (fun _ => y).
+Proof.
+intros y A [B HB]; destruct (in_dec B y). ; apply measurable_Prop.
+Qed.
+
+(* Lemma 528 p. 94 *)
+Lemma measurable_fun_gen :
+  forall f,
+    measurable_fun f <->
+    (forall A, genF A -> measurable genE (fun x => A (f x))).
+Proof.
+intros f; split; intros H1.
+intros A HA.
+apply H1; apply measurable_gen; easy.
+intros A HA.
+induction HA.
+apply H1; easy.
+apply measurable_empty.
+apply measurable_compl; easy.
+apply measurable_union_countable; easy.
+Qed.
+End Measurable_fun_def.
+
+Section Measurable_fun_equiv.
+
+Context {E : Type}.
+Context {F : Type}.
+Variable genE : (E -> Prop) -> Prop.
+Variable genF : (F -> Prop) -> Prop.
+
+Lemma measurable_fun_gen_ext1 :
+  forall genE' : (E -> Prop) -> Prop,
+    (forall A, genE A -> measurable genE' A) ->
+    (forall A, genE' A -> measurable genE A) ->
+    forall f, measurable_fun genE genF f <-> measurable_fun genE' genF f.
+Proof.
+intros genE' H1 H2 f; split; intros Hf A HA.
+rewrite <- (measurable_gen_ext _ _ H1 H2).
+now apply Hf.
+rewrite (measurable_gen_ext _ _ H1 H2).
+now apply Hf.
+Qed.
+
+Lemma measurable_fun_gen_ext2 :
+  forall genF' : (F -> Prop) -> Prop,
+    (forall A, genF A -> measurable genF' A) ->
+    (forall A, genF' A -> measurable genF A) ->
+    forall f, measurable_fun genE genF f <-> measurable_fun genE genF' f.
+Proof.
+intros genF' H1 H2 f.
+generalize (measurable_gen_ext _ _ H1 H2); intros H.
+split; intros Hf A HA.
+rewrite <- H in HA; now apply Hf.
+rewrite H in HA; now apply Hf.
+Qed.
+
+End Measurable_fun_equiv.
+
+
+Section Measurable_fun_composition.
+
+Context {E F G : Type}.
+Variable genE : (E -> Prop) -> Prop.
+Variable genF : (F -> Prop) -> Prop.
+Variable genG : (G -> Prop) -> Prop.
+
+(* Lemma 530 p. 94 *)
+Lemma measurable_fun_composition :
+  forall (f1 : E -> F) (f2 : F -> G),
+    measurable_fun genE genF f1 ->
+    measurable_fun genF genG f2 ->
+    measurable_fun genE genG (fun x => f2 (f1 x)).
+Proof.
+intros f1 f2 H1 H2 A HA.
+apply H1 with (A:= fun x => A (f2 x)).
+now apply H2.
+Qed.
+
+End Measurable_fun_composition.
+
+
+Section Measurable_fun_swap.
+
+Context {E1 E2 F : Type}.
+
+Context {genE1 : (E1 -> Prop) -> Prop}.
+Context {genE2 : (E2 -> Prop) -> Prop}.
+Context {genF : (F -> Prop) -> Prop}.
+
+Let genE1xE2 := Gen_Product genE1 genE2.
+Let genE2xE1 := Gen_Product genE2 genE1.
+
+Let swap_var := swap (fun x : E1 * E2 => x).
+
+Lemma measurable_fun_swap_var :
+  measurable_fun genE2xE1 genE1xE2 swap_var.
+Proof.
+intros A HA; apply measurable_swap; easy.
+Qed.
+
+Lemma measurable_fun_swap :
+  forall f, measurable_fun genE1xE2 genF f -> measurable_fun genE2xE1 genF (swap f).
+Proof.
+intros f Hf.
+apply measurable_fun_composition with (2:= Hf).
+apply measurable_fun_swap_var.
+Qed.
+
+End Measurable_fun_swap.
+
+
+Section Measurable_fun_continuous.
+
+Context {E F : UniformSpace}.
+
+(* Lemma 529 p. 94 *)
+Lemma measurable_fun_continuous :
+  forall (f : E -> F),
+    (forall x, continuous f x) ->
+    measurable_fun open open f.
+Proof.
+intros f H.
+apply measurable_fun_gen.
+intros A HA.
+apply measurable_gen.
+intros x Hx.
+apply H.
+now apply HA.
+Qed.
+
+End Measurable_fun_continuous.