measurable.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

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.
*)

From Coq Require Import ClassicalDescription.
(*From Coq Require Import PropExtensionality FunctionalExtensionality.*)
From Coquelicot Require Import Hierarchy.

Require Import Subset Subset_finite Subset_seq.
Require Import Subset_system_base Subset_system_gen Subset_system.


Section measurable_Facts.

Context {E : Type}.
Variable genE : (E -> Prop) -> Prop.

(* From Definitions 474 p. 84 and 482 p. 85 *)
Definition measurable : (E -> Prop) -> Prop := Sigma_algebra genE.

Lemma measurable_ext :
  forall A1 A2, same A1 A2 -> measurable A1 -> measurable A2.
Proof.
intros A1 A2 H H1; apply subset_ext in H; now rewrite <- H.
Qed.

Lemma measurable_gen : forall A, genE A -> measurable A.
  (* Incl genE measurable. *)
Proof.
apply Sigma_algebra_Gen.
Qed.

Lemma measurable_empty : measurable emptyset.
(* wEmpty measurable. *)
Proof.
apply Sigma_algebra_wEmpty.
Qed.

(* From Lemma 475 p. 84 *)
Lemma measurable_full : measurable fullset.
(* wFull measurable. *)
Proof.
apply Sigma_algebra_wFull.
Qed.

Lemma measurable_Prop : forall P, measurable (fun _ => P).
Proof.
intros P; case (excluded_middle_informative P); intros HP.
now apply measurable_ext with (2:=measurable_full).
now apply measurable_ext with (2:=measurable_empty).
Qed.

Lemma measurable_compl :
  forall A, measurable A -> measurable (compl A).
  (* Compl measurable. *)
Proof.
apply Sigma_algebra_Compl.
Qed.

Lemma measurable_compl_rev :
  forall A, measurable (compl A) -> measurable A.
  (* Compl_rev measurable. *)
Proof.
apply Sigma_algebra_Compl_rev.
Qed.

Lemma measurable_union :
  forall A1 A2, measurable A1 -> measurable A2 -> measurable (union A1 A2).
  (* Union measurable. *)
Proof.
apply Sigma_algebra_Union.
Qed.

Lemma measurable_inter :
  forall A1 A2, measurable A1 -> measurable A2 -> measurable (inter A1 A2).
  (* Inter measurable. *)
Proof.
apply Sigma_algebra_Inter.
Qed.

Lemma measurable_union_finite :
  forall A N,
    (forall n, (n < S N)%nat -> measurable (A n)) ->
    measurable (union_finite A N).
  (* Union_finite measurable. *)
Proof.
apply Sigma_algebra_Union_finite.
Qed.

Lemma measurable_inter_finite :
  forall A N,
    (forall n, (n < S N)%nat -> measurable (A n)) ->
    measurable (inter_finite A N).
  (* Inter_finite measurable. *)
Proof.
apply Sigma_algebra_Inter_finite.
Qed.

Lemma measurable_union_seq :
  forall A, (forall n, measurable (A n)) -> measurable (union_seq A).
  (* Union_seq measurable. *)
Proof.
apply Sigma_algebra_Union_seq.
Qed.

(* From Lemma 475 p. 84 *)
Lemma measurable_inter_seq :
  forall A, (forall n, measurable (A n)) -> measurable (inter_seq A).
  (* Inter_seq measurable. *)
Proof.
apply Sigma_algebra_Inter_seq.
Qed.

Lemma measurable_diff :
  forall A1 A2, measurable A1 -> measurable A2 -> measurable (diff A1 A2).
  (* Diff measurable. *)
Proof.
apply Sigma_algebra_Diff.
Qed.

(* From Lemma 480 pp. 84-85 *)
Lemma measurable_DU :
  forall A, (forall n, measurable (A n)) -> forall n, measurable (DU A n).
Proof.
intros A HA n; destruct n; simpl; try easy.
apply measurable_diff; try easy.
now apply measurable_union_finite.
Qed.

End measurable_Facts.


Section measurable_gen_Facts.

Context {E : Type}.
Variable genE : (E -> Prop) -> Prop.

