From d558da89efce54e023a44e05cd31a16bfc8b70b1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 26 May 2022 12:18:12 +0900 Subject: [PATCH 1/4] lebesgue measure of intervals --- CHANGELOG_UNRELEASED.md | 4 + theories/lebesgue_measure.v | 205 ++++++++++++++++++++++++++++++++++-- 2 files changed, 201 insertions(+), 8 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8674d429e..714269e9f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -92,6 +92,10 @@ + lemma `restrict_lee` - in file `lebesgue_integral.v`: + lemmas `integral_set0`, `ge0_integral_bigsetU`, `ge0_integral_bigcup` +- in file `lebesgue_measure.v`: + + lemmas `itv_bnd_open_bigcup`, `itv_bnd_infty_bigcup`, `itv_infty_bnd_bigcup` + + lemma `lebesgue_measure_set1` + + lemma `lebesgue_measure_itv` ### Changed diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 0ef4e0dcf..9a93b35c5 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -543,6 +543,48 @@ rewrite -addn1 natrD natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. by rewrite -RfloorE lt_succ_Rfloor. Qed. +Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : + [set` Interval (BSide b r) (BLeft s)] = + \bigcup_n [set` Interval (BSide b r) (BRight (s - n.+1%:R^-1))]. +Proof. +apply/seteqP; split => [x/=|]; last first. + move=> x [n _ /=]; rewrite !in_itv => /andP[-> /le_lt_trans]; apply. + by rewrite ltr_subl_addr ltr_addl invr_gt0 ltr0n. +rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=. +rewrite in_itv/= sx/= ler_subr_addl addrC -ler_subr_addl. +rewrite -[in X in _ <= X](invrK (s - x)) ler_pinv. +- rewrite -addn1 natrD natr_absz ger0_norm; last first. + by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW. + by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?ler_addl// ceil_ge. +- by rewrite inE unitfE ltr0n andbT pnatr_eq0. +- by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF. +Qed. + +Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) : + [set` Interval (BSide b x) +oo%O] = + \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))]. +Proof. +apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. + by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. +move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -ler_subl_addl. +rewrite !natr_absz/= ger0_norm ?ceil_ge0// ?subr_ge0//; last first. + by case: b xy => //= /ltW. +by rewrite -RceilE Rceil_ge. +Qed. + +Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) : + [set` Interval -oo%O (BSide b x)] = + \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)]. +Proof. +apply/seteqP; split=> y /=; rewrite !in_itv/=. + move=> xy; exists `|ceil (x - y)|%N => //=. + rewrite in_itv/= xy andbT ler_subl_addl addrC -ler_subl_addl. + rewrite natr_absz ger0_norm// ?ceil_ge0 ?subr_ge0//; last first. + by case: b xy => //= /ltW. + by rewrite -RceilE Rceil_ge. +by move=> [k _ /=]; rewrite in_itv/= => /andP[]. +Qed. + Section salgebra_R_ssets. Variable R : realType. @@ -567,15 +609,8 @@ Lemma measurable_itv (i : interval R) : measurable [set` i]. Proof. have moc (a b : R) : measurable `]a, b]%classic. by apply: sub_sigma_algebra; apply: is_ocitv. -have pooE (x : R) : `]x, +oo[%classic = \bigcup_i `]x, x + i%:R]%classic. - apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. - by move=> [k _ /=] /itvP->. - move=> xy; exists `|ceil (y - x)|%N => //=. - rewrite in_itv/= xy/= -ler_subl_addl !natr_absz/=. - rewrite ger0_norm ?ceil_ge0 ?subr_ge0//; last exact: ltW. - by rewrite -RceilE Rceil_ge. have mopoo (x : R) : measurable `]x, +oo[%classic. - by rewrite pooE; exact: bigcup_measurable. + by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable. have mnooc (x : R) : measurable `]-oo, x]%classic. by rewrite -setCitvr; exact/measurableC. have ooE (a b : R) : `]a, b[%classic = `]a, b]%classic `\ b. @@ -773,6 +808,160 @@ End salgebra_R_ssets. Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| apply: emeasurable_set1] : core. +Section lebesgue_measure_itv. +Variable R : realType. + +Let lebesgue_measure_itvoc (a b : R) : + (lebesgue_measure `]a, b] = hlength `]a, b])%classic. +Proof. +rewrite /lebesgue_measure/= /Hahn_ext measurable_mu_extE//; last first. + by exists (a, b). +exact: hlength_sigma_sub_additive. +Qed. + +Let lebesgue_measure_itvoo_subr1 (a : R) : + lebesgue_measure `]a - 1, a[%classic = 1%E. +Proof. +rewrite itv_bnd_open_bigcup//; transitivity (lim (lebesgue_measure \o + (fun k => `]a - 1, a - k.+1%:R^-1]%classic))). + apply/esym/cvg_lim => //; apply: cvg_mu_inc. + - by move=> ?; exact: measurable_itv. + - by apply: bigcup_measurable => k _; exact: measurable_itv. + - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. + by move/le_trans; apply; rewrite ler_sub// ler_pinv ?ler_nat//; + rewrite inE ltr0n andbT unitfE. +rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first. + apply/funext => n /=; rewrite lebesgue_measure_itvoc. + have [->|n0] := eqVneq n 0%N; first by rewrite invr1 subrr set_itvoc0. + rewrite hlength_itv/= lte_fin ifT; last first. + by rewrite ler_lt_sub// invr_lt1 ?unitfE// ltr1n ltnS lt0n. + by rewrite !(EFinB,EFinN) oppeB// addeAC addeA subee// add0e. +apply/cvg_lim => //=; apply/ereal_cvg_real; split => /=; first exact: nearW. +apply/(@cvg_distP _ [pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e]. +rewrite !near_simpl; near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//. +by near: n; exact: near_infty_natSinv_lt. +Unshelve. all: by end_near. Qed. + +Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0%E. +Proof. +suff : (lebesgue_measure `]a - 1, a]%classic%R = + lebesgue_measure `]a - 1, a[%classic%R + + lebesgue_measure [set a])%E. + rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP. + rewrite hlength_itv lte_fin ltr_subl_addr ltr_addl ltr01. + rewrite [in X in X == _]/= EFinN EFinB oppeB// addeA subee// add0e. + rewrite addeC -sube_eq//; last by rewrite fin_num_adde_def. + by rewrite subee// => /eqP. +rewrite -setUitv1// ?bnd_simp; last by rewrite ltr_subl_addr ltr_addl. +rewrite measureU//; first exact: measurable_itv. +apply/seteqP; split => // x []/=; rewrite in_itv/= => + xa. +by rewrite xa ltxx andbF. +Qed. + +Let lebesgue_measure_itvoo (a b : R) : + (lebesgue_measure `]a, b[ = hlength `]a, b[)%classic. +Proof. +have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. +have := lebesgue_measure_itvoc a b. +rewrite 2!hlength_itv => <-; rewrite -setUitv1// measureU//. +- by have /= -> := lebesgue_measure_set1 b; rewrite adde0. +- exact: measurable_itv. +- by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF. +Qed. + +Let lebesgue_measure_itvcc (a b : R) : + (lebesgue_measure `[a, b] = hlength `[a, b])%classic. +Proof. +have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt. +have := lebesgue_measure_itvoc a b. +rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//. +- by have /= -> := lebesgue_measure_set1 a; rewrite add0e. +- exact: measurable_itv. +- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. +Qed. + +Let lebesgue_measure_itvco (a b : R) : + (lebesgue_measure `[a, b[ = hlength `[a, b[)%classic. +Proof. +have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. +have := lebesgue_measure_itvoo a b. +rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//. +- by have /= -> := lebesgue_measure_set1 a; rewrite add0e. +- exact: measurable_itv. +- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. +Qed. + +Lemma lebesgue_measure_itv_bnd (x y : bool) (a b : R) : + lebesgue_measure [set` (Interval (BSide x a) (BSide y b))] = + hlength [set` (Interval (BSide x a) (BSide y b))]. +Proof. +by move: x y => [|] [|]; [exact: lebesgue_measure_itvco | + exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo | + exact: lebesgue_measure_itvoc]. +Qed. + +Let limnatR : lim (fun k => (k%:R)%:E : \bar R) = +oo%E. +Proof. +apply/cvg_lim => //; apply/dvg_ereal_cvg/cvgPpinfty => A. +exists `|ceil A|%N => //= => n/=; rewrite -(@ler_nat R); apply: le_trans. +by rewrite natr_absz (le_trans (ceil_ge _))// intr_norm ler_norm. +Qed. + +Let lebesgue_measure_itv_bnd_infty x (a : R) : + lebesgue_measure [set` Interval (BSide x a) +oo%O] = +oo%E. +Proof. +rewrite itv_bnd_infty_bigcup; transitivity (lim (lebesgue_measure \o + (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))]))). + apply/esym/cvg_lim => //; apply: cvg_mu_inc => //. + + by move=> k; exact: measurable_itv. + + by apply: bigcup_measurable => k _; exact: measurable_itv. + + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=]. + by move=> /le_trans; apply; rewrite ler_add// ler_nat. +rewrite (_ : _ \o _ = (fun k => k%:R%:E))//. +apply/funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/=. +rewrite lte_fin; have [->|n0] := eqVneq n 0%N; first by rewrite addr0 ltxx. +by rewrite ltr_addl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e. +Qed. + +Let lebesgue_measure_itv_infty_bnd y (b : R) : + lebesgue_measure [set` Interval -oo%O (BSide y b)] = +oo%E. +Proof. +rewrite itv_infty_bnd_bigcup; transitivity (lim (lebesgue_measure \o + (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)]))). + apply/esym/cvg_lim => //; apply: cvg_mu_inc => //. + + by move=> k; exact: measurable_itv. + + by apply: bigcup_measurable => k _; exact: measurable_itv. + + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->]. + by rewrite andbT; apply: le_trans; rewrite ler_sub// ler_nat. +rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//. +apply/funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/= lte_fin. +have [->|n0] := eqVneq n 0%N; first by rewrite subr0 ltxx. +rewrite ltr_subl_addr ltr_addl ltr0n lt0n n0 EFinN EFinB oppeB// addeA subee//. +by rewrite add0e. +Qed. + +Lemma lebesgue_measure_itv (i : interval R) : + lebesgue_measure [set` i] = hlength [set` i]. +Proof. +move: i => [[x a|[|]]] [y b|[|]]; first exact: lebesgue_measure_itv_bnd. +- by rewrite set_itvE ?measure0. +- by rewrite lebesgue_measure_itv_bnd_infty hlength_bnd_infty. +- by rewrite lebesgue_measure_itv_infty_bnd hlength_infty_bnd. +- by rewrite set_itvE ?measure0. +- rewrite set_itvE hlength_setT. + rewrite (_ : setT = [set` `]-oo, 0[] `|` [set` `[0, +oo[]); last first. + by apply/seteqP; split=> // => x _; have [x0|x0] := leP 0 x; [right|left]; + rewrite /= in_itv//= x0. + rewrite measureU//=; try exact: measurable_itv. + + by rewrite lebesgue_measure_itv_infty_bnd lebesgue_measure_itv_bnd_infty. + + by apply/seteqP; split => // x []/=; rewrite !in_itv/= andbT leNgt => ->. +- by rewrite set_itvE ?measure0. +- by rewrite set_itvE ?measure0. +- by rewrite set_itvE ?measure0. +Qed. + +End lebesgue_measure_itv. + Section measurable_fun_measurable. Local Open Scope ereal_scope. Variables (T : measurableType) (R : realType) (D : set T) (f : T -> \bar R). From 53f88df0a62ba378e7e5a507144a34d8dedf9bac Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 27 May 2022 02:15:34 +0900 Subject: [PATCH 2/4] measure of set of rationals --- CHANGELOG_UNRELEASED.md | 1 + theories/lebesgue_measure.v | 16 ++++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 714269e9f..a574b3fa5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -96,6 +96,7 @@ + lemmas `itv_bnd_open_bigcup`, `itv_bnd_infty_bigcup`, `itv_infty_bnd_bigcup` + lemma `lebesgue_measure_set1` + lemma `lebesgue_measure_itv` + + lemma `lebesgue_measure_rat` ### Changed diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 9a93b35c5..999fcc35e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -962,6 +962,22 @@ Qed. End lebesgue_measure_itv. +Lemma lebesgue_measure_rat (R : realType) : + lebesgue_measure (range ratr : set R) = 0%E. +Proof. +have /pcard_eqP/bijPex[f bijf] := card_rat; set f1 := 'pinv_(fun=> 0) setT f. +rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first. + apply/seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n). + exists (f q) => //=; rewrite /f1 pinvKV// ?in_setE// => x y _ _. + by apply: bij_inj; rewrite -setTT_bijective. +rewrite measure_bigcup//; last first. + apply/trivIsetP => i j _ _ ij; apply/seteqP; split => //= _ [/= ->]. + move=> /fmorph_inj. + have /set_bij_inj /[apply] := bijpinv_bij (fun=> 0) bijf. + by rewrite in_setE => /(_ Logic.I Logic.I); exact/eqP. +by rewrite nneseries0// => n _; rewrite lebesgue_measure_set1. +Qed. + Section measurable_fun_measurable. Local Open Scope ereal_scope. Variables (T : measurableType) (R : realType) (D : set T) (f : T -> \bar R). From 7b4667fd024ab0738059c0364e9911fd7d7dd301 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 31 May 2022 11:57:30 +0900 Subject: [PATCH 3/4] generalizations Co-authored-by: Pierre Roux --- CHANGELOG_UNRELEASED.md | 9 ++++++++- theories/classical_sets.v | 7 +++++++ theories/lebesgue_measure.v | 27 ++++++++++++++++++--------- theories/set_interval.v | 22 +++++++++++++++++----- 4 files changed, 50 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a574b3fa5..9de39f813 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -93,10 +93,15 @@ - in file `lebesgue_integral.v`: + lemmas `integral_set0`, `ge0_integral_bigsetU`, `ge0_integral_bigcup` - in file `lebesgue_measure.v`: - + lemmas `itv_bnd_open_bigcup`, `itv_bnd_infty_bigcup`, `itv_infty_bnd_bigcup` + + lemmas `itv_bnd_open_bigcup`, `itv_bnd_infty_bigcup`, `itv_infty_bnd_bigcup`, + `itv_open_bnd_bigcup` + lemma `lebesgue_measure_set1` + lemma `lebesgue_measure_itv` + lemma `lebesgue_measure_rat` +- in file `classical_sets.v`: + + lemma `bigcup_oppr` +- in file `set_interval.v`: + + lemma `opp_itv_infty_bnd` ### Changed @@ -110,6 +115,8 @@ + generalize `card_fset_sum1` - in `lebesgue_integral.v`: + change the notation `\int_` +- in `set_interval.v`: + + generalize `opp_itvoo` to `opp_itv_bnd_bnd` ### Renamed diff --git a/theories/classical_sets.v b/theories/classical_sets.v index a4b334d18..bd4f3b1bd 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -2703,6 +2703,13 @@ rewrite -Order.TotalTheory.ltNge => kn. by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)). Qed. +Lemma bigcup_oppr (R : zmodType) (I : Type) (F : I -> set R) : + \bigcup_i (-%R @` F i) = -%R @` \bigcup_i F i. +Proof. +by apply/seteqP; split=> [_ [i _/= [r Fir <-]]|x/= [r [i _ Fir <-]]]; + [exists r => //; exists i | exists i]. +Qed. + (** ** Intersection of classes of set *) Definition meets T (F G : set (set T)) := diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 999fcc35e..68e8d91fe 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -548,7 +548,7 @@ Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : \bigcup_n [set` Interval (BSide b r) (BRight (s - n.+1%:R^-1))]. Proof. apply/seteqP; split => [x/=|]; last first. - move=> x [n _ /=]; rewrite !in_itv => /andP[-> /le_lt_trans]; apply. + move=> x [n _ /=] /[!in_itv] /andP[-> /le_lt_trans]; apply. by rewrite ltr_subl_addr ltr_addl invr_gt0 ltr0n. rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=. rewrite in_itv/= sx/= ler_subr_addl addrC -ler_subr_addl. @@ -560,6 +560,17 @@ rewrite -[in X in _ <= X](invrK (s - x)) ler_pinv. - by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF. Qed. +Lemma itv_open_bnd_bigcup (R : realType) b (r s : R) : + [set` Interval (BRight s) (BSide b r)] = + \bigcup_n [set` Interval (BLeft (s + n.+1%:R^-1)) (BSide b r)]. +Proof. +have /(congr1 (fun x => -%R @` x)) := itv_bnd_open_bigcup (~~ b) (- r) (- s). +rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite -bigcup_oppr. +apply eq_bigcupr => k _; apply/seteqP; split=> [_/= [y ysr] <-|x/= xsr]. + by rewrite oppr_itv/= opprD. +by exists (- x); rewrite ?oppr_itv//= opprK// negbK opprB opprK addrC. +Qed. + Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) : [set` Interval (BSide b x) +oo%O] = \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))]. @@ -576,13 +587,11 @@ Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) : [set` Interval -oo%O (BSide b x)] = \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)]. Proof. -apply/seteqP; split=> y /=; rewrite !in_itv/=. - move=> xy; exists `|ceil (x - y)|%N => //=. - rewrite in_itv/= xy andbT ler_subl_addl addrC -ler_subl_addl. - rewrite natr_absz ger0_norm// ?ceil_ge0 ?subr_ge0//; last first. - by case: b xy => //= /ltW. - by rewrite -RceilE Rceil_ge. -by move=> [k _ /=]; rewrite in_itv/= => /andP[]. +have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x). +rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite -bigcup_oppr. +apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb]. + by rewrite oppr_itv/= opprB addrC. +by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK]. Qed. Section salgebra_R_ssets. @@ -891,7 +900,7 @@ rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//. - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. Qed. -Lemma lebesgue_measure_itv_bnd (x y : bool) (a b : R) : +Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) : lebesgue_measure [set` (Interval (BSide x a) (BSide y b))] = hlength [set` (Interval (BSide x a) (BSide y b))]. Proof. diff --git a/theories/set_interval.v b/theories/set_interval.v index 39623521b..1e877e134 100644 --- a/theories/set_interval.v +++ b/theories/set_interval.v @@ -239,12 +239,24 @@ exists (- r); rewrite ?opprK //. by case: b xr; rewrite !in_itv/= andbT (ler_oppr, ltr_oppr). Qed. -Lemma opp_itvoo (R : numDomainType) (x y : R) : - -%R @` `]x, y[%classic = `](- y), (- x)[%classic. +Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b : + -%R @` [set` Interval -oo%O (BSide b x)] = + [set` Interval (BSide (negb b) (- x)) +oo%O]. +Proof. +rewrite predeqE => /= r; split=> [[y xy <-]|xr]. + by case: b xy; rewrite !in_itv/= andbT (ler_opp2, ltr_opp2). +exists (- r); rewrite ?opprK //. +by case: b xr; rewrite !in_itv/= andbT (ler_oppl, ltr_oppl). +Qed. + +Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) : + -%R @` [set` Interval (BSide a x) (BSide b y)] = + [set` Interval (BSide (~~ b) (- y)) (BSide (~~ a) (- x))]. Proof. rewrite predeqE => /= r; split => [[{}r + <-]|]. - by rewrite !in_itv/= !ltr_opp2 andbC. -by exists (- r); rewrite ?opprK// !in_itv/= ltr_oppl ltr_oppr andbC. + by rewrite !in_itv/= 2!lteif_opp2 negbK andbC. +rewrite in_itv/= negbK => yrab. +by exists (- r); rewrite ?opprK// !in_itv lteif_oppr andbC lteif_oppl. Qed. Section interval_sup_inf. @@ -298,7 +310,7 @@ Let inf_itv_bnd_o x y b : (BSide b x < BLeft y)%O -> Proof. case: b => xy. by rewrite -setU1itv// inf_setU ?inf1// => _ ? -> /andP[/ltW]. -by rewrite /inf opp_itvoo sup_itv_o_bnd ?opprK // ltr_oppl opprK. +by rewrite /inf opp_itv_bnd_bnd sup_itv_o_bnd ?opprK // ltr_oppl opprK. Qed. Let inf_itv_bounded x y a b : (BSide a x < BSide b y)%O -> From 561cf329f1236629775d891a6a8f48b1359f479a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 3 Jun 2022 23:35:51 +0900 Subject: [PATCH 4/4] lemma generalization --- CHANGELOG_UNRELEASED.md | 4 ++-- theories/classical_sets.v | 15 ++++----------- theories/lebesgue_measure.v | 4 ++-- 3 files changed, 8 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9de39f813..5cc62dfd7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -98,8 +98,6 @@ + lemma `lebesgue_measure_set1` + lemma `lebesgue_measure_itv` + lemma `lebesgue_measure_rat` -- in file `classical_sets.v`: - + lemma `bigcup_oppr` - in file `set_interval.v`: + lemma `opp_itv_infty_bnd` @@ -117,6 +115,8 @@ + change the notation `\int_` - in `set_interval.v`: + generalize `opp_itvoo` to `opp_itv_bnd_bnd` +- in `classical_sets.v`: + + lemma `some_bigcup` generalized and renamed to `image_bigcup` ### Renamed diff --git a/theories/classical_sets.v b/theories/classical_sets.v index bd4f3b1bd..d52bb139a 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -1411,11 +1411,11 @@ apply: setC_inj; rewrite setC_bigcup setCK. by apply: eq_bigcapr => ?; rewrite setCK. Qed. -Lemma some_bigcup P F : - some @` (\bigcup_(i in P) (F i)) = \bigcup_(i in P) some @` F i. +Lemma image_bigcup rT P F (f : T -> rT) : + f @` (\bigcup_(i in P) (F i)) = \bigcup_(i in P) f @` F i. Proof. -apply/seteqP; split; last by move=> _ [i ? [x ? <-]]; exists x => //; exists i. -by move=> _ [x [i ? ?] <-]; exists i => //; exists x. +apply/seteqP; split=> [_/= [x [i Pi Fix <-]]|]; first by exists i. +by move=> _ [i Pi [x Fix <-]]; exists x => //; exists i. Qed. Lemma some_bigcap P F : some @` (\bigcap_(i in P) (F i)) = @@ -2703,13 +2703,6 @@ rewrite -Order.TotalTheory.ltNge => kn. by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)). Qed. -Lemma bigcup_oppr (R : zmodType) (I : Type) (F : I -> set R) : - \bigcup_i (-%R @` F i) = -%R @` \bigcup_i F i. -Proof. -by apply/seteqP; split=> [_ [i _/= [r Fir <-]]|x/= [r [i _ Fir <-]]]; - [exists r => //; exists i | exists i]. -Qed. - (** ** Intersection of classes of set *) Definition meets T (F G : set (set T)) := diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 68e8d91fe..df55b188a 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -565,7 +565,7 @@ Lemma itv_open_bnd_bigcup (R : realType) b (r s : R) : \bigcup_n [set` Interval (BLeft (s + n.+1%:R^-1)) (BSide b r)]. Proof. have /(congr1 (fun x => -%R @` x)) := itv_bnd_open_bigcup (~~ b) (- r) (- s). -rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite -bigcup_oppr. +rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite image_bigcup. apply eq_bigcupr => k _; apply/seteqP; split=> [_/= [y ysr] <-|x/= xsr]. by rewrite oppr_itv/= opprD. by exists (- x); rewrite ?oppr_itv//= opprK// negbK opprB opprK addrC. @@ -588,7 +588,7 @@ Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) : \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)]. Proof. have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x). -rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite -bigcup_oppr. +rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup. apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb]. by rewrite oppr_itv/= opprB addrC. by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK].