From 3e2830ce5653f4142476e5380a46219cfac456d5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 29 Jun 2026 20:55:11 +0900 Subject: [PATCH 01/27] reduce dep --- theories/measure_theory/measurable_function.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 061d3b958c..ea845e68e5 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -1,11 +1,10 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat algebra. +From mathcomp Require Import all_ssreflect_compat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import boolp classical_sets functions cardinality reals. -From mathcomp Require Import ereal topology normedtype. -From mathcomp Require Import sequences measurable_structure. +From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import measurable_structure. (**md**************************************************************************) (* # Measurable Functions *) @@ -29,7 +28,6 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import ProperNotations. -Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -358,7 +356,7 @@ Context {d} {T : measurableType d} {d1} {T1 : measurableType d1} Lemma g_sigma_algebra_preimage_comp (X : {mfun T >-> T1}) (f : T1 -> T2) : measurable_fun [set: T1] f -> - g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X. + g_sigma_algebra_preimage (f \o X) `<=` g_sigma_algebra_preimage X. Proof. exact: preimage_set_system_compS. Qed. End g_sigma_algebra_preimage_comp. From e9c4b2ccfcc64ac93a0fb277049852f0f8d5a25c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 16:13:36 +0900 Subject: [PATCH 02/27] make normed module depends on metric --- .../normedtype_theory/matrix_normedtype.v | 3 ++ theories/normedtype_theory/normed_module.v | 34 +++++++++++++++++-- 2 files changed, 34 insertions(+), 3 deletions(-) diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 3cd89248c9..af82f8eaa1 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -251,6 +251,9 @@ HB.instance Definition _ (K : numFieldType) m n := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n) (@mx_normZ K m n). +HB.instance Definition _ (K : numFieldType) m n := + isNormedModule.Build _ 'M[K]_(m, n). + End matrix_NormedModule. Lemma continuous_mx {V : topologicalType} {R : realFieldType} {m n : nat} diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index c57a771abc..57ef3929aa 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -92,11 +92,33 @@ HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -#[short(type="normedModType")] -HB.structure Definition NormedModule (K : numDomainType) := +HB.structure Definition NormedModule0 (K : numDomainType) := {T of PseudoMetricNormedZmod K T & ConvexTvs K T & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}. +#[short(type="normedModType")] +HB.structure Definition NormedModule (K : numDomainType) := + {T of NormedModule0 K T & Metric K T}. + +HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. + +HB.builders Context K T of isNormedModule K T. + +Let mdist (x y : T) : K := `|x - y|. + +Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed. + +Let mdist_positivity x y : mdist x y = 0 -> x = y. +Proof. by move=> /normr0_eq0/subr0_eq. Qed. + +Let ballEmdist x d : ball x d = [set y | mdist x y < d]. +Proof. by rewrite -ball_normE. Qed. + +HB.instance Definition _ := + @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist. + +HB.end. + #[short(type="subNormedModType")] HB.structure Definition SubNormedModule (R : numDomainType) (V : normedModType R) (S : pred V) := @@ -1721,7 +1743,7 @@ Qed. Section prod_NormedModule. Context {K : numFieldType} {U V : normedModType K}. -Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. +Let prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. HB.instance Definition _ := @@ -1730,6 +1752,9 @@ HB.instance Definition _ := End prod_NormedModule. +HB.instance Definition _ (R : numFieldType) (U V' : normedModType R) := + isNormedModule.Build _ (U * V')%type. + Section prod_NormedModule_lemmas. Context {T : Type} {K : numDomainType} {U V : normedModType K}. @@ -2657,6 +2682,9 @@ HB.instance Definition _ (V : vectType R) := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) (@Norm.normZ _ _ (@max_norm V)). +HB.instance Definition _ (V : vectType R) := + isNormedModule.Build _ (max_space V). + (* NB: Get Trocq to prove the continuity part automatically. *) Lemma sup_closed_ball_compact (V : vectType R) : compact (closed_ball (0 : max_space V) 1). From 2cf3927216e17f8f9fab9e113b8dfb698de549e8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 19:01:36 +0900 Subject: [PATCH 03/27] fix --- theories/normedtype_theory/normed_module.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 57ef3929aa..a6d9267c53 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -100,7 +100,7 @@ HB.structure Definition NormedModule0 (K : numDomainType) := HB.structure Definition NormedModule (K : numDomainType) := {T of NormedModule0 K T & Metric K T}. -HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. +HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. HB.builders Context K T of isNormedModule K T. From 7f296d8d2b65a8296c349f3d2130e1024667e679 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 21:12:05 +0900 Subject: [PATCH 04/27] fix --- theories/normedtype_theory/normed_module.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index a6d9267c53..7716dd3a5c 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -102,7 +102,7 @@ HB.structure Definition NormedModule (K : numDomainType) := HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. -HB.builders Context K T of isNormedModule K T. +HB.builders Context K T & isNormedModule K T. Let mdist (x y : T) : K := `|x - y|. From 504002402ede121c2ce1234f755f5b5dc018bf47 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Mon, 29 Jun 2026 16:18:06 +0200 Subject: [PATCH 05/27] added cvg_mu lemmas + sigma_algebra_subl --- CHANGELOG_UNRELEASED.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d22dbf2c37..2b80ad57be 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -2,6 +2,21 @@ ## [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` From ef2fbf7758edfc0dfce99279a8fa942232b753f9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 16:30:45 +0900 Subject: [PATCH 06/27] fix --- CHANGELOG_UNRELEASED.md | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2b80ad57be..4be1ea0f15 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` @@ -241,6 +226,11 @@ ### Changed +- in `realsum.v`: + + lemma `__admitted__psumB` proved and renamed to `psumB` + +### Changed + - in `realsum.v`: + lemma `__admitted__psumB` proved and renamed to `psumB` From eb1b97ad7cf0969114f525768525f2f36a0ebd15 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Tue, 30 Jun 2026 10:46:17 +0200 Subject: [PATCH 07/27] added preimageD --- classical/functions.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/classical/functions.v b/classical/functions.v index d60b235ce8..a2ea074f8a 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,12 +2766,21 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). +<<<<<<< HEAD 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 eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. +======= +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. +>>>>>>> b6d8fd45 (added preimageD) by rewrite subrKC. Qed. From 1e3fdd986ff2220849fd89ff9c17946542677d03 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 19:20:28 +0900 Subject: [PATCH 08/27] actually use preimageD1 --- classical/functions.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/classical/functions.v b/classical/functions.v index a2ea074f8a..af7062d3ed 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,6 +2766,7 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). +<<<<<<< HEAD <<<<<<< HEAD Lemma preimageD1 {T : Type} {Z : zmodType} (f g : T -> Z) (z : Z) : (f \+ g) @^-1`[set z] = @@ -2781,6 +2782,14 @@ Proof. rewrite/preimage eqEsubset; split=>[x /= fgz| x [a _ [/= <- -> ]]]. exists (f x)=>//; split=>//=. by rewrite -fgz addrC addKr. >>>>>>> b6d8fd45 (added preimageD) +======= +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 eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. + by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. +>>>>>>> 328801e7 (actually use preimageD1) by rewrite subrKC. Qed. From 60ee49c97ca19f01d6204fe137d54a2ce10b9d3a Mon Sep 17 00:00:00 2001 From: adjevahi Date: Tue, 30 Jun 2026 15:29:16 +0200 Subject: [PATCH 09/27] added sub_sigma_algebra_measurable and subset_g_sigma_algebra --- theories/measure_theory/measurable_structure.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 9512b6b6d9..a491449a2c 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1287,6 +1287,16 @@ Variables (T : choiceType) (G : set (set T)). Lemma sigma_algebraC (A : set T) : <> A -> <> (~` A). Proof. by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed. +Lemma sub_sigma_algebra_measurable {d} {M : measurableType d} {H : set (set M)} +(mH : H `<=`d.-measurable) : <> `<=` d.-measurable. +Proof. + by rewrite /smallest/bigcap=> K/= /(_ measurable) oK; apply: oK; + split=>[|//]; apply:sigma_algebra_measurable. +Qed. + +Lemma subset_g_sigma_algebra : G `<=`<>. +Proof. by rewrite /smallest=>A hA H [saH GH]; apply: GH. Qed. + HB.instance Definition _ := Choice.on (g_sigma_algebraType G). HB.instance Definition _ := @isMeasurable.Build (sigma_display G) (g_sigma_algebraType G) From 9b9f4c30ff1fdf633f5828f6236598573dbeb3ea Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 1 Jul 2026 08:33:20 +0200 Subject: [PATCH 10/27] added cvg_mu lemmas + sigma_algebra_subl --- CHANGELOG_UNRELEASED.md | 3 ++ .../measure_theory/measurable_structure.v | 10 ++++-- theories/measure_theory/measure_function.v | 31 +++++++++++++++++++ 3 files changed, 42 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4be1ea0f15..1a44e89e6e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,6 +18,7 @@ - in `measurable_structure.v`: + lemmas `g_sigma_algebra_cross`, `g_sigma_algebra_rectangle` + + lemma `sigma_algebra_sub` - in `measurable_function.v`: + lemma `preimage_measurability` @@ -49,6 +50,7 @@ - in `measure_function.v`: + lemma `g_sigma_algebra_finite_measure_unique` + + lemmas `bigcap_cvg_mu`, `bigcup_cvg_mu` - new file `independence.v`: + definition `independent_events` @@ -366,6 +368,7 @@ - in `measurable_structure.v`: + `measurable_prod_measurableType` -> `prod_measurable_rectangle` + + `sub_sigma_algebra2` -> `sigma_algebra_sub` - in `measurable_realfun.v`: + `measurable_fun_itv_co` -> `measurable_fun_itvbb_itvco` + `measurable_fun_itv_oc` -> `measurable_fun_itvbb_itvoc` diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index a491449a2c..6f623b5d1f 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -355,7 +355,13 @@ by apply: (PU) => n; apply: GA. Qed. Hint Resolve smallest_sigma_algebra : core. -Lemma sub_sigma_algebra2 M : M `<=` G -> <> `<=` <>. +Lemma sigma_algebra_subl M : M `<=` <> -> <> `<=` <>. +Proof. +rewrite /smallest/==> /[dup] MsG K A sMA H [sH GH]. apply : (sMA H); split=>//. +apply: (subset_trans MsG). by apply: bigcap_inf; split. +Qed. + +Lemma sigma_algebra_sub M : M `<=` G -> <> `<=` <>. Proof. exact: sub_smallest2r. Qed. Lemma sigma_algebra_id : sigma_algebra D G -> <> = G. @@ -1626,7 +1632,7 @@ move=> sX sY; apply/seteqP; split. apply: (@measurableI _ (@g_sigma_algebraType _ (X `x` Y))). + by apply: sub_sigma_algebra; left; exists A1 => //; rewrite setTI. + by apply: sub_sigma_algebra; right; exists A2 => //; rewrite setTI. -- apply: sub_sigma_algebra2 => A [|]. +- apply: sigma_algebra_sub => A [|]. + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}]. by rewrite -setXT setTI; exact: rectangle_setX. + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}]. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 2d997d9280..ebec11e695 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1723,6 +1723,37 @@ apply: nondecreasing_cvg_mu. - by move=> n m NM; apply/subsetPset; apply: setDS; apply/subsetPset/niF. Qed. +Lemma bigcup_cvg_mu {d} {M : sigmaRingType d} {R : realFieldType} +{mu : {measure set M -> \bar R}} (A : (set M)^nat) +(mA : forall i, measurable (A i)) : +mu (\bigcup_(i\oo] --> mu (\bigcup_n A n). +Proof. +rewrite [\bigcup_n A n] (_:_ = \bigcup_n (\bigcup_(i [a [n _ Ana]|a [n _ [k kn aka]]]. + by exists n.+1=>//; exists n=>/=. by exists k. +apply: nondecreasing_cvg_mu=>[i||n m nm]; try apply: bigcup_measurable=>k _//. + exact: bigcup_measurable. +apply/subsetPset=> x [i/= i_n Aix]; exists i=>//=. exact: (ltn_leq_trans i_n). +Qed. + +(* can remove the finite hyp if we have \bigcap_(i \bar R}} (A : (set M)^nat) +(mA : forall i, measurable (A i)) : +mu (\bigcap_(i\oo] --> mu (\bigcap_n A n). +Proof. +rewrite [\bigcap_n A n] (_:_ = \bigcap_n (\bigcap_(i [a/=aia j _ i _|a/= aIa i _]. exact: aia. + exact: (aIa i.+1). +apply: nonincreasing_cvg_mu. +apply: (le_lt_trans (le_measure mu _ _ (subsetT _)) + (fin_num_fun_lty (fin_num_measure mu))); rewrite ?in_setE//. + exact: bigcap_measurableType. move=>i; exact: bigcap_measurableType. + apply: bigcap_measurableType=> k _; exact: bigcap_measurableType. +move=> n m nm; apply/subsetPset=> x bAx i/= i_n. +apply: (bAx i); exact: (ltn_leq_trans i_n nm). +Qed. + End measure_continuity. Section g_sigma_algebra_measure_unique_trace. From 9f692119507bae0f4017a6d07ca8b43d7fb92898 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 1 Jul 2026 08:38:20 +0200 Subject: [PATCH 11/27] rebase --- classical/functions.v | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/classical/functions.v b/classical/functions.v index af7062d3ed..d60b235ce8 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,30 +2766,12 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). -<<<<<<< HEAD -<<<<<<< HEAD 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 eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. -======= -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. ->>>>>>> b6d8fd45 (added preimageD) -======= -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 eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. - by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. ->>>>>>> 328801e7 (actually use preimageD1) by rewrite subrKC. Qed. From 1c329b72b23f0c69e5ea9eb4b9df7aa26d5d624a Mon Sep 17 00:00:00 2001 From: adjevahi Date: Mon, 29 Jun 2026 16:18:06 +0200 Subject: [PATCH 12/27] rebase + added cvg_mu and sigma_algebra_subl --- CHANGELOG_UNRELEASED.md | 15 +++++++++++++++ classical/classical_sets.v | 8 ++++++++ 2 files changed, 23 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1a44e89e6e..40c952ad0b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -2,6 +2,21 @@ ## [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` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index dd3a74ea1c..3e91415457 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2115,6 +2115,7 @@ 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. +<<<<<<< HEAD #[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. @@ -2125,6 +2126,13 @@ Lemma setD_bigcupr (F : I -> set T) (P : set I) (A : set T) : P !=set0 -> 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_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) : +>>>>>>> 93b0d36e (added setD_bigcapr + renamed bigcupDr to setD_bigcupr) A `\` \bigcap_(i in P) F i = \bigcup_(i in P) (A `\` F i). Proof. by rewrite setDE setC_bigcap setI_bigcupr. Qed. From dfcd8900186a734f756d8560f746507382cb08e8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 16:30:45 +0900 Subject: [PATCH 13/27] fix --- CHANGELOG_UNRELEASED.md | 15 --------------- classical/classical_sets.v | 8 -------- 2 files changed, 23 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 40c952ad0b..1a44e89e6e 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` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 3e91415457..dd3a74ea1c 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2115,7 +2115,6 @@ 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. -<<<<<<< HEAD #[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. @@ -2126,13 +2125,6 @@ Lemma setD_bigcupr (F : I -> set T) (P : set I) (A : set T) : P !=set0 -> 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_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) : ->>>>>>> 93b0d36e (added setD_bigcapr + renamed bigcupDr to setD_bigcupr) A `\` \bigcap_(i in P) F i = \bigcup_(i in P) (A `\` F i). Proof. by rewrite setDE setC_bigcap setI_bigcupr. Qed. From 9f140959399d7fee15d39d1e232f751c76beb00b Mon Sep 17 00:00:00 2001 From: adjevahi Date: Tue, 30 Jun 2026 10:46:17 +0200 Subject: [PATCH 14/27] added preimageD --- classical/functions.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/classical/functions.v b/classical/functions.v index d60b235ce8..a2ea074f8a 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,12 +2766,21 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). +<<<<<<< HEAD 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 eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. +======= +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. +>>>>>>> b6d8fd45 (added preimageD) by rewrite subrKC. Qed. From a7f1fd2b05f21a1bd0b10d43f155f4e0d82546d9 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 1 Jul 2026 08:54:58 +0200 Subject: [PATCH 15/27] cleanup --- CHANGELOG_UNRELEASED.md | 5 ---- classical/functions.v | 9 ------- .../measure_theory/measurable_structure.v | 10 -------- theories/measure_theory/measure_function.v | 24 +++++++++---------- 4 files changed, 12 insertions(+), 36 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1a44e89e6e..a684c757b0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -228,11 +228,6 @@ ### Changed -- in `realsum.v`: - + lemma `__admitted__psumB` proved and renamed to `psumB` - -### Changed - - in `realsum.v`: + lemma `__admitted__psumB` proved and renamed to `psumB` diff --git a/classical/functions.v b/classical/functions.v index a2ea074f8a..d60b235ce8 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2766,21 +2766,12 @@ Definition fctE := (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE, zerofctE, onefctE). -<<<<<<< HEAD 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 eqEsubset; split => [x <-|x [a _ /= [<- ->]]]. by exists (f x) => /=; [exact/imageT|rewrite addrC addKr]. -======= -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. ->>>>>>> b6d8fd45 (added preimageD) by rewrite subrKC. Qed. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 6f623b5d1f..e10e386d70 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1293,16 +1293,6 @@ Variables (T : choiceType) (G : set (set T)). Lemma sigma_algebraC (A : set T) : <> A -> <> (~` A). Proof. by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed. -Lemma sub_sigma_algebra_measurable {d} {M : measurableType d} {H : set (set M)} -(mH : H `<=`d.-measurable) : <> `<=` d.-measurable. -Proof. - by rewrite /smallest/bigcap=> K/= /(_ measurable) oK; apply: oK; - split=>[|//]; apply:sigma_algebra_measurable. -Qed. - -Lemma subset_g_sigma_algebra : G `<=`<>. -Proof. by rewrite /smallest=>A hA H [saH GH]; apply: GH. Qed. - HB.instance Definition _ := Choice.on (g_sigma_algebraType G). HB.instance Definition _ := @isMeasurable.Build (sigma_display G) (g_sigma_algebraType G) diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index ebec11e695..6c8ce84914 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1723,13 +1723,13 @@ apply: nondecreasing_cvg_mu. - by move=> n m NM; apply/subsetPset; apply: setDS; apply/subsetPset/niF. Qed. -Lemma bigcup_cvg_mu {d} {M : sigmaRingType d} {R : realFieldType} -{mu : {measure set M -> \bar R}} (A : (set M)^nat) -(mA : forall i, measurable (A i)) : +Lemma bigcup_cvg_mu {d} {M : sigmaRingType d} {R : realFieldType} +{mu : {measure set M -> \bar R}} (A : (set M)^nat) +(mA : forall i, measurable (A i)) : mu (\bigcup_(i\oo] --> mu (\bigcup_n A n). Proof. -rewrite [\bigcup_n A n] (_:_ = \bigcup_n (\bigcup_(i [a [n _ Ana]|a [n _ [k kn aka]]]. +rewrite [\bigcup_n A n] (_:_ = \bigcup_n (\bigcup_(i [a [n _ Ana]|a [n _ [k kn aka]]]. by exists n.+1=>//; exists n=>/=. by exists k. apply: nondecreasing_cvg_mu=>[i||n m nm]; try apply: bigcup_measurable=>k _//. exact: bigcup_measurable. @@ -1737,20 +1737,20 @@ apply/subsetPset=> x [i/= i_n Aix]; exists i=>//=. exact: (ltn_leq_trans i_n). Qed. (* can remove the finite hyp if we have \bigcap_(i \bar R}} (A : (set M)^nat) +Lemma bigcap_cvg_mu {d} {M : measurableType d} {R : realType} +{mu : {finite_measure set M -> \bar R}} (A : (set M)^nat) (mA : forall i, measurable (A i)) : mu (\bigcap_(i\oo] --> mu (\bigcap_n A n). Proof. -rewrite [\bigcap_n A n] (_:_ = \bigcap_n (\bigcap_(i [a/=aia j _ i _|a/= aIa i _]. exact: aia. exact: (aIa i.+1). -apply: nonincreasing_cvg_mu. -apply: (le_lt_trans (le_measure mu _ _ (subsetT _)) - (fin_num_fun_lty (fin_num_measure mu))); rewrite ?in_setE//. +apply: nonincreasing_cvg_mu. +apply: (le_lt_trans (le_measure mu _ _ (subsetT _)) + (fin_num_fun_lty (fin_num_measure mu))); rewrite ?in_setE//. exact: bigcap_measurableType. move=>i; exact: bigcap_measurableType. apply: bigcap_measurableType=> k _; exact: bigcap_measurableType. -move=> n m nm; apply/subsetPset=> x bAx i/= i_n. +move=> n m nm; apply/subsetPset=> x bAx i/= i_n. apply: (bAx i); exact: (ltn_leq_trans i_n nm). Qed. From 0311531e79d503e28affbc66a828cfc442a970a9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 1 Jul 2026 17:47:47 +0900 Subject: [PATCH 16/27] fix --- CHANGELOG_UNRELEASED.md | 7 ++- classical/classical_sets.v | 11 ++++ .../measure_theory/measurable_structure.v | 4 +- theories/measure_theory/measure_function.v | 58 ++++++++++--------- 4 files changed, 49 insertions(+), 31 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a684c757b0..b25faea857 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -50,7 +50,6 @@ - in `measure_function.v`: + lemma `g_sigma_algebra_finite_measure_unique` - + lemmas `bigcap_cvg_mu`, `bigcup_cvg_mu` - new file `independence.v`: + definition `independent_events` @@ -226,6 +225,12 @@ - in `functions.v`: + lemma `preimageD1` +- in `measure_function.v`: + + lemmas `cvg_measure_bigcap`, `cvg_measure_bigcup` + +- in `classical_sets.v`: + + lemma `bigcup_bigsetU` + ### Changed - in `realsum.v`: diff --git a/classical/classical_sets.v b/classical/classical_sets.v index dd3a74ea1c..9e713ee41a 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2343,6 +2343,17 @@ rewrite -(big_mkord xpredT F) -bigcup_seq. by apply: eq_bigcupl; split=> i; rewrite /= mem_index_iota leq0n. Qed. +Lemma bigcup_bigsetU F : + \bigcup_k \big[setU/set0]_(i < k.+1) F i = + \bigcup_k \big[setU/set0]_(i < k) F i. +Proof. +transitivity (\bigcup_(k in S @` setT) \big[setU/set0]_(i < k) F i). + by rewrite bigcup_image. +rewrite [RHS](bigcup_setD1 0%N)// big_ord0 set0U; apply: eq_bigcupl. +split=> [x [? _ <-//]|x [_ x0]]/=; exists x.-1 => //; rewrite prednK// lt0n. +exact/eqP. +Qed. + Lemma bigcup_bigsetU_bigcup F : \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. Proof. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index e10e386d70..cb16be3226 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -357,8 +357,8 @@ Hint Resolve smallest_sigma_algebra : core. Lemma sigma_algebra_subl M : M `<=` <> -> <> `<=` <>. Proof. -rewrite /smallest/==> /[dup] MsG K A sMA H [sH GH]. apply : (sMA H); split=>//. -apply: (subset_trans MsG). by apply: bigcap_inf; split. +move=> MsG A + H [sH GH]; apply; split => //; apply: (subset_trans MsG). +exact: bigcap_inf. Qed. Lemma sigma_algebra_sub M : M `<=` G -> <> `<=` <>. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 6c8ce84914..593f507bb0 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1674,7 +1674,7 @@ Qed. Section measure_continuity. Local Open Scope ereal_scope. -Lemma nondecreasing_cvg_mu d (T : ringOfSetsType d) (R : realFieldType) +Lemma nondecreasing_cvg_measure d (T : ringOfSetsType d) (R : realFieldType) (mu : {measure set T -> \bar R}) (F : (set T) ^nat) : (forall i, measurable (F i)) -> measurable (\bigcup_n F n) -> nondecreasing_seq F -> @@ -1697,7 +1697,7 @@ under eq_fun do rewrite -(big_mkord predT (mu \o seqD F)). exact/(nS m.+1)/(leq_trans nm). Qed. -Lemma nonincreasing_cvg_mu d (T : algebraOfSetsType d) (R : realFieldType) +Lemma nonincreasing_cvg_measure d (T : algebraOfSetsType d) (R : realFieldType) (mu : {measure set T -> \bar R}) (F : (set T) ^nat) : mu (F 0%N) < +oo -> (forall i, measurable (F i)) -> measurable (\bigcap_n F n) -> @@ -1716,45 +1716,47 @@ have -> : \bigcap_n F n = F 0%N `&` \bigcap_n F n. rewrite -measureD // setDE setC_bigcap setI_bigcupr -[x in bigcup _ x]/G. have -> : (fun n => mu (F 0%N) - mu (F n)) = mu \o G. by apply: funext => n /=; rewrite measureD// setIidr//; exact/subsetPset/niF. -apply: nondecreasing_cvg_mu. +apply: nondecreasing_cvg_measure. - by move=> ?; apply: measurableD; exact: mF. - rewrite -setI_bigcupr; apply: measurableI; first exact: mF. by rewrite -@setC_bigcap; exact: measurableC. - by move=> n m NM; apply/subsetPset; apply: setDS; apply/subsetPset/niF. Qed. -Lemma bigcup_cvg_mu {d} {M : sigmaRingType d} {R : realFieldType} -{mu : {measure set M -> \bar R}} (A : (set M)^nat) -(mA : forall i, measurable (A i)) : -mu (\bigcup_(i\oo] --> mu (\bigcup_n A n). +Lemma cvg_measure_bigcup {d} {M : sigmaRingType d} {R : realFieldType} + {mu : {measure set M -> \bar R}} (A : (set M)^nat) + (mA : forall i, measurable (A i)) : + mu (\bigcup_(i < n) A i) @[n-->\oo] --> mu (\bigcup_n A n). Proof. -rewrite [\bigcup_n A n] (_:_ = \bigcup_n (\bigcup_(i [a [n _ Ana]|a [n _ [k kn aka]]]. - by exists n.+1=>//; exists n=>/=. by exists k. -apply: nondecreasing_cvg_mu=>[i||n m nm]; try apply: bigcup_measurable=>k _//. - exact: bigcup_measurable. -apply/subsetPset=> x [i/= i_n Aix]; exists i=>//=. exact: (ltn_leq_trans i_n). +rewrite -bigcup_bigsetU_bigcup bigcup_bigsetU. +under eq_bigcupr do rewrite -bigcup_mkord. +apply: nondecreasing_cvg_measure => [i||n m nm]; [exact: bigcup_measurable| + by apply: bigcup_measurable => ? ?; exact: bigcup_measurable|]. +by apply/subsetPset => x [i/= i_n Aix]; exists i => //=; exact: leq_trans nm. Qed. -(* can remove the finite hyp if we have \bigcap_(i \bar R}} (A : (set M)^nat) -(mA : forall i, measurable (A i)) : -mu (\bigcap_(i\oo] --> mu (\bigcap_n A n). +Lemma cvg_measure_bigcap {d} {M : measurableType d} {R : realFieldType} + {mu : {measure set M -> \bar R}} (A : (set M)^nat) + (mA : forall i, measurable (A i)) : + mu (A 0%N) \is a fin_num -> + mu (\bigcap_(i < n.+1) A i) @[n-->\oo] --> mu (\bigcap_n A n). Proof. -rewrite [\bigcap_n A n] (_:_ = \bigcap_n (\bigcap_(i [a/=aia j _ i _|a/= aIa i _]. exact: aia. - exact: (aIa i.+1). -apply: nonincreasing_cvg_mu. -apply: (le_lt_trans (le_measure mu _ _ (subsetT _)) - (fin_num_fun_lty (fin_num_measure mu))); rewrite ?in_setE//. - exact: bigcap_measurableType. move=>i; exact: bigcap_measurableType. - apply: bigcap_measurableType=> k _; exact: bigcap_measurableType. -move=> n m nm; apply/subsetPset=> x bAx i/= i_n. -apply: (bAx i); exact: (ltn_leq_trans i_n nm). +move=> muA0. +rewrite [\bigcap_n A n] (_:_ = \bigcap_n (\bigcap_(i < n.+1) A i)). + by rewrite eqEsubset/bigcap; split=> [a/= + j _ i _|a/= aIa i _]; + [exact|exact: (aIa i.+1)]. +apply: nonincreasing_cvg_measure. +- by rewrite bigcap_mkord big_ord1 -ge0_fin_numE. +- by move=> i; exact: bigcap_measurableType. +- by apply: bigcap_measurableType=> k _; exact: bigcap_measurableType. +- by move=> n m nm; apply/subsetPset=> x + i/= i_n; apply; exact: leq_trans nm. Qed. End measure_continuity. +#[deprecated(since="mathcomp-analysis 1.17.0", use=nondecreasing_cvg_measure)] +Notation nondecreasing_cvg_mu := nondecreasing_cvg_measure. +#[deprecated(since="mathcomp-analysis 1.17.0", use=nonincreasing_cvg_measure)] +Notation nonincreasing_cvg_mu := nonincreasing_cvg_measure. Section g_sigma_algebra_measure_unique_trace. Context d (R : realType) (T : measurableType d). From 16c6713e0b88abe8e0401c83da7d958235e680d7 Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 1 Jul 2026 11:13:27 +0200 Subject: [PATCH 17/27] added countable_big(a/u)p measurable --- theories/measure_theory/measurable_structure.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index cb16be3226..7959144310 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1163,6 +1163,22 @@ Lemma bigcapT_measurable F : (forall k, measurable (F k)) -> measurable (\bigcap_i F i). Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed. +Lemma countable_bigcup_measurable {U} {F : U -> set T} + {P : set U} : countable P -> (forall i, P i -> measurable (F i)) -> + measurable (\bigcup_(i in P) F i). +Proof. +move=>/[dup] cP /pfcard_geP=>[[-> _|/surjfunPex [f ->] mF]]. by rewrite bigcup0. +rewrite bigcup_image; apply: bigcupT_measurable=>// i; exact: mF. +Qed. + +Lemma countable_bigcap_measurable {U} {F : U -> set T} {P : set U} : + P !=set0 -> countable P -> (forall k, P k -> measurable (F k)) -> + measurable (\bigcap_(i in P) F i). +Proof. +move=> [j Pj] /pfcard_geP=>[[P0|/surjfunPex [f ->] mF]]. by rewrite P0/= in Pj. +by rewrite bigcap_image; apply: bigcap_measurable=>// k _; exact: mF. +Qed. + End sigmaring_lemmas. (* Adapted from mathlib induction_on_inter *) From 00c09ec50239c01a70df716ff6d5a370682e12e3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 1 Jul 2026 18:28:47 +0900 Subject: [PATCH 18/27] changelog --- CHANGELOG_UNRELEASED.md | 3 +++ theories/measure_theory/measurable_structure.v | 14 ++++++++------ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b25faea857..2d85fdc0a5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -231,6 +231,9 @@ - in `classical_sets.v`: + lemma `bigcup_bigsetU` +- in `measurable_structure.v`: + + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` + ### Changed - in `realsum.v`: diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 7959144310..cff4a5f0df 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1164,18 +1164,20 @@ Lemma bigcapT_measurable F : Proof. by move=> PF; apply: bigcap_measurable => //; exists 1. Qed. Lemma countable_bigcup_measurable {U} {F : U -> set T} - {P : set U} : countable P -> (forall i, P i -> measurable (F i)) -> + {P : set U} : countable P -> (forall i, P i -> measurable (F i)) -> measurable (\bigcup_(i in P) F i). Proof. -move=>/[dup] cP /pfcard_geP=>[[-> _|/surjfunPex [f ->] mF]]. by rewrite bigcup0. -rewrite bigcup_image; apply: bigcupT_measurable=>// i; exact: mF. +move=>/[dup] cP /pfcard_geP =>[[-> _|/surjfunPex [f ->] mF]]. + by rewrite bigcup0. +by rewrite bigcup_image; apply: bigcupT_measurable=>// i; exact: mF. Qed. -Lemma countable_bigcap_measurable {U} {F : U -> set T} {P : set U} : - P !=set0 -> countable P -> (forall k, P k -> measurable (F k)) -> +Lemma countable_bigcap_measurable {U} {F : U -> set T} ({P : set U) : + P !=set0 -> countable P -> (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i). Proof. -move=> [j Pj] /pfcard_geP=>[[P0|/surjfunPex [f ->] mF]]. by rewrite P0/= in Pj. +move=> [j Pj] /pfcard_geP=>[[P0|/surjfunPex [f ->] mF]]. + by rewrite P0/= in Pj. by rewrite bigcap_image; apply: bigcap_measurable=>// k _; exact: mF. Qed. From a3708e83f721f05ca67607c5a40ad87b7ecddfbd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 1 Jul 2026 18:30:40 +0900 Subject: [PATCH 19/27] fix --- theories/measure_theory/measurable_structure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index cff4a5f0df..3a7e60006b 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1172,7 +1172,7 @@ move=>/[dup] cP /pfcard_geP =>[[-> _|/surjfunPex [f ->] mF]]. by rewrite bigcup_image; apply: bigcupT_measurable=>// i; exact: mF. Qed. -Lemma countable_bigcap_measurable {U} {F : U -> set T} ({P : set U) : +Lemma countable_bigcap_measurable {U} {F : U -> set T} (P : set U) : P !=set0 -> countable P -> (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i). Proof. From 83bc0d5e6fae43121e9d819d156e84baf4e42bbe Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 16:13:36 +0900 Subject: [PATCH 20/27] make normed module depends on metric --- .../normedtype_theory/matrix_normedtype.v | 3 ++ theories/normedtype_theory/normed_module.v | 34 +++++++++++++++++-- 2 files changed, 34 insertions(+), 3 deletions(-) diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 76783da1e7..7c05bcc233 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -253,6 +253,9 @@ HB.instance Definition _ (K : numFieldType) m n := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n) (@mx_normZ K m n). +HB.instance Definition _ (K : numFieldType) m n := + isNormedModule.Build _ 'M[K]_(m, n). + End matrix_NormedModule. Lemma continuous_mx {V : topologicalType} {R : realFieldType} {m n : nat} diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index c57a771abc..57ef3929aa 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -92,11 +92,33 @@ HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -#[short(type="normedModType")] -HB.structure Definition NormedModule (K : numDomainType) := +HB.structure Definition NormedModule0 (K : numDomainType) := {T of PseudoMetricNormedZmod K T & ConvexTvs K T & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}. +#[short(type="normedModType")] +HB.structure Definition NormedModule (K : numDomainType) := + {T of NormedModule0 K T & Metric K T}. + +HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. + +HB.builders Context K T of isNormedModule K T. + +Let mdist (x y : T) : K := `|x - y|. + +Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed. + +Let mdist_positivity x y : mdist x y = 0 -> x = y. +Proof. by move=> /normr0_eq0/subr0_eq. Qed. + +Let ballEmdist x d : ball x d = [set y | mdist x y < d]. +Proof. by rewrite -ball_normE. Qed. + +HB.instance Definition _ := + @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist. + +HB.end. + #[short(type="subNormedModType")] HB.structure Definition SubNormedModule (R : numDomainType) (V : normedModType R) (S : pred V) := @@ -1721,7 +1743,7 @@ Qed. Section prod_NormedModule. Context {K : numFieldType} {U V : normedModType K}. -Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. +Let prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. HB.instance Definition _ := @@ -1730,6 +1752,9 @@ HB.instance Definition _ := End prod_NormedModule. +HB.instance Definition _ (R : numFieldType) (U V' : normedModType R) := + isNormedModule.Build _ (U * V')%type. + Section prod_NormedModule_lemmas. Context {T : Type} {K : numDomainType} {U V : normedModType K}. @@ -2657,6 +2682,9 @@ HB.instance Definition _ (V : vectType R) := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) (@Norm.normZ _ _ (@max_norm V)). +HB.instance Definition _ (V : vectType R) := + isNormedModule.Build _ (max_space V). + (* NB: Get Trocq to prove the continuity part automatically. *) Lemma sup_closed_ball_compact (V : vectType R) : compact (closed_ball (0 : max_space V) 1). From 61fd9b80bcb19028c8b72e9585c4ad5db5c34fe9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 19:01:36 +0900 Subject: [PATCH 21/27] fix --- theories/normedtype_theory/normed_module.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 57ef3929aa..a6d9267c53 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -100,7 +100,7 @@ HB.structure Definition NormedModule0 (K : numDomainType) := HB.structure Definition NormedModule (K : numDomainType) := {T of NormedModule0 K T & Metric K T}. -HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. +HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. HB.builders Context K T of isNormedModule K T. From d3a6630e5749726450f407808bfc9ef0343c737b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 21:12:05 +0900 Subject: [PATCH 22/27] fix --- theories/normedtype_theory/normed_module.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index a6d9267c53..7716dd3a5c 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -102,7 +102,7 @@ HB.structure Definition NormedModule (K : numDomainType) := HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. -HB.builders Context K T of isNormedModule K T. +HB.builders Context K T & isNormedModule K T. Let mdist (x y : T) : K := `|x - y|. From eb9c712babc403b449582c04e44a90d5063e6d29 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 16:13:36 +0900 Subject: [PATCH 23/27] make normed module depends on metric --- theories/normedtype_theory/normed_module.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 7716dd3a5c..46b222d17b 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -100,9 +100,15 @@ HB.structure Definition NormedModule0 (K : numDomainType) := HB.structure Definition NormedModule (K : numDomainType) := {T of NormedModule0 K T & Metric K T}. +<<<<<<< HEAD HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. HB.builders Context K T & isNormedModule K T. +======= +HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. + +HB.builders Context K T of isNormedModule K T. +>>>>>>> e9c4b2cc (make normed module depends on metric) Let mdist (x y : T) : K := `|x - y|. From 01faf804bfa8190a28898a54463fed6e5b612e6a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 19:01:36 +0900 Subject: [PATCH 24/27] fix --- theories/normedtype_theory/normed_module.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 46b222d17b..2df820e17a 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -100,12 +100,16 @@ HB.structure Definition NormedModule0 (K : numDomainType) := HB.structure Definition NormedModule (K : numDomainType) := {T of NormedModule0 K T & Metric K T}. +<<<<<<< HEAD <<<<<<< HEAD HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. HB.builders Context K T & isNormedModule K T. ======= HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. +======= +HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. +>>>>>>> 2cf39272 (fix) HB.builders Context K T of isNormedModule K T. >>>>>>> e9c4b2cc (make normed module depends on metric) From 249f5a8a80477a3c7377a3840adf2a55ed91cc09 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 30 Jun 2026 21:12:05 +0900 Subject: [PATCH 25/27] fix --- theories/normedtype_theory/normed_module.v | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 2df820e17a..7716dd3a5c 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -100,19 +100,9 @@ HB.structure Definition NormedModule0 (K : numDomainType) := HB.structure Definition NormedModule (K : numDomainType) := {T of NormedModule0 K T & Metric K T}. -<<<<<<< HEAD -<<<<<<< HEAD HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. HB.builders Context K T & isNormedModule K T. -======= -HB.factory Record isNormedModule (K : numDomainType) T of NormedModule0 K T := { }. -======= -HB.factory Record isNormedModule (K : numDomainType) T & NormedModule0 K T := { }. ->>>>>>> 2cf39272 (fix) - -HB.builders Context K T of isNormedModule K T. ->>>>>>> e9c4b2cc (make normed module depends on metric) Let mdist (x y : T) : K := `|x - y|. From ad3a1d37088c13b003fc3f3a8112b352c5394d0d Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 1 Jul 2026 17:03:07 +0200 Subject: [PATCH 26/27] added separable def, +sigma algebras generated by basis --- CHANGELOG_UNRELEASED.md | 8 ++ _CoqProject | 1 + theories/topology_theory/topology_structure.v | 89 +++++++++++++++++-- 3 files changed, 93 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..1e7cac042a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,14 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in `topology_structure.v` : + + definitions `separable`, `separable_set` + + lemmas `basisP`, `separableE`, `second_countable_separable`, + `bigcupT_separable`, `bigcup_separable` + +- new file `measurable_topology.v` + + lemmas `salgebra_countable_basis`, `salgebra_open_closedE` + ### Changed - in `realsum.v`: diff --git a/_CoqProject b/_CoqProject index f0b745c7f6..98873fe72a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -99,6 +99,7 @@ theories/derive.v theories/numfun.v theories/measure_theory/measurable_structure.v +theories/measure_theory/measurable_topology.v theories/measure_theory/measure_function.v theories/measure_theory/counting_measure.v theories/measure_theory/dirac_measure.v diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 6661159148..6388976e25 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -45,6 +45,8 @@ From mathcomp Require Export filter. (* isolated A == the set of isolated points of A *) (* dense S == the set (S : set T) is dense in T, with T of *) (* type topologicalType *) +(* separable T == T has a countable dense subset *) +(* separable_set A == A : set T has a countable dense subset *) (* continuousType == type of continuous functions *) (* The HB structures is Continuous. *) (* mkcts f_cts == object of type continuousType corresponding to *) @@ -122,11 +124,6 @@ Context {T : topologicalType}. Definition open_nbhs (p : T) (A : set T) := open A /\ A p. -Definition basis (B : set (set T)) := - B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x. - -Definition second_countable := exists2 B, countable B & basis B. - Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p). Proof. by apply: nbhs_pfilter_subproof; case: T p => ? []. Qed. Typeclasses Opaque nbhs. @@ -998,6 +995,88 @@ apply/not_implyP; split; first exact: openT. by rewrite setTI => -[]. Qed. +Section basis. +Context {T : topologicalType}. + +Definition basis (B : set (set T)) := + B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x. + +(* Maybe rename separable_space*) +Definition separable := exists D : set T, + countable D /\ dense D. + +Definition separable_set (A : set T) := +exists D, + [/\ countable D, D `<=` A & forall O, A`&`O !=set0 -> open O -> O`&`D !=set0]. + +Definition second_countable := exists2 B, countable B & basis B. + +Lemma basisP {B : set_system T} : basis B <-> B `<=`open +/\ (forall U: set T, open U -> U = \bigcup_(V in [set W | B W /\ W `<=`U]) V). +Proof. +split=> [[oB bB]|[Bo dec]]. split=> //U oU. + rewrite eqEsubset /bigcup; split=>[x Ux/=|x [A/= [BA AU] /AU //]]. + have:= bB x. rewrite/cvg_to {2}/nbhs/filter_from/= => /(_ U)/=. + have nT: \near x, U x by apply: (open_in_nearW oU)=>[y|]; rewrite in_setE. + rewrite nbhs_nearE !exists2E/= => /(_ nT). + by under eq_exists=>x0 do rewrite -andA {1}(andC (x0 x) _) andA. +split=>// x. rewrite/cvg_to/=nbhsE/open_nbhs => P /= + [U [/(dec U)->] [A [BA AU] Ax] UP]. exists A=>// t At; apply: UP. by exists A. +Qed. + +(* Could be renamed to separableTE*) +Lemma separableE : separable = separable_set [set:T]. +Proof. +apply: eq_exists=>A. rewrite [X in [/\ _, _ & X]] (_:_ = dense A)//. + by under eq_forall do rewrite setTI. +by rewrite propeqE; split=>[[cA dA]|[cA _ dA]]. +Qed. + +Lemma second_countable_separable : + second_countable -> separable. +Proof. +move=> [B] /(sub_countable (card_le_setD B [set set0])). +rewrite/countable=> /pfcard_geP. case=> [|[f] /basisP [oB bB]]. + rewrite setD_eq0=> /subset_set1. case=> -> /basisP [oB bB]; + have:= (bB [set:T]) openT. rewrite [X in \bigcup_(_ in X) _] (_:_ = set0). + by apply: eq_set=>x/=; rewrite andB. rewrite bigcup0=>//. + move=> T0; exists set0; split=>// O [x /(subsetT O)]. by rewrite T0. + rewrite [X in \bigcup_(_ in X) _] (_:_ = [set set0]). + apply: eq_set=>x/=; rewrite [X in _/\ X] (_:_ = True). + by apply: propT; exact: subsetT. by rewrite andB.1.2. rewrite bigcup_set1. + move=> T0; exists set0; split=>// O [x /(subsetT O)]. by rewrite T0. +have:= image_eq f. rewrite eqEsubset=> [[rfbs bsrf]]. +have: forall n, exists x:T, B (f n) /\ f n x. + move:rfbs=>/[swap] n. rewrite/subset/= => /(_ (f n)). + have:exists2 x, True & f x = f n by exists n. + move=> /[swap] /[apply] [[bfn /eqP /set0P [x fnx]]]. by exists x. +move=> /choice [g gP]. exists (range g). +split=> [|U /[swap] /(bB U) -> /bigcup_nonempty [A/= [BA AU] /set0P /eqP An0]]. + apply: card_image_le. have: (B `\ set0) A by[]. move=> /bsrf [n _ fnA]. +exists (g n). split=>/=. by exists A=>//; rewrite -fnA; +have [_] := gP n. by exists n. +Qed. + +Lemma bigcupT_separable [A : (set T)^nat] : (forall n, separable_set (A n)) -> +separable_set (\bigcup_n A n). +Proof. +move=>/choice [D_ /all_and3 [cDx DAx dDx]]. exists (\bigcup_n D_ n); split. + exact: bigcup_countable. exact: subset_bigcup. move=> O [x [[n _ Anx] Ox] oO]. +have /(dDx n O) /(_ oO) [y [Oy Dny]] : A n `&` O !=set0 by exists x. +by exists y; split=>//; exists n. +Qed. + +Lemma bigcup_separable [A : (set T)^nat] [P : set nat] : +(forall n, P n -> separable_set (A n)) +-> separable_set (\bigcup_(i in P) A i). +Proof. +rewrite bigcup_mkcond => nsPA. apply: bigcupT_separable=>n. +case: ifPn=>[|_]. rewrite in_setE. apply: (nsPA n). +by exists set0; split=>// O [x [F]]. +Qed. + +End basis. + Section ClopenSets. Implicit Type T : topologicalType. From 721478df8e66822259e47b1425bd43dbfb27142a Mon Sep 17 00:00:00 2001 From: adjevahi Date: Wed, 1 Jul 2026 17:07:33 +0200 Subject: [PATCH 27/27] added measurable_topology --- theories/measure_theory/measurable_topology.v | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 theories/measure_theory/measurable_topology.v diff --git a/theories/measure_theory/measurable_topology.v b/theories/measure_theory/measurable_topology.v new file mode 100644 index 0000000000..56546867ec --- /dev/null +++ b/theories/measure_theory/measurable_topology.v @@ -0,0 +1,56 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect_compat algebra finmap. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import boolp classical_sets functions cardinality reals. +From mathcomp Require Import measurable_structure topology_structure metric_structure. + +(**md**************************************************************************) +(* # Measure theory applied to topological spaces via the Borel sigma-algebra.*) +(* *) +(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *) +(* *) +(* *) +(* ## Mathematical structures *) +(* ```Soon : default display open.-sigma for topological types *) +(* ``` *) +(******************************************************************************) + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import ProperNotations. +Import Order.TTheory GRing.Theory Num.Theory. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section measurable_topology. +Context {T : topologicalType}. + +Lemma salgebra_countable_basis {B : set_system T} (D : set T) : +countable B -> basis B -> <> = <>. +Proof. +rewrite eqEsubset => /countable_bijP [A /card_esym/pcard_eqP/bijPex/= + [g [fg _ ag]]] /basisP [BO bB]; split. exact: sigma_algebra_sub. +apply: sigma_algebra_subl=> U /bB ->. +have sgU : set_surj (A `&` [set n | g n `<=` U]) (B `&` [set W | W `<=` U]) g. +by rewrite surjE in ag; rewrite surjE=> W [/ag [n An <-]/= gnU]; exists n. +rewrite (reindex_bigcup _ _ _ _ _ sgU). move=> n /= [a u]; split=>//. exact: fg. +rewrite bigcup_mkcond; apply: sigma_algebra_bigcup=> i. case: ifP=>//[|_]. + rewrite in_setE=> [[Ai _]]. apply: sub_sigma_algebra. exact: fg. +exact: sigma_algebra0. +Qed. + +Lemma salgebra_open_closedE : +<> = <>. +Proof. +rewrite eqEsubset; split; apply: sigma_algebra_subl. + move=> U oU; rewrite -(setCK U); apply: (sigma_algebraC (sub_sigma_algebra _)); + exact: open_closedC. +move=> F cF; rewrite -(setCK F); apply: (sigma_algebraC (sub_sigma_algebra _)); +exact: closed_openC. +Qed. + +End measurable_topology. \ No newline at end of file