Skip to content

factorize code about powerset sigma-algebras #1438

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

Merged
CohenCyril merged 1 commit into from
Dec 18, 2024
Merged

factorize code about powerset sigma-algebras #1438

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 4 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,10 @@
- in `lebesgue_measure.v`:
+ lemma `measurable_powRr`

- in `measure.v`:
+ definition `discrete_measurable`
+ lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU`

### Changed

- in `lebesgue_integrale.v`
Expand Down
75 changes: 19 additions & 56 deletions theories/measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,12 +45,7 @@ From HB Require Import structures.
(* *)
(* ## Instances of mathematical structures *)
(* ``` *)
(* discrete_measurable_unit == the measurableType corresponding to *)
(* [set: set unit] *)
(* discrete_measurable_bool == the measurableType corresponding to *)
(* [set: set bool] *)
(* discrete_measurable_nat == the measurableType corresponding to *)
(* [set: set nat] *)
(* discrete_measurable T == alias for the sigma-algebra [set: set T] *)
(* setring G == the set of sets G contains the empty set, is *)
(* closed by union, and difference (it is a ring *)
(* of sets in the sense of ringOfSetsType) *)
Expand Down Expand Up @@ -1420,67 +1415,35 @@ Qed.

End measurable_lemmas.

Section discrete_measurable_unit.

Definition discrete_measurable_unit : set (set unit) := [set: set unit].
Section discrete_measurable.
Context {T : Type}.

Let discrete_measurable0 : discrete_measurable_unit set0. Proof. by []. Qed.
Definition discrete_measurable : set (set T) := [set: set T].

Let discrete_measurableC X :
discrete_measurable_unit X -> discrete_measurable_unit (~` X).
Proof. by []. Qed.
Lemma discrete_measurable0 : discrete_measurable set0. Proof. by []. Qed.

Let discrete_measurableU (F : (set unit)^nat) :
(forall i, discrete_measurable_unit (F i)) ->
discrete_measurable_unit (\bigcup_i F i).
Lemma discrete_measurableC X :
discrete_measurable X -> discrete_measurable (~` X).
Proof. by []. Qed.

HB.instance Definition _ := @isMeasurable.Build default_measure_display unit
discrete_measurable_unit discrete_measurable0
discrete_measurableC discrete_measurableU.

End discrete_measurable_unit.

Section discrete_measurable_bool.

Definition discrete_measurable_bool : set (set bool) := [set: set bool].

Let discrete_measurable0 : discrete_measurable_bool set0. Proof. by []. Qed.

Let discrete_measurableC X :
discrete_measurable_bool X -> discrete_measurable_bool (~` X).
Lemma discrete_measurableU (F : (set T)^nat) :
(forall i, discrete_measurable (F i)) ->
discrete_measurable (\bigcup_i F i).
Proof. by []. Qed.

Let discrete_measurableU (F : (set bool)^nat) :
(forall i, discrete_measurable_bool (F i)) ->
discrete_measurable_bool (\bigcup_i F i).
Proof. by []. Qed.
End discrete_measurable.

HB.instance Definition _ := @isMeasurable.Build default_measure_display bool
discrete_measurable_bool discrete_measurable0
HB.instance Definition _ := @isMeasurable.Build default_measure_display
unit discrete_measurable discrete_measurable0
discrete_measurableC discrete_measurableU.

End discrete_measurable_bool.

Section discrete_measurable_nat.

Definition discrete_measurable_nat : set (set nat) := [set: set nat].

Let discrete_measurable_nat0 : discrete_measurable_nat set0. Proof. by []. Qed.

Let discrete_measurable_natC X :
discrete_measurable_nat X -> discrete_measurable_nat (~` X).
Proof. by []. Qed.

Let discrete_measurable_natU (F : (set nat)^nat) :
(forall i, discrete_measurable_nat (F i)) ->
discrete_measurable_nat (\bigcup_i F i).
Proof. by []. Qed.

HB.instance Definition _ := isMeasurable.Build default_measure_display nat
discrete_measurable_nat0 discrete_measurable_natC discrete_measurable_natU.
HB.instance Definition _ := @isMeasurable.Build default_measure_display
bool discrete_measurable discrete_measurable0
discrete_measurableC discrete_measurableU.

End discrete_measurable_nat.
HB.instance Definition _ := @isMeasurable.Build default_measure_display
nat discrete_measurable discrete_measurable0
discrete_measurableC discrete_measurableU.

Definition sigma_display {T} : set (set T) -> measure_display.
Proof. exact. Qed.
Expand Down