From 9fcf29b61e08401865e9f14c1d5f2cd8ea511e70 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 22 Apr 2025 14:26:15 +0900 Subject: [PATCH 1/2] generic lemmas from the prob_lang PR Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 18 ++++++++++++++++++ classical/classical_sets.v | 23 +++++++++++++++++++++++ classical/mathcomp_extra.v | 6 ++++++ reals/constructive_ereal.v | 5 +++++ theories/ftc.v | 18 ++++++++++++++++++ theories/kernel.v | 4 ++-- theories/measure.v | 14 ++++++++++++++ theories/probability.v | 28 ++++++++++++++++++++++++++++ 8 files changed, 114 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3a2ed8859f..854a789d13 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,24 @@ ### Added +- in `probability.v`: + + lemmas `eq_bernoulli`, `eq_bernoulliV2` + +- in `measure.v`: + + lemmas `mnormalize_id`, `measurable_fun_eqP` + +- in `ftc.v`: + + lemma `integrable_locally` + +- in `constructive_ereal.v`: + + lemma `EFin_bigmax` + +- in `mathcomp_extra.v`: + + lemmas `inr_inj`, `inl_inj` + +- in `classical_sets.v`: + + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f` + ### Changed ### Renamed diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 21edb0eb0b..2f68504bd3 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -555,6 +555,7 @@ Qed. Notation setTP := setTPn (only parsing). Lemma in_set0 (x : T) : (x \in set0) = false. Proof. by rewrite memNset. Qed. + Lemma in_setT (x : T) : x \in setT. Proof. by rewrite mem_set. Qed. Lemma in_setC (x : T) A : (x \in ~` A) = (x \notin A). @@ -1441,9 +1442,15 @@ Implicit Types (A B : set aT) (f : aT -> rT) (Y : set rT). Lemma imageP f A a : A a -> (f @` A) (f a). Proof. by exists a. Qed. +Lemma image_f f A a : a \in A -> f a \in [set f x | x in A]. +Proof. by rewrite !inE; apply/imageP. Qed. + Lemma imageT (f : aT -> rT) (a : aT) : range f (f a). Proof. by apply: imageP. Qed. +Lemma mem_range f a : f a \in range f. +Proof. by rewrite !inE; apply/imageT. Qed. + End base_image_lemmas. #[global] Hint Extern 0 ((?f @` _) (?f _)) => solve [apply: imageP; assumption] : core. @@ -1458,6 +1465,10 @@ Proof. by move=> f_inj; rewrite propeqE; split => [[b Ab /f_inj <-]|/(imageP f)//]. Qed. +Lemma mem_image {f A a} : injective f -> + (f a \in [set f x | x in A]) = (a \in A). +Proof. by move=> /image_inj finj; apply/idP/idP; rewrite !inE finj. Qed. + Lemma image_id A : id @` A = A. Proof. by rewrite eqEsubset; split => a; [case=> /= x Ax <-|exists a]. Qed. @@ -1732,6 +1743,15 @@ Proof. by apply/disj_setPS/disj_setPS; rewrite -some_setI -some_set0 sub_image_someP. Qed. + +Lemma inl_in_set_inr A B (x : A) (Y : set B) : + inl x \in [set inr y | y in Y] = false. +Proof. by apply/negP; rewrite inE/= => -[]. Qed. + +Lemma inr_in_set_inr A B (y : B) (Y : set B) : + inr y \in [set @inr A B y | y in Y] = (y \in Y). +Proof. by apply/idP/idP => [/[!inE][/= [x ? [<-]]]|/[!inE]]//; exists y. Qed. + Section bigop_lemmas. Context {T I : Type}. Implicit Types (A : set T) (i : I) (P : set I) (F G : I -> set T). @@ -2219,6 +2239,9 @@ Proof. by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed. End bigcup_seq. +Lemma in_set1 [T : finType] (x y : T) : (x \in [set y]) = (x \in [set y]%SET). +Proof. by apply/idP/idP; rewrite !inE /= => /eqP. Qed. + Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) : \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t. Proof. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index cac221b080..6245db399c 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -464,3 +464,9 @@ End trunc_floor_ceil. Lemma natr_int {R : archiNumDomainType} n : n%:R \is a @Num.int R. Proof. by rewrite Num.Theory.intrEge0. Qed. + +Lemma inr_inj {A B} : injective (@inr A B). +Proof. by move=> ? ? []. Qed. + +Lemma inl_inj {A B} : injective (@inl A B). +Proof. by move=> ? ? []. Qed. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index f1ca3fa3e0..560f65caed 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -2509,6 +2509,11 @@ by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y; [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW]. Qed. +Lemma EFin_bigmax {I : Type} (s : seq I) (P : I -> bool) (F : I -> R) r : + \big[maxe/r%:E]_(i <- s | P i) (F i)%:E = + (\big[Num.max/r]_(i <- s | P i) F i)%:E. +Proof. by rewrite (big_morph _ EFin_max erefl). Qed. + Lemma fine_min : {in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}. Proof. diff --git a/theories/ftc.v b/theories/ftc.v index ddd76c9473..29495cdc38 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -65,6 +65,24 @@ Notation mu := (@lebesgue_measure R). Local Open Scope ereal_scope. Implicit Types (f : R -> R) (a : itv_bound R). +Lemma integrable_locally f (A : set R) : measurable A -> + mu.-integrable A (EFin \o f) -> locally_integrable [set: R] (f \_ A). +Proof. +move=> mA intf; split. +- move/integrableP : intf => [mf _]. + by apply/(measurable_restrictT _ _).1 => //; exact/EFin_measurable_fun. +- exact: openT. +- move=> K _ cK. + move/integrableP : intf => [mf]. + rewrite integral_mkcond/=. + under eq_integral do rewrite restrict_EFin restrict_normr. + apply: le_lt_trans. + apply: ge0_subset_integral => //=; first exact: compact_measurable. + apply/EFin_measurable_fun/measurableT_comp/EFin_measurable_fun => //=. + move/(measurable_restrictT _ _).1 : mf => /=. + by rewrite restrict_EFin; exact. +Qed. + Let FTC0 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in forall x, a < BRight x -> lebesgue_pt f x -> diff --git a/theories/kernel.v b/theories/kernel.v index a9cce84569..b94e43867e 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1577,14 +1577,14 @@ Definition mkproduct := End kproduct_measure. -(* [Theorem 14.22, Klenke 2014] (3/3): the composition of finite transition - kernels is sigma-finite *) HB.instance Definition _ d0 d1 d2 (T0 : measurableType d0) (T1 : measurableType d1) (T2 : measurableType d2) {R : realType} (k1 : R.-ftker T0 ~> T1) (k2 : R.-ftker (T0 * T1) ~> T2) := @isKernel.Build _ _ T0 (T1 * T2)%type R (mkproduct k1 k2) (measurable_kproduct k1 k2). +(* [Theorem 14.22, Klenke 2014] (3/3): the composition of finite transition + kernels is sigma-finite *) Section sigma_finite_kproduct. Context d0 d1 d2 (T0 : measurableType d0) (T1 : measurableType d1) (T2 : measurableType d2) {R : realType} diff --git a/theories/measure.v b/theories/measure.v index 1e5eec41b3..1cde392724 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1516,6 +1516,12 @@ by move=> fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1` A); [exact: mf|exact/esym/eq_preimage]. Qed. +Lemma measurable_fun_eqP D (f g : T1 -> T2) : + {in D, f =1 g} -> measurable_fun D f <-> measurable_fun D g. +Proof. +by move=> eq_fg; split; apply/eq_measurable_fun => // ? ?; rewrite eq_fg. +Qed. + Lemma measurable_cst D (r : T2) : measurable_fun D (cst r : T1 -> _). Proof. by move=> mD /= Y mY; rewrite preimage_cst; case: ifPn; rewrite ?setIT ?setI0. @@ -1582,6 +1588,7 @@ End measurable_fun. #[global] Hint Extern 0 (measurable_fun _ id) => solve [apply: measurable_id] : core. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. +Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}. #[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")] Notation measurable_fun_ext := eq_measurable_fun (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")] @@ -3647,6 +3654,13 @@ HB.instance Definition _ := End mnormalize. +Lemma mnormalize_id d (T : measurableType d) (R : realType) + (P P' : probability T R) : mnormalize P P' = P. +Proof. +apply/funext => x; rewrite /mnormalize/= probability_setT. +by rewrite onee_eq0/= invr1 mule1. +Qed. + Section pdirac. Context d (T : measurableType d) (R : realType). diff --git a/theories/probability.v b/theories/probability.v index ea66fdc908..bb799a3891 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1047,6 +1047,23 @@ Qed. HB.instance Definition _ := @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT. +Lemma eq_bernoulli (P : probability bool R) : + P [set true] = p%:E -> P =1 bernoulli. +Proof. +move=> Ptrue sb; rewrite /bernoulli /bernoulli_pmf. +have Pfalse: P [set false] = (1 - p%:E)%E. + rewrite -Ptrue -(@probability_setT _ _ _ P) setT_bool measureU//; last first. + by rewrite disjoints_subset => -[]//. + by rewrite addeAC subee ?add0e//= Ptrue. +have: (0 <= p%:E <= 1)%E by rewrite -Ptrue measure_ge0 probability_le1. +rewrite !lee_fin => ->. +have eq_sb := etrans (bigcup_imset1 (_ : set bool) id) (image_id _). +rewrite -[in LHS](eq_sb sb)/= measure_fin_bigcup//; last 2 first. +- exact: finite_finset. +- by move=> [] [] _ _ [[]]//= []. +- by apply: eq_fsbigr => /= -[]. +Qed. + End bernoulli. Section bernoulli_measure. @@ -1076,6 +1093,17 @@ Qed. End bernoulli_measure. Arguments bernoulli {R}. +Lemma eq_bernoulliV2 {R : realType} (P : probability bool R) : + P [set true] = P [set false] -> P =1 bernoulli 2^-1. +Proof. +move=> Ptrue_eq_false; apply/eq_bernoulli. +have : P [set: bool] = 1%E := probability_setT. +rewrite setT_bool measureU//=; last first. + by rewrite disjoints_subset => -[]//. +rewrite Ptrue_eq_false -mule2n; move/esym/eqP. +by rewrite -mule_natl -eqe_pdivrMl// mule1 => /eqP<-. +Qed. + Section integral_bernoulli. Context {R : realType}. Variables (p : R) (p01 : (0 <= p <= 1)%R). From 830147ab95dfdf838d4e3b0b96bd5859f306bf50 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 25 Apr 2025 19:21:18 +0900 Subject: [PATCH 2/2] addressing comments --- CHANGELOG_UNRELEASED.md | 1 + classical/classical_sets.v | 9 ++++++++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 854a789d13..0070825c51 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,6 +21,7 @@ - in `classical_sets.v`: + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f` + + lemmas `inr_in_set_inl`, `inl_in_set_inl` ### Changed diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 2f68504bd3..2123c01bc5 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1743,15 +1743,22 @@ Proof. by apply/disj_setPS/disj_setPS; rewrite -some_setI -some_set0 sub_image_someP. Qed. - Lemma inl_in_set_inr A B (x : A) (Y : set B) : inl x \in [set inr y | y in Y] = false. Proof. by apply/negP; rewrite inE/= => -[]. Qed. +Lemma inr_in_set_inl A B (y : B) (X : set A) : + inr y \in [set inl x | x in X] = false. +Proof. by apply/negP; rewrite inE/= => -[]. Qed. + Lemma inr_in_set_inr A B (y : B) (Y : set B) : inr y \in [set @inr A B y | y in Y] = (y \in Y). Proof. by apply/idP/idP => [/[!inE][/= [x ? [<-]]]|/[!inE]]//; exists y. Qed. +Lemma inl_in_set_inl A B (x : A) (X : set A) : + inl x \in [set @inl A B x | x in X] = (x \in X). +Proof. by apply/idP/idP => [/[!inE][/= [y ? [<-]]]|/[!inE]]//; exists x. Qed. + Section bigop_lemmas. Context {T I : Type}. Implicit Types (A : set T) (i : I) (P : set I) (F G : I -> set T).