(* Lemma 501 p. 87 *)
Lemma measurable_gen_ext :
  forall genE',
    Incl genE (measurable genE') -> Incl genE' (measurable genE) ->
    measurable genE = measurable genE'.
Proof.
apply Sigma_algebra_ext.
Qed.

Lemma measurable_gen_add :
  forall A B,
    measurable genE A -> measurable genE B ->
    measurable (add genE A) B.
Proof.
intros A B HA HB; induction HB as [B HB | | B HB | B HB1 HB2].
now apply measurable_gen, union_ub_l.
apply measurable_empty.
now apply measurable_compl.
now apply measurable_union_seq.
Qed.

(* From Lemma 502 p. 87 *)
Lemma measurable_gen_remove :
  forall A B,
    measurable genE A -> measurable (add genE A) B ->
    measurable genE B.
Proof.
intros A B HA HB; induction HB as [C HC1 | | B HB | B HB1 HB2].
case HC1; intros HC2; [now apply measurable_gen | now rewrite HC2].
apply measurable_empty.
now apply measurable_compl.
now apply measurable_union_seq.
Qed.

End measurable_gen_Facts.


Section measurable_correct.

Context {E : Type}.

(* Lemma 485 p. 85 *)
Lemma is_Sigma_algebra_correct :
  forall calS : (E -> Prop) -> Prop,
    is_Sigma_algebra calS <-> wEmpty calS /\ Compl calS /\ Union_seq calS.
Proof.
exact Sigma_algebra_equiv.
Qed.

Lemma measurable_idem :
  forall genE : (E -> Prop) -> Prop, is_Sigma_algebra (measurable genE).
Proof.
exact Sigma_algebra_idem.
Qed.

Lemma measurable_correct :
  forall P : ((E -> Prop) -> Prop) -> Prop,
    IIncl is_Sigma_algebra P <-> forall gen, P (measurable gen).
Proof.
intros P; split.
intros HP gen; apply HP, measurable_idem.
intros HP calS HcalS; rewrite <- HcalS; apply HP.
Qed.

Lemma is_sigma_algebra_trivial :
  is_Sigma_algebra (pair (@emptyset E) fullset).
Proof.
apply Ext_equiv; split; try apply Sigma_algebra_Gen.
intros A HA; induction HA as [ | | A HA1 HA2 | A HA1 HA2]; try easy.
now left.
(* *)
destruct HA2 as [HA2 | HA2].
right; rewrite HA2; apply compl_empty.
left; rewrite HA2; apply compl_full.
(* *)
case (excluded_middle_informative (exists n, A n = fullset)); intros H.
right; now apply union_seq_full.
left; apply empty_union_seq; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy.
contradict H; now exists n.
Qed.

Lemma is_Sigma_algebra_discrete : is_Sigma_algebra (@fullset (E -> Prop)).
Proof.
apply Ext_equiv; split; try easy.
apply Sigma_algebra_Gen.
Qed.

End measurable_correct.


Section Borel_subsets.

Context {E : UniformSpace}.

Definition measurable_Borel := @measurable E open.

(* From Lemma 518 p. 91 *)
Lemma measurable_Borel_closed : Incl closed measurable_Borel.
Proof.
intros A HA; now apply measurable_compl_rev, measurable_gen, open_not.
Qed.

(* Lemma 519 pp. 91-92 *)
Lemma measurable_Borel_gen :
  forall genE : (E -> Prop) -> Prop,
    Incl genE open -> Incl open (Union_seq_closure genE) ->
    measurable genE = measurable_Borel.
Proof.
intros genE H1 H2; apply measurable_gen_ext; intros A H3.
now apply measurable_gen, H1.
destruct (H2 A H3) as [B [HB1 HB2]].
rewrite HB2; apply measurable_union_seq.
intros n; apply measurable_gen, HB1.
Qed.

End Borel_subsets.


Section Cartesian_product_def.

Context {E1 E2 : Type}.
Variable genE1 : (E1 -> Prop) -> Prop.
Variable genE2 : (E2 -> Prop) -> Prop.

Definition measurable_Prod := measurable (Prod_Sigma_algebra genE1 genE2).

(* From Lemma 546 p. 99 (case m=2) *)
Definition Gen_Prod : (E1 * E2 -> Prop) -> Prop :=
  Prod (add genE1 fullset) (add genE2 fullset).

End Cartesian_product_def.


Section Cartesian_product_Facts1.

Context {E1 E2 : Type}.
Variable genE1 : (E1 -> Prop) -> Prop.
Variable genE2 : (E2 -> Prop) -> Prop.

Let genE1xE2 := Gen_Prod genE1 genE2.
Let genE2xE1 := Gen_Prod genE2 genE1.

(* From Lemma 542 p. 98 (case m=2) *)
Lemma measurable_prod :
  forall A1 A2,
    measurable genE1 A1 -> measurable genE2 A2 ->
    measurable_Prod genE1 genE2 (prod A1 A2).
Proof.
intros; apply measurable_gen; now exists A1, A2.
Qed.

Lemma measurable_Prod_equiv :
  measurable genE1xE2 = measurable_Prod genE1 genE2.
Proof.
apply measurable_gen_ext; intros A [A1 [A2 [H1 [H2 H3]]]].
(* *)
apply measurable_gen; exists A1, A2; repeat split; try easy.
destruct H1 as [H1 | H1].
now apply Sigma_algebra_Gen.
rewrite H1; apply Sigma_algebra_wFull.
destruct H2 as [H2 | H2].
now apply Sigma_algebra_Gen.
rewrite H2; apply Sigma_algebra_wFull.
(* *)
rewrite H3; clear H3 A; apply measurable_inter.
(* . *)
induction H1 as [A1 H1 | | A1 H1 K1 | A1 H1 K1].
apply measurable_gen; exists A1, fullset; repeat split.
now apply add_incl.
apply add_in.
now rewrite prod_fullset_r.
apply measurable_empty.
rewrite <- prod_fullset_r.
apply measurable_compl_rev.
now rewrite prod_compl_union, compl_invol, compl_full,
    prod_emptyset_r, union_empty_r, prod_fullset_r.
now apply measurable_union_seq.
(* . *)
induction H2 as [A2 H2 | | A2 H2 K2 | A2 H2 K2].
apply measurable_gen; exists fullset, A2; repeat split.
apply add_in.
now apply add_incl.
now rewrite prod_fullset_l.
apply measurable_empty.
rewrite <- prod_fullset_l.
apply measurable_compl_rev.
now rewrite prod_compl_union, compl_invol, compl_full,
    prod_emptyset_l, union_empty_l, prod_fullset_l.
now apply measurable_union_seq.
Qed.

Definition swap_var : E2 * E1 -> E1 * E2 := fun x => (snd x, fst x).

Definition swap : forall {F : Type}, (E1 * E2 -> F) -> E2 * E1 -> F :=
  fun F f x => f (swap_var x).

Lemma measurable_swap :
  forall A, measurable genE1xE2 A -> measurable genE2xE1 (swap A).
Proof.
intros A HA.
induction HA.
apply measurable_gen.
destruct H as [A1 [A2 [H1 [H2 H3]]]].
exists A2; exists A1.
split; try easy.
split; try easy.
unfold swap; rewrite H3; apply subset_ext; subset_auto.
apply measurable_empty.
now apply measurable_compl.
now apply measurable_union_seq.
Qed.

End Cartesian_product_Facts1.


(* WIP.
Section Cartesian_product_Facts2.

Context {E F : Type}.
Variable genE1 genE1' : (E -> Prop) -> Prop.
Variable genE2 genE2' : (F -> Prop) -> Prop.

Let genE1xE2 := Gen_Prod genE1 genE2.
Let genE1'xE2' := Gen_Prod genE1' genE2'.

Lemma measurable_Gen_Product_equiv_aux1 :
  (forall A, measurable genE1 A <-> measurable genE1' A) ->
  (forall A, measurable genE2 A <-> measurable genE2' A) ->
  forall A, genE1xE2 A -> measurable genE1'xE2' A.
Proof.
(*
intros H1 H2 A (A1,(A2,(K1,(K2,K3)))).
apply measurable_ext with (fun X => A1 (fst X) /\ A2 (snd X)).
intros; split; apply K3.
apply measurable_inter.
assert (L1:measurable genE1' A1).
case K1; intros K1'.
apply H1.
apply measurable_gen; easy.
rewrite K1'; apply measurable_full.
clear -L1.
induction L1.
apply measurable_gen.
exists A; exists (fun _ => True).
split; try easy.
left; easy.
split; try easy.
right; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
(* *)
assert (L1:measurable genE2' A2).
case K2; intros K2'.
apply H2.
apply measurable_gen; easy.
rewrite K2'; apply measurable_full.
clear -L1.
induction L1.
apply measurable_gen.
exists (fun _ => True); exists A.
split; try easy.
right; easy.
split; try easy.
left; easy.
apply measurable_empty.
apply measurable_compl; easy.
apply measurable_union_countable; easy.
Qed.
*)
Aglopted.

Lemma measurable_Gen_Product_equiv_aux2 :
  (forall A, measurable genE1 A <-> measurable genE1' A) ->
  (forall A, measurable genE2 A <-> measurable genE2' A) ->
  forall A, measurable genE1xE2 A -> measurable genE1'xE2' A.
Proof.
intros H1 H2 A HA.
induction HA.
apply measurable_Gen_Product_equiv_aux1; try easy.
apply measurable_empty.
now apply measurable_compl.
now apply measurable_union_seq.
Qed.

End Cartesian_product_Facts2.


Section Cartesian_product_Facts3.

Context {E F : Type}.
Variable genE1 genE1' : (E -> Prop) -> Prop.
Variable genE2 genE2' : (F -> Prop) -> Prop.

Let genE1xE2 := Gen_Prod genE1 genE2.
Let genE1'xE2' := Gen_Prod genE1' genE2'.

Lemma measurable_Gen_Product_equiv :
  (forall A, measurable genE1 A <-> measurable genE1' A) ->
  (forall A, measurable genE2 A <-> measurable genE2' A) ->
  forall A, measurable genE1xE2 A <-> measurable genE1'xE2' A.
Proof.
intros; split; now apply measurable_Gen_Product_equiv_aux2.
Qed.

End Cartesian_product_Facts3.
*)