From 81c445343c5349908f0d67bf223860d332608db9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 May 2026 18:25:26 +0900 Subject: [PATCH 1/6] 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 dd71a6733a..1c86c500c6 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 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 *) @@ -98,8 +98,6 @@ From mathcomp Require Import ereal topology normedtype sequences. (* This is an HB alias. *) (* f.-preimage.-measurable A == A is measurable for *) (* g_sigma_algebra_preimage f *) -(* subset_sigma_subadditive mu == alternative predicate defining *) -(* sigma-subadditivity *) (* ``` *) (* *) (* ## Product of measurable spaces *) @@ -155,6 +153,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)). @@ -1418,11 +1493,6 @@ Qed. End measurability. -(** 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 f08d2972f6..7925364a94 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 23b334066f0e2514a7950a6f77562d821fc23e2a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 May 2026 19:13:03 +0900 Subject: [PATCH 2/6] 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 b166a3fd0a..c2ae84d78b 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -3499,3 +3499,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 1c86c500c6..9512b6b6d9 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 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 *) @@ -153,83 +152,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) : From 6fbaccd89a82297e7d49a7a05be0256d227ebe35 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 16 Jun 2026 19:43:25 +0900 Subject: [PATCH 3/6] fix changelog --- CHANGELOG_UNRELEASED.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0023dbb5e0..f806d65e14 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -131,16 +131,6 @@ - in `lebesgue_stieltjes_measure.v`: + definition `lebesgue_display` -### 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`, - `preimage_set_system_id` -- in `functions.v`: - + lemmas `linfunP`, `linfun_eqP` - + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }` - - in `tvs.v`: + structure `LinearContinuous` + factory `isLinearContinuous` @@ -226,6 +216,16 @@ `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`, `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule` +- moved from `measurable_structure.v` to `measure_function.v`: + + definition `subset_sigma_subadditive` + +- moved from `measurable_structure.v` to `unstable.v`: + + defintion `sequence` + + defintion `seqDU` + + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` + + definition `seqD` + + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, ``bigcup_bigsetU_bigcup` + ### Renamed - in `tvs.v`: From 205aeea3b3d08ee9c986552a7db56631cf3d2b85 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 16 Jun 2026 20:05:40 +0900 Subject: [PATCH 4/6] fix changelog --- CHANGELOG_UNRELEASED.md | 3 + classical/classical_sets.v | 297 ++++++++++++++++++------------------- classical/unstable.v | 7 + 3 files changed, 153 insertions(+), 154 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f806d65e14..647a026088 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -220,6 +220,9 @@ + definition `subset_sigma_subadditive` - moved from `measurable_structure.v` to `unstable.v`: + + notations `nondecreasing_seq`, `nonincreasing_seq` + +- moved from `measurable_structure.v` to `classical_sets.v`: + defintion `sequence` + defintion `seqDU` + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index c2ae84d78b..669de6ba49 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1,7 +1,9 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg matrix finmap ssrnum. From mathcomp Require Import ssrint rat interval. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp wochoice. (**md**************************************************************************) @@ -116,6 +118,11 @@ From mathcomp Require Import mathcomp_extra boolp wochoice. (* ``` *) (* *) (* ``` *) +(* *) +(* R ^nat == notation for the type of sequences, i.e., *) +(* functions of type nat -> R *) +(* bigcup2 A B == the sequence A, B, 0, 0, ... *) +(* bigcup2 A B == the sequence A, B, T, T, ... *) (* smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A *) (* A `<=` B <-> A is included in B *) (* A `<` B := A `<=` B /\ ~ (B `<=` A) *) @@ -180,6 +187,8 @@ From mathcomp Require Import mathcomp_extra boolp wochoice. (* D : set I, form a partition of A *) (* pblock_index D F x == index i such that i \in D and x \in F i *) (* pblock D F x := F (pblock_index D F x) *) +(* 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,... *) (* *) (* maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) *) (* disjoint subcollection of the collection *) @@ -2181,7 +2190,11 @@ move=> Pj; apply/seteqP; split => [t [Fjt UFt] i Pi|t UFt]. by split=> [|[k [Pk kj]] [Fjt]]; [|apply]; exact: UFt. Qed. -Definition bigcup2 T (A B : set T) : nat -> set T := +Definition sequence R := nat -> R. + +Notation "R ^nat" := (sequence R) : type_scope. + +Definition bigcup2 T (A B : set T) : (set T)^nat := fun i => if i == 0 then A else if i == 1 then B else set0. Arguments bigcup2 T A B n /. @@ -2197,7 +2210,7 @@ rewrite predeqE => t; split=> [|[At|Bt]]; [|by exists 0|by exists 1]. by case=> -[_ At|[_ Bt|//]]; [left|right]. Qed. -Definition bigcap2 T (A B : set T) : nat -> set T := +Definition bigcap2 T (A B : set T) : (set T)^nat := fun i => if i == 0 then A else if i == 1 then B else setT. Arguments bigcap2 T A B n /. @@ -2213,7 +2226,7 @@ apply: setC_inj; rewrite setC_bigcap setCI -bigcup2inE /bigcap2 /bigcup2. by apply: eq_bigcupr => // -[|[|[]]]. Qed. -Lemma bigcup_recl T (F : nat -> set T) : +Lemma bigcup_recl T (F : (set T)^nat) : \bigcup_n F n = F 0%N `|` \bigcup_(n in ~` `I_1) F n. Proof. by apply/seteqP; split => [t [[_ F0t|n _ Fnt]]|t [F0t|[n /= n0 Fnt]]]; @@ -2310,71 +2323,9 @@ Proof. by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed. End bigcup_seq. -Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) : - \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t. -Proof. -apply/predeqP => u; split=> [[x Px fxu]|]; first by rewrite (bigD1 x)//; left. -move=> /mem_set; rewrite (@big_morph _ _ (fun X => u \in X) false orb). -- by move=> /= x y; apply/idP/orP; rewrite !inE. -- by rewrite in_set0. -- by rewrite big_has_cond => /hasP[x _ /andP[xP]]; rewrite inE => ufx; exists x. -Qed. - -Section smallest. -Context {T} (C : set T -> Prop). - -Definition smallest (G : set T) := \bigcap_(A in [set M | C M /\ G `<=` M]) A. - -Lemma smallest_sub G X : C X -> G `<=` X -> smallest G `<=` X. -Proof. by move=> XC GX A; apply. Qed. - -Lemma smallest_sub_sub G X : smallest G `<=` X -> G `<=` X. -Proof. by apply: subset_trans => t Gt B [CB]; exact. Qed. - -Lemma sub_smallest G X : X `<=` G -> X `<=` smallest G. -Proof. by move=> XG A /XG GA Y /= [PY]; exact. Qed. - -Lemma sub_gen_smallest G : G `<=` smallest G. Proof. exact: sub_smallest. Qed. - -Lemma smallest_id G : C G -> smallest G = G. -Proof. -by move=> Cs; apply/seteqP; split; [exact: smallest_sub|exact: sub_smallest]. -Qed. - -End smallest. -#[global] Hint Resolve sub_gen_smallest : core. - -Lemma smallest_sub_iff {T} (C : set T -> Prop) (X Y : set T) : - C Y -> smallest C X `<=` Y <-> X `<=` Y. -Proof. -by move=> CY; split; [exact: smallest_sub_sub|exact: smallest_sub]. -Qed. - -Definition bigcap_closed {T} (C : set T -> Prop) := - forall (MM : set_system T), MM `<=` C -> C (\bigcap_(A in MM) A). - -Section bigcap_closed_smallest. -Context {T} (C : set T -> Prop). - -Lemma bigcap_closed_smallest (G : set T) : bigcap_closed C -> C (smallest C G). -Proof. by apply; exact: subIsetl. Qed. - -End bigcap_closed_smallest. - -Lemma sub_smallest2r {T} (C : set T -> Prop) G1 G2 : - C (smallest C G2) -> G1 `<=` G2 -> smallest C G1 `<=` smallest C G2. -Proof. -by move=> CCG2 G12; apply: smallest_sub => //; exact: sub_smallest. -Qed. - -Lemma sub_smallest2l {T} (C1 C2 : set T -> Prop) : - (forall G, C2 G -> C1 G) -> - forall G, smallest C1 G `<=` smallest C2 G. -Proof. by move=> C12 G X sX M [/C12 C1M GM]; exact: sX. Qed. - Section bigop_nat_lemmas. Context {T : Type}. -Implicit Types (A : set T) (F : nat -> set T). +Implicit Types (A : set T) (F : (set T)^nat). Lemma bigcup_mkord n F : \bigcup_(i < n) F i = \big[setU/set0]_(i < n) F i. Proof. @@ -2467,6 +2418,68 @@ Qed. End bigop_nat_lemmas. +Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) : + \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t. +Proof. +apply/predeqP => u; split=> [[x Px fxu]|]; first by rewrite (bigD1 x)//; left. +move=> /mem_set; rewrite (@big_morph _ _ (fun X => u \in X) false orb). +- by move=> /= x y; apply/idP/orP; rewrite !inE. +- by rewrite in_set0. +- by rewrite big_has_cond => /hasP[x _ /andP[xP]]; rewrite inE => ufx; exists x. +Qed. + +Section smallest. +Context {T} (C : set T -> Prop). + +Definition smallest (G : set T) := \bigcap_(A in [set M | C M /\ G `<=` M]) A. + +Lemma smallest_sub G X : C X -> G `<=` X -> smallest G `<=` X. +Proof. by move=> XC GX A; apply. Qed. + +Lemma smallest_sub_sub G X : smallest G `<=` X -> G `<=` X. +Proof. by apply: subset_trans => t Gt B [CB]; exact. Qed. + +Lemma sub_smallest G X : X `<=` G -> X `<=` smallest G. +Proof. by move=> XG A /XG GA Y /= [PY]; exact. Qed. + +Lemma sub_gen_smallest G : G `<=` smallest G. Proof. exact: sub_smallest. Qed. + +Lemma smallest_id G : C G -> smallest G = G. +Proof. +by move=> Cs; apply/seteqP; split; [exact: smallest_sub|exact: sub_smallest]. +Qed. + +End smallest. +#[global] Hint Resolve sub_gen_smallest : core. + +Lemma smallest_sub_iff {T} (C : set T -> Prop) (X Y : set T) : + C Y -> smallest C X `<=` Y <-> X `<=` Y. +Proof. +by move=> CY; split; [exact: smallest_sub_sub|exact: smallest_sub]. +Qed. + +Definition bigcap_closed {T} (C : set T -> Prop) := + forall (MM : set_system T), MM `<=` C -> C (\bigcap_(A in MM) A). + +Section bigcap_closed_smallest. +Context {T} (C : set T -> Prop). + +Lemma bigcap_closed_smallest (G : set T) : bigcap_closed C -> C (smallest C G). +Proof. by apply; exact: subIsetl. Qed. + +End bigcap_closed_smallest. + +Lemma sub_smallest2r {T} (C : set T -> Prop) G1 G2 : + C (smallest C G2) -> G1 `<=` G2 -> smallest C G1 `<=` smallest C G2. +Proof. +by move=> CCG2 G12; apply: smallest_sub => //; exact: sub_smallest. +Qed. + +Lemma sub_smallest2l {T} (C1 C2 : set T -> Prop) : + (forall G, C2 G -> C1 G) -> + forall G, smallest C1 G `<=` smallest C2 G. +Proof. by move=> C12 G X sX M [/C12 C1M GM]; exact: sX. Qed. + Definition is_subset1 {T} (A : set T) := forall x y, A x -> A y -> x = y. Definition is_fun {T1 T2} (f : T1 -> T2 -> Prop) := Logic.all (is_subset1 \o f). Definition is_total {T1 T2} (f : T1 -> T2 -> Prop) := Logic.all (nonempty \o f). @@ -2925,10 +2938,72 @@ rewrite (nth_map O)// ts1 ?(nth_uniq,(perm_uniq ss1),iota_uniq)//; apply/s1D. Qed. End partitions. - #[deprecated(note="Use trivIset_setIl instead")] Notation trivIset_setI := trivIset_setIl (only parsing). +Section seqD. +Variable T : Type. +Implicit Types F : (set T)^nat. + +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. + Section Zorn. Definition total_on T (A : set T) (R : T -> T -> Prop) := @@ -3499,89 +3574,3 @@ 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/classical/unstable.v b/classical/unstable.v index cf8b4ce04a..527eb71528 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -16,6 +16,8 @@ From mathcomp Require Import vector archimedean interval. (* ``` *) (* swap x := (x.2, x.1) *) (* map_pair f x := (f x.1, f x.2) *) +(* nondecreasing_seq u == the sequence u is non-decreasing *) +(* nonincreasing_seq u == the sequence u is non-increasing *) (* monotonic A f := {in A &, {homo f : x y / x <= y}} \/ *) (* {in A &, {homo f : x y /~ x <= y}} *) (* strict_monotonic A f := {in A &, {homo f : x y / x < y}} \/ *) @@ -197,6 +199,11 @@ rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r. by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l. Qed. +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 monotonic d (T : porderType d) d' (T' : porderType d') (pT : predType T) (A : pT) (f : T -> T') := {in A &, nondecreasing f} \/ {in A &, {homo f : x y /~ (x <= y)%O}}. From b7e27ba647c8ae936c7efc33231a626247548132 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 16 Jun 2026 20:23:15 +0900 Subject: [PATCH 5/6] fix --- classical/classical_sets.v | 130 ++++++++++++++++++------------------- 1 file changed, 65 insertions(+), 65 deletions(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 669de6ba49..a9c1555e3f 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -153,6 +153,8 @@ From mathcomp Require Import mathcomp_extra boolp wochoice. (* if there is one, to f0 x otherwise *) (* F `#` G <-> intersections beween elements of F an G are *) (* all non empty *) +(* 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,... *) (* ``` *) (* *) (* ## Pointed types *) @@ -187,8 +189,6 @@ From mathcomp Require Import mathcomp_extra boolp wochoice. (* D : set I, form a partition of A *) (* pblock_index D F x == index i such that i \in D and x \in F i *) (* pblock D F x := F (pblock_index D F x) *) -(* 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,... *) (* *) (* maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) *) (* disjoint subcollection of the collection *) @@ -2941,69 +2941,6 @@ End partitions. #[deprecated(note="Use trivIset_setIl instead")] Notation trivIset_setI := trivIset_setIl (only parsing). -Section seqD. -Variable T : Type. -Implicit Types F : (set T)^nat. - -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. - Section Zorn. Definition total_on T (A : set T) (R : T -> T -> Prop) := @@ -3397,6 +3334,69 @@ End Exports. End SetOrder. Export SetOrder.Exports. +Section seqD. +Variable T : Type. +Implicit Types F : (set T)^nat. + +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. + Section product. Variables (T1 T2 : Type). Implicit Type A B : set (T1 * T2). From f902df981bf20e7d650e700e77034824ae46419a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 16 Jun 2026 21:21:25 +0900 Subject: [PATCH 6/6] fix --- CHANGELOG_UNRELEASED.md | 3 ++- classical/classical_sets.v | 16 ++++++++-------- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 647a026088..743cbdb092 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -223,11 +223,12 @@ + notations `nondecreasing_seq`, `nonincreasing_seq` - moved from `measurable_structure.v` to `classical_sets.v`: + + notation `^nat` + defintion `sequence` + defintion `seqDU` + lemmas `seqDU_bigcup_eq`, `trivIset_seqDU` + definition `seqD` - + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, ``bigcup_bigsetU_bigcup` + + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup` ### Renamed diff --git a/classical/classical_sets.v b/classical/classical_sets.v index a9c1555e3f..2b8643c465 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2333,6 +2333,14 @@ rewrite -(big_mkord xpredT F) -bigcup_seq. by apply: eq_bigcupl; split=> i; rewrite /= mem_index_iota leq0n. 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. + Lemma bigcup_mkord_ord n (G : 'I_n.+1 -> set T) : \bigcup_(i < n.+1) G (inord i) = \big[setU/set0]_(i < n.+1) G i. Proof. @@ -3338,14 +3346,6 @@ Section seqD. Variable T : Type. Implicit Types F : (set T)^nat. -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).