(* THIS IS A DRAFT !!!! Ceci est un Brouillon. *)

Require Import Reals.
Require Export Ensembles.

Open Scope R_scope.

Ltac casser_les_cailloux :=
 match goal with
| [ id: ex _ |- _] => inversion_clear id; casser_les_cailloux
| [id: _ /\ _ |- _] => inversion_clear id; casser_les_cailloux
| [id: _ <-> _ |- _] => inversion_clear id; casser_les_cailloux
| [|- _ ] => idtac
end.


(* D'abord, quelques lemmes triviaux. *)

Module Trivial_Ensembles.

Lemma Fonct_intersection : forall (U : Type) (A B : Ensemble U),
Intersection U A B = (fun x => A x /\ B x)
.
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H.
intuition.
compute.
intuition.
apply Intersection_intro.
trivial.
trivial.
Qed.

Lemma Fonct_union : forall (U : Type) (A B : Ensemble U),
Union U A B = (fun x => A x \/ B x)
.
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H.
intuition.
intuition.
compute.
intuition.
apply Union_introl.
trivial.
apply Union_intror.
trivial.
Qed.


Lemma Refl_incl : forall (U : Type) (A : Ensemble U),
Included U A A.
intros.
unfold Included.
trivial.
Qed.

Lemma Antisym_incl : forall (U : Type) (A B : Ensemble U),
Included U A B ->
Included U B A ->
A = B.
intros.
apply Extensionality_Ensembles.
split.
trivial.
trivial.
Qed.

Lemma Trans_incl :  forall (U : Type) (A B C : Ensemble U),
Included U A B ->
Included U B C ->
Included U A C.
intros.
unfold Included.
intros.
apply H0.
apply H.
trivial.
Qed.

Lemma Trans_in_incl : forall (U : Type) (A B : Ensemble U) (x : U),
In U A x ->
Included U A B ->
In U B x.
intros.
apply H0.
trivial.
Qed.

Lemma Full_set_is_true : forall (U : Type),
Full_set U = fun _ => True.
intros.
apply Extensionality_Ensembles.
split.
compute.
trivial.
compute.
intros.
apply Full_intro.
Qed.

Lemma Empty_set_is_false : forall (U:Type),
Empty_set U = fun _ => False.
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
contradiction.
compute.
contradiction.
Qed.

Lemma Full_includes_all : forall (U : Type) (A : Ensemble U),
Included U A (Full_set U).
compute.
intuition.
apply Full_intro.
Qed.


Lemma Empty_included_in_all : forall (U : Type) (A : Ensemble U),
Included U (Empty_set U) A.
intros.
unfold Included.
intros.
contradiction.
Qed.

Lemma Intersection_included : forall (U : Type) (A B : Ensemble U),
Included U (Intersection U A B) A.
intros.
compute.
intuition.
inversion_clear H.
trivial.
Qed.

Lemma Intersection_commut : forall (U : Type) (A B : Ensemble U),
Intersection U A B = Intersection U B A.
intros.
apply Extensionality_Ensembles.
split.
compute.
intuition.
inversion_clear H.
apply Intersection_intro.
trivial.
trivial.
compute.
intuition.
inversion_clear H.
apply Intersection_intro.
trivial.
trivial.
Qed.

Lemma Intersection_included_2 : forall (U : Type) (A B : Ensemble U),
Included U (Intersection U A B) B.
intros.
rewrite Intersection_commut.
apply Intersection_included.
Qed.

Lemma Intersection_and_inclusion : forall (U : Type) (A B : Ensemble U),
Included U A B ->
Intersection U A B = A.
intros.
apply Extensionality_Ensembles.
split.
apply Intersection_included.
generalize H.
clear H.
unfold Included.
intros.
apply Intersection_intro.
trivial.
apply H.
trivial.
Qed.

Lemma Intersection_empty_absorb : forall (U : Type) (A:Ensemble U),
Intersection U A (Empty_set U) = Empty_set U.
intros.
rewrite Intersection_commut.
apply Intersection_and_inclusion.
apply Empty_included_in_all.
Qed.

Lemma Intersection_full_neutral : forall (U: Type) (A : Ensemble U),
Intersection U A (Full_set U) = A.
intros.
apply Intersection_and_inclusion.
apply Full_includes_all.
Qed.

Lemma Union_includes : forall (U: Type) (A B : Ensemble U),
Included U A (Union U A B).
intros.
compute.
intros.
apply Union_introl.
trivial.
Qed.

Lemma Union_commut : forall (U : Type) (A B : Ensemble U),
Union U A B = Union U B A.
intros.
apply Extensionality_Ensembles.
split.
compute.
intuition.
inversion_clear H.
apply Union_intror.
trivial.
apply Union_introl.
trivial.
compute.
intuition.
inversion_clear H.
apply Union_intror.
trivial.
apply Union_introl.
trivial.
Qed.

Lemma Union_includes_2 : forall (U: Type) (A B : Ensemble U),
Included U B (Union U A B).
intros.
rewrite Union_commut.
apply Union_includes.
Qed.


Lemma Union_and_inclusion : forall (U : Type) (A B : Ensemble U),
Included U A B ->
Union U A B = B.
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H0.
apply H.
trivial.
trivial.

apply Union_includes_2.
Qed.

Lemma Union_full_absorb : forall (U : Type) (A:Ensemble U),
Union U A (Full_set U) = Full_set U.
intros.
apply Union_and_inclusion.
apply Full_includes_all.
Qed.

Lemma Union_empty_neutral : forall (U: Type) (A : Ensemble U),
Union U A (Empty_set U) = A.
intros.
rewrite Union_commut.
apply Union_and_inclusion.
apply Empty_included_in_all.
Qed.

Lemma Complement_involutive : forall (U : Type) (A : Ensemble U),
Complement U (Complement U A) = A.
intuition.
apply Extensionality_Ensembles.
split.
compute.
intuition.
apply Classical_Prop.NNPP.
trivial.
compute.
intros.
apply H0.
apply H.
Qed.

Lemma Complement_injective : forall (U : Type) (A B : Ensemble U),
Complement U A = Complement U B -> A = B.
intros.
rewrite <- (Complement_involutive _ B).
rewrite <- (Complement_involutive _ A).
rewrite H.
trivial.
Qed.

Lemma Complement_full_is_empty : forall (U : Type),
Complement U (Full_set U) = Empty_set U.
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
absurd (Full_set U x).
trivial.
apply Full_intro.
compute.
intros.
contradiction.
Qed.

Lemma Complement_empty_is_full : forall (U : Type),
Complement U (Empty_set U) = Full_set U.
intros.
rewrite <- Complement_full_is_empty.
apply Complement_involutive.
Qed.

Lemma Complement_contravar : forall (U : Type) (A B : Ensemble U),
Included U A B -> Included U (Complement U B) (Complement U A).
intros.
compute.
intros.
compute in H.
apply H0.
apply H.
trivial.
Qed.

Lemma Morgan_not_cap_is_cup : forall (U : Type) (A B : Ensemble U),
Complement U (Intersection U A B) = Union U (Complement U A) (Complement U B).
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
generalize (Classical_Prop.classic (A x)).
intros.
inversion_clear H0.
apply Union_intror.
compute.
intros.
apply H.
split.
trivial.
trivial.
apply Union_introl.
compute.
trivial.

compute.
intros.
inversion_clear H0.
inversion_clear H.
contradiction.
contradiction.
Qed.

Lemma Morgan_not_cup_is_cap : forall (U : Type) (A B : Ensemble U),
Complement U (Union U A B) = Intersection U (Complement U A) (Complement U B).
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
split.
compute.
intros.
apply H.
apply Union_introl.
trivial.
compute.
intros.
apply H.
apply Union_intror.
trivial.

compute.
intros.
inversion_clear H.
compute in H1.
compute in H2.
inversion_clear H0.
contradiction.
contradiction.

Qed.

Lemma Complement_total : forall (U : Type) (A : Ensemble U) (x : U),
In U A x \/ In U (Complement U A) x.
intros.
generalize (Classical_Prop.classic (A x)).
intros.
inversion_clear H.
apply or_introl.
trivial.
apply or_intror.
trivial.
Qed.

Lemma Disjonctive : forall (U : Type) (A B : Ensemble U),
A = Union U (Intersection U A B) (Intersection U A (Complement U B))
.
intros.
apply Extensionality_Ensembles.
generalize (Complement_total _ B).
intros.
split.
compute.
intros.
case (H x).
intros.
apply Union_introl.
apply Intersection_intro.
trivial.
trivial.
intros.
apply Union_intror.
apply Intersection_intro.
trivial.
trivial.
compute.
intros.
inversion_clear H0.
inversion_clear H1.
trivial.
inversion_clear H1.
trivial.
Qed.

Lemma Disjonctive_full : forall (U : Type) (A : Ensemble U),
Full_set U = Union U A (Complement U A).
intros.
rewrite <- (Intersection_full_neutral _ A).
assert (Complement U (Intersection U A (Full_set U)) = Intersection U (Full_set U) (Complement U A) ).
rewrite (Intersection_full_neutral _ A).
rewrite Intersection_commut.
rewrite (Intersection_full_neutral _ (Complement U A)).
trivial.
rewrite H.
rewrite (Intersection_commut).
apply Disjonctive.
Qed.

Lemma Conjonctive : forall (U : Type) (A B : Ensemble U),
A = Intersection U (Union U A B) (Union U A (Complement U B))
.
intros.
apply Complement_injective.
rewrite Morgan_not_cap_is_cup.
rewrite Morgan_not_cup_is_cap.
rewrite Morgan_not_cup_is_cap.
rewrite Complement_involutive.
rewrite Union_commut.
apply Disjonctive.
Qed.
Print Conjonctive.

Lemma Sets_plus_minus : forall (U : Type) (A B : Ensemble U),
Included U A B ->
B = Union U A (Setminus U B A).
intros.
apply Extensionality_Ensembles.
split.
compute.
intros.
generalize (Classical_Prop.classic (A x)).
intros.
inversion_clear H1.
apply Union_introl.
trivial.
apply Union_intror.
compute.
split.
trivial.
trivial.
compute.
intros.
inversion_clear H0.
apply H.
trivial.
inversion_clear H1.
trivial.
Qed.

Lemma Setminus_cup : forall (U : Type) (A B : Ensemble U),
Setminus U B A = Intersection U B (Complement U A).
intros.
apply Extensionality_Ensembles.
split.
compute.
intuition.
apply Intersection_intro.
trivial.
compute.
trivial.
compute.
intros.
inversion_clear H.
split.
trivial.
trivial.
Qed.

Lemma Setminus_complement : forall (U : Type) (A : Ensemble U),
Setminus U (Full_set U) A = Complement U A.
intros.
rewrite Setminus_cup.
rewrite Intersection_commut.
rewrite Intersection_full_neutral.
trivial.
Qed.

Lemma Disjoint_commut : forall (U : Type) (A B : Ensemble U),
Disjoint U A B -> Disjoint U B A.
intros.
inversion_clear H.
apply Disjoint_intro.
rewrite Intersection_commut.
trivial.
Qed.

Lemma Disjoint_setminus : forall (U : Type) (A B : Ensemble U),
Disjoint U A (Setminus U B A).
intros.
rewrite Setminus_cup.
apply Disjoint_intro.
intuition.
inversion_clear H.
inversion_clear H1.
contradiction.
Qed.

Lemma Disjoint_complement : forall (U : Type) (A : Ensemble U),
Disjoint U A (Complement U A).
intros.
rewrite <- Setminus_complement.
apply Disjoint_setminus.
Qed.

Lemma Disjoint_decreases : forall (U : Type) (A B C : Ensemble U),
Disjoint U A C ->
Included U B A ->
Disjoint U B C.
intros.
inversion_clear H.
apply Disjoint_intro.
intuition.
compute in H0.
compute in H.
inversion_clear H.
apply (H1 x).
compute.
split.
compute.
apply H0.
trivial.
trivial.
Qed.

Lemma Disjoint_empty : forall (U : Type) (A  :Ensemble U),
Disjoint U A (Empty_set U).
intros.
rewrite <- Complement_full_is_empty.
apply (Disjoint_decreases U (Full_set U)).
apply Disjoint_complement.
apply Full_includes_all.
Qed.

Lemma Case_disjunction : forall (U : Type) (A B : Ensemble U),
Disjoint U (Intersection U A B) (Intersection U A (Complement U B))
.
intros.
apply Disjoint_intro.
unfold not.
intros.
inversion_clear H.
inversion_clear H0.
inversion_clear H1.
contradiction.
Qed.
Print Case_disjunction.

End Trivial_Ensembles.

Import Trivial_Ensembles.

(* Eventuellement, parlons de familles. *)

Module Familles_parties.

Definition Famille_parties (U:Type) (I:Type) : Type := I -> Ensemble U.

Definition Union (U:Type) (I:Type) (F:Famille_parties U I) : Ensemble U :=
fun u:U => exists i:I, In U (F i) u.

Definition Intersection (U:Type) (I:Type) (F:Famille_parties U I) : Ensemble U :=
fun u:U => forall i:I, In U (F i) u.

Definition Conversion (U:Type) (f : Ensemble U -> Ensemble U -> Ensemble U)
(F:Famille_parties U nat) : Famille_parties U nat := fix G (n:nat) := match n with
O => F O | S n' => f (F n) (G n') end.

