From e55f63fb86f34a871d396c7f527000d7c385a60f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 May 2026 18:25:26 +0900 Subject: [PATCH 1/2] reduce dependencies in measurable_structure.v --- .../measure_theory/measurable_structure.v | 86 +++++++++++++++++-- theories/measure_theory/measure_function.v | 6 ++ 2 files changed, 84 insertions(+), 8 deletions(-) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index fe676545ac..fbaa27e15f 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect_compat all_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 ereal topology normedtype sequences. +From mathcomp Require Import constructive_ereal. (**md**************************************************************************) (* # Measure Theory *) @@ -100,8 +100,6 @@ From mathcomp Require Import ereal topology normedtype sequences. (* g_sigma_algebra_preimage f *) (* image_set_system D f G == set system of the sets with a preimage *) (* by f in G *) -(* subset_sigma_subadditive mu == alternative predicate defining *) -(* sigma-subadditivity *) (* ``` *) (* *) (* ## Product of measurable spaces *) @@ -157,6 +155,83 @@ Bind Scope measure_display_scope with measure_display. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +(* dup from sequences.v *) +Notation "'nondecreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n <= m)%O}) + (at level 10). + +Notation "'nonincreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n >= m)%O}) + (at level 10). + +Definition sequence R := nat -> R. + +Reserved Notation "R ^nat". + +Notation "R ^nat" := (sequence R) : type_scope. + +Section seqD. +Variable T : Type. +Implicit Types F : nat -> (set T). + +Lemma bigcup_bigsetU_bigcup F : + \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. +Proof. +apply/seteqP; split=> [x [i _]|x [i _ Fix]]. + by rewrite -bigcup_mkord => -[j _ Fjx]; exists j. +by exists i => //; rewrite big_ord_recr/=; right. +Qed. + +Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k. + +Lemma trivIset_seqDU F : trivIset setT (seqDU F). +Proof. +move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. + by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB ->. +move=> /set0P; apply: contraNeq => _; apply/eqP. +rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=. +by rewrite setCU setIAC !setIA setICl !set0I. +Qed. + +Definition seqD F := fun n => if n isn't n'.+1 then F O else F n `\` F n'. + +Lemma seqDU_seqD F : nondecreasing_seq F -> seqDU F = seqD F. +Proof. +move=> ndF; rewrite funeqE => -[|n] /=; first by rewrite /seqDU big_ord0 setD0. +rewrite /seqDU big_ord_recr /= setUC; congr (_ `\` _); apply/setUidPl. +by rewrite -bigcup_mkord => + [k /= kn]; exact/subsetPset/ndF/ltnW. +Qed. + +Lemma trivIset_seqD F : nondecreasing_seq F -> trivIset setT (seqD F). +Proof. by move=> ndF; rewrite -seqDU_seqD //; exact: trivIset_seqDU. Qed. + +Lemma eq_bigcup_seqD F : \bigcup_n seqD F n = \bigcup_n F n. +Proof. +apply/seteqP; split => [x []|x []]. + by elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; [exists O | exists n.+1]. +elim=> [_ F0x|n ih _ Fn1x]; first by exists O. +have [|Fnx] := pselect (F n x); last by exists n.+1. +by move=> /(ih I)[m _ Fmx]; exists m. +Qed. + +Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k. +Proof. +rewrite /seqDU predeqE => t; split=> [[n _ Fnt]|[n _]]; last first. + by rewrite setDE => -[? _]; exists n. +have [UFnt|UFnt] := pselect ((\big[setU/set0]_(k < n) F k) t); last by exists n. +suff [m [Fmt FNmt]] : exists m, F m t /\ forall k, (k < m)%N -> ~ F k t. + by exists m => //; split => //; rewrite -bigcup_mkord => -[k kj]; exact: FNmt. +move: UFnt; rewrite -bigcup_mkord => -[/= k _ Fkt] {Fnt n}. +have [n kn] := ubnP k; elim: n => // n ih in t k Fkt kn *. +case: k => [|k] in Fkt kn *; first by exists O. +have [?|] := pselect (forall m, (m <= k)%N -> ~ F m t); first by exists k.+1. +move=> /existsNP[i] /not_implyP[ik] /contrapT Fit; apply: (ih t i) => //. +by rewrite (leq_ltn_trans ik). +Qed. + +End seqD. +Arguments trivIset_seqDU {T} F. +#[global] Hint Resolve trivIset_seqDU : core. +(* /dup from sequences.v *) + Section set_systems. Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)). @@ -1435,11 +1510,6 @@ Notation sigma_algebra_image_class := sigma_algebra_image (only parsing). #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")] Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing). -(** This predicate is used also by `measure_function.v` *) -Definition subset_sigma_subadditive {T} {R : numFieldType} - (mu : set T -> \bar R) (A : set T) (F : nat -> set T) := - A `<=` \bigcup_n F n -> (mu A <= \sum_(n set T) (F : set T -> R) : finite_set D -> trivIset D A -> F set0 = idx -> diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index d8a4ac0721..0d06ee317c 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -19,6 +19,8 @@ From mathcomp Require Import measurable_structure measurable_function. (* etc. Also contains a number of details about its implementation. *) (* *) (* ``` *) +(* subset_sigma_subadditive mu == alternative predicate defining *) +(* sigma-subadditivity *) (* {content set T -> \bar R} == type of contents *) (* T is expected to be a semiring of sets and R *) (* a numFieldType. *) @@ -172,6 +174,10 @@ Definition subadditive := forall (A : set T) (F : nat -> set T) n, A `<=` \big[setU/set0]_(k < n) F k -> (mu A <= \sum_(k < n) mu (F k))%E. +Definition subset_sigma_subadditive {T} {R : numFieldType} + (mu : set T -> \bar R) (A : set T) (F : (set T)^nat) := + A `<=` \bigcup_n F n -> (mu A <= \sum_(n set T), (forall n, measurable (F n)) -> measurable A -> From 8495d56dd186b33f4090039a58c9ba26923e9ede Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 May 2026 19:13:03 +0900 Subject: [PATCH 2/2] fix dup --- classical/classical_sets.v | 86 +++++++++++++++++++ .../measure_theory/measurable_structure.v | 78 ----------------- theories/sequences.v | 62 ------------- 3 files changed, 86 insertions(+), 140 deletions(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index b19cdca9e1..e105ce3a2f 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -3493,3 +3493,89 @@ Lemma diagonalP {T : Type} (x y : T) : diagonal (x, y) <-> x = y. Proof. by []. Qed. Local Close Scope relation_scope. + +(* from sequences.v *) + +(* nondecreasing_seq u == the sequence u is non-decreasing *) +(* nonincreasing_seq u == the sequence u is non-increasing *) +(* R ^nat == notation for the type of sequences, i.e., *) +(* functions of type nat -> R *) +(* Definition sequence *) +(* seqDU F == sequence F_0, F_1 \ F_0, F_2 \ (F_0 U F_1),... *) +(* seqD F == the sequence F_0, F_1 \ F_0, F_2 \ F_1,... *) + +Notation "'nondecreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n <= m)%O}) + (at level 10). + +Notation "'nonincreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n >= m)%O}) + (at level 10). + +Definition sequence R := nat -> R. + +Reserved Notation "R ^nat". + +Notation "R ^nat" := (sequence R) : type_scope. + +Section seqD. +Variable T : Type. +Implicit Types F : nat -> (set T). + +Lemma bigcup_bigsetU_bigcup F : + \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. +Proof. +apply/seteqP; split=> [x [i _]|x [i _ Fix]]. + by rewrite -bigcup_mkord => -[j _ Fjx]; exists j. +by exists i => //; rewrite big_ord_recr/=; right. +Qed. + +Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k. + +Lemma trivIset_seqDU F : trivIset setT (seqDU F). +Proof. +move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. + by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB ->. +move=> /set0P; apply: contraNeq => _; apply/eqP. +rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=. +by rewrite setCU setIAC !setIA setICl !set0I. +Qed. + +Definition seqD F := fun n => if n isn't n'.+1 then F O else F n `\` F n'. + +Lemma seqDU_seqD F : nondecreasing_seq F -> seqDU F = seqD F. +Proof. +move=> ndF; rewrite funeqE => -[|n] /=; first by rewrite /seqDU big_ord0 setD0. +rewrite /seqDU big_ord_recr /= setUC; congr (_ `\` _); apply/setUidPl. +by rewrite -bigcup_mkord => + [k /= kn]; exact/subsetPset/ndF/ltnW. +Qed. + +Lemma trivIset_seqD F : nondecreasing_seq F -> trivIset setT (seqD F). +Proof. by move=> ndF; rewrite -seqDU_seqD //; exact: trivIset_seqDU. Qed. + +Lemma eq_bigcup_seqD F : \bigcup_n seqD F n = \bigcup_n F n. +Proof. +apply/seteqP; split => [x []|x []]. + by elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; [exists O | exists n.+1]. +elim=> [_ F0x|n ih _ Fn1x]; first by exists O. +have [|Fnx] := pselect (F n x); last by exists n.+1. +by move=> /(ih I)[m _ Fmx]; exists m. +Qed. + +Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k. +Proof. +rewrite /seqDU predeqE => t; split=> [[n _ Fnt]|[n _]]; last first. + by rewrite setDE => -[? _]; exists n. +have [UFnt|UFnt] := pselect ((\big[setU/set0]_(k < n) F k) t); last by exists n. +suff [m [Fmt FNmt]] : exists m, F m t /\ forall k, (k < m)%N -> ~ F k t. + by exists m => //; split => //; rewrite -bigcup_mkord => -[k kj]; exact: FNmt. +move: UFnt; rewrite -bigcup_mkord => -[/= k _ Fkt] {Fnt n}. +have [n kn] := ubnP k; elim: n => // n ih in t k Fkt kn *. +case: k => [|k] in Fkt kn *; first by exists O. +have [?|] := pselect (forall m, (m <= k)%N -> ~ F m t); first by exists k.+1. +move=> /existsNP[i] /not_implyP[ik] /contrapT Fit; apply: (ih t i) => //. +by rewrite (leq_ltn_trans ik). +Qed. + +End seqD. +Arguments trivIset_seqDU {T} F. +#[global] Hint Resolve trivIset_seqDU : core. +(* /dup from sequences.v *) diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index fbaa27e15f..75f633075f 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -4,7 +4,6 @@ From mathcomp Require Import all_ssreflect_compat all_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 constructive_ereal. (**md**************************************************************************) (* # Measure Theory *) @@ -155,83 +154,6 @@ Bind Scope measure_display_scope with measure_display. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -(* dup from sequences.v *) -Notation "'nondecreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n <= m)%O}) - (at level 10). - -Notation "'nonincreasing_seq' f" := ({homo f : n m / (n <= m)%nat >-> (n >= m)%O}) - (at level 10). - -Definition sequence R := nat -> R. - -Reserved Notation "R ^nat". - -Notation "R ^nat" := (sequence R) : type_scope. - -Section seqD. -Variable T : Type. -Implicit Types F : nat -> (set T). - -Lemma bigcup_bigsetU_bigcup F : - \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. -Proof. -apply/seteqP; split=> [x [i _]|x [i _ Fix]]. - by rewrite -bigcup_mkord => -[j _ Fjx]; exists j. -by exists i => //; rewrite big_ord_recr/=; right. -Qed. - -Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k. - -Lemma trivIset_seqDU F : trivIset setT (seqDU F). -Proof. -move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. - by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB ->. -move=> /set0P; apply: contraNeq => _; apply/eqP. -rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=. -by rewrite setCU setIAC !setIA setICl !set0I. -Qed. - -Definition seqD F := fun n => if n isn't n'.+1 then F O else F n `\` F n'. - -Lemma seqDU_seqD F : nondecreasing_seq F -> seqDU F = seqD F. -Proof. -move=> ndF; rewrite funeqE => -[|n] /=; first by rewrite /seqDU big_ord0 setD0. -rewrite /seqDU big_ord_recr /= setUC; congr (_ `\` _); apply/setUidPl. -by rewrite -bigcup_mkord => + [k /= kn]; exact/subsetPset/ndF/ltnW. -Qed. - -Lemma trivIset_seqD F : nondecreasing_seq F -> trivIset setT (seqD F). -Proof. by move=> ndF; rewrite -seqDU_seqD //; exact: trivIset_seqDU. Qed. - -Lemma eq_bigcup_seqD F : \bigcup_n seqD F n = \bigcup_n F n. -Proof. -apply/seteqP; split => [x []|x []]. - by elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; [exists O | exists n.+1]. -elim=> [_ F0x|n ih _ Fn1x]; first by exists O. -have [|Fnx] := pselect (F n x); last by exists n.+1. -by move=> /(ih I)[m _ Fmx]; exists m. -Qed. - -Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k. -Proof. -rewrite /seqDU predeqE => t; split=> [[n _ Fnt]|[n _]]; last first. - by rewrite setDE => -[? _]; exists n. -have [UFnt|UFnt] := pselect ((\big[setU/set0]_(k < n) F k) t); last by exists n. -suff [m [Fmt FNmt]] : exists m, F m t /\ forall k, (k < m)%N -> ~ F k t. - by exists m => //; split => //; rewrite -bigcup_mkord => -[k kj]; exact: FNmt. -move: UFnt; rewrite -bigcup_mkord => -[/= k _ Fkt] {Fnt n}. -have [n kn] := ubnP k; elim: n => // n ih in t k Fkt kn *. -case: k => [|k] in Fkt kn *; first by exists O. -have [?|] := pselect (forall m, (m <= k)%N -> ~ F m t); first by exists k.+1. -move=> /existsNP[i] /not_implyP[ik] /contrapT Fit; apply: (ih t i) => //. -by rewrite (leq_ltn_trans ik). -Qed. - -End seqD. -Arguments trivIset_seqDU {T} F. -#[global] Hint Resolve trivIset_seqDU : core. -(* /dup from sequences.v *) - Section set_systems. Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)). diff --git a/theories/sequences.v b/theories/sequences.v index 9207b9ecb9..03ed244a4c 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -14,8 +14,6 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* The purpose of this file is to gather generic definitions and lemmas about *) (* sequences. Incidentally, it defines the exponential function. *) (* ``` *) -(* nondecreasing_seq u == the sequence u is non-decreasing *) -(* nonincreasing_seq u == the sequence u is non-increasing *) (* increasing_seq u == the sequence u is (strictly) increasing *) (* decreasing_seq u == the sequence u is (strictly) decreasing *) (* ``` *) @@ -23,10 +21,6 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* ## About sequences of real numbers *) (* ``` *) (* [sequence u_n]_n == the sequence of general element u_n *) -(* R ^nat == notation for the type of sequences, i.e., *) -(* functions of type nat -> R *) -(* seqDU F == sequence F_0, F_1 \ F_0, F_2 \ (F_0 U F_1),... *) -(* seqD F == the sequence F_0, F_1 \ F_0, F_2 \ F_1,... *) (* series u_ == the sequence of partial sums of u_ *) (* telescope u_ := [sequence u_ n.+1 - u_ n]_n *) (* harmonic == harmonic sequence *) @@ -160,7 +154,6 @@ Reserved Notation "\sum_ ( i ' R. Definition mk_sequence R f : sequence R := f. Arguments mk_sequence R f /. Notation "[ 'sequence' E ]_ n" := (mk_sequence (fun n => E%E)) : ereal_scope. @@ -258,17 +251,6 @@ Section seqDU. Variables (T : Type). Implicit Types F : (set T)^nat. -Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k. - -Lemma trivIset_seqDU F : trivIset setT (seqDU F). -Proof. -move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. - by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB ->. -move=> /set0P; apply: contraNeq => _; apply/eqP. -rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=. -by rewrite setCU setIAC !setIA setICl !set0I. -Qed. - Lemma bigsetU_seqDU F n : \big[setU/set0]_(k < n) F k = \big[setU/set0]_(k < n) seqDU F k. Proof. @@ -281,21 +263,6 @@ rewrite !big_ord_recr /= predeqE => t; split=> [[Ft|Fnt]|[Ft|[Fnt Ft]]]. - by right. Qed. -Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k. -Proof. -rewrite /seqDU predeqE => t; split=> [[n _ Fnt]|[n _]]; last first. - by rewrite setDE => -[? _]; exists n. -have [UFnt|UFnt] := pselect ((\big[setU/set0]_(k < n) F k) t); last by exists n. -suff [m [Fmt FNmt]] : exists m, F m t /\ forall k, (k < m)%N -> ~ F k t. - by exists m => //; split => //; rewrite -bigcup_mkord => -[k kj]; exact: FNmt. -move: UFnt; rewrite -bigcup_mkord => -[/= k _ Fkt] {Fnt n}. -have [n kn] := ubnP k; elim: n => // n ih in t k Fkt kn *. -case: k => [|k] in Fkt kn *; first by exists O. -have [?|] := pselect (forall m, (m <= k)%N -> ~ F m t); first by exists k.+1. -move=> /existsNP[i] /not_implyP[ik] /contrapT Fit; apply: (ih t i) => //. -by rewrite (leq_ltn_trans ik). -Qed. - Lemma seqDUIE (S : set T) (F : (set T)^nat) : seqDU (fun n => S `&` F n) = (fun n => S `&` F n `\` \bigcup_(i < n) F i). Proof. @@ -316,18 +283,6 @@ Section seqD. Variable T : Type. Implicit Types F : (set T) ^nat. -Definition seqD F := fun n => if n isn't n'.+1 then F O else F n `\` F n'. - -Lemma seqDU_seqD F : nondecreasing_seq F -> seqDU F = seqD F. -Proof. -move=> ndF; rewrite funeqE => -[|n] /=; first by rewrite /seqDU big_ord0 setD0. -rewrite /seqDU big_ord_recr /= setUC; congr (_ `\` _); apply/setUidPl. -by rewrite -bigcup_mkord => + [k /= kn]; exact/subsetPset/ndF/ltnW. -Qed. - -Lemma trivIset_seqD F : nondecreasing_seq F -> trivIset setT (seqD F). -Proof. by move=> ndF; rewrite -seqDU_seqD //; exact: trivIset_seqDU. Qed. - Lemma bigsetU_seqD F n : \big[setU/set0]_(i < n) F i = \big[setU/set0]_(i < n) seqD F i. Proof. @@ -360,15 +315,6 @@ move=> ndF; elim: n => [|n ih]; rewrite funeqE => x; rewrite propeqE; split. by rewrite big_ord_recr /=; right. Qed. -Lemma eq_bigcup_seqD F : \bigcup_n seqD F n = \bigcup_n F n. -Proof. -apply/seteqP; split => [x []|x []]. - by elim=> [_ /= F0x|n ih _ /= [Fn1x Fnx]]; [exists O | exists n.+1]. -elim=> [_ F0x|n ih _ Fn1x]; first by exists O. -have [|Fnx] := pselect (F n x); last by exists n.+1. -by move=> /(ih I)[m _ Fmx]; exists m. -Qed. - Lemma eq_bigcup_seqD_bigsetU F : \bigcup_n (seqD (fun n => \big[setU/set0]_(i < n.+1) F i) n) = \bigcup_n F n. Proof. @@ -378,14 +324,6 @@ rewrite eqEsubset; split => [t [i _]|t [i _ Fit]]. by exists i => //; rewrite big_ord_recr /=; right. Qed. -Lemma bigcup_bigsetU_bigcup F : - \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. -Proof. -apply/seteqP; split=> [x [i _]|x [i _ Fix]]. - by rewrite -bigcup_mkord => -[j _ Fjx]; exists j. -by exists i => //; rewrite big_ord_recr/=; right. -Qed. - End seqD. Lemma seqDUE {R : realDomainType} n (r : R) :