Skip to content

reduce dependencies in measurable_structure.v #1979

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
affeldt-aist wants to merge 6 commits into
base: master
Choose a base branch
from
Open

reduce dependencies in measurable_structure.v #1979

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
81c4453
reduce dependencies in measurable_structure.v
affeldt-aist May 27, 2026
23b3340
fix dup
affeldt-aist May 27, 2026
6fbaccd
fix changelog
affeldt-aist Jun 16, 2026
205aeea
fix changelog
affeldt-aist Jun 16, 2026
b7e27ba
fix
affeldt-aist Jun 16, 2026
f902df9
fix
affeldt-aist Jun 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 14 additions & 10 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down Expand Up @@ -226,6 +216,20 @@
`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`:
+ 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`

### Renamed

- in `tvs.v`:
Expand Down
211 changes: 143 additions & 68 deletions classical/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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**************************************************************************)
Expand Down Expand Up @@ -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) *)
Expand Down Expand Up @@ -146,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 *)
Expand Down Expand Up @@ -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.

@hoheinzollern hoheinzollern Jun 22, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why is this notation introduced here? isn't it part of mathcomp already?


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 /.

Expand All @@ -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 /.

Expand All @@ -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]]];
Expand Down Expand Up @@ -2310,78 +2323,24 @@ 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.
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.

@t6s t6s Jun 22, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

not about this PR itself, but why do lemmas around here have .+1 in the indexing for finite parts?

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.
Expand Down Expand Up @@ -2467,6 +2426,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).
Expand Down Expand Up @@ -2925,7 +2946,6 @@ 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).

Expand Down Expand Up @@ -3322,6 +3342,61 @@ End Exports.
End SetOrder.
Export SetOrder.Exports.

Section seqD.
Variable 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.

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).
Expand Down
7 changes: 7 additions & 0 deletions classical/unstable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}} \/ *)
Expand Down Expand Up @@ -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}}.
Expand Down
8 changes: 0 additions & 8 deletions theories/measure_theory/measurable_structure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ereal topology normedtype sequences.

(**md**************************************************************************)
(* # Measure Theory *)
Expand Down Expand Up @@ -98,8 +97,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 *)
Expand Down Expand Up @@ -1418,11 +1415,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 <oo) mu (F n))%E.

Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R)
(op : Monoid.com_law idx) (A : I -> set T) (F : set T -> R) :
finite_set D -> trivIset D A -> F set0 = idx ->
Expand Down
6 changes: 6 additions & 0 deletions theories/measure_theory/measure_function.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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 <oo) mu (F n))%E.

Definition measurable_subset_sigma_subadditive :=
forall (A : set T) (F : nat -> set T),
(forall n, measurable (F n)) -> measurable A ->
Expand Down
Loading
Loading