Definition Union_partielle (U:Type) (F:Famille_parties U nat) :
Famille_parties U nat := Conversion U (Ensembles.Union U) F.

Definition Intersection_partielle (U:Type) (F:Famille_parties U nat) :
Famille_parties U nat := Conversion U (Ensembles.Intersection U) F.

End Familles_parties.

Module Operations_ensembles.

Definition Union (U:Type) (E:Ensemble (Ensemble U)) : Ensemble U :=
fun (u:U) => exists e:Ensemble U, (In (Ensemble U) E e /\ In U e u).

Definition Intersection (U:Type) (E:Ensemble (Ensemble U)) : Ensemble U :=
fun (u:U) => forall e:Ensemble U, (In (Ensemble U) E e -> In U e u).

Definition Parties (U:Type) (e:Ensemble U) : Ensemble (Ensemble U) :=
fun (E:Ensemble U) => Ensembles.Included U E e.

End Operations_ensembles.

Module Mesure.
(* Theorie de la mesure *)

(* algebre stable par union finie *)

Definition Algebre (U: Type) (F:Ensemble (Ensemble U)) : Prop :=
let e := Ensemble U in let E := Ensemble e in
(In e F (Empty_set U)) /\
(forall a : e, In e F a -> In e F (Complement U a)) /\
(forall a b : e, In e F a -> In e F b -> In e F (Ensembles.Union U a b)).

(*
Definition Sigma_algebre (U:Type) (F:Ensemble (Ensemble U)) : Prop :=
let e := Ensemble U in let E := Ensemble e in forall F:E, 
forall F:E,
Algebre U F /\
(forall A : nat -> e, (forall n:nat, In e F (A n)) -> (In e F (fun u:U => exists n : nat, In U (A n) u ))).
*)

Definition Sigma_algebre (U:Type) (F:Ensemble (Ensemble U)) : Prop :=
let e := Ensemble U in let E := Ensemble e in
Algebre U F /\
(forall (A : Familles_parties.Famille_parties U nat), (forall n:nat, In e F (A n)) -> In e F (Familles_parties.Union U nat A)).

Inductive sigma2 (U : Type) (G : Ensemble (Ensemble U)) : Ensemble (Ensemble U) :=
| sigma_0 : forall (e : Ensemble U), In (Ensemble U) G e -> In (Ensemble U) (sigma2 U G) e
| sigma_vide : In (Ensemble U) (sigma2 U G) (Empty_set U)
| sigma_complement : forall (e : Ensemble U), In (Ensemble U) (sigma2 U G) e ->
In (Ensemble U) (sigma2 U G) (Complement U e)
| sigma_union : forall (e1 e2 : Ensemble U), In (Ensemble U) (sigma2 U G) e1 ->
In (Ensemble U) (sigma2 U G) e2 ->
In (Ensemble U) (sigma2 U G) (Union U e1 e2)
| sigma_union_denomb : forall (A : Familles_parties.Famille_parties U nat),
(forall n:nat, In (Ensemble U) (sigma2 U G) (A n)) ->
In (Ensemble U) (sigma2 U G) (Familles_parties.Union U nat A).

Definition sigma (U:Type) (G: Ensemble (Ensemble U)) : Ensemble (Ensemble U) :=
let e := Ensemble U in let E := Ensemble e in 
let F : Ensemble E := fun f:E => (Sigma_algebre U f /\ Included e G f) in
Operations_ensembles.Intersection e F.

Theorem sigma_est_sigma2 : forall (U : Type) (G : Ensemble (Ensemble U)),
sigma2 U G = sigma U G.
Proof.
intros.
apply Extensionality_Ensembles.
split.
unfold Included.
intros.
induction H.
unfold sigma.
unfold Operations_ensembles.Intersection.
unfold Sigma_algebre.
unfold Algebre.
unfold Included.
unfold In.
intuition.
unfold sigma.
unfold Operations_ensembles.Intersection.
unfold Sigma_algebre.
unfold Algebre.
unfold Included.
unfold In.
intuition.
unfold sigma.
unfold Operations_ensembles.Intersection.
unfold Sigma_algebre.
unfold Algebre.
unfold Included.
unfold In.
intuition.
apply H0.
compute in IHsigma2.
apply IHsigma2.
intuition.
unfold sigma.
unfold Operations_ensembles.Intersection.
unfold Sigma_algebre.
unfold Algebre.
unfold Included.
unfold In.
intuition.
apply H6.
compute in IHsigma2.
apply IHsigma2.
intuition.
compute in IHsigma0.
apply IHsigma0.
intuition.
unfold sigma.
unfold Operations_ensembles.Intersection.
unfold Sigma_algebre.
unfold Algebre.
unfold Included.
unfold In.
intuition.
apply H4.
compute in H0.
intros n.
apply H0 .
intuition.

unfold sigma.
unfold Operations_ensembles.Intersection.
unfold Sigma_algebre.
unfold Algebre.
unfold Included.
unfold In.
intuition.
apply H.
split.
split.
split.
apply sigma_vide.
split.
intros.
apply sigma_complement.
trivial.
intros.
apply sigma_union.
trivial.
trivial.
intros.
apply sigma_union_denomb.
trivial.
intros.
apply sigma_0.
trivial.
Qed.

Theorem Stabilite_intersection : forall (U:Type) (F:Ensemble (Ensemble U)) (A B : Ensemble U),
Algebre U F -> In (Ensemble U) F A -> In (Ensemble U) F B ->
In (Ensemble U) F (Ensembles.Intersection U A B).
Proof.
intros U F A B HF HA HB.
case HF.
intros _.
intros H ; case H.
intros Hc Hu.
rewrite <- Complement_involutive .
rewrite Morgan_not_cap_is_cup.

