From 5e78ceae9bda711e4052d9b127769bc6ad26aeae Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 23 Jul 2024 11:54:54 +0900 Subject: [PATCH] rebase --- theories/kernel.v | 4 ---- theories/lang_syntax.v | 4 ++-- theories/lebesgue_measure.v | 25 ++----------------------- theories/measure.v | 15 +++++++++++++++ theories/prob_lang.v | 14 +++++++------- 5 files changed, 26 insertions(+), 36 deletions(-) diff --git a/theories/kernel.v b/theories/kernel.v index 8ea604304..03dcb71c1 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -765,8 +765,6 @@ HB.instance Definition _ (P : probability Y R):= End knormalize. -<<<<<<< HEAD -(* TODO: useful? *) Lemma measurable_fun_mnormalize d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) : measurable_fun [set: X] (fun x => @@ -797,8 +795,6 @@ apply: measurable_fun_if => //. + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel. Qed. -======= ->>>>>>> ea7f1064 (rm duplicate, more uniform naming) Section kcomp_def. Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) (Z : measurableType d3) (R : realType). diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v index 432d41797..1e011f3de 100644 --- a/theories/lang_syntax.v +++ b/theories/lang_syntax.v @@ -168,10 +168,10 @@ rewrite /ubeta_nat_pdf /=; apply: measurable_fun_if => //=; last first. by rewrite setTI; apply: measurable_funTS; exact: measurable_fun_expn_onem. apply: measurable_and => /=. apply: (measurable_fun_bool true). - rewrite [X in measurable X](_ : _ = `[0, +oo[%classic)//. + rewrite setTI [X in measurable X](_ : _ = `[0, +oo[%classic)//. by rewrite set_interval.set_itv_c_infty. apply: (measurable_fun_bool true). -by rewrite [X in measurable X](_ : _ = `]-oo, 1]%classic)//. +by rewrite setTI [X in measurable X](_ : _ = `]-oo, 1]%classic)//. Qed. Local Notation mu := lebesgue_measure. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index dd7bf3bb6..d0b86c8f6 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1728,7 +1728,7 @@ Lemma measurable_fun_pow D f n : measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). Proof. move=> mf. -apply: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f) => //. +exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). Qed. Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g -> @@ -1747,20 +1747,6 @@ under eq_fun do rewrite -subr_ge0. by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB. Qed. -Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x <= g x). -Proof. -move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. -- under eq_fun do rewrite -subr_ge0. - rewrite preimage_true -preimage_itv_c_infty. - by apply: (measurable_funB mg mf) => //; exact: measurable_itv. -- under eq_fun do rewrite leNgt -subr_gt0. - rewrite preimage_false set_predC setCK -preimage_itv_o_infty. - by apply: (measurable_funB mf mg) => //; exact: measurable_itv. -- by rewrite preimage_set0 setI0. -- by rewrite preimage_setT setIT. -Qed. - (* setT should be D? (derived from measurable_and) *) Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (fun x => f x == g x). @@ -1876,7 +1862,7 @@ have [Y0|Y0] := boolP (0%E \in Y). rewrite [X in _ -> X](_ : _ = Y (\d_r U)) //. rewrite diracE. move/mem_set. - case (_ \in _) => //= _. + case: (_ \in _) => //= _. by rewrite inE in Y1. + rewrite [X in measurable X](_ : _ = set0). exact: measurable0. @@ -1922,13 +1908,6 @@ under eq_fun do rewrite -mulr_natr. by do 2 apply: measurable_funM => //. Qed. -Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f -> - measurable_fun D (fun x => f x ^+ n). -Proof. -move=> mf. -exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). -Qed. - Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). Proof. diff --git a/theories/measure.v b/theories/measure.v index 8622ea91d..e3765762f 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1615,6 +1615,21 @@ rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` by apply: measurableI; [exact: mf|exact: mg]. Qed. +Lemma measurable_or D (f : T1 -> bool) (g : T1 -> bool) : + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x || g x). +Proof. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `|` + (D `&` g @^-1` [set true])); last first. + apply/seteqP; split=> [x [Dx/= /orP[]->]|x [|]/=]. + by left. + by right. + by move=> [Dx ->]; split. + by move=> [Dx ->]; split => //; apply/orP; right. +by apply: measurableU; [exact: mf|exact: mg]. +Qed. + End measurable_fun_measurableType. #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => solve [apply: measurable_cst] : core. diff --git a/theories/prob_lang.v b/theories/prob_lang.v index 14daaaea0..73e831df9 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import rat. +From mathcomp Require Import rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum measure. @@ -921,14 +921,14 @@ pose floor_f := widen_ord (leq_addl n `|floor `|f t| |.+1) (Ordinal (ltnSn `|floor `|f t| |)). rewrite big_mkord (bigD1 floor_f)//= ifT; last first. rewrite lee_fin lte_fin; apply/andP; split. - by rewrite natr_absz (@ger0_norm _ (floor `|f t|)) ?floor_ge0 ?floor_le. - rewrite -addn1 natrD natr_absz. - by rewrite (@ger0_norm _ (floor `|f t|)) ?floor_ge0 ?lt_succ_floor. + by rewrite natr_absz (@ger0_norm _ (floor `|f t|)) ?floor_ge0// ?ge_floor. + rewrite -natr1 natr_absz. + by rewrite (@ger0_norm _ (floor `|f t|)) ?floor_ge0// intrD1 lt_succ_floor. rewrite big1 ?adde0//= => j jk. rewrite ifF// lte_fin lee_fin. move: jk; rewrite neq_ltn/= => /orP[|] jr. - suff : (j.+1%:R <= `|f t|)%R by rewrite leNgt => /negbTE ->; rewrite andbF. - rewrite (_ : j.+1%:R = j.+1%:~R)// floor_ge_int. + rewrite (_ : j.+1%:R = j.+1%:~R)// floor_ge_int//. move: jr; rewrite -lez_nat => /le_trans; apply. by rewrite -[leRHS](@ger0_norm _ (floor `|f t|)) ?floor_ge0. - suff : (`|f t| < j%:R)%R by rewrite ltNge => /negbTE ->. @@ -1823,7 +1823,7 @@ Hypotheses (mf : measurable_fun setT f) (mg : measurable_fun setT g). Lemma measurable_fun_flift_neq : measurable_fun setT flift_neq. Proof. apply: (measurable_fun_bool true). -rewrite /flift_neq /= (_ : _ @^-1` _ = ([set x | f x] `&` [set x | ~~ g x]) `|` +rewrite setTI /flift_neq /= (_ : _ @^-1` _ = ([set x | f x] `&` [set x | ~~ g x]) `|` ([set x | ~~ f x] `&` [set x | g x])). apply: measurableU; apply: measurableI. - by rewrite -[X in measurable X]setTI; exact: mf. @@ -2074,7 +2074,7 @@ Lemma sample_and_branchE t U : sample_and_branch t U = (2 / 7)%:E * \d_(3 : R) U + (5 / 7)%:E * \d_(10 : R) U. Proof. rewrite /sample_and_branch letin_sample_bernoulli/=; last lra. -by rewrite !iteE !retE onem27. +by rewrite !iteE/= onem27. Qed. End sample_and_branch.