From 93b0d36eea1b8e1dd22174fc915fae75b9e08850 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Mon, 29 Jun 2026 16:18:06 +0200 Subject: [PATCH 1/4] added setD_bigcapr + renamed bigcupDr to setD_bigcupr --- CHANGELOG_UNRELEASED.md | 4 ++++ classical/classical_sets.v | 8 ++++++-- .../measurable_fun_approximation.v | 2 +- theories/measure_theory/measure_function.v | 4 ++-- 4 files changed, 13 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de4c407ce2..4a70560664 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -6,6 +6,9 @@ - in `functions.v` + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`) +- in `classical_sets.v` + + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) + ### Changed - in `functions.v` + lemma `fctE` (include `zerofctE` and `onefctE`) @@ -26,6 +29,7 @@ + definitions `cross`, `cross12` + lemmas `smallest_sub_sub`, `bigcap_closed_smallest`, `smallest_sub_iff` + lemma `preimage_set_systemS` + + lemma `setD_bigcapr` - in `measurable_structure.v`: + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index d46b2b42b2..66f4240ae0 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2115,10 +2115,14 @@ Lemma setC_bigsetI U (s : seq T) (f : T -> set U) (P : pred T) : \big[setU/set0]_(t <- s | P t) ~` f t. Proof. by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setCT ?setCI. Qed. -Lemma bigcupDr (F : I -> set T) (P : set I) (A : set T) : P !=set0 -> - \bigcap_(i in P) (A `\` F i) = A `\` \bigcup_(i in P) F i. +Lemma setD_bigcupr (F : I -> set T) (P : set I) (A : set T) : P !=set0 -> + A `\` \bigcup_(i in P) F i = \bigcap_(i in P) (A `\` F i). Proof. by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed. +Lemma setD_bigcapr (F : I -> set T) [P : set I] (A : set T) : + A `\` \bigcap_(i in P) F i = \bigcup_(i in P) (A `\` F i). +Proof. by rewrite setDE setC_bigcap setI_bigcupr. Qed. + Lemma setD_bigcupl (F : I -> set T) (P : set I) (A : set T) : \bigcup_(i in P) F i `\` A = \bigcup_(i in P) (F i `\` A). Proof. by rewrite setDE setI_bigcupl; under eq_bigcupr do rewrite -setDE. Qed. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 929c4fa3ab..21282d6590 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -725,7 +725,7 @@ exists (\bigcup_(i in range f) dK i); split. - by rewrite -bigsetU_fset_set//; apply: bigsetU_compact=>// i _; case: (dkP i). - by move=> z [y _ dy]; have [_ /(_ _ dy) []] := dkP y. - have -> : A `\` \bigcup_(i in range f) dK i = \bigcup_(i in range f) J i. - rewrite -bigcupDr /= ?eqEsubset; first by exists (f point), point. + rewrite setD_bigcupr /= ?eqEsubset; first by exists (f point), point. split => z; first by move=> /(_ (f z)) [//| ? ?]; exists (f z). case => ? [? _ <-] [[zab /= <- nfz]] ? [r _ <-]; split => //. by move: nfz; apply: contra_not => /[dup] /dKsub ->. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 63907c0f6c..2d997d9280 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -739,7 +739,7 @@ have mDbigcup I (D : set I) (A : set T) (B : I -> set T) : finite_set D -> measurable_fin_trivIset (A `\` \bigcup_(i in D) B i). have [->|/set0P D0] := eqVneq D set0. by rewrite bigcup0// setD0 => *; apply: mdW. - move=> Dfin Am Bm; rewrite -bigcupDr//; apply: mdisj_bigcap=> // i Di. + move=> Dfin Am Bm; rewrite setD_bigcupr//; apply: mdisj_bigcap=> // i Di. by have [F [Ffin Fm -> ?]] := semi_measurableD A (B i) Am (Bm _ Di); exists F. have mdU : fin_trivIset_closed measurable_fin_trivIset. elim/Pchoice=> I D F Dfin Ftriv Fm. @@ -760,7 +760,7 @@ have mdDI : setD_closed measurable_fin_trivIset. have [->|/set0P F'N0] := eqVneq F' set0. by rewrite bigcup_set0 setD0; exists F. rewrite setD_bigcupl; apply: mdU => //; first by apply: trivIset_setIr. - move=> X DX; rewrite -bigcupDr//; apply: mdisj_bigcap => //. + move=> X DX; rewrite setD_bigcupr//; apply: mdisj_bigcap => //. move=> Y DY; case: (semi_measurableD X Y); [exact: Fm|exact: F'm|]. by move=> G [Gfin Gm -> Gtriv]; exists G. apply: smallest_sub => //; split=> //; first by apply: mdW. From 1f427d8d4dbc176d348b8acf33f922580c953154 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 16:30:45 +0900 Subject: [PATCH 2/4] fix --- CHANGELOG_UNRELEASED.md | 35 +++++++++++++---------------------- classical/classical_sets.v | 7 ++++++- 2 files changed, 19 insertions(+), 23 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4a70560664..13930973c6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -2,21 +2,6 @@ ## [Unreleased] -### Renamed -- in `functions.v` - + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`) - -- in `classical_sets.v` - + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) - -### Changed -- in `functions.v` - + lemma `fctE` (include `zerofctE` and `onefctE`) - -### Added -- in `functions.v`: - + lemmas `zerofctE`, `onefctE` - ### Added - in `set_interval.v`: + lemmas `setU_itvob1`, `setU_1itvob` @@ -174,12 +159,9 @@ - in `esum.v`: + lemma `fsetsTE` -### Changed +- in `functions.v`: + + lemmas `zerofctE`, `onefctE` -- moved from `measurable_structure.v` to `classical_sets.v`: - + definition `preimage_set_system` - + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, - `preimage_set_system_id` - in `functions.v`: + lemmas `linfunP`, `linfun_eqP` + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` @@ -209,11 +191,11 @@ + lemma `ge0_esum` + lemma `esum_ge` +### Changed + - in `realsum.v`: + lemma `__admitted__psumB` proved and renamed to `psumB` -### Changed - - moved from `measurable_structure.v` to `classical_sets.v`: + definition `preimage_set_system` + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, @@ -321,6 +303,12 @@ + definition `seqD` + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` +- in `functions.v` + + lemma `fctE` (include `zerofctE` and `onefctE`) + +- in `classical_sets.v` + + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`) + ### Renamed - in `tvs.v`: @@ -370,6 +358,9 @@ - in `realsum.v`: + `psum` -> `PosSum.psum` +- in `functions.v` + + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`) + ### Generalized - in `measurable_structure.v`: diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 66f4240ae0..dd3a74ea1c 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2115,11 +2115,16 @@ Lemma setC_bigsetI U (s : seq T) (f : T -> set U) (P : pred T) : \big[setU/set0]_(t <- s | P t) ~` f t. Proof. by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setCT ?setCI. Qed. +#[deprecated(since="mathcomp-analysis 1.17.0", note="use `setD_bigcupr` instead")] +Lemma bigcupDr (F : I -> set T) (P : set I) (A : set T) : P !=set0 -> + \bigcap_(i in P) (A `\` F i) = A `\` \bigcup_(i in P) F i. +Proof. by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed. + Lemma setD_bigcupr (F : I -> set T) (P : set I) (A : set T) : P !=set0 -> A `\` \bigcup_(i in P) F i = \bigcap_(i in P) (A `\` F i). Proof. by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed. -Lemma setD_bigcapr (F : I -> set T) [P : set I] (A : set T) : +Lemma setD_bigcapr (F : I -> set T) [P : set I] (A : set T) : A `\` \bigcap_(i in P) F i = \bigcup_(i in P) (A `\` F i). Proof. by rewrite setDE setC_bigcap setI_bigcupr. Qed. From b6d8fd4563767ed7bf992e3fbde16ee66fcdc2af Mon Sep 17 00:00:00 2001 From: adjevahi Date: Tue, 30 Jun 2026 10:46:17 +0200 Subject: [PATCH 3/4] added preimageD --- classical/functions.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/classical/functions.v b/classical/functions.v index f58e231537..404afbb3b6 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,6 +2766,15 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). +Lemma preimageD {T : Type} {Z : zmodType} (f g : T -> Z) (z : Z) : +(f \+ g) @^-1`[set z] + = \bigcup_(a in range f) (f@^-1`[set a] `&` g@^-1`[set z-a]). +Proof. +rewrite/preimage eqEsubset; split=>[x /= fgz| x [a _ [/= <- -> ]]]. + exists (f x)=>//; split=>//=. by rewrite -fgz addrC addKr. +by rewrite subrKC. +Qed. + End function_space_lemmas. #[deprecated(since="mathcomp-analysis 1.17.0", use=scalerfctE)] From 328801e719276e1f42ccb61a40a7e4d47528436c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 19:20:28 +0900 Subject: [PATCH 4/4] actually use preimageD1 --- CHANGELOG_UNRELEASED.md | 3 +++ classical/functions.v | 10 +++++----- .../lebesgue_integral_definition.v | 2 +- theories/lebesgue_integral_theory/simple_functions.v | 10 ---------- 4 files changed, 9 insertions(+), 16 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 13930973c6..f8c18ee6ea 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -191,6 +191,9 @@ + lemma `ge0_esum` + lemma `esum_ge` +- in `functions.v`: + + lemma `preimageD1` + ### Changed - in `realsum.v`: diff --git a/classical/functions.v b/classical/functions.v index 404afbb3b6..d60b235ce8 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,12 +2766,12 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). -Lemma preimageD {T : Type} {Z : zmodType} (f g : T -> Z) (z : Z) : -(f \+ g) @^-1`[set z] - = \bigcup_(a in range f) (f@^-1`[set a] `&` g@^-1`[set z-a]). +Lemma preimageD1 {T : Type} {Z : zmodType} (f g : T -> Z) (z : Z) : + (f \+ g) @^-1`[set z] = + \bigcup_(a in range f) (f @^-1` [set a] `&` g @^-1` [set z - a]). Proof. -rewrite/preimage eqEsubset; split=>[x /= fgz| x [a _ [/= <- -> ]]]. - exists (f x)=>//; split=>//=. by rewrite -fgz addrC addKr. +rewrite eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. + by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. by rewrite subrKC. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 917f991730..e4efb00d05 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -170,7 +170,7 @@ Proof. rewrite !sintegralE; set F := f @` _; set G := g @` _; set FG := _ @` _. pose pf x := f @^-1` [set x]; pose pg y := g @^-1` [set y]. transitivity (\sum_(z \in FG) z%:E * \sum_(a \in F) m (pf a `&` pg (z - a)%R)). - apply: eq_fsbigr => z _; rewrite preimage_add -fsbig_setU// measure_fsbig//. + apply: eq_fsbigr => z _; rewrite preimageD1 -fsbig_setU// measure_fsbig//. by move=> x Fx; exact: measurableI. exact/trivIset_setIr/trivIset_preimage1. under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//=. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 0029be1576..8e1a5bd7e2 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -227,16 +227,6 @@ move=> x0; apply/seteqP. by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK). Qed. -Lemma preimage_add T (R : numDomainType) (f g : T -> R) z : - (f \+ g) @^-1` [set z] = \bigcup_(a in f @` setT) - ((f @^-1` [set a]) `&` (g @^-1` [set z - a])). -Proof. -apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] [fxfy gzf]]; last first. - by rewrite gzf -fxfy addrC subrK. -exists (z - g x); first by exists x; rewrite // -fgz addrK. -by split; rewrite 1?subKr // -fgz addrK. -Qed. - Section simple_bounded. Context d (T : sigmaRingType d) (R : realType).