apply Hc.
apply Hu.
apply Hc.
exact HA.
apply Hc.
exact HB.
Qed.

Theorem sigma_algebre_sigma : forall (U:Type) (G:Ensemble (Ensemble U)),
Sigma_algebre U (sigma U G).
Proof.
 intros U G.
 split.
 split.
 unfold In.
 unfold sigma.
 compute.
 intuition.

 split.
 intros a.
 unfold In.
 unfold sigma.
 intros.
 compute in H.
 compute.
 intuition.
 apply H0.
 apply H.
 intuition.

 compute.
 intuition.
 apply H6.
 apply H.
 intuition.
 apply H0.
 intuition.

 compute.
 intuition.
 apply H3.
 intros n.
 apply H.
 intuition.

Qed.
(* en fait on a montré qu'une intersection quelconque non vide de sigma-algèbres
est une sigma-algèbre. Réécrire cette propriété plus générale. *)

(* Parlons de mesures. *)

Definition Mesure_positive (U:Type)
(F:Ensemble (Ensemble U)) (mu : Ensemble U  -> R) : Prop := 
 mu (Empty_set U) = 0 /\
 (forall (a:Ensemble U), (In (Ensemble U) F a -> 0 <= mu a)).

Definition Mesure_croissante (U:Type)
(F:Ensemble (Ensemble U)) (mu : Ensemble U  -> R) : Prop := 
 (forall (a b : Ensemble U), 
   (In (Ensemble U) F a -> In (Ensemble U) F b -> Included U a b ->
    mu a <= mu b)).

Definition Mesure_additive  (U:Type)
(F:Ensemble (Ensemble U)) (mu : Ensemble U  -> R) : Prop := 
 (forall (a b : Ensemble U), 
   (In (Ensemble U) F a -> In (Ensemble U) F b -> Disjoint U a b ->
    mu (Union U a b) = mu a + mu b)).

Definition Mesure_denomb_additive  (U:Type)
(F:Ensemble (Ensemble U)) (mu : Ensemble U  -> R) : Prop := 
 (forall (f:Familles_parties.Famille_parties U nat), 
   (forall (n:nat), In (Ensemble U) F (f n)) ->
   (forall (p q:nat), (p <> q -> Disjoint U (f p) (f q))) ->
   (In (Ensemble U) F (Familles_parties.Union U nat f)) ->
   (infinit_sum (fun (n:nat) => mu (f n))
      (mu (Familles_parties.Union U nat f))) )
.

Lemma  Mesure_positive_additive_est_croissante :
 forall (U:Type) (F:Ensemble (Ensemble U)) (mu : Ensemble U  -> R),
 Algebre U F -> Mesure_positive U F mu -> Mesure_additive U F mu ->
 Mesure_croissante U F mu.
 intros U F mu HF HPos HAdd.
 unfold Mesure_croissante.
 intros a b Ha Hb Hi.
 case HF.
 intros HFNil HF1.
 case HF1. 
 intros HFC HFU.

 generalize (Sets_plus_minus U a b Hi). 
 rewrite Setminus_cup.
 intros.
 
assert (mu b = mu a + mu (Intersection U b (Complement U a))).
case HAdd.
exact Ha.
apply Stabilite_intersection.
exact HF.
exact Hb.
apply HFC.
exact Ha.
rewrite <- Setminus_cup.
apply Disjoint_setminus.
rewrite <- H.
trivial.
rewrite H0.
apply Rle_trans with (mu a + 0).
rewrite Rplus_0_r.
apply Rle_refl.
apply Rplus_le_compat_l.
inversion HPos.
apply H2.
apply Stabilite_intersection.
exact HF.
exact Hb.
apply HFC.
exact Ha.
Qed.

Lemma eq_epsilon : forall (a b : R),
(forall eps : R, (eps > 0 -> R_dist a b < eps)) ->
 a = b.
Proof.
intros a b.
unfold R_dist.
unfold Rabs.
case Rcase_abs.
intros Hab.
intros H.
absurd (-(a - b) < -(a - b)).
apply Rlt_irrefl. 
apply H.
rewrite <- Ropp_0.
auto with real.
intros Hab Heps.
assert (a <= b).
apply le_epsilon.
intros eps HeP.
apply Rminus_le.
assert (a - (b + eps) = (a - b) - eps).
ring.
rewrite H.
apply Rle_minus.
apply Rlt_le.
apply Heps.
apply HeP.
apply Rge_antisym.
apply minus_Rge.
exact Hab.
apply Rle_ge.
exact H.
Qed.

Theorem mesure_denomb_additive_est_additive : forall (U:Type) (F:Ensemble (Ensemble U)) (mu : Ensemble U  -> R),
 Algebre U F -> Mesure_positive U F mu -> Mesure_denomb_additive U F mu ->
 Mesure_additive U F mu.
