Require Import Reals. Require Import Rtrigo. Require Import Rpower. Set Contextual Implicit. Definition Exp := exp. Definition Ln := ln. Definition Zero := 0%nat. Definition Succ := S%nat. Definition Pred := pred%nat. Definition Le := le. Definition Lt := lt. Definition Ge := ge. Definition Gt := gt. Definition Plus := plus. Definition Minus := minus. Definition Mult := mult. Check ( ( 1 + 2 ) * Ln 1 ) % R. Check (1 + 2) % R. Load proba. Import Mesure. Import Probabilites. Check 0. Module Type PROBA_FLOTS_PARAM. Parameter Element_flot : Set. Parameter Espace_elem_flot : Ensemble (Ensemble Element_flot). Parameter Eef_mesure : Ensemble Element_flot -> R. Parameter Eef_mesure_proba : Espace_proba Element_flot Espace_elem_flot Eef_mesure. End PROBA_FLOTS_PARAM. Module Principal (Proba_flots_param : PROBA_FLOTS_PARAM). (* Définissons le flot. Seront-ce des booléens ? des réels ? On ne sait pas. En tous cas, les éléments du flot sont tous de même type, et ce type est fixé au départ pour tous les programmes. *) Export Proba_flots_param. CoInductive Flot : Set := | Flot_cons : Element_flot -> Flot -> Flot. Notation "a :: b" := (Flot_cons a b) (at level 60, right associativity). Inductive Sous_flot : Flot -> Flot -> Prop := | sous_flot_0 : forall (f : Flot), Sous_flot f f | sous_flot_n : forall (f g : Flot) (e : Element_flot), Sous_flot f g -> Sous_flot f (e::g) . Print Sous_flot_ind. CoFixpoint flot_constant (n : Element_flot) : Flot := Flot_cons n (flot_constant n) . CoFixpoint flot_of_func (f : nat -> Element_flot) : Flot := Flot_cons (f Zero) (flot_of_func (fun n => f (Succ n))) . Fixpoint func_of_flot (f : Flot) (n : nat) {struct n} : Element_flot := match f with | Flot_cons e f' => match n with | Zero => e | Succ n' => func_of_flot f' n' end end. Section Ensf_ord. (*Ensemble de flots, ordonné par une relation bien fondée. *) Variable P : Element_flot -> Prop. Variable Ptrue : Element_flot. Hypothesis P_true : P Ptrue. Variable Pfalse : Element_flot. Hypothesis P_false : ~P Pfalse. Inductive Ensf : Ensemble Flot := | ensf_0 : forall (x : Element_flot) (t : Flot), P x -> In _ Ensf (x::t) | ensf_S : forall (x : Element_flot) (t : Flot), ~P x -> In _ Ensf t -> In _ Ensf (x::t) . Lemma Ensf_sous_flot : forall (x:Element_flot) (t:Flot), In _ Ensf (x::t) -> ~P x -> In _ Ensf t . intros. inversion H. contradiction. subst. trivial. Qed. Inductive Lt_ensf : Flot -> Flot -> Prop := | lt_ensf_0 : forall (x y : Element_flot) (s t : Flot), P x -> ~P y -> In _ Ensf t -> Lt_ensf (x::s) (y::t) | lt_ensf_S : forall (x y : Element_flot) (s t : Flot), ~P x -> ~P y -> Lt_ensf s t -> Lt_ensf (x::s) (y::t) . Lemma Lt_ensf_l : forall (s t :Flot), Lt_ensf s t -> In _ Ensf s . intros. induction H. apply ensf_0. trivial. apply ensf_S. trivial. trivial. Qed. Lemma Lt_ensf_r : forall (s t :Flot), Lt_ensf s t -> In _ Ensf t . intros. induction H. apply ensf_S. trivial. trivial. apply ensf_S. trivial. trivial. Qed. Lemma Lt_ensf_min0 : forall (x : Element_flot) (s t u : Flot), P x -> s = x :: t -> Lt_ensf u s -> False. intros. generalize x t H0 H. clear H0 H x t. induction H1. intros. injection H2. intros. subst. contradiction. intros. injection H2. intros. subst. contradiction. Qed. Lemma Lt_ensf_min : forall (x : Element_flot) (t u : Flot), P x -> Lt_ensf u (x::t) -> False. intros. apply Lt_ensf_min0 with x (x::t) t u. trivial. trivial. trivial. Qed. Lemma Lt_ensf_trans : forall (s t u :Flot), Lt_ensf s t -> Lt_ensf t u -> Lt_ensf s u . intros s t u H. generalize u. clear u. induction H. intros. inversion H2. contradiction. apply lt_ensf_0. trivial. trivial. apply (Lt_ensf_r _ _ H8). intros. inversion H2. contradiction. apply lt_ensf_S. trivial. trivial. apply IHLt_ensf. trivial. Qed. Lemma Lt_ensf_irrefl : forall s t:Flot, Lt_ensf s t -> s = t -> False. intros. generalize H0. clear H0. induction H. intros. injection H2. intros. subst. contradiction. intros. injection H2. intros. apply IHLt_ensf. trivial. Qed. Lemma Lt_ensf_sous_flot_1bis : forall (x: Element_flot) (s t : Flot), ~P x -> s = x::t -> In _ Ensf t -> Lt_ensf t s . intros. generalize x s H H0. clear x s H H0. induction H1. intros. rewrite H1. apply lt_ensf_0. trivial. trivial. apply ensf_0. trivial. intros. rewrite H2. apply lt_ensf_S. trivial. trivial. apply IHEnsf with x. trivial. trivial. Qed. Lemma Lt_ensf_sous_flot_1 : forall (x: Element_flot) (t : Flot), ~P x -> In _ Ensf t -> Lt_ensf t (x::t) . intros. apply Lt_ensf_sous_flot_1bis with x. trivial. trivial. trivial. Qed. Lemma Lt_ensf_sous_flot_2 : forall (x: Element_flot) (t : Flot), ~P x -> In _ Ensf (x::t) -> Lt_ensf t (x::t) . intros. apply Lt_ensf_sous_flot_1. trivial. apply Ensf_sous_flot with x. trivial. trivial. Qed. (* Check Ensf_rec. Definition F_Lt_ensf_0 : forall (s:Flot), In _ Ensf s -> nat. fix 2. intros. case s. intros. induction H. --> ne marche pas. *) Lemma Lt_ensf_S_n : forall (x y : Element_flot) (t u : Flot), ~P x -> ~P y -> Lt_ensf (x::t) (y::u) -> Lt_ensf t u . intros. inversion_clear H1. contradiction. trivial. Qed. Fixpoint Ensf_n (n : nat) :Flot := match n with | Zero => Ptrue :: flot_constant Ptrue | Succ n' => Pfalse :: Ensf_n n' end . Lemma Ensf_n_ensf : forall n:nat, In _ Ensf (Ensf_n n). induction n. unfold Ensf_n. apply ensf_0. trivial. unfold Ensf_n. fold Ensf_n. apply ensf_S. trivial. trivial. Qed. Lemma Ensf_majore : forall a:Flot, In _ Ensf a -> exists n, Lt_ensf a (Ensf_n (S n)) . intros. induction H. exists 0%nat. unfold Ensf_n. apply lt_ensf_0. trivial. trivial. apply ensf_0. trivial. casser_les_cailloux. exists (S x0). unfold Ensf_n. fold Ensf_n. apply lt_ensf_S. trivial. trivial. trivial. Qed. Lemma Ensf_n_inc_nat : forall n p : nat, Lt n p -> Lt_ensf (Ensf_n n) (Ensf_n p) . intros. induction H. unfold Ensf_n. fold Ensf_n. apply Lt_ensf_sous_flot_1. trivial. apply Ensf_n_ensf. apply Lt_ensf_trans with (Ensf_n m). trivial. unfold Ensf_n. fold Ensf_n. apply Lt_ensf_sous_flot_1. trivial. apply Ensf_n_ensf. Qed. Lemma Ensf_n_inc_ensf : forall n p : nat, Lt_ensf (Ensf_n n) (Ensf_n p) -> Lt n p . intros. case le_or_lt with p n. intro. inversion H0. subst. case Lt_ensf_irrefl with (1 := H). trivial. case Lt_ensf_irrefl with (Ensf_n n) (Ensf_n n). apply Lt_ensf_trans with (Ensf_n p). trivial. apply Ensf_n_inc_nat. subst. apply le_lt_n_Sm. trivial. trivial. trivial. Qed. Lemma Ensf_n_borne : forall (n : nat) (a b : Flot), Lt_ensf a (Ensf_n (S n)) -> Lt_ensf b a -> Lt_ensf b (Ensf_n n) . induction n. unfold Ensf_n. intros. inversion H. subst. case Lt_ensf_min with (2 := H0). trivial. subst. case Lt_ensf_min with (2 := H6). trivial. intros. inversion H. subst. case Lt_ensf_min with (2 := H0). trivial. subst. generalize (Lt_ensf_l _ _ H0). intros. inversion H1. subst. unfold Ensf_n. fold Ensf_n. apply lt_ensf_0. trivial. trivial. apply Ensf_n_ensf. subst. unfold Ensf_n. fold Ensf_n. apply lt_ensf_S. trivial. trivial. apply IHn with s. trivial. inversion H0. subst. contradiction. trivial. Qed. Lemma Ensf_acc : forall n:nat, forall a:Flot, Lt_ensf a (Ensf_n n) -> Acc Lt_ensf a. induction n. unfold Ensf_n. intros. case Lt_ensf_min with (2:=H). trivial. intros. inversion_clear H. apply Acc_intro. intros. case Lt_ensf_min with (2:= H). trivial. apply Acc_intro. intros. inversion H. subst. apply Acc_intro. intros. case Lt_ensf_min with (2:= H3). trivial. subst. generalize H2 IHn. case n. intros. unfold Ensf_n in H3. case Lt_ensf_min with (2:= H3). trivial. intros. apply IHn0. unfold Ensf_n. fold Ensf_n. apply lt_ensf_S. trivial. trivial. apply Ensf_n_borne with s. trivial. trivial. Qed. Theorem Wf_lt_ensf : well_founded Lt_ensf. compute. intros. case (Classical_Prop.classic (In _ Ensf a)). intros. case Ensf_majore with a. trivial. intros. apply Ensf_acc with (S x). trivial. intros. apply Acc_intro. intros. case H. apply (Lt_ensf_r y a H0). Qed. End Ensf_ord. Module Lambda_o. (* Type pour les Fonctions. *) Variable Fleche : Set -> Set -> Set. (* Ou bien, on peut utiliser le m\u00eame qu'en Coq : Definition Fleche : Set -> Set -> Set. intros a b. exact (a -> b). Defined. *) (* En tous cas, on utilisera toujours, dans les Preuves, le constructeur T_fleche plutôt que la flèche de Coq. *) Notation "a ->> b" := (Fleche a b) (at level 49, right associativity). (* Pareil pour le couple. *) Variable Couple : Set -> Set -> Set. Notation "a ** b" := (Couple a b) (at level 40). (* Definition Couple : Set -> Set -> Set. intros a b. exact ((a * b)%type). Defined. *) (* Par contre, pour le O, impossible de faire autrement que Variable. *) Variable o : Set -> Set. (* Fonctions : le triangle et la relation d'application. *) Variable Relation_triangle : forall (A B : Set), B -> (A ->> B) -> A -> Prop. Implicit Arguments Relation_triangle. Notation "b <-- f -- a" := (Relation_triangle b f a) (at level 73). Notation "a -- f --> b" := (Relation_triangle b f a) (at level 73). Axiom Fonctionnalite_triangle : forall (A B : Set) (f : A ->> B) (a : A) (b b' : B), a -- f --> b -> a -- f --> b' -> b = b'. Definition Triangle (A B : Set) (f : Fleche A B) (beta : A -> B -> Prop) : Prop := forall (a : A) (b : B), a -- f --> b -> beta a b. Implicit Arguments Triangle. Notation "f |> b" := (Triangle f b) (at level 74, right associativity). Theorem Triangle_elim : forall (A B : Set) (f : A ->> B) (beta : A -> B -> Prop) (a : A) (b : B), a -- f --> b -> f |> beta -> beta a b. Proof. intros. unfold Triangle in H0. apply H0. trivial. Qed. Implicit Arguments Triangle_elim [ A B ]. Theorem Triangle_intro : forall (A B : Set) (f : A ->> B) (beta : A -> B -> Prop), (forall (a : A) (b : B), a -- f --> b -> beta a b) -> f |> beta. Proof. intros. unfold Triangle. intros. apply H. trivial. Qed. Implicit Arguments Triangle_intro [ A B ]. (* Oui, mais il faut aussi la terminaison. *) Definition Terminaison_triangle (A B :Set) (f : A ->> B) (alpha : A -> Prop) : Prop := forall a : A, alpha a -> exists b, a -- f --> b. Implicit Arguments Terminaison_triangle [ A B ]. Definition Double_triangle (A B : Set) (f : Fleche A B) (alpha : A -> Prop) (beta : A -> B -> Prop) : Prop := Terminaison_triangle f alpha /\ Triangle f beta. Implicit Arguments Double_triangle [ A B ]. (* Couple : la croix et la relation de couple. Ici, pas besoin de terminaison, le couple n'étant pas à évaluation retardée *) Variable Relation_croix : forall (A B : Set), A ** B -> A -> B -> Prop. Implicit Arguments Relation_croix. Notation "a << c >> b" := (Relation_croix c a b) (at level 73). Definition Croix : forall (A B : Set), A ** B -> (A -> B -> Prop) -> Prop := fun A B c beta => forall (a : A) (b : B), a << c >> b -> beta a b. Implicit Arguments Croix. Notation "c (X) b" := (Croix c b) (at level 74, right associativity). Theorem Croix_elim : forall (A B : Set) (c : A ** B) (beta : A -> B -> Prop) (a : A) (b : B), a << c >> b -> c (X) beta -> beta a b. Proof. intros. unfold Croix in H0. apply H0. trivial. Qed. Implicit Arguments Croix_elim [ A B ]. Theorem Croix_intro : forall (A B : Set) (c : A ** B) (beta : A -> B -> Prop), (forall (a : A) (b : B), a << c >> b -> beta a b) -> c (X) beta. Proof. intros. unfold Croix. intros. apply H. trivial. Qed. Implicit Arguments Croix_intro [ A B ]. Axiom Fonctionnalite_croix : forall (A B : Set) (c : A ** B) (a1 a2 : A) (b1 b2 : B), a1 << c >> b1 -> a2 << c >> b2 -> a1 = a2 /\ b1 = b2 . (* Prob : le carré et la relation de loi. Attention, l\u00e0, le flot est important. *) Variable Relation_carre : forall (A : Set), Flot -> A -> Flot -> o A -> Prop. Implicit Arguments Relation_carre. Notation "{ s >> p ~> x >> t }" := (Relation_carre s x t p) (at level 0). Definition Carre (A : Set) (p : o A) (beta : Flot -> A -> Flot -> Prop) : Prop := forall (x : A) (s t : Flot), { s >> p ~> x >> t } -> beta s x t. Implicit Arguments Carre. Notation "p [] b" := (Carre p b) (at level 74, right associativity). Axiom Fonctionnalite_carre : forall (A : Set) (p : o A) (y y' : A) (s t t' : Flot), {s >> p ~> y >> t} -> {s >> p ~> y' >> t'} -> y = y' /\ t = t' . (* Axiome du sous-flot. *) Axiom Relation_carre_sous_flot : forall (A : Set) (s t : Flot) (p : o A) (x : A), { s >> p ~> x >> t } -> Sous_flot t s. Theorem Carre_elim : forall (A : Set) (distri : o A) (beta : Flot -> A -> Flot -> Prop) (flot_entree flot_sortie : Flot) (a : A), {flot_entree >> distri ~> a >> flot_sortie} -> distri [] beta -> beta flot_entree a flot_sortie. Proof. intros. unfold Carre in H0. apply H0. trivial. Qed. Implicit Arguments Carre_elim [ A ]. Theorem Carre_intro : forall (A : Set) (distri : o A) (beta : Flot -> A -> Flot -> Prop), (forall (flot_entree flot_sortie : Flot) (a : A), {flot_entree >> distri ~> a >> flot_sortie} -> beta flot_entree a flot_sortie ) -> distri [] beta. Proof. intros. unfold Carre. intros. apply H. trivial. Qed. Implicit Arguments Carre_intro [ A ]. (* Et là aussi, la terminaison. *) Definition Terminaison_carre (A : Set) (p : o A) (alpha : Flot -> Prop) : Prop := forall s:Flot, alpha s -> exists y:A, exists t:Flot, {s >> p ~> y >> t}. Implicit Arguments Terminaison_carre [ A ]. Definition Double_carre (A : Set) (p : o A) (alpha : Flot -> Prop) (beta : Flot -> A -> Flot -> Prop) : Prop := Terminaison_carre p alpha /\ Carre p beta. Implicit Arguments Double_carre [ A ]. (* Quelques lemmes d'introduction triviaux. Pas tant que cela : on se rend compte que l'on ne peut montrer qu'un seul sens. L'autre doit \u00eatre posé en axiome. (\u00e0 moins de supposer que les ensembles sont non vides) Inductive Non_vide : Set -> Prop := | non_vide_R : Non_vide R | non_vide_bool : Non_vide bool | non_vide_nat : Non_vide nat | non_vide_fleche : forall (U V : Set), Non_vide V -> Non_vide (Fleche U V) | non_vide_couple : forall (U V : Set), Non_vide U -> Non_vide V -> Non_vide (Couple U V) | non_vide_o : forall (U : Set), Non_vide U -> Non_vide (o U) . Axiom Ensemble_non_vide : forall (A : Set), Non_vide A -> exists a : A, True. *) Lemma Triangle_inutile_intro : forall (P : Prop) (A B : Set) (f : A ->> B), P -> f |> (fun _ _ => P). Proof. intros. apply Triangle_intro. trivial. Qed. Axiom Triangle_inutile_elim : forall (P : Prop) (A B : Set) (f : A ->> B), f |> (fun _ _ => P) -> P. Lemma Croix_inutile_intro : forall (P : Prop) (A B : Set) (c : A ** B), P -> c (X) (fun _ _ => P). Proof. intros. apply Croix_intro. trivial. Qed. Axiom Croix_inutile_elim : forall (P : Prop) (A B : Set) (c : A ** B), c (X) (fun _ _ => P) -> P. Lemma Carre_inutile_intro : forall (P : Prop) (A : Set) (p : o A), P -> p [] (fun _ _ _ => P). intros. apply Carre_intro. trivial. Qed. Axiom Carre_inutile_elim : forall (P : Prop) (A : Set) (p : o A), p [] (fun _ _ _ => P) -> P. (* Lemmes d'implication. *) Lemma Triangle_imp : forall (A B : Set) (f : A ->> B) (beta beta' : A -> B -> Prop), (forall (a : A) (b : B), beta a b -> beta' a b) -> f |> beta -> f |> beta'. Proof. intros. apply Triangle_intro. intros. apply H. Print Triangle_elim. apply (Triangle_elim f). trivial. trivial. Qed. Lemma Croix_imp : forall (A B : Set) (c : A ** B) (beta beta' : A -> B -> Prop), (forall (a : A) (b : B), beta a b -> beta' a b) -> c (X) beta -> c (X) beta'. Proof. intros. apply Croix_intro. intros. apply H. apply (Croix_elim c). trivial. trivial. Qed. Lemma Carre_imp : forall (A: Set) (p : o A) (beta beta' : Flot -> A ->Flot -> Prop), (forall (a : A) (s s' : Flot), beta s a s' -> beta' s a s') -> p [] beta -> p [] beta'. Proof. intros. apply Carre_intro. intros. apply H. apply (Carre_elim p). trivial. trivial. Qed. (* Conjonction. *) Lemma Triangle_and_out : forall (A B : Set) (f : A ->> B) (beta beta' : A -> B -> Prop), f |> (fun a b => beta a b /\ beta' a b) -> (f |> beta /\ f |> beta'). Proof. split. apply Triangle_imp with (fun a b => beta a b /\ beta' a b). intros. inversion H0. trivial. trivial. apply Triangle_imp with (fun a b => beta a b /\ beta' a b). intros. inversion H0. trivial. trivial. Qed. Lemma Triangle_and_in : forall (A B : Set) (f : A ->> B) (beta beta' : A -> B -> Prop), (f |> beta /\ f |> beta')-> f |> (fun a b => beta a b /\ beta' a b). Proof. intros. inversion H. apply Triangle_intro. intros. split. apply Triangle_elim with A B f. trivial. trivial. apply Triangle_elim with A B f. trivial. trivial. Qed. (* Un théorème de permutation des triangles, pour donner le goût. *) (* Mais d'abord, un axiome d'êta-expansion. *) Axiom Egalite_observationnelle : forall (U V : Type) (b b' : U -> V), (forall u, b u = b' u) -> b = b'. Theorem Triangle_permut : forall (A B A' B' : Set) (f : A ->> B) (f' : A' ->> B') (Beta : A -> B -> A' -> B' -> Prop), f |> (fun a b => f' |> (fun a' b' => Beta a b a' b')) -> f' |> (fun a' b' => f |> (fun a b => Beta a b a' b')). Proof. intros. apply Triangle_intro. intros. apply Triangle_intro. intros. apply (Triangle_elim f'). trivial. assert (Beta a0 b0 = fun a' b' => Beta a0 b0 a' b'). apply Egalite_observationnelle. intros. apply Egalite_observationnelle. trivial. rewrite H2. apply (Triangle_elim f (fun a b => f' |> (fun (a' : A') (b' : B') => Beta a b a' b') ) ). trivial. apply H. Qed. End Lambda_o. Print Module Lambda_o. (* On va mettre ici tout ce qui concerne la mesure (espace mesurable, etc.) Commen\u00e7ons par une approche na\u00efve. *) Module Proba_flots. Inductive Predicat_sur_flot_fini : Type := | pred_ff_0 : Prop -> Predicat_sur_flot_fini | pred_ff_n : (Element_flot -> Predicat_sur_flot_fini) -> Predicat_sur_flot_fini. Definition Pred_ff_application (phi : Predicat_sur_flot_fini) (f : Flot) : Prop := (fix aux (phi : Predicat_sur_flot_fini) (f : Flot) {struct phi} : Prop := match phi with | pred_ff_0 psi => psi | pred_ff_n psi => match f with | Flot_cons epsilon f' => aux (psi epsilon) f' end end) phi f. Definition Pred_ff_app_sur_queue (phi : Predicat_sur_flot_fini) (beta : Flot -> Prop) (f : Flot) : Prop := (fix aux (phi : Predicat_sur_flot_fini) (beta : Flot -> Prop) (f : Flot) {struct phi} : Prop := match phi with | pred_ff_0 psi => beta f | pred_ff_n psi => match f with | Flot_cons epsilon f' => aux (psi epsilon) beta f' end end) phi beta f. Fixpoint Predicat_vrai_sur_extractions (n : nat) {struct n} : Predicat_sur_flot_fini := match n with | Zero => pred_ff_0 True | Succ n' => pred_ff_n (fun _ => Predicat_vrai_sur_extractions n') end. Definition Produit_ensembles_flots (e:Ensemble Element_flot) (E:Ensemble Flot) : Ensemble Flot := (fun f => match f with Flot_cons eps f' => In Element_flot e eps /\ In Flot E f' end). Inductive Est_rectangle (F : Ensemble (Ensemble Element_flot)) : Ensemble Flot -> Prop := | est_rectangle_0 : Est_rectangle F (fun _ => True) | est_rectangle_n : forall (e:Ensemble Element_flot) (E:Ensemble Flot), In (Ensemble Element_flot) F e -> Est_rectangle F E -> Est_rectangle F (Produit_ensembles_flots e E). Definition Espace_flots := Mesure.sigma Flot (Est_rectangle Espace_elem_flot). Variable Ef_mesure : Ensemble Flot -> R. Axiom Ef_mesure_proba : Espace_proba Flot Espace_flots Ef_mesure. Definition Predicat_sur_tete (g : Ensemble Element_flot) : Ensemble Flot := (fun s => match s with Flot_cons eps _ => g eps end). Definition Predicat_sur_queue (beta : Ensemble Flot) : Ensemble Flot := (fun s => match s with Flot_cons _ s' => beta s' end). Lemma Predicat_sur_tete_est_produit : forall (g : Ensemble Element_flot), Predicat_sur_tete g = Produit_ensembles_flots g (fun _ => True) . intros. apply Extensionality_Ensembles. split. compute. intro x. case x. intros. split. trivial. trivial. compute. intro x ; case x. intros. intuition. Qed. Lemma Predicat_sur_queue_est_produit : forall (g : Ensemble Flot), Predicat_sur_queue g = Produit_ensembles_flots (fun _ => True) g . intros. apply Extensionality_Ensembles. split. compute. intro x. case x. intros. split. trivial. trivial. compute. intro x ; case x. intros. intuition. Qed. Axiom Flot_mesure_tete : forall (e:Ensemble Element_flot), Ef_mesure (Predicat_sur_tete e) = Eef_mesure e. Axiom Invariance_translation : forall (beta : Ensemble Flot), Ef_mesure (Predicat_sur_queue beta) = Ef_mesure beta. Lemma Est_rectangle_tete : forall (F : Ensemble (Ensemble Element_flot)) (e : Ensemble Element_flot), In (Ensemble Element_flot) F e -> Est_rectangle F (Predicat_sur_tete e). intros. rewrite Predicat_sur_tete_est_produit. apply est_rectangle_n. trivial. apply est_rectangle_0. Qed. Lemma Est_rectangle_queue_decalee : forall (F : Ensemble (Ensemble Element_flot)) (g : Ensemble Flot), In _ F (Full_set _) -> Est_rectangle F g -> Est_rectangle F (Predicat_sur_queue g). intros. rewrite Predicat_sur_queue_est_produit. apply est_rectangle_n. rewrite <- Full_set_is_true. trivial. trivial. Qed. Axiom Ef_extractions_indep : forall (phi : Predicat_sur_flot_fini) (beta : Flot -> Prop), In (Ensemble Flot) Espace_flots (Pred_ff_application phi) -> In (Ensemble Flot) Espace_flots (Pred_ff_app_sur_queue phi beta) -> Evenements_independants Flot Espace_flots Ef_mesure (Pred_ff_application phi) (Pred_ff_app_sur_queue phi beta) . Lemma Flot_une_extraction_indep : forall (g : Element_flot -> Prop) (beta : Flot -> Prop), In (Ensemble Flot) Espace_flots (Predicat_sur_tete g) -> In (Ensemble Flot) Espace_flots (Predicat_sur_queue beta) -> Evenements_independants Flot Espace_flots Ef_mesure (Predicat_sur_tete g) (Predicat_sur_queue beta) . Proof. intros. apply (Ef_extractions_indep (pred_ff_n (fun eps => pred_ff_0 (g eps))) beta). trivial. trivial. Qed. Lemma Flot_mesure_rectangle : forall (e:Ensemble Element_flot) (E:Ensemble Flot), In (Ensemble Element_flot) Espace_elem_flot e -> Est_rectangle Espace_elem_flot E -> Ef_mesure (Produit_ensembles_flots e E) = (Eef_mesure e * Ef_mesure E)%R . Proof. intros. assert (Evenements_independants Flot Espace_flots Ef_mesure (Predicat_sur_tete e) (Predicat_sur_queue E) ). apply Flot_une_extraction_indep. unfold Espace_flots. rewrite <- (sigma_est_sigma2). apply sigma_0. unfold In. rewrite Predicat_sur_tete_est_produit. apply est_rectangle_n. trivial. apply est_rectangle_0. rewrite Predicat_sur_queue_est_produit. unfold Espace_flots. rewrite <- (sigma_est_sigma2). apply sigma_0. unfold In. apply est_rectangle_n. unfold In. rewrite <- Full_set_is_true. rewrite <- Complement_empty_is_full. generalize (Eef_mesure_proba). unfold Espace_proba. unfold Espace_mesurable. unfold Sigma_algebre. unfold Algebre. intuition. apply H2. trivial. trivial. inversion_clear H1. casser_les_cailloux. rewrite <- (Flot_mesure_tete). rewrite <- (Invariance_translation E). transitivity ( Ef_mesure (Intersection Flot (Predicat_sur_tete e) (Predicat_sur_queue E)) ). assert ( Produit_ensembles_flots e E = Intersection Flot (Predicat_sur_tete e) (Predicat_sur_queue E) ). apply Extensionality_Ensembles. split. unfold Included. unfold In. unfold Produit_ensembles_flots. intro x. case x ; intros. casser_les_cailloux. apply Intersection_intro. unfold In. unfold Predicat_sur_tete. trivial. unfold In. unfold Predicat_sur_queue. trivial. unfold Included. unfold In. intro x. case x ; intros. inversion_clear H3. generalize H5 H6. unfold Produit_ensembles_flots. unfold In. unfold Predicat_sur_tete. unfold Predicat_sur_queue. intuition. rewrite H3. trivial. rewrite <- H4. trivial. (* unfold Espace_flots. rewrite <- sigma_est_sigma2. apply sigma_0. unfold In. trivial. trivial. *) Qed. End Proba_flots. Module Proba_locale. Export Lambda_o. Export Proba_flots. (* Probabilités locales sur les flots. *) Variable Proba_locale : Flot -> Prop -> R. Axiom Proba_globale : forall (s : Flot) (phi : Ensemble Flot), Proba_locale s (phi s) = Ef_mesure phi. Axiom Proba_proprietes_equiv : forall (phi1 phi2 : Prop) (s : Flot), (phi1 <-> phi2) -> Proba_locale s phi1 = Proba_locale s phi2. Lemma Proba_un_ajout : forall (s : Flot) (eps : Element_flot) (phi : Flot -> Prop), Proba_locale s (phi s) = Proba_locale (eps::s) (phi s) . intros. rewrite Proba_globale. transitivity (Ef_mesure (Predicat_sur_queue phi)). rewrite Invariance_translation. trivial. trivial. rewrite (Proba_globale (eps :: s) (fun s' => match s' with eps::s => phi s end)). compute. trivial. Qed. Lemma Proba_queue : forall (s t : Flot) (phi : Flot -> Prop), Sous_flot t s -> Proba_locale s (phi t) = Proba_locale t (phi t) . intros. induction H. trivial. rewrite <- IHSous_flot. rewrite <- (Proba_un_ajout g e (fun _ => phi f)). trivial. Qed. Axiom Proba_tete_queue_indep : forall (U V : Set) (phi : U -> Prop) (psi : V -> Prop) (p : o U) (q : o V) (y : U) (z : V) (s t u : Flot), {s >> p ~> y >> t} -> {t >> q ~> z >> u} -> Proba_locale s (phi y /\ psi z) = Proba_locale s (phi y) * Proba_locale t (psi z) . End Proba_locale. Export Proba_locale. End Principal. Module Alice_param : PROBA_FLOTS_PARAM with Definition Element_flot := R with Definition Espace_elem_flot := B01 with Definition Eef_mesure := B01_uniforme . Definition Element_flot := R. Definition Espace_elem_flot := B01. Definition Eef_mesure := B01_uniforme. Lemma Eef_mesure_proba : Espace_proba R Espace_elem_flot Eef_mesure. apply B01_Proba. Qed. End Alice_param. Module Alice := Principal Alice_param. Import Alice. Print Element_flot. Lemma bidon : forall x : Element_flot, (x = x + 0)%R. intros. auto with real. Qed. Lemma Bernoulli1 : forall (p:R), 0 <= p <= 1 -> Ef_mesure (fun s => exists eps, exists s', s = Flot_cons eps s' /\ eps <= p) = p. Proof. intros. inversion_clear H. assert ( Produit_ensembles_flots (fun eps => eps <= p) (fun _ => True) = fun s => exists eps, exists s', s = Flot_cons eps s' /\ eps <= p ). apply Extensionality_Ensembles. compute. intuition. generalize H. case x. intros. casser_les_cailloux. exists e. exists f. split. trivial. trivial. case H. intros eps. intros (s', (H2,H3)). (* remplace : inversion_clear H. inversion_clear H2. inversion_clear H. *) rewrite H2. split. trivial. trivial. rewrite <- H. rewrite Flot_mesure_rectangle. rewrite <- Full_set_is_true. generalize Ef_mesure_proba. intros. inversion_clear H2. rewrite H4. rewrite Rmult_1_r. rewrite B01_etendu. assert ( Intervalle_ferme 0 p = Intersection R (fun eps : Element_flot => eps <= p) U01). apply Extensionality_Ensembles. split. compute. intros. inversion_clear H2. apply Intersection_intro. compute. trivial. compute. split. trivial. assert (x <= 1). apply (Rle_trans x p). trivial. trivial. trivial. compute. intros. inversion_clear H2. compute in H6. compute in H5. inversion_clear H6. split. trivial. trivial. rewrite <- H2. rewrite B01_fondamental. apply Rminus_0_r. compute. intros. inversion_clear H5. split. trivial. assert (x <= 1). apply (Rle_trans x p). trivial. trivial. trivial. trivial. compute. intros. casser_les_cailloux. apply H6. exists 0. exists p. assert ( Intersection R (fun x : R => (0 < x \/ 0 = x) /\ (x < 1 \/ x = 1)) (fun eps : R => eps < p \/ eps = p) = (fun x : R => (0 < x \/ 0 = x) /\ (x < p \/ x = p)) ). apply Extensionality_Ensembles. split. compute. intros. inversion_clear H8. compute in H10. inversion_clear H10. compute in H11. split. trivial. trivial. compute. intros. inversion_clear H8. apply Intersection_intro. compute. split. trivial. assert (x <= 1). apply (Rle_trans x p). trivial. trivial. trivial. compute. trivial. trivial. compute. intros. casser_les_cailloux. apply H4. exists 0. exists p. assert ( Intersection R (fun x : R => (0 < x \/ 0 = x) /\ (x < 1 \/ x = 1)) (fun eps : R => eps < p \/ eps = p) = (fun x : R => (0 < x \/ 0 = x) /\ (x < p \/ x = p)) ). apply Extensionality_Ensembles. split. compute. intros. inversion_clear H6. compute in H8. inversion_clear H8. compute in H9. split. trivial. trivial. compute. intros. inversion_clear H6. apply Intersection_intro. compute. split. trivial. assert (x <= 1). apply (Rle_trans x p). trivial. trivial. trivial. compute. trivial. trivial. apply est_rectangle_0. Qed. Print Bernoulli1. Theorem Point_pathologique : forall (E : Ensemble R) (p q z : R), p <= q -> In R (Intervalle_ferme p q) z -> Intersection R (Union R E (Intervalle_ferme z z)) U01 = Intervalle_ferme p q -> In (Ensemble R) B01 E /\ B01_uniforme E = q - p. Proof. intros. assert (Included R (Intervalle_ferme p q) U01). rewrite <- H1. apply Intersection_included_2. assert (Included R (Intervalle_ferme z z) (Intervalle_ferme p q)). apply Trans_incl with (Intervalle_ferme p q). unfold Included. unfold In. intros. rewrite (Intervalle_singleton z x). trivial. trivial. apply Refl_incl. assert (In (Ensemble R) B01 (Union R E (Intervalle_ferme z z))). unfold B01. unfold Boreliens. unfold sigma. unfold Operations_ensembles.Intersection. unfold Included. unfold In. intuition. apply H6. exists p. exists q. rewrite Intersection_commut. rewrite H1. trivial. assert (In R E z -> Union R E (Intervalle_ferme z z) = E). intros. apply Extensionality_Ensembles. split. unfold Included. intros. unfold In in H6. inversion_clear H6. trivial. unfold In in H7. rewrite (Intervalle_singleton z x). trivial. trivial. apply Union_includes. assert ( (In R E z -> False) -> E = Intersection R (Union R E (Intervalle_ferme z z)) (Complement R (Intervalle_ferme z z))). intros. apply Extensionality_Ensembles. split. unfold Included. intros. unfold In. apply Intersection_intro. apply Union_introl. trivial. unfold In. unfold Complement. unfold not. intros. generalize H7. rewrite (Intervalle_singleton z x). trivial. trivial. unfold Included. intros. unfold In in H7. inversion_clear H7. unfold In in H9. unfold In in H8. inversion_clear H8. trivial. rewrite (Intervalle_singleton z x). unfold Complement in H9. contradiction. trivial. assert (In (Ensemble R) B01 E). generalize (Classical_Prop.classic (In R E z)). intros. inversion_clear H7. intuition. rewrite <- H7. trivial. intuition. unfold B01. unfold Boreliens. unfold sigma. unfold In. unfold Operations_ensembles.Intersection. unfold In. unfold Included. unfold In. unfold Sigma_algebre. intuition. generalize (Stabilite_intersection R e). intuition. generalize H6. unfold Algebre. intuition. rewrite H7. apply H9. trivial. unfold In. apply H10. exists p. exists q. rewrite Intersection_commut. trivial. apply H12. unfold In. apply H10. exists z. exists z. rewrite Intersection_commut. apply Intersection_and_inclusion. apply Trans_incl with (Intervalle_ferme p q). trivial. trivial. split. trivial. generalize (Classical_Prop.classic (In R E z)). intros. inversion_clear H8. intuition. rewrite <- H8. rewrite B01_etendu. rewrite H1. apply B01_fondamental. trivial. trivial. trivial. transitivity (B01_uniforme E + B01_uniforme (Intervalle_ferme z z)). symmetry. rewrite <- Rplus_0_r. apply (Rplus_eq_compat_l). transitivity (z - z). 2: auto with real. apply B01_fondamental. apply Trans_incl with (Intervalle_ferme p q). trivial. trivial. apply Rle_refl. generalize B01_uniforme_additive . unfold Mesure_additive. unfold In. intuition. rewrite <- H8. rewrite B01_etendu. rewrite H1. apply B01_fondamental. trivial. trivial. trivial. trivial. unfold B01. unfold Boreliens. unfold sigma. unfold Operations_ensembles.Intersection. unfold Included. unfold In. intuition. apply H12. exists z. exists z. rewrite Intersection_commut. apply Intersection_and_inclusion. apply Trans_incl with (Intervalle_ferme p q). trivial. trivial. apply Disjoint_intro. intros. unfold In. intro. inversion_clear H6. apply H9. rewrite <- (Intervalle_singleton z x). trivial. trivial. Qed. Lemma exp_large_increasing : forall (x y : R), x <= y -> Exp x <= Exp y . Proof. intros. unfold Rle. inversion_clear H. apply or_introl. apply exp_increasing. trivial. apply or_intror. rewrite H0. trivial. Qed. Lemma ln_large_increasing : forall (x y : R), 0 < x -> x <= y -> Ln x <= Ln y . Proof. intros. unfold Rle. inversion_clear H0. apply or_introl. apply ln_increasing. trivial. trivial. apply or_intror. rewrite H1. trivial. Qed. Lemma Expo1 : forall (p:R), 0 <= p -> Ef_mesure (fun s => exists eps, exists s', s = Flot_cons eps s' /\ (0 - Ln eps) >= p) = Exp (0 - p). Proof. intros. assert ( In (Ensemble R) B01 (fun eps : R => 0 - Ln eps >= p) /\ B01_uniforme (fun eps : R => 0 - Ln eps >= p) = Exp (0 - p) - 0 ). apply Point_pathologique with 0. apply Rlt_le. apply exp_pos. unfold In. unfold Intervalle_ferme. split. apply Rle_refl. apply Rlt_le. apply exp_pos. apply Extensionality_Ensembles. split. unfold Included. unfold In. intros. inversion_clear H0. generalize H1 H2. unfold In. intros. inversion_clear H3. unfold Intervalle_ferme. split. trivial. inversion_clear H0. inversion_clear H4. unfold In in H3. generalize H3. unfold Rminus. repeat rewrite Rplus_0_l. intros. rewrite <- (exp_ln x). apply exp_large_increasing. rewrite <- (Ropp_involutive (ln x)). apply Ropp_ge_le_contravar. trivial. trivial. rewrite <- H0. apply Rlt_le. apply exp_pos. rewrite (Intervalle_singleton 0 x). apply Rlt_le. apply exp_pos. trivial. unfold Included. unfold In. intros. inversion_clear H0. apply Intersection_intro. unfold In. case H1 ; intro. apply Union_introl. unfold In. generalize H2. unfold Rminus. repeat rewrite Rplus_0_l. intros. rewrite <- (Ropp_involutive p). apply Ropp_le_ge_contravar. rewrite <- (ln_exp (-p)). apply ln_large_increasing. trivial. trivial. apply Union_intror. rewrite H0. split. apply Rle_refl. apply Rle_refl. split. trivial. apply (Rle_trans x (Exp (0 - p))). trivial. rewrite <- exp_0. apply exp_large_increasing. unfold Rminus. rewrite Rplus_0_l. rewrite <- Ropp_0. apply Ropp_ge_le_contravar. apply Rle_ge. trivial. inversion_clear H0. assert (Exp (0 - p) - 0 = Exp (0 - p)). unfold Rminus. rewrite Ropp_0. apply Rplus_0_r. rewrite H0 in H2. assert ( Produit_ensembles_flots (fun eps => 0 - Ln eps >= p) (fun _ => True) = fun s => exists eps, exists s', s = Flot_cons eps s' /\ 0 - Ln eps >= p ). apply Extensionality_Ensembles. split. unfold Included. unfold In. intro x. case x. unfold Produit_ensembles_flots. unfold In. intros. inversion_clear H3. exists e. exists f. split. trivial. trivial. unfold Included. unfold In. unfold Produit_ensembles_flots. intro x. case x. intros. inversion_clear H3. inversion_clear H4. inversion_clear H3. unfold In. split. trivial. injection H4. intros. rewrite H6. trivial. trivial. rewrite <- H3. rewrite Flot_mesure_rectangle. assert (Ef_mesure (fun _ => True) = 1). generalize Ef_mesure_proba. intros. inversion_clear H4. rewrite <- Full_set_is_true. trivial. rewrite H4. rewrite Rmult_1_r. trivial. trivial. apply est_rectangle_0. Qed. (* Prochainement : le binomial. *)