Proof.
intros U F mu HF HPos HDA. 
unfold Mesure_additive.
intros a b Ha Hb HD.
assert  (exists f : Familles_parties.Famille_parties U nat,
f O = a /\ f (S O) = b /\ forall n:nat, lt (S O)  n -> f n = Empty_set U).
compute.
exists (fun n:nat => match n with O => a | S O => b | _ => Empty_set U end).
split.
trivial.
split.
trivial.
intros n.
case n.
assert ((0 < 2)%nat).
auto with arith.
intros Habsurde.
assert (~(0 < 2)%nat).
apply le_not_lt.
exact Habsurde.
contradiction.
intros n0.
case n0.
intros Habsurde.
assert ((1 < 2)%nat).
auto with arith.
assert (~(1 < 2)%nat).
apply le_not_lt.
exact Habsurde.
contradiction.
auto.
inversion H as [f Hf'].
case Hf'.
intros Hf0 Hf''.
case Hf''.
intros Hf1 Hf.
assert (HfSS : forall n0 : nat, f (S (S n0)) = Empty_set U).
intros n0.
apply Hf.
auto with arith.

assert (Union U a b = Familles_parties.Union U nat f).
apply Extensionality_Ensembles.
compute.
split.
intros x HUx.
inversion HUx.
exists O.
rewrite Hf0.
exact H0.
exists (S O).
rewrite Hf1.
apply H0.
intros x Hix.
inversion Hix as [i Hi].
generalize Hi.
case i.
rewrite Hf0.
intros Hax.
apply Union_introl.
exact Hax.
intros n.
case n.
rewrite Hf1.
intros Hbx.
apply Union_intror.
exact Hbx.
intros n0.
rewrite Hf.
intros Habsurde.
inversion Habsurde.
auto with arith.
rewrite H0.
apply eq_epsilon.
intros eps eps_positive.
unfold Mesure_denomb_additive in HDA.
unfold infinit_sum in HDA.
assert (exists N : nat,
        (forall n : nat,
         (n >= N)%nat ->
         R_dist (sum_f_R0 (fun n0 : nat => mu (f n0)) n)
           (mu (Familles_parties.Union U nat f)) < eps)).
apply HDA.
intros n.
case n.
rewrite Hf0.
exact Ha.
intros n0.
case n0.
rewrite Hf1.
apply Hb.
intros n1.
rewrite HfSS.
case HF.
auto.
intros p q.
case p.
case q.
intros Habsurde.
assert (O = O).
auto.
contradiction.
intros n _.
case n.
rewrite Hf0.
rewrite Hf1.
exact HD.
intros n0.
rewrite HfSS.
apply Disjoint_empty.
intros n.
case n.
case q.
intros _.
rewrite Hf0.
rewrite Hf1.
apply Disjoint_commut.
exact HD.
intros n0.
case n0.
intros Habsurde.
assert (S O = S O).
trivial.
contradiction.
intros n1 _.
rewrite HfSS.
apply Disjoint_empty.
intros n0 _.
rewrite HfSS.
apply Disjoint_commut.
apply Disjoint_empty.

rewrite <- H0.
case HF.
intros _ HF1.
case HF1.
intros _ HFU.
apply HFU.
exact Ha.
exact Hb.

exact eps_positive.
inversion H1.
generalize H2.
assert (forall n : nat, sum_f_R0 (fun n0 : nat => mu (f n0)) (S n) = mu a + mu b).
induction n.
compute.
rewrite Hf0.
rewrite Hf1.
trivial.

cbv delta iota.
fold sum_f_R0.
cbv beta.
cbv iota.
cbv beta.
rewrite IHn.
rewrite HfSS.
case HPos.
intros Hmu0 _.
rewrite Hmu0.
apply Rplus_0_r.

intros _.
rewrite <- (H3 x).
rewrite R_dist_sym.
apply H2.
unfold ge.
auto with arith.
Qed.

Definition Espace_mesurable (U:Type)
(F:Ensemble (Ensemble U)) (mu : Ensemble U -> R) : Prop :=
 Sigma_algebre U F /\
Mesure_positive U F mu /\ Mesure_denomb_additive U F mu.

Theorem Convergence_monotone : 
 forall (U:Type) (F:Ensemble (Ensemble U)) (mu : Ensemble U -> R)
(A : Ensemble U) (f : Familles_parties.Famille_parties U nat),
Espace_mesurable U F mu ->
(forall n:nat, In (Ensemble U) F (f n)) ->
(forall n:nat, Included U (f n) (f (S n))) ->
A = Familles_parties.Union U nat f ->
Un_cv (fun n:nat => mu (f n)) (mu A).
Proof.
intros U F mu A f HM Hf_F Hf_croiss HA.
assert (exists g : Familles_parties.Famille_parties U nat,
(g O = f O /\ forall n:nat, g (S n) = Setminus U (f (S n)) (f n))).
exists (fun n' => match n' with
O => f O | S n => Setminus U (f (S n)) (f n) end).
split.
trivial.
trivial.
inversion H as [g Hg'].
case Hg'.
intros Hg0 Hg.

assert (forall (i j : nat), le i j -> forall x:U, f i x -> f j x).
induction j.
intros Hi.
assert (i = O).
symmetry.
apply le_n_O_eq.
exact Hi.
rewrite H0.
trivial.

intros Hi.
case (le_lt_dec i j).
intros Hi' x Hxi.
apply Hf_croiss.
unfold In.
apply IHj.
exact Hi'.
exact Hxi.
intros Hi'.
assert (i = S j).
apply le_antisym.
exact Hi.
apply lt_le_S.
exact Hi'.
rewrite H0.
trivial.

assert (forall (i j : nat), i <> j -> Disjoint U (g i) (g j)).
intros i j.
case (le_lt_dec i j).
intros Hij1 Hij2.
apply Disjoint_intro.
intros x Hx.
inversion Hx.
assert (lt i  j).
assert (lt i j \/ i = j).
apply le_lt_or_eq.
exact Hij1.
inversion H4.
exact H5.
contradiction.
assert (exists j':nat,  j = S j').
exists (pred j).
apply S_pred with i.
exact H4.
inversion H5 as [j' Hj'].
assert (le i j').
apply lt_n_Sm_le.
rewrite <- Hj'.
exact H4.
rewrite Hj' in H2.
rewrite Hg in H2.
compute in H2.
case H2.
intros Hsj'x.
intros Hj'x.
absurd (f j' x).
exact Hj'x.
apply H0 with i.
exact H6.
generalize H1.
case i.
compute.
rewrite Hg0.
trivial.
intros n.
rewrite Hg .
intros Hmoins.
inversion Hmoins.
exact H7.

intros Hij _.
apply Disjoint_intro.
intros x Hx.
inversion Hx.
assert (exists i':nat,  i = S i').
exists (pred i).
apply S_pred with j.
exact Hij.
inversion H4 as [i' Hi'].
assert (le j i').
apply lt_n_Sm_le.
rewrite <- Hi'.
exact Hij.
rewrite Hi' in H1.
rewrite Hg in H1.
compute in H1.
case H1.
intros Hsi'x.
intros Hi'x.
absurd (f i' x).
exact Hi'x.
apply H0 with j.
exact H5.
generalize H2.
case j.
compute.
rewrite Hg0.
trivial.
intros n.
rewrite Hg .
intros Hmoins.
inversion Hmoins.
exact H6.

elim HM.
intros HFsigma Hmu.
elim HFsigma.
intros HFalg HFdu.
elim HFalg.
intros HF0 HF1.
elim HF1.
intros HFc HFu.
elim Hmu.
intros Hmupos Hmuda.

assert (forall n:nat, Intersection U (f (S n)) (Complement U (f n)) = fun x : U => f (S n) x /\ (f n x -> False)).
intros n.
apply Extensionality_Ensembles.
compute.
split.
intros x Hx.
inversion Hx.
split.
exact H2.
apply H3. 
intros x Hx.
inversion Hx.
apply Intersection_intro.
exact H2.
exact H3.

assert (forall n, mu (f n) = sum_f_R0 (fun k => mu (g k)) n).
induction n.
compute.
rewrite Hg0.
trivial.
unfold sum_f_R0.
fold sum_f_R0.
rewrite <- IHn.
rewrite Hg.
assert (f (S n) = Union U (f n) (Setminus U (f (S n)) (f n))).
apply Extensionality_Ensembles.
unfold Same_set.
split.
compute.
intros x.
intros Hx.
assert (f n x \/ ~ f n x).
apply Classical_Prop.classic.
case H3.
intros Hfnx.
apply Union_introl.
exact Hfnx.
intros Hfnx.
apply Union_intror.
compute.
split.
exact Hx.
exact Hfnx.
compute.
intros x Hu.
inversion Hu.
apply Hf_croiss.
exact H3.
compute in H3.
case H3.
trivial.
compute.
rewrite <- H2.

assert (Mesure_additive U F mu).
apply mesure_denomb_additive_est_additive.
exact HFalg.
exact Hmupos.
exact Hmuda.
compute in H4.
apply trans_eq with (mu (Union U (f n) (Setminus U (f (S n)) (f n)))).
rewrite <- H3;reflexivity.
unfold Setminus.
unfold In.
unfold not.
rewrite <- H2.
apply H4.
apply Hf_F.
apply Stabilite_intersection.
apply HFalg.
compute.
apply Hf_F.
compute.
compute in HFc.
apply HFc.
apply Hf_F.
apply Disjoint_commut.
apply (Disjoint_decreases U (Complement U (f n)) (Intersection U (f (S n)) (Complement U (f n)))).
apply Disjoint_commut.
apply Disjoint_complement.
apply Intersection_included_2.

unfold Un_cv.
unfold Mesure_denomb_additive in Hmuda.
unfold infinit_sum in Hmuda.

assert (Familles_parties.Union U nat f = Familles_parties.Union U nat g).
apply Extensionality_Ensembles.
compute.
split.
intros x Hx.
inversion Hx.
induction x0.
exists O.
rewrite Hg0.
exact H4.
assert (f x0 x \/ ~ f x0 x).
apply Classical_Prop.classic.
case H5.
exact IHx0.
intros Hx0.
exists (S x0).
rewrite Hg.
compute.
split.
exact H4.
exact Hx0.
intros x Hx.
inversion Hx.
generalize H4.
case  x0.
rewrite Hg0.
intros Hx0.
exists O.
exact Hx0.
intros n Hxn.
exists (S n).
rewrite Hg in Hxn.
inversion Hxn.
exact H5.

assert ( forall eps : R,
        eps > 0 ->
        exists N : nat,
          (forall n : nat,
           (n >= N)%nat ->
           R_dist (sum_f_R0 (fun n0 : nat => mu (g n0)) n)
             (mu (Familles_parties.Union U nat g)) < eps) ).
apply Hmuda.
intros n.
case n.
rewrite Hg0.
apply Hf_F.
intros n0.
rewrite Hg.
compute.
rewrite <- H2.
apply Stabilite_intersection.
auto.
compute.
apply Hf_F.
compute.
compute in HFc.
apply HFc.
apply Hf_F.
auto.
rewrite <- H4.
apply HFdu.
auto.
intros eps Heps.
case H5 with eps.
auto.
intros N.
intros Hgeps.
exists N.
intros n HnN.
rewrite H3.
rewrite HA.
rewrite H4.
apply Hgeps.
auto.

Qed.

Print Convergence_monotone.

(* Fonctions mesurables *)

Definition preimage (U:Type) (V:Type) (f:U -> V) (Y:Ensemble V) : Ensemble U :=
fun u : U => In V Y (f u).

Definition fonctions_mesurables (U:Type) (V:Type)
(F:Ensemble (Ensemble U)) (G:Ensemble (Ensemble V)) :
Ensemble (U -> V) :=
fun (f : U -> V) => forall g:Ensemble V, (In (Ensemble V) G g -> 
  In (Ensemble U) F (preimage U V f g)).

Theorem Fonction_mesurable_sur_generateurs :
 forall (U V : Type) (f: U -> V) (F : Ensemble (Ensemble U)) (C : Ensemble (Ensemble V)),
Sigma_algebre U F ->
In (U -> V) (fonctions_mesurables U V F C) f ->
In (U -> V) (fonctions_mesurables U V F (sigma V C)) f.
Proof.

intros U V f F C HF Hf.

unfold In.
intros g Hg.
case HF.
intros HFA HFdu.
case HFA.
intros HF0 HF1.
case HF1.
intros HFc HFu.
compute in Hf.
apply Hg.
compute.
split.
split.
split.
assert (exists vide : Ensemble U, vide = fun u : U => Empty_set V (f u)).
exists (fun u : U => Empty_set V (f u)).
trivial.
inversion H as [vide Hvide].
rewrite <- Hvide.
assert (vide = Empty_set U).
apply Extensionality_Ensembles.
rewrite Hvide.
compute.
split.
intros x Hx.
inversion Hx.
intros x Hx.
inversion Hx.
rewrite H0.
apply HF0.
split.
intros a Ha.
compute in HFc.
apply (HFc (fun u : U => a (f u))).
exact Ha.
intros a b Ha Hb.
compute in HFu.
assert (exists union : Ensemble U, union = fun u : U => Union V a b (f u)).
exists (fun (u : U) => Union V a b (f u)).
trivial.
inversion  H as [union Hunion].
rewrite <- Hunion.
assert (union = Union U (fun u => a (f u)) (fun u => b (f u))).
apply Extensionality_Ensembles.
rewrite Hunion.
compute.
split.
intros x Hx.
inversion Hx.
apply Union_introl.
compute.
compute in H0.
exact H0.
apply Union_intror.
compute.
compute in H0.
exact H0.
intros x Hx.
inversion Hx.
compute in H0.
apply Union_introl.
exact H0.
apply Union_intror.
exact H0.
rewrite H0.
apply HFu.
exact Ha.
exact Hb.
intros A HA.
compute in HFdu.
apply (HFdu (fun i u => A i (f u))).
exact HA.
exact Hf.
Qed.

Definition Preservation_mesure (U V : Type)
(F : Ensemble (Ensemble U)) (mu : Ensemble U -> R)
(G : Ensemble (Ensemble V)) (nu : Ensemble V -> R) :
Ensemble (U -> V) := fun f =>
fonctions_mesurables U V F G f /\
forall (A:Ensemble V), (G A -> mu (preimage U V f A) = nu A).

(* Pour continuer, l'on a besoin du théorème de Carathéodory. *)

Definition Lambda_systeme (U:Type)
(F:Ensemble (Ensemble U)) (lambda : Ensemble U -> R) : Ensemble (Ensemble U) :=
fun (L : Ensemble U) => 
In (Ensemble U) F L /\ forall A:Ensemble U,
In (Ensemble U) F A -> 
lambda (Intersection U L A) + lambda (Intersection U (Complement U L) A)
= lambda A.

Definition Mesure_denomb_subadditive (U:Type)
(F:Ensemble (Ensemble U)) (lambda : Ensemble U -> R) : Prop :=
forall (E:Familles_parties.Famille_parties U nat) (s:R),
infinit_sum (fun n=>lambda (E n)) s ->
lambda (Familles_parties.Union U nat E) <= s.

Definition Mesure_exterieure (U:Type)
(F:Ensemble (Ensemble U)) (lambda : Ensemble U -> R) : Prop :=
Mesure_positive U F lambda /\
Mesure_croissante U F lambda /\
Mesure_denomb_subadditive U F lambda.

Axiom 
(* Lemma *) Caratheodory : forall (U:Type) (F:Ensemble (Ensemble U))
(lambda : Ensemble U -> R),
Sigma_algebre U F ->
Mesure_exterieure U F lambda ->
(Sigma_algebre U (Lambda_systeme U F lambda) /\
 Mesure_denomb_additive U (Lambda_systeme U F lambda) lambda).
(* Proof.
intros U F lambda HF Hlambda.
inversion HF as [HFA HFdu].
inversion HFA as [HF0 HF1].
inversion HF1 as [HFc HFu].
inversion Hlambda as [Hlpos0 Hl1].
inversion Hlpos0 as [Hl0 Hlpos].
inversion Hl1 as [Hlcroiss Hldsa].
assert (Sigma_algebre U (Lambda_systeme U F lambda)).
split.
split.
compute.
split.
apply HF0.
intros A HA.
assert (forall V:Ensemble U, Intersection U (Empty_set U) V = Empty_set U).
intros V.
apply Extensionality_Ensembles.
compute.
split.
intros x Hx.
inversion Hx.
exact H.
intros x Hx.
apply Intersection_intro.
exact Hx.
contradiction.
assert (forall V:Ensemble U, Intersection U (fun x : U => Empty_set U x -> False) V = V).
intros V.
apply Extensionality_Ensembles.
compute.
split.
intros x Hx.
inversion Hx.
exact H1.
intros x Hx.
apply Intersection_intro.
compute.
contradiction.
trivial.
rewrite H.
rewrite H0.
rewrite Hl0.
apply Rplus_0_l.
split.
intros a Ha.
inversion Ha.
compute.
split.
compute in HFc.
apply HFc.
apply H.
compute in H0.
intros A HA.
rewrite Rplus_comm.
assert (a = fun x : U => (a x -> False) -> False).
apply Extensionality_Ensembles.
compute.
split.
contradiction.
intros x Hx.
apply Classical_Prop.NNPP.
unfold not.
apply Hx.
rewrite <- H1.
apply H0.
exact HA.
intros a b Ha Hb.
inversion Ha.
inversion Hb.
compute.
split.
apply HFu.
trivial.
trivial.
intros A HA.
*)

Axiom Caratheodory_Extension :
forall (U:Type) (F0:Ensemble (Ensemble U)) (mu0:Ensemble U->R),
Algebre U F0 ->
Mesure_positive U F0 mu0 ->
Mesure_denomb_additive U F0 mu0 ->
exists mu:Ensemble U->R, exists F:Ensemble(Ensemble U),
(forall A:Ensemble U, In (Ensemble U) F0 A -> mu A = mu0 A) /\
F = sigma U F0 /\ Espace_mesurable U F mu.

(* Mesure de Lebesgue *)

(* Utilisons les classes monotones. Le problème, c'est de pouvoir définir des
mesures infinies. *)

(* Pour le moment, voilà. *)

Definition Intervalle_ouvert (u:R) (v:R) : Ensemble R := fun x:R =>u<x<v.
Definition Intervalle_ferme (u:R) (v:R) : Ensemble R := fun x:R =>u<=x<=v.

Lemma Intervalles_fermes_inclus : forall (a b c d : R),
a <= b ->
b <= c ->
c <= d ->
Included R (Intervalle_ferme b c) (Intervalle_ferme a d).
intros.
unfold Included.
intro x.
unfold In.
unfold Intervalle_ferme.
intros.
inversion_clear H2.
split.
apply Rle_trans with b.
trivial.
trivial.
apply Rle_trans with c.
trivial.
trivial.
Qed.


Lemma Intervalle_singleton : forall (z : R) (x : R),
In R (Intervalle_ferme z z) x -> x = z.
unfold In.
unfold Intervalle_ferme.
intuition.
Qed.

Definition Boreliens (E : Ensemble R) : Ensemble (Ensemble R) := sigma R (fun A =>
exists u:R, exists v:R, Intersection R E A = Intervalle_ferme u v).
(* eh oui, en fait il faut supposer que l'intervalle est fermé, pour simplifier les choses.
On voit tout de suite, d'ailleurs, que dans ce cas la mesure d'un singleton est zéro. *)

Axiom Existe_Lebesgue :
forall E : Ensemble R, exists lambda : Ensemble R -> R,
Espace_mesurable R (Boreliens E) lambda /\
forall u v : R,
u <=v -> Included R (Intervalle_ferme u v) E ->
lambda (Intervalle_ferme u v) = v - u.

End Mesure.

Module Probabilites.

 Definition Espace_proba (U:Type) (F:Ensemble (Ensemble U)) (mu : Ensemble U -> R)
: Prop :=
Mesure.Espace_mesurable U F mu /\ mu (Full_set U) = 1.

Definition Evenements_independants
(U:Type) (F:Ensemble (Ensemble U)) (mu : Ensemble U -> R)
(A B : Ensemble U) : Prop :=
In (Ensemble U) F A /\ In (Ensemble U) F B /\ 
mu (Intersection U A B) = mu A * mu B.

Definition Familles_independantes
(U:Type) (F:Ensemble (Ensemble U)) (mu: Ensemble U -> R)
(A B : Ensemble (Ensemble U)) : Prop :=
forall (a b : Ensemble U),
In (Ensemble U) A a -> In (Ensemble U) B b ->
Evenements_independants U F mu a b.

Lemma Independants_commut :
forall (U:Type) (F:Ensemble (Ensemble U)) (mu: Ensemble U -> R) (A B : Ensemble U),
Evenements_independants U F mu A B -> Evenements_independants U F mu B A.
Proof.
intros U F mu A B H.
inversion H as [Ha H0].
inversion H0 as [Hb Hp].
compute.
split.
trivial.
split.
trivial.
rewrite Rmult_comm.
rewrite Intersection_commut.
trivial.
Qed.

Lemma Independants_vide :
forall (U:Type) (F:Ensemble (Ensemble U)) (mu: Ensemble U -> R) (A : Ensemble U),
Espace_proba U F mu -> In (Ensemble U) F A ->
 Evenements_independants U F mu A (Empty_set U).
Proof.
intros U F mu A HF HA.
inversion HF as [HF' Hmutot].
inversion HF' as [HFsigma Hmu].
inversion HFsigma as [HFA HFdu].
inversion HFA as [HF0 HF1].
inversion Hmu as [Hmupos' Hmuda].
inversion Hmupos' as [Hmu0 Hmupos].
compute.
split.
trivial.
split.
trivial.
rewrite Hmu0.
rewrite Rmult_0_r.
rewrite Intersection_empty_absorb.
trivial.
Qed.

Lemma Independants_plein :
forall (U:Type) (F:Ensemble (Ensemble U)) (mu: Ensemble U -> R) (A : Ensemble U),
Espace_proba U F mu -> In (Ensemble U) F A ->
 Evenements_independants U F mu A (Full_set U).
Proof.
intros U F mu A HF HA.
inversion HF as [HF' Hmutot].
inversion HF' as [HFsigma Hmu].
inversion HFsigma as [HFA HFdu].
inversion HFA as [HF0 HF1].
inversion HF1 as [HFc HFu].
inversion Hmu as [Hmupos' Hmuda].
inversion Hmupos' as [Hmu0 Hmupos].
compute.
split.
trivial.
split.
rewrite <- Complement_empty_is_full.
apply HFc.
trivial.
rewrite Hmutot.
rewrite Rmult_1_r.
rewrite Intersection_full_neutral.
trivial.
Qed.

Lemma Independance_self_discr : 
forall (U:Type) (F:Ensemble (Ensemble U)) (mu: Ensemble U -> R) (A : Ensemble U),
Espace_proba U F mu -> In (Ensemble U) F A ->
Evenements_independants U F mu A A ->
(mu A = 0 \/ mu A = 1).
Proof.
intros U F mu A HF HA.
inversion HF as [HF' Hmutot].
inversion HF' as [HFsigma Hmu].
inversion HFsigma as [HFA HFdu].
inversion HFA as [HF0 HF1].
inversion HF1 as [HFc HFu].
inversion Hmu as [Hmupos' Hmuda].
inversion Hmupos' as [Hmu0 Hmupos].
intros Haa.
inversion Haa as [_ Haa1].
inversion Haa1 as [_ Hmua].
assert (Intersection U A A = A).
apply Extensionality_Ensembles.
compute.
split.
intros x Hx.
inversion Hx.
trivial.
intros x Hx.
apply Intersection_intro.
trivial.
trivial.
rewrite H in Hmua.
assert (mu A = 0 \/ ~(mu A = 0)).
auto with real.
case H0.
intros HmuA0.
apply or_introl.
trivial.
intros HmuA0.
apply or_intror.
assert (mu A * 1 = mu A * mu A).
rewrite <- Hmua.
apply Rmult_1_r.
apply Rmult_eq_reg_l with (mu A).
symmetry.
apply H1.
trivial.
Qed.

Theorem Proba_compl : forall (U : Type) (F: Ensemble (Ensemble U))
(mu : Ensemble U -> R) (A : Ensemble U),
Espace_proba U F mu ->
In (Ensemble U) F A ->
mu (Complement _ A) = 1 - mu A
.
Proof.
intros.
apply (Rplus_eq_reg_l  (mu A)).
rewrite Rplus_minus.
inversion_clear H.
rewrite <- H2.
rewrite (Disjonctive_full _ A).
inversion_clear H1.
inversion_clear H.
inversion_clear H3.
generalize (Mesure.mesure_denomb_additive_est_additive _ _ _ H1 H H5).
intros.
compute in H3.
rewrite H3.
trivial.
apply H0.
inversion_clear H1.
casser_les_cailloux.
apply H1.
trivial.
apply Disjoint_complement.
Qed.

(* Quantificateurs probabilistes *)

Definition Pour_presque_tout 
(U : Type) (E : Ensemble (Ensemble U)) (p : Ensemble U -> R)
(phi : U -> Prop) : Prop := 
In (Ensemble U) E phi /\ p phi = 1.

Definition Existe_presque_surement 
(U : Type) (E : Ensemble (Ensemble U)) (p : Ensemble U -> R)
(phi : U -> Prop) : Prop := 
In (Ensemble U) E phi /\ p phi <> 0.


(* Distributions de probabilités de référence. *)
Definition U01 := Mesure.Intervalle_ferme 0 1.

Definition B01 := Mesure.Boreliens U01.

Variable B01_uniforme : Ensemble R -> R.
Axiom B01_Proba : Espace_proba R B01 B01_uniforme.
Axiom B01_fondamental : forall u v : R,
Included R (Mesure.Intervalle_ferme u v) U01 ->
u<=v ->
B01_uniforme (Mesure.Intervalle_ferme u v) = v - u.
Axiom B01_etendu : forall (E : Ensemble R),
In (Ensemble R) B01 E ->
B01_uniforme E = B01_uniforme (Intersection R E U01).

Theorem B01_uniforme_additive : 
Mesure.Mesure_additive R B01 B01_uniforme.
Proof.
generalize B01_Proba.
intros.
inversion_clear H.
inversion_clear H0.
inversion_clear H2.
inversion_clear H.
apply Mesure.mesure_denomb_additive_est_additive.
trivial.
trivial.
trivial.
Qed.

End Probabilites.