Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect all_algebra finmap.Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.Pred.subring_smul;
GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From mathcomp.classical Require Import boolp classical_sets functions.
From mathcomp.classical Require Import cardinality fsbigop mathcomp_extra.
Require Import reals ereal signed topology normedtype sequences esum numfun.
From HB Require Import structures.
(******************************************************************************)
(* Measure Theory *)
(* *)
(* This files provides a formalization of the basics of measure theory. This *)
(* includes the formalization of mathematical structures for measure theory *)
(* and of measures, as well as standard theorems such as the Boole *)
(* inequality, Caratheodory's theorem, the Hahn extension, etc. *)
(* *)
(* Main references: *)
(* - Daniel Li, Intégration et applications, 2016 *)
(* - Achim Klenke, Probability Theory 2nd edition, 2014 *)
(* *)
(* setI_closed G == the set of sets G is closed under finite *)
(* intersection *)
(* setU_closed G == the set of sets G is closed under finite union *)
(* setC_closed G == the set of sets G is closed under complement *)
(* setD_closed G == the set of sets G is closed under difference *)
(* ndseq_closed G == the set of sets G is closed under non-decreasing *)
(* countable union *)
(* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *)
(* countable union *)
(* *)
(* setring G == the set of sets G contains the empty set, is *)
(* closed by union, and difference *)
(* <<r G >> := smallest setring G *)
(* sigma_algebra D G == the set of sets G forms a sigma algebra on D *)
(* <<s D, G >> == sigma-algebra generated by G on D *)
(* := smallest (sigma_algebra D) G *)
(* <<s G >> := <<s setT, G >> *)
(* monotone_class D G == G is a monotone class of subsets of D *)
(* <<m D, G >> == monotone class generated by G on D *)
(* <<m G >> := <<m setT, G >> *)
(* dynkin G == G is a set of sets that form a Dynkin *)
(* (or a lambda) system *)
(* <<d G >> == Dynkin system generated by G, i.e., *)
(* smallest dynkin G *)
(* *)
(* * Mathematical structures for measure theory: *)
(* semiRingOfSetsType == the type of semirings of sets; *)
(* the carrier is a set of sets A such that *)
(* "measurable A" holds; *)
(* "measurable A" is printed as "d.-measurable A" *)
(* where d is a "display parameter" whose purpose *)
(* is to distinguish different measurable's within *)
(* the same context *)
(* ringOfSetsType == the type of rings of sets *)
(* <<r G >> is equipped with a canonical structure *)
(* of ring of sets *)
(* G.-ring.-measurable A == A is measurable for the ring of sets <<r G >> *)
(* algebraOfSetsType == the type of algebras of sets *)
(* measurableType == the type of sigma-algebras *)
(* <<s G >> is equipped with a canonical structure *)
(* of measurableType *)
(* G.-sigma.-measurable A == A is measurable for the sigma-algebra <<s G >> *)
(* *)
(* 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] *)
(* salgebraType G == the measurableType corresponding to <<s G >> *)
(* *)
(* measurable_fun D f == the function f with domain D is measurable *)
(* preimage_class D f G == class of the preimages by f of sets in G *)
(* image_class D f G == class of the sets with a preimage by f in G *)
(* *)
(* * Measures: *)
(* {content set T -> \bar R} == type of a function over sets of elements of *)
(* type T where R is expected to be a numFieldType such *)
(* that this function maps set0 to 0, is non-negative over *)
(* measurable sets, and is semi-additive *)
(* isContent == corresponding mixin *)
(* Content == corresponding structure *)
(* {measure set T -> \bar R} == type of a function over sets of elements *)
(* of type T where R is expected to be a numFieldType such *)
(* that this function maps set0 to 0, is non-negative over *)
(* measurable sets and is semi-sigma-additive *)
(* isMeasure0 == mixin that extends a content to a measure with the proof *)
(* that it is semi_sigma_additive *)
(* isMeasure == factory corresponding to the type of measures *)
(* Measure == structure corresponding to measures *)
(* finite_measure mu == the measure mu is finite *)
(* {sigma_finite_content set T -> \bar R} == contents that are also sigma *)
(* finite *)
(* {sigma_finite_measure set T -> \bar R} == *)
(* measures that are also sigma finite *)
(* isSigmaFinite == factory corresponding to sigma finiteness *)
(* *)
(* pushforward mf m == pushforward/image measure of m by f, where mf is a *)
(* proof that f is measurable *)
(* \d_a == Dirac measure *)
(* msum mu n == the measure corresponding to the sum of the measures *)
(* mu_0, ..., mu_{n-1} *)
(* @mzero T R == the zero measure *)
(* measure_add m1 m2 == the measure corresponding to the sum of the *)
(* measures m1 and m2 *)
(* mscale r m == the measure of corresponding to fun A => r * m A *)
(* where r has type {nonneg R} *)
(* mseries mu n == the measure corresponding to the sum of the *)
(* measures mu_n, mu_{n+1}, ... *)
(* mrestr mu mD == restriction of the measure mu to a set D; mD is a *)
(* proof that D is measurable *)
(* counting T R == counting measure *)
(* *)
(* sigma_finite A f == the measure f is sigma-finite on A : set T with *)
(* T : ringOfSetsType. *)
(* mu.-negligible A == A is mu negligible *)
(* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu *)
(* *)
(* {outer_measure set T -> \bar R} == type of an outer measure over sets *)
(* of elements of type T where R is expected to be a *)
(* numFieldType *)
(* isOuterMeasure == corresponding mixin *)
(* OuterMeasure == corresponding structure *)
(* mu.-measurable A == A is Caratheodory measurable for the outer measure *)
(* mu, i.e., *)
(* forall B, mu A = mu (A `&` B) + mu (A `&` ~` B) *)
(* measure_is_complete mu == the measure mu is complete *)
(* *)
(* * Caratheodory theorem (from an outer measure to a measure): *)
(* caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R} *)
(* it is a canonical mesurableType copy of T *)
(* the restriction of the outer measure mu to the *)
(* sigma algebra of Caratheodory measurable sets is a *)
(* measure *)
(* Remark: sets that are negligible for *)
(* this measure are Caratheodory measurable *)
(* *)
(* * Caratheodory theorem (from a premeasure to an outer measure): *)
(* measurable_cover X == the set of sequences F such that *)
(* - forall k, F k is measurable *)
(* - X `<=` \bigcup_k (F k) *)
(* mu^* == extension of the measure mu over a semiring of *)
(* sets; it is an outer measure, declared as; we have *)
(* the notation [the outer_measure of mu^*]) *)
(* *)
(* * Hahn Extension: *)
(* Hahn_ext mu == extension of the content mu over a semiring of *)
(* sets to a measure over the generated sigma algebra *)
(* (requires a proof of sigma-sub-additivity) *)
(* *)
(* * Product of measurable spaces: *)
(* preimage_classes f1 f2 == sigma-algebra generated by the union of the *)
(* preimages by f1 and the preimages by f2 with *)
(* f1 : T -> T1 and f : T -> T2, T1 and T2 being *)
(* measurableType's *)
(* (d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra *)
(* generated from T1 x T2, with T1 and T2 *)
(* measurableType's with resp. display d1 and d2 *)
(* *)
(* probability T R == probability measure over the measurableType T with *)
(* value in R : realType *)
(******************************************************************************)
Set Implicit Arguments .
Unset Strict Implicit .
Unset Printing Implicit Defensive .
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Reserved Notation "'s<|' D , G '|>'" (at level 40 , G, D at next level ).
Reserved Notation "'s<<' A '>>'" .
Reserved Notation "'d<<' D '>>'" .
Reserved Notation "mu .-negligible" (at level 2 , format "mu .-negligible" ).
Reserved Notation "{ 'ae' m , P }" (at level 0 , format "{ 'ae' m , P }" ).
Reserved Notation "mu .-measurable" (at level 2 , format "mu .-measurable" ).
Reserved Notation "'\d_' a" (at level 8 , a at level 2 , format "'\d_' a" ).
Reserved Notation "G .-sigma" (at level 1 , format "G .-sigma" ).
Reserved Notation "G .-sigma.-measurable"
(at level 2 , format "G .-sigma.-measurable" ).
Reserved Notation "d .-ring" (at level 1 , format "d .-ring" ).
Reserved Notation "d .-ring.-measurable"
(at level 2 , format "d .-ring.-measurable" ).
Reserved Notation "mu .-cara" (at level 1 , format "mu .-cara" ).
Reserved Notation "mu .-cara.-measurable"
(at level 2 , format "mu .-cara.-measurable" ).
Reserved Notation "mu .-caratheodory"
(at level 2 , format "mu .-caratheodory" ).
Reserved Notation "'<<m' D , G '>>'"
(at level 2 , format "'<<m' D , G '>>'" ).
Reserved Notation "'<<m' G '>>'"
(at level 2 , format "'<<m' G '>>'" ).
Reserved Notation "'<<d' G '>>'"
(at level 2 , format "'<<d' G '>>'" ).
Reserved Notation "'<<s' D , G '>>'"
(at level 2 , format "'<<s' D , G '>>'" ).
Reserved Notation "'<<s' G '>>'"
(at level 2 , format "'<<s' G '>>'" ).
Reserved Notation "'<<r' G '>>'"
(at level 2 , format "'<<r' G '>>'" ).
Reserved Notation "{ 'content' fUV }" (at level 0 , format "{ 'content' fUV }" ).
Reserved Notation "[ 'content' 'of' f 'as' g ]"
(at level 0 , format "[ 'content' 'of' f 'as' g ]" ).
Reserved Notation "[ 'content' 'of' f ]"
(at level 0 , format "[ 'content' 'of' f ]" ).
Reserved Notation "{ 'measure' fUV }"
(at level 0 , format "{ 'measure' fUV }" ).
Reserved Notation "[ 'measure' 'of' f 'as' g ]"
(at level 0 , format "[ 'measure' 'of' f 'as' g ]" ).
Reserved Notation "[ 'measure' 'of' f ]"
(at level 0 , format "[ 'measure' 'of' f ]" ).
Reserved Notation "{ 'outer_measure' fUV }"
(at level 0 , format "{ 'outer_measure' fUV }" ).
Reserved Notation "[ 'outer_measure' 'of' f 'as' g ]"
(at level 0 , format "[ 'outer_measure' 'of' f 'as' g ]" ).
Reserved Notation "[ 'outer_measure' 'of' f ]"
(at level 0 , format "[ 'outer_measure' 'of' f ]" ).
Reserved Notation "p .-prod" (at level 1 , format "p .-prod" ).
Reserved Notation "p .-prod.-measurable"
(at level 2 , format "p .-prod.-measurable" ).
Inductive measure_display := default_measure_display.
Declare Scope measure_display_scope.
Delimit Scope measure_display_scope with mdisp.
Bind Scope measure_display_scope with measure_display.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Section classes .
Context {T } (C : set (set T) -> Prop ) (D : set T) (G : set (set T)).
Definition setC_closed := forall A , G A -> G (~` A).
Definition setI_closed := forall A B , G A -> G B -> G (A `&` B).
Definition setU_closed := forall A B , G A -> G B -> G (A `|` B).
Definition setD_closed := forall A B , B `<=` A -> G A -> G B -> G (A `\` B).
Definition setDI_closed := forall A B , G A -> G B -> G (A `\` B).
Definition fin_bigcap_closed :=
forall I (D : set I) A_ , finite_set D -> (forall i , D i -> G (A_ i)) ->
G (\bigcap_(i in D) (A_ i)).
Definition finN0_bigcap_closed :=
forall I (D : set I) A_ , finite_set D -> D !=set0 ->
(forall i , D i -> G (A_ i)) ->
G (\bigcap_(i in D) (A_ i)).
Definition fin_bigcup_closed :=
forall I (D : set I) A_ , finite_set D -> (forall i , D i -> G (A_ i)) ->
G (\bigcup_(i in D) (A_ i)).
Definition semi_setD_closed := forall A B , G A -> G B -> exists D ,
[/\ finite_set D, D `<=` G, A `\` B = \bigcup_(X in D) X & trivIset D id].
Definition ndseq_closed :=
forall F , nondecreasing_seq F -> (forall i , G (F i)) -> G (\bigcup_i (F i)).
Definition trivIset_closed :=
forall F : (set T)^nat, trivIset setT F -> (forall n , G (F n)) ->
G (\bigcup_k F k).
Definition fin_trivIset_closed :=
forall I (D : set I) (F : I -> set T), finite_set D -> trivIset D F ->
(forall i , D i -> G (F i)) -> G (\bigcup_(k in D) F k).
Definition setring := [/\ G set0, setU_closed & setDI_closed].
Definition sigma_algebra :=
[/\ G set0, (forall A , G A -> G (D `\` A)) &
(forall A : (set T)^nat, (forall n , G (A n)) -> G (\bigcup_k A k))].
Definition dynkin := [/\ G setT, setC_closed & trivIset_closed].
Definition monotone_class :=
[/\ forall A , G A -> A `<=` D, G D, setD_closed & ndseq_closed].
End classes .
Notation "'<<m' D , G '>>'" := (smallest (monotone_class D) G) :
classical_set_scope.
Notation "'<<m' G '>>'" := (<<m setT, G>>) : classical_set_scope.
Notation "'<<d' G '>>'" := (smallest dynkin G) : classical_set_scope.
Notation "'<<s' D , G '>>'" := (smallest (sigma_algebra D) G) :
classical_set_scope.
Notation "'<<s' G '>>'" := (<<s setT, G>>) : classical_set_scope.
Notation "'<<r' G '>>'" := (smallest setring G) : classical_set_scope.
Lemma fin_bigcup_closedP T (G : set (set T)) :
(G set0 /\ setU_closed G) <-> fin_bigcup_closed G.
Proof .
split => [[G0 GU] I D A DF GA|GU]; last first .
have G0 : G set0 by have := GU void set0 point; rewrite bigcup0//; apply .
by split => // A B GA GB; rewrite -bigcup2inE; apply : GU => // -[|[|[]]].
elim /Pchoice: I => I in D DF A GA *; rewrite -bigsetU_fset_set// big_seq.
by elim /big_ind: _ => // i; rewrite in_fset_set// inE => /GA.
Qed .
Lemma finN0_bigcap_closedP T (G : set (set T)) :
setI_closed G <-> finN0_bigcap_closed G.
Proof .
split => [GI I D A DF [i Di] GA|GI A B GA GB]; last first .
by rewrite -bigcap2inE; apply : GI => // [|[|[|[]]]]; first by exists 0 %N.
elim /Pchoice: I => I in D DF i Di A GA *.
have finDDi : finite_set (D `\ i) by exact : finite_setD.
rewrite (bigcap_setD1 i)// -bigsetI_fset_set// big_seq.
elim /big_rec: _ => // [|j B]; first by rewrite setIT; apply : GA.
rewrite in_fset_set// inE => -[Dj /eqP nij] GAB.
by rewrite setICA; apply : GI => //; apply : GA.
Qed .
Lemma sedDI_closedP T (G : set (set T)) :
setDI_closed G <-> (setI_closed G /\ setD_closed G).
Proof .
split => [GDI|[GI GD]].
by split => A B => [|AB] => GA GB; rewrite -?setDD //; do ?apply : (GDI).
move => A B GA GB; suff <- : A `\` (A `&` B) = A `\` B.
by apply : GD => //; apply : GI.
by rewrite setDE setCI setIUr -setDE setDv set0U.
Qed .
Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T)
(F : I -> set (set T)) (J : set I) :
(forall n , J n -> sigma_algebra D (F n)) ->
sigma_algebra D (\bigcap_(i in J) F i).
Proof .
move => mG; split => [i Ji|A AJ i Ji|H GH i Ji]; first by have [] := mG i.
- by have [_ mGiC _] := mG i Ji; exact /mGiC/AJ.
- by have [_ _ mGiU] := mG i Ji; apply : mGiU => j; exact : GH.
Qed .
Lemma sigma_algebraP T U (C : set (set T)) :
(forall X , C X -> X `<=` U) ->
sigma_algebra U C <->
[/\ C U, setD_closed C, ndseq_closed C & setI_closed C].
Proof .
move => C_subU; split => [[C0 CD CU]|[DT DC DU DI]]; split .
- by rewrite -(setD0 U); apply : CD.
- move => A B BA CA CB; rewrite (_ : A `\` B = U `\` ((U `\` A) `|` B)).
by apply CD; rewrite -bigcup2E; apply : CU => -[|[|[|]]] //=; exact : CD.
rewrite setDUr setDD [in RHS]setDE setIACA setIid -setDE setIidr//.
by rewrite setDE; apply : subIset; left ; apply : C_subU.
- by move => F ndF DF; exact : CU.
- move => A B DA DB; rewrite (_ : A `&` B = U `\` ((U `\` A) `|` (U `\` B))).
by apply CD; rewrite -bigcup2E; apply : CU => -[|[|[|]]] //; exact : CD.
rewrite setDUr !setDD setIACA setIid (@setIidr _ U)//.
by apply : subIset; left ; exact : C_subU.
- by rewrite -(setDv U); exact : DC.
- by move => A CA; apply : DC => //; exact : C_subU.
- move => F DF.
rewrite [X in C X](_ : _ = \bigcup_i \big[setU/set0]_(j < i.+1 ) F j).
apply : DU; first by move => *; exact /subsetPset/subset_bigsetU.
elim => [|n ih]; first by rewrite big_ord_recr /= big_ord0 set0U; exact : DF.
have CU : setU_closed C.
move => A B DA DB; rewrite (_ : A `|` B = U `\` ((U `\` A) `&` (U `\` B))).
apply DC => //; last by apply : DI; apply : DC => //; exact : C_subU.
by apply : subIset; left ; apply : subIset; left .
by rewrite setDIr// !setDD (setIidr (C_subU _ DA)) (setIidr (C_subU _ _)).
by rewrite big_ord_recr; exact : CU.
rewrite predeqE => x; split => [[n _ Fnx]|[n _]].
by exists n => //; rewrite big_ord_recr /=; right .
by rewrite -bigcup_mkord => -[m /=]; rewrite ltnS => _ Fmx; exists m .
Qed .
Section generated_sigma_algebra .
Context {T : Type } (D : set T) (G : set (set T)).
Implicit Types (M : set (set T)).
Lemma smallest_sigma_algebra : sigma_algebra D <<s D, G >>.
Proof .
split => [|A GA|A GA] P [[P0 PD PU]] GP //.
by apply : (PD); apply : GA.
by apply : (PU) => n; apply : GA.
Qed .
Hint Resolve smallest_sigma_algebra : core.
Lemma sub_sigma_algebra2 M : M `<=` G -> <<s D, M >> `<=` <<s D, G >>.
Proof . exact : sub_smallest2r. Qed .
Lemma sigma_algebra_id : sigma_algebra D G -> <<s D, G >> = G.
Proof . by move => /smallest_id->. Qed .
Lemma sub_sigma_algebra : G `<=` <<s D, G >>. Proof . exact : sub_smallest. Qed .
Lemma sigma_algebra0 : <<s D, G >> set0.
Proof . by case : smallest_sigma_algebra. Qed .
Lemma sigma_algebraCD : forall A , <<s D, G >> A -> <<s D, G >> (D `\` A).
Proof . by case : smallest_sigma_algebra. Qed .
Lemma sigma_algebra_bigcup (A : (set T)^nat) :
(forall i , <<s D, G >> (A i)) -> <<s D, G >> (\bigcup_i (A i)).
Proof . by case : smallest_sigma_algebra A. Qed .
End generated_sigma_algebra .
#[global ] Hint Resolve smallest_sigma_algebra : core.
Section generated_setring .
Context {T : Type } (G : set (set T)).
Implicit Types (M : set (set T)).
Lemma smallest_setring : setring <<r G >>.
Proof .
split => [|A B GA GB|A B GA GB] P [[P0 PU PDI]] GP //.
by apply : (PU); [apply : GA|apply : GB].
by apply : (PDI); [apply : GA|apply : GB].
Qed .
Hint Resolve smallest_setring : core.
Lemma sub_setring2 M : M `<=` G -> <<r M >> `<=` <<r G >>.
Proof . exact : sub_smallest2r. Qed .
Lemma setring_id : setring G -> <<r G >> = G.
Proof . by move => /smallest_id->. Qed .
Lemma sub_setring : G `<=` <<r G >>. Proof . exact : sub_smallest. Qed .
Lemma setring0 : <<r G >> set0.
Proof . by case : smallest_setring. Qed .
Lemma setringDI : setDI_closed <<r G>>.
Proof . by case : smallest_setring. Qed .
Lemma setringU : setU_closed <<r G>>.
Proof . by case : smallest_setring. Qed .
Lemma setring_fin_bigcup : fin_bigcup_closed <<r G>>.
Proof .
by apply /fin_bigcup_closedP; split ; [apply : setring0|apply : setringU].
Qed .
End generated_setring .
#[global ] Hint Resolve smallest_setring setring0 : core.
Lemma monotone_class_g_salgebra T (G : set (set T)) (D : set T) :
(forall X , <<s D, G >> X -> X `<=` D) -> G D ->
monotone_class D (<<s D, G >>).
Proof .
move => sDGD GD; have := smallest_sigma_algebra D G.
by move => /(sigma_algebraP sDGD) [sT sD snd sI]; split .
Qed .
Section smallest_monotone_classE .
Variables (T : Type ) (G : set (set T)) (setIG : setI_closed G).
Variables (D : set T) (GD : G D).
Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H).
Lemma smallest_monotone_classE : (forall X , <<s D, G >> X -> X `<=` D) ->
(forall E , monotone_class D E -> G `<=` E -> H `<=` E) ->
H = <<s D, G >>.
Proof .
move => sDGD smallestH; rewrite eqEsubset; split .
apply : (smallestH _ _ (@sub_sigma_algebra _ D G)).
exact : monotone_class_g_salgebra.
suff : setI_closed H.
move => IH; apply : smallest_sub => //.
by apply /sigma_algebraP; by case : monoH.
pose H_ A := [set X | H X /\ H (X `&` A)].
have setDH_ A : setD_closed (H_ A).
move => X Y XY [HX HXA] [HY HYA]; case : monoH => h _ setDH _; split .
exact : setDH.
rewrite (_ : _ `&` _ = (X `&` A) `\` (Y `&` A)); last first .
rewrite predeqE => x; split => [[[? ?] ?]|]; first by split => // -[].
by move => [[? ?] YAx]; split => //; split => //; apply : contra_not YAx.
by apply : setDH => //; exact : setSI.
have ndH_ A : ndseq_closed (H_ A).
move => F ndF H_AF; split .
by case : monoH => h _ _; apply => // => n; have [] := H_AF n.
rewrite setI_bigcupl; case : monoH => h _ _; apply => //.
by move => m n mn; apply /subsetPset; apply : setSI; apply /subsetPset/ndF.
by move => n; have [] := H_AF n.
have GGH_ X : G X -> G `<=` H_ X.
by move => *; split ; [exact : GH | apply : GH; exact : setIG].
have GHH_ X : G X -> H `<=` H_ X.
move => CX; apply : smallestH; [split => //; last exact : GGH_|exact : GGH_].
by move => ? [? ?]; case : monoH => + _ _ _; exact .
have HGH_ X : H X -> G `<=` H_ X.
by move => *; split ; [exact : GH|rewrite setIC; apply GHH_].
have HHH_ X : H X -> H `<=` H_ X.
move => HX; apply : (smallestH _ _ (HGH_ _ HX)); split => //.
- by move => ? [? ?]; case : monoH => + _ _ _; exact .
- exact : HGH_.
by move => *; apply HHH_.
Qed .
End smallest_monotone_classE .
Section monotone_class_subset .
Variables (T : Type ) (G : set (set T)) (setIG : setI_closed G).
Variables (D : set T) (GD : G D).
Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H).
Lemma monotone_class_subset : (forall X , (<<s D, G >>) X -> X `<=` D) ->
<<s D, G >> `<=` H.
Proof .
move => sDGD; set M := <<m D, G >>.
rewrite -(@smallest_monotone_classE _ _ setIG _ _ M) //.
- exact : smallest_sub.
- split => [A MA | E [monoE] | A B BA MA MB E [[EsubD ED setDE ndE] GE] |].
+ by case : monoH => + _ _ _; apply ; exact : MA.
+ exact .
+ by apply setDE => //; [exact : MA|exact : MB].
+ by move => F ndF MF E [[EsubD ED setDE ndE] CE]; apply ndE=> // n; exact : MF.
- exact : sub_smallest.
- by move => ? ? ?; exact : smallest_sub.
Qed .
End monotone_class_subset .
Section dynkin .
Variable T : Type .
Implicit Types G D : set (set T).
Lemma dynkinT G : dynkin G -> G setT. Proof . by case . Qed .
Lemma dynkinC G : dynkin G -> setC_closed G. Proof . by case . Qed .
Lemma dynkinU G : dynkin G -> (forall F : (set T)^nat, trivIset setT F ->
(forall n , G (F n)) -> G (\bigcup_k F k)). Proof . by case . Qed .
End dynkin .
Section dynkin_lemmas .
Variable T : Type .
Implicit Types D G : set (set T).
Lemma dynkin_monotone G : dynkin G <-> monotone_class setT G.
Proof .
split => [[GT setCG trG]|[_ GT setDG ndG]]; split => //.
- move => A B BA GA GB; rewrite setDE -(setCK (_ `&` _)) setCI; apply : (setCG).
rewrite setCK -bigcup2E; apply trG.
+ by rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint.
+ by move => [|[//|n]]; [exact : setCG|rewrite /bigcup2 -setCT; apply : setCG].
- move => F ndF GF; rewrite eq_bigcup_seqD; apply : (trG).
exact : trivIset_seqD.
move => [/=|n]; first exact : GF.
rewrite /seqD setDE -(setCK (_ `&` _)) setCI; apply : (setCG).
rewrite setCK -bigcup2E; apply : trG.
+ rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint.
exact /subsetPset/ndF/ltnW.
+ move => [|[|]]; rewrite /bigcup2 /=; [exact /setCG/GF|exact /GF|].
by move => _; rewrite -setCT; apply : setCG.
- by move => A B; rewrite -setTD; apply : setDG.
- move => F tF GF; pose A i := \big[setU/set0]_(k < i.+1 ) F k.
rewrite (_ : bigcup _ _ = \bigcup_i A i); last first .
rewrite predeqE => t; split => [[n _ Fn]|[n _]].
by exists n => //; rewrite /A -bigcup_mkord; exists n => //=; rewrite ltnS.
by rewrite /A -bigcup_mkord => -[m /=]; rewrite ltnS => mn Fmt; exists m .
apply : ndG; first by move => a b ab; exact /subsetPset/subset_bigsetU.
elim => /= => [|n ih].
by rewrite /A big_ord_recr /= big_ord0 set0U; exact : GF.
rewrite /A /= big_ord_recr /= -/(A n).
rewrite (_ : _ `|` _ = ~` (~` A n `\` F n.+1 )); last first .
by rewrite setDE setCI !setCK.
rewrite -setTD; apply : (setDG) => //; apply : (setDG) => //; last first .
by rewrite -setTD; apply : setDG.
apply /disjoints_subset; rewrite setIC.
by apply : (@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE.
Qed .
Lemma dynkin_g_dynkin G : dynkin (<<d G >>).
Proof .
split => [D /= [] []//| | ].
- by move => Y sGY D /= [dD GD]; exact /(dynkinC dD)/(sGY D).
- by move => F tF gGF D /= [dD GD]; apply dD => // k; exact : gGF.
Qed .
Lemma sigma_algebra_dynkin G : sigma_algebra setT G -> dynkin G.
Proof .
case => ? DC DU; split => [| |? ? ?]; last exact : DU.
- by rewrite -setC0 -setTD; exact : DC.
- by move => A GA; rewrite -setTD; apply : DC.
Qed .
Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G -> setI_closed G ->
(forall n , G (F n)) -> forall n , G (\big[setI/setT]_(i < n) F i).
Proof .
move => dG GI GF; elim => [|n ih]; last by rewrite big_ord_recr /=; apply : GI.
by rewrite big_ord0; exact : (dynkinT dG).
Qed .
Lemma dynkin_setI_sigma_algebra G : dynkin G -> setI_closed G ->
sigma_algebra setT G.
Proof .
move => dG GI; split => [|//|F DF].
- by rewrite -setCT; exact /(dynkinC dG)/(dynkinT dG).
- by move => A GA; rewrite setTD; exact : (dynkinC dG).
- rewrite seqDU_bigcup_eq; apply /(dynkinU dG) => //.
move => n; rewrite /seqDU setDE; apply GI => //.
rewrite -bigcup_mkord setC_bigcup bigcap_mkord.
by apply : (@dynkin_setI_bigsetI _ (fun x => ~` F x)) => // ?; exact /(dynkinC dG).
Qed .
Lemma setI_closed_gdynkin_salgebra G : setI_closed G -> <<d G >> = <<s G >>.
Proof .
move => GI; rewrite eqEsubset; split .
by apply : sub_smallest2l; apply : sigma_algebra_dynkin.
pose delta (D : set T) := [set E | <<d G >> (E `&` D)].
have ddelta (D : set T) : <<d G >> D -> dynkin (delta D).
move => dGD; split ; first by rewrite /delta /= setTI.
- move => E DE; rewrite /delta /=.
have -> : (~` E) `&` D = ~` ((E `&` D) `|` (~` D)).
by rewrite -[LHS]setU0 -(setICl D) -setIUl -setCI -{2 }(setCK D) -setCU.
have : <<d G >> ((E `&` D) `|` ~` D).
rewrite -bigcup2E => S [dS GS]; apply : (dynkinU dS).
move => [|[|i]] [|[|j]] => // _ _; rewrite /bigcup2 /=.
+ by rewrite -setIA setICr setI0 => /set0P; rewrite eqxx.
+ by rewrite setI0 => /set0P; rewrite eqxx.
+ by rewrite setICA setICl setI0 => /set0P; rewrite eqxx.
+ by rewrite setI0 => /set0P; rewrite eqxx.
+ by rewrite set0I => /set0P; rewrite eqxx.
+ by rewrite set0I => /set0P; rewrite eqxx.
+ by rewrite set0I => /set0P; rewrite eqxx.
move => [|[|n]] //; rewrite /bigcup2 /=; [exact : DE| |].
+ suff : <<d G >> (~` D) by exact .
by move => F [dF GF]; apply : (dynkinC dF) => //; exact : dGD.
+ by rewrite -setCT; apply /(dynkinC dS)/(dynkinT dS).
by move => dGEDD S /= [+ GS] => dS; apply /(dynkinC dS); exact : dGEDD.
- move => F tF deltaDF; rewrite /delta /= => S /= [dS GS].
rewrite setI_bigcupl; apply : (dynkinU dS) => //.
by under eq_fun do rewrite setIC; exact : trivIset_setIl.
by move => n; exact : deltaDF.
have GdG : G `<=` <<d G >> by move => ? ? ? [_]; apply .
have Gdelta A : G A -> G `<=` delta A.
by move => ? ? ?; rewrite /delta /= => ? [?]; apply ; exact /GI.
have GdGdelta A : G A -> <<d G >> `<=` delta A.
move => ?; apply : smallest_sub => //; last exact : Gdelta.
by apply /ddelta; exact : GdG.
have dGGI A B : <<d G >> A -> G B -> <<d G >> (A `&` B).
by move => ? ?; apply : GdGdelta.
have dGGdelta A : <<d G >> A -> G `<=` delta A.
by move => ? ? ?; rewrite /delta /= setIC; exact : dGGI.
have dGdGdelta A : <<d G >> A -> <<d G >> `<=` delta A.
by move => ?; exact : smallest_sub (ddelta _ _) (dGGdelta _ _).
have dGdGdG A B : <<d G >> A -> <<d G >> B -> <<d G >> (A `&` B).
by move => ? ?; exact : dGdGdelta.
apply : smallest_sub => //; apply : dynkin_setI_sigma_algebra => //.
exact : dynkin_g_dynkin.
Qed .
End dynkin_lemmas .
HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
ptclass : Pointed.class_of T;
measurable : set (set T) ;
measurable0 : measurable set0 ;
measurableI : setI_closed measurable;
semi_measurableD : semi_setD_closed measurable;
}.
#[short(type=semiRingOfSetsType)]
HB.structure Definition SemiRingOfSets d := {T of isSemiRingOfSets d T}.
Canonical semiRingOfSets_eqType d (T : semiRingOfSetsType d) := EqType T ptclass.
Canonical semiRingOfSets_choiceType d (T : semiRingOfSetsType d) :=
ChoiceType T ptclass.
Canonical semiRingOfSets_ptType d (T : semiRingOfSetsType d) :=
PointedType T ptclass.
Lemma measurable_curry (T1 T2 : Type ) d (T : semiRingOfSetsType d)
(G : T1 * T2 -> set T) (x : T1 * T2) :
measurable (G x) <-> measurable (curry G x.1 x.2 ).
Proof . by case : x. Qed .
Notation "d .-measurable" := (@measurable d%mdisp) : classical_set_scope.
Notation "'measurable" :=
(@measurable default_measure_display) : classical_set_scope.
HB.mixin Record RingOfSets_from_semiRingOfSets d T of isSemiRingOfSets d T := {
measurableU : setU_closed (@measurable d [the semiRingOfSetsType d of T]) }.
#[short(type=ringOfSetsType)]
HB.structure Definition RingOfSets d :=
{T of RingOfSets_from_semiRingOfSets d T & SemiRingOfSets d T}.
Canonical ringOfSets_eqType d (T : ringOfSetsType d) := EqType T ptclass.
Canonical ringOfSets_choiceType d (T : ringOfSetsType d) := ChoiceType T ptclass.
Canonical ringOfSets_ptType d (T : ringOfSetsType d) := PointedType T ptclass.
HB.mixin Record AlgebraOfSets_from_RingOfSets d T of RingOfSets d T := {
measurableT : measurable [set : T]
}.
#[short(type=algebraOfSetsType)]
HB.structure Definition AlgebraOfSets d :=
{T of AlgebraOfSets_from_RingOfSets d T & RingOfSets d T}.
Canonical algebraOfSets_eqType d (T : algebraOfSetsType d) := EqType T ptclass.
Canonical algebraOfSets_choiceType d (T : algebraOfSetsType d) :=
ChoiceType T ptclass.
Canonical algebraOfSets_ptType d (T : algebraOfSetsType d) :=
PointedType T ptclass.
HB.mixin Record Measurable_from_algebraOfSets d T of AlgebraOfSets d T := {
bigcupT_measurable : forall F : (set T)^nat, (forall i , measurable (F i)) ->
measurable (\bigcup_i (F i))
}.
#[short(type=measurableType)]
HB.structure Definition Measurable d :=
{T of Measurable_from_algebraOfSets d T & AlgebraOfSets d T}.
Canonical measurable_eqType d (T : measurableType d) := EqType T ptclass.
Canonical measurable_choiceType d (T : measurableType d) := ChoiceType T ptclass.
Canonical measurable_ptType d (T : measurableType d) := PointedType T ptclass.
HB.factory Record isRingOfSets (d : measure_display) T := {
ptclass : Pointed.class_of T;
measurable : set (set T) ;
measurable0 : measurable set0 ;
measurableU : setU_closed measurable;
measurableD : setDI_closed measurable;
}.
HB.builders Context d T of isRingOfSets d T .
Implicit Types (A B C D : set T).
Lemma mI : setI_closed measurable.
Proof . by move => A B mA mB; rewrite -setDD; do ?apply : measurableD. Qed .
Lemma mD : semi_setD_closed measurable.
Proof .
move => A B Am Bm; exists [set A `\` B]; split ; rewrite ?bigcup_set1 //.
by move => C ->; apply : measurableD.
by move => X Y -> ->.
Qed .
HB.instance Definition T_isSemiRingOfSets :=
@isSemiRingOfSets.Build d T ptclass measurable measurable0 mI mD.
HB.instance Definition T_isRingOfSets :=
RingOfSets_from_semiRingOfSets.Build d T measurableU.
HB.end .
HB.factory Record isAlgebraOfSets (d : measure_display) T := {
ptclass : Pointed.class_of T;
measurable : set (set T) ;
measurable0 : measurable set0 ;
measurableU : setU_closed measurable;
measurableC : setC_closed measurable
}.
HB.builders Context d T of isAlgebraOfSets d T .
Lemma mD : setDI_closed measurable.
Proof .
move => A B mA mB; rewrite setDE -[A]setCK -setCU.
by do ?[apply : measurableU | apply : measurableC].
Qed .
HB.instance Definition T_isRingOfSets := @isRingOfSets.Build d T ptclass
measurable measurable0 measurableU mD.
Lemma measurableT : measurable [set : T].
Proof . by rewrite -setC0; apply : measurableC; exact : measurable0. Qed .
HB.instance Definition T_isAlgebraOfSets : AlgebraOfSets_from_RingOfSets d T :=
AlgebraOfSets_from_RingOfSets.Build d T measurableT.
HB.end .
HB.factory Record isMeasurable (d : measure_display) T := {
ptclass : Pointed.class_of T;
measurable : set (set T) ;
measurable0 : measurable set0 ;
measurableC : forall A , measurable A -> measurable (~` A) ;
measurable_bigcup : forall F : (set T)^nat, (forall i , measurable (F i)) ->
measurable (\bigcup_i (F i))
}.
HB.builders Context d T of isMeasurable d T .
Obligation Tactic := idtac .
Lemma mU : setU_closed measurable.
Proof .
move => A B mA mB; rewrite -bigcup2E.
by apply : measurable_bigcup => -[//|[//|i]]; exact : measurable0.
Qed .
Lemma mC : setC_closed measurable. Proof . by move => *; apply : measurableC. Qed .
HB.instance Definition T_isAlgebraOfSets :=
@isAlgebraOfSets.Build d T ptclass measurable measurable0 mU mC.
HB.instance Definition T_isMeasurable :=
@Measurable_from_algebraOfSets.Build d T measurable_bigcup.
HB.end .
#[global ] Hint Extern 0 (measurable set0) => solve [apply : measurable0] : core.
#[global ] Hint Extern 0 (measurable setT) => solve [apply : measurableT] : core.
Section ringofsets_lemmas .
Context d (T : ringOfSetsType d).
Implicit Types A B : set T.
Lemma bigsetU_measurable I r (P : pred I) (F : I -> set T) :
(forall i , P i -> measurable (F i)) ->
measurable (\big[setU/set0]_(i <- r | P i) F i).
Proof . by move => mF; elim /big_ind : _ => //; exact : measurableU. Qed .
Lemma fin_bigcup_measurable I (D : set I) (F : I -> set T) :
finite_set D ->
(forall i , D i -> measurable (F i)) ->
measurable (\bigcup_(i in D) F i).
Proof .
elim /Pchoice: I => I in D F * => Dfin Fm.
rewrite -bigsetU_fset_set// big_seq; apply : bigsetU_measurable => i.
by rewrite in_fset_set ?inE // => *; apply : Fm.
Qed .
Lemma measurableD : setDI_closed (@measurable d T).
Proof .
move => A B mA mB; case : (semi_measurableD A B) => // [D [Dfin Dl -> _]].
by apply : fin_bigcup_measurable.
Qed .
End ringofsets_lemmas .
Section algebraofsets_lemmas .
Context d (T : algebraOfSetsType d).
Implicit Types A B : set T.
Lemma measurableC A : measurable A -> measurable (~` A).
Proof . by move => mA; rewrite -setTD; exact : measurableD. Qed .
Lemma bigsetI_measurable I r (P : pred I) (F : I -> set T) :
(forall i , P i -> measurable (F i)) ->
measurable (\big[setI/setT]_(i <- r | P i) F i).
Proof .
move => mF; rewrite -[X in measurable X]setCK setC_bigsetI; apply : measurableC.
by apply : bigsetU_measurable => i Pi; apply /measurableC/mF.
Qed .
Lemma fin_bigcap_measurable I (D : set I) (F : I -> set T) :
finite_set D ->
(forall i , D i -> measurable (F i)) ->
measurable (\bigcap_(i in D) F i).
Proof .
elim /Pchoice: I => I in D F * => Dfin Fm.
rewrite -bigsetI_fset_set// big_seq; apply : bigsetI_measurable => i.
by rewrite in_fset_set ?inE // => *; apply : Fm.
Qed .
End algebraofsets_lemmas .
Section measurable_lemmas .
Context d (T : measurableType d).
Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat).
Lemma sigma_algebra_measurable : sigma_algebra setT (@measurable d T).
Proof . by split => // [A|]; [exact : measurableD|exact : bigcupT_measurable]. Qed .
Lemma bigcup_measurable F P :
(forall k , P k -> measurable (F k)) -> measurable (\bigcup_(i in P) F i).
Proof .
move => PF; rewrite bigcup_mkcond; apply : bigcupT_measurable => k.
by case : ifP => //; rewrite inE; exact : PF.
Qed .
Lemma bigcap_measurable F P :
(forall k , P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i).
Proof .
move => PF; rewrite -[X in measurable X]setCK setC_bigcap; apply : measurableC.
by apply : bigcup_measurable => k Pk; exact /measurableC/PF.
Qed .
Lemma bigcapT_measurable F : (forall i , measurable (F i)) ->
measurable (\bigcap_i (F i)).
Proof . by move => ?; exact : bigcap_measurable. Qed .
End measurable_lemmas .
Lemma bigcupT_measurable_rat d (T : measurableType d) (F : rat -> set T) :
(forall i , measurable (F i)) -> measurable (\bigcup_i F i).
Proof .
move => Fm; have /ppcard_eqP[f] := card_rat.
by rewrite (reindex_bigcup f^-1 %FUN setT)//=; exact : bigcupT_measurable.
Qed .
Section discrete_measurable_unit .
Definition discrete_measurable_unit : set (set unit) := [set : set unit].
Let discrete_measurable0 : discrete_measurable_unit set0. Proof . by []. Qed .
Let discrete_measurableC X :
discrete_measurable_unit X -> discrete_measurable_unit (~` X).
Proof . by []. Qed .
Let discrete_measurableU (F : (set unit)^nat) :
(forall i , discrete_measurable_unit (F i)) ->
discrete_measurable_unit (\bigcup_i F i).
Proof . by []. Qed .
HB.instance Definition _ := @isMeasurable.Build default_measure_display unit
(Pointed.class _) 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).
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 .
HB.instance Definition _ := @isMeasurable.Build default_measure_display bool
(Pointed.class _) discrete_measurable_bool 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
(Pointed.class _) discrete_measurable_nat discrete_measurable_nat0
discrete_measurable_natC discrete_measurable_natU.
End discrete_measurable_nat .
Definition sigma_display {T } : set (set T) -> measure_display.
Proof . exact . Qed .
Definition salgebraType {T } (G : set (set T)) := T.
Section g_salgebra_instance .
Variables (T : pointedType) (G : set (set T)).
Lemma sigma_algebraC (A : set T) : <<s G >> A -> <<s G >> (~` A).
Proof . by move => sGA; rewrite -setTD; exact : sigma_algebraCD. Qed .
Canonical salgebraType_eqType := EqType (salgebraType G) (Equality.class T).
Canonical salgebraType_choiceType := ChoiceType (salgebraType G) (Choice.class T).
Canonical salgebraType_ptType := PointedType (salgebraType G) (Pointed.class T).
HB.instance Definition _ := @isMeasurable.Build (sigma_display G)
(salgebraType G) (Pointed.class T)
<<s G >> (@sigma_algebra0 _ setT G) (@sigma_algebraC)
(@sigma_algebra_bigcup _ setT G).
End g_salgebra_instance .
Notation "G .-sigma" := (sigma_display G) : measure_display_scope.
Notation "G .-sigma.-measurable" :=
(measurable : set (set (salgebraType G))) : classical_set_scope.
Lemma measurable_g_measurableTypeE (T : pointedType) (G : set (set T)) :
sigma_algebra setT G -> G.-sigma.-measurable = G.
Proof . exact : sigma_algebra_id. Qed .
Definition measurable_fun d d' (T : measurableType d) (U : measurableType d')
(D : set T) (f : T -> U) :=
measurable D -> forall Y , measurable Y -> measurable (D `&` f @^-1 ` Y).
Section measurable_fun .
Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2)
(T3 : measurableType d3).
Implicit Type D E : set T1.
Lemma measurable_fun_id D : measurable_fun D id.
Proof . by move => mD A mA; apply : measurableI. Qed .
Lemma measurable_fun_comp F (f : T2 -> T3) E (g : T1 -> T2) :
measurable F -> g @` E `<=` F ->
measurable_fun F f -> measurable_fun E g -> measurable_fun E (f \o g).
Proof .
move => mF FgE mf mg /= mE A mA.
rewrite comp_preimage.
rewrite (_ : _ `&` _ = E `&` g @^-1 ` (F `&` f @^-1 ` A)); last first .
apply /seteqP; split => [|? [?] []//].
by move => x/= [Ex Afgx]; split => //; split => //; exact : FgE.
by apply /mg => //; exact : mf.
Qed .
Lemma measurable_funT_comp (f : T2 -> T3) E (g : T1 -> T2) :
measurable_fun setT f -> measurable_fun E g -> measurable_fun E (f \o g).
Proof . exact : measurable_fun_comp. Qed .
Lemma eq_measurable_fun D (f g : T1 -> T2) :
{in D, f =1 g} -> measurable_fun D f -> measurable_fun D g.
Proof .
move => Dfg Df mD A mA; rewrite (_ : D `&` _ = D `&` f @^-1 ` A); first exact : Df.
apply /seteqP; rewrite /preimage; split => [x /= [Dx Agx]|x /= [Dx Afx]].
by split => //; rewrite Dfg// inE.
by split => //; rewrite -Dfg// inE.
Qed .
Lemma measurable_fun_cst D (r : T2) : measurable_fun D (cst r : T1 -> _).
Proof .
by move => mD /= Y mY; rewrite preimage_cst; case : ifPn; rewrite ?setIT ?setI0 .
Qed .
Lemma measurable_funU D E (f : T1 -> T2) :
measurable D -> measurable E ->
measurable_fun (D `|` E) f <-> measurable_fun D f /\ measurable_fun E f.
Proof .
move => mD mE; split => [mDEf|[mDf mEf] mDE A mA]; last first .
by rewrite setIUl; apply : measurableU; [exact : mDf|exact : mEf].
split .
- move => {}mD A /mDEf => /(_ (measurableU _ _ mD mE))/(measurableI D)-/(_ mD).
by rewrite setICA setIA setUK.
- move => {}mE A /mDEf => /(_ (measurableU _ _ mD mE))/(measurableI E)-/(_ mE).
by rewrite setICA setIA setUC setUK.
Qed .
Lemma measurable_funS E D (f : T1 -> T2) :
measurable E -> D `<=` E -> measurable_fun E f ->
measurable_fun D f.
Proof .
move => mE DE mf mD; have mC : measurable (E `\` D) by exact : measurableD.
move : (mD).
have := measurable_funU f mD mC.
suff -> : D `|` (E `\` D) = E by move => [[]] //.
by rewrite setDUK.
Qed .
Lemma measurable_funTS D (f : T1 -> T2) :
measurable_fun setT f -> measurable_fun D f.
Proof . exact : measurable_funS. Qed .
Lemma measurable_fun_ext D (f g : T1 -> T2) :
{in D, f =1 g} -> measurable_fun D f -> measurable_fun D g.
Proof .
by move => fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1 ` A);
[exact : mf|exact /esym/eq_preimage].
Qed .
Lemma measurable_restrict D E (f : T1 -> T2) :
measurable D -> measurable E -> D `<=` E ->
measurable_fun D f <-> measurable_fun E (f \_ D).
Proof .
move => mD mE DE; split => mf _ /= X mX.
- rewrite preimage_restrict; apply /measurableI => //.
by apply /measurableU/mf => //; case : ifP => // _; apply : measurableC.
- have := mf mE _ mX; rewrite preimage_restrict.
case : ifP => ptX; last first .
rewrite set0U => /(measurableI _ _ mD).
by rewrite (setIA D) (setIidl DE) setIA setIid.
rewrite setUIr setvU setTI => /(measurableI _ _ mD).
by rewrite setIA (setIidl DE) setIUr setICr set0U.
Qed .
Lemma measurable_fun_if (g h : T1 -> T2) D (mD : measurable D)
(f : T1 -> bool) (mf : measurable_fun D f) :
measurable_fun (D `&` (f @^-1 ` [set true])) g ->
measurable_fun (D `&` (f @^-1 ` [set false])) h ->
measurable_fun D (fun t => if f t then g t else h t).
Proof .
move => mx my /= _ B mB; rewrite (_ : _ @^-1 ` B =
((f @^-1 ` [set true]) `&` (g @^-1 ` B) `&` (f @^-1 ` [set true])) `|`
((f @^-1 ` [set false]) `&` (h @^-1 ` B) `&` (f @^-1 ` [set false]))).
rewrite setIUr; apply : measurableU.
- by rewrite setIAC setIid setIA; apply : mx => //; exact : mf.
- by rewrite setIAC setIid setIA; apply : my => //; exact : mf.
apply /seteqP; split => [t /=| t]; first by case : ifPn => ft; [left |right ].
by move => /= [|]; case : ifPn => ft; case => -[].
Qed .
Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool)
(mf : measurable_fun setT f) :
measurable_fun setT g -> measurable_fun setT h ->
measurable_fun setT (fun t => if f t then g t else h t).
Proof .
by move => mx my; apply : measurable_fun_if => //;
[exact : measurable_funS mx|exact : measurable_funS my].
Qed .
Lemma measurable_fun_bool D (f : T1 -> bool) b :
measurable (f @^-1 ` [set b]) -> measurable_fun D f.
Proof .
have FNT : [set false] = [set ~ true] by apply /seteqP; split => -[]//=.
wlog {b}-> : b / b = true.
case : b => [|h]; first exact .
by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact : h.
move => mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT.
have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
- by rewrite preimage0 ?setI0 .
- by apply : measurableI => //; exact : mfT.
- rewrite -[X in measurable X]setCK; apply : measurableC; rewrite setCI.
apply : measurableU; first exact : measurableC.
by rewrite FNT preimage_setC setCK; exact : mfT.
- by rewrite -setT_bool preimage_setT setIT.
Qed .
End measurable_fun .
Arguments measurable_fun_ext {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_bool {d1 T1 D f} b.
Section measurability .
Definition preimage_class (aT rT : Type ) (D : set aT) (f : aT -> rT)
(G : set (set rT)) : set (set aT) :=
[set D `&` f @^-1 ` B | B in G].
(* f is measurable on the sigma-algebra generated by itself *)
Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d)
(D : set aT) (f : aT -> rT) :
measurable_fun (D : set (salgebraType (preimage_class D f measurable))) f.
Proof . by move => mD A mA; apply : sub_sigma_algebra; exists A . Qed .
Lemma sigma_algebra_preimage_class (aT rT : Type ) (G : set (set rT))
(D : set aT) (f : aT -> rT) :
sigma_algebra setT G -> sigma_algebra D (preimage_class D f G).
Proof .
case => h0 hC hU; split ; first by exists set0 => //; rewrite preimage_set0 setI0.
- move => A; rewrite /preimage_class /= => -[B mB <-{A}].
exists (~` B); first by rewrite -setTD; exact : hC.
rewrite predeqE => x; split => [[Dx Bfx]|[Dx]]; first by split => // -[] _ /Bfx.
by move => /not_andP[].
- move => F; rewrite /preimage_class /= => mF.
have {}mF n : exists x , G x /\ D `&` f @^-1 ` x = F n.
by have := mF n => -[B mB <-]; exists B .
have [F' mF'] := @choice _ _ (fun x y => G y /\ D `&` f @^-1 ` y = F x) mF.
exists (\bigcup_k (F' k)); first by apply : hU => n; exact : (mF' n).1 .
rewrite preimage_bigcup setI_bigcupr; apply : eq_bigcupr => i _.
exact : (mF' i).2 .
Qed .
Definition image_class (aT rT : Type ) (D : set aT) (f : aT -> rT)
(G : set (set aT)) : set (set rT) :=
[set B : set rT | G (D `&` f @^-1 ` B)].
Lemma sigma_algebra_image_class (aT rT : Type ) (D : set aT) (f : aT -> rT)
(G : set (set aT)) :
sigma_algebra D G -> sigma_algebra setT (image_class D f G).
Proof .
move => [G0 GC GU]; split ; rewrite /image_class.
- by rewrite /= preimage_set0 setI0.
- move => A /= GfAD; rewrite setTD -preimage_setC -setDE.
rewrite (_ : _ `\` _ = D `\` (D `&` f @^-1 ` A)); first exact : GC.
rewrite predeqE => x; split => [[Dx fAx]|[Dx fADx]].
by split => // -[] _ /fAx.
by split => //; exact : contra_not fADx.
- by move => F /= mF; rewrite preimage_bigcup setI_bigcupr; exact : GU.
Qed .
Lemma sigma_algebra_preimage_classE aT (rT : pointedType) (D : set aT)
(f : aT -> rT) (G' : set (set rT)) :
<<s D, preimage_class D f G' >> =
preimage_class D f (G'.-sigma.-measurable).
Proof .
rewrite eqEsubset; split .
have mG : sigma_algebra D
(preimage_class D f (G'.-sigma.-measurable)).
exact /sigma_algebra_preimage_class/sigma_algebra_measurable.
have subset_preimage : preimage_class D f G' `<=`
preimage_class D f (G'.-sigma.-measurable).
by move => A [B CCB <-{A}]; exists B => //; apply : sub_sigma_algebra.
exact : smallest_sub.
have G'pre A' : G' A' -> (preimage_class D f G') (D `&` f @^-1 ` A').
by move => ?; exists A' .
pose I : set (set aT) := <<s D, preimage_class D f G' >>.
have G'sfun : G' `<=` image_class D f I.
by move => A' /G'pre[B G'B h]; apply : sub_sigma_algebra; exists B .
have sG'sfun : <<s G' >> `<=` image_class D f I.
apply : smallest_sub => //; apply : sigma_algebra_image_class.
exact : smallest_sigma_algebra.
by move => _ [B mB <-]; exact : sG'sfun.
Qed .
Lemma measurability d d' (aT : measurableType d) (rT : measurableType d')
(D : set aT) (f : aT -> rT)
(G' : set (set rT)) :
@measurable _ rT = <<s G' >> -> preimage_class D f G' `<=` @measurable _ aT ->
measurable_fun D f.
Proof .
move => sG_rT fG_aT mD.
suff h : preimage_class D f (@measurable _ rT) `<=` @measurable _ aT.
by move => A mA; apply : h; exists A .
have -> : preimage_class D f (@measurable _ rT) =
<<s D , (preimage_class D f G')>>.
by rewrite [in LHS]sG_rT [in RHS]sigma_algebra_preimage_classE.
apply : smallest_sub => //; split => //.
- by move => A mA; exact : measurableD.
- by move => F h; exact : bigcupT_measurable.
Qed .
End measurability .
Local Open Scope ereal_scope.
Section additivity .
Context d (R : numFieldType) (T : semiRingOfSetsType d)
(mu : set T -> \bar R).
Definition semi_additive2 := forall A B , measurable A -> measurable B ->
measurable (A `|` B) ->
A `&` B = set0 -> mu (A `|` B) = mu A + mu B.
Definition semi_additive := forall F n ,
(forall k : nat, measurable (F k)) -> trivIset setT F ->
measurable (\big[setU/set0]_(k < n) F k) ->
mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Definition semi_sigma_additive :=
forall F , (forall i : nat, measurable (F i)) -> trivIset setT F ->
measurable (\bigcup_n F n) ->
(fun n => \sum_(0 <= i < n) mu (F i)) --> mu (\bigcup_n F n).
Definition additive2 := forall A B , measurable A -> measurable B ->
A `&` B = set0 -> mu (A `|` B) = mu A + mu B.
Definition additive :=
forall F , (forall i : nat, measurable (F i)) -> trivIset setT F ->
forall n , mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Definition sigma_additive :=
forall F , (forall i : nat, measurable (F i)) -> trivIset setT F ->
(fun n => \sum_(0 <= i < n) mu (F i)) --> mu (\bigcup_n F n).
Definition sub_additive := forall (A : set T) (F : nat -> set T) n ,
(forall k , `I_n k -> measurable (F k)) -> measurable A ->
A `<=` \big[setU/set0]_(k < n) F k ->
mu A <= \sum_(k < n) mu (F k).
Definition sigma_sub_additive := forall (A : set T) (F : nat -> set T),
(forall n , measurable (F n)) -> measurable A ->
A `<=` \bigcup_n F n ->
mu A <= \sum_(n <oo) mu (F n).
Definition sigma_finite (A : set T) (mu : set T -> \bar R) :=
exists2 F : (set T)^nat, A = \bigcup_(i : nat) F i &
forall i , measurable (F i) /\ mu (F i) < +oo.
Lemma semi_additiveW : mu set0 = 0 -> semi_additive -> semi_additive2.
Proof .
move => mu0 amx A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord.
move => /(amx (bigcup2 A B))->.
- by rewrite !(big_ord_recl, big_ord0)/= adde0.
- by move => [|[|[]]]//=.
- by move => [|[|i]] [|[|j]]/= _ _; rewrite ?(AB, setI0, set0I, setIC) => -[].
Qed .
End additivity .
Section ring_additivity .
Context d (R : numFieldType) (T : ringOfSetsType d) (mu : set T -> \bar R).
Lemma semi_additiveE : semi_additive mu = additive mu.
Proof .
rewrite propeqE; split => [sa A mA tA n|+ A m mA tA UAm]; last by move ->.
by rewrite sa //; exact : bigsetU_measurable.
Qed .
Lemma semi_additive2E : semi_additive2 mu = additive2 mu.
Proof .
rewrite propeqE; split => [amu A B ? ? ?|amu A B ? ? _ ?]; last by rewrite amu.
by rewrite amu //; exact : measurableU.
Qed .
Lemma additive2P : mu set0 = 0 -> semi_additive mu <-> additive2 mu.
Proof .
move => mu0; rewrite -semi_additive2E; split ; first exact : semi_additiveW.
rewrite semi_additiveE semi_additive2E => muU A Am Atriv n.
elim : n => [|n IHn]; rewrite ?(big_ord_recr, big_ord0) ?mu0 //=.
rewrite muU ?IHn //=; first by apply : bigsetU_measurable.
rewrite -bigcup_mkord -subset0 => x [[/= m + Amx] Anx].
by rewrite (Atriv m n) ?ltnn //=; exists x .
Qed .
End ring_additivity .
Lemma semi_sigma_additive_is_additive d
(R : realFieldType (*TODO: numFieldType if possible?*))
(X : semiRingOfSetsType d) (mu : set X -> \bar R) :
mu set0 = 0 -> semi_sigma_additive mu -> semi_additive mu.
Proof .
move => mu0 samu A n Am Atriv UAm.
have := samu (fun i => if (i < n)%N then A i else set0).
rewrite (bigcup_splitn n) bigcup0 ?setU0 ; last first .
by move => i _; rewrite -ltn_subRL subnn.
under eq_bigr do rewrite ltn_ord.
move => /(_ _ _ UAm)/(@cvg_lim _) <-//; last 2 first .
- by move => i; case : ifP.
- move => i j _ _; do 2 ![case : ifP] => ? ?; do ?by rewrite (setI0, set0I) => -[].
by move => /Atriv; apply .
apply : lim_near_cst => //=; near=> i.
have /subnKC<- : (n <= i)%N by near: i; exists n .
transitivity (\sum_(j < n + (i - n)) mu (if (j < n)%N then A j else set0)).
by rewrite big_mkord.
rewrite big_split_ord/=; under eq_bigr do rewrite ltn_ord.
by rewrite [X in _ + X]big1 ?adde0 // => ?; rewrite -ltn_subRL subnn.
Unshelve . all : by end_near. Qed .
Lemma semi_sigma_additiveE
(R : numFieldType) d (X : measurableType d) (mu : set X -> \bar R) :
semi_sigma_additive mu = sigma_additive mu.
Proof .
rewrite propeqE; split => [amu A mA tA|amu A mA tA mbigcupA]; last exact : amu.
by apply : amu => //; exact : bigcupT_measurable.
Qed .
Lemma sigma_additive_is_additive
(R : realFieldType) d (X : measurableType d) (mu : set X -> \bar R) :
mu set0 = 0 -> sigma_additive mu -> additive mu.
Proof .
move => mu0; rewrite -semi_sigma_additiveE -semi_additiveE.
exact : semi_sigma_additive_is_additive.
Qed .
HB.mixin Record isContent d
(R : numFieldType) (T : semiRingOfSetsType d) (mu : set T -> \bar R) := {
measure_ge0 : forall x , 0 <= mu x ;
measure_semi_additive : semi_additive mu }.
HB.structure Definition Content d
(R : numFieldType) (T : semiRingOfSetsType d) := {
mu & isContent d R T mu }.
Notation content := Content.type.
Notation "{ 'content' 'set' T '->' '\bar' R }" :=
(content R T) (at level 36 , T, R at next level ,
format "{ 'content' 'set' T '->' '\bar' R }" ) : ring_scope.
Arguments measure_ge0 {d R T} _.
Section content_signed .
Context d (R : numFieldType) (T : semiRingOfSetsType d).
Variable mu : {content set T -> \bar R}.
Lemma content_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).
Proof . exact : measure_ge0. Qed .
Canonical content_snum S := Signed.mk (content_snum_subproof S).
End content_signed .
Section content_on_semiring_of_sets .
Context d (R : numFieldType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}).
Lemma measure0 : mu set0 = 0 .
Proof .
have /[!big_ord0] ->// := @measure_semi_additive _ _ _ mu (fun => set0) 0 %N.
exact : trivIset_set0.
Qed .
Hint Resolve measure0 : core.
Hint Resolve measure_ge0 : core.
Hint Resolve measure_semi_additive : core.
Lemma measure_semi_additive_ord (n : nat) (F : 'I_n -> set T) :
(forall (k : 'I_n), measurable (F k)) ->
trivIset setT F ->
measurable (\big[setU/set0]_(k < n) F k) ->
mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Proof .
move => mF tF mUF; pose F' (i : nat) := oapp F set0 (insub i).
have FE (i : 'I_n) : F i = (F' \o val) i by rewrite /F'/= valK/=.
rewrite (eq_bigr (F' \o val))// (eq_bigr (mu \o F' \o val))//; last first .
by move => i _; rewrite FE.
rewrite -measure_semi_additive//.
- by move => k; rewrite /F'; case : insubP => /=.
- apply /trivIsetP=> i j _ _; rewrite /F'.
do 2 ?[case : insubP; rewrite ?(set0I, setI0)//= => ? _ <-].
by move /trivIsetP: tF; apply .
- by rewrite (eq_bigr (F' \o val)) in mUF.
Qed .
Lemma measure_semi_additive_ord_I (F : nat -> set T) (n : nat) :
(forall k , (k < n)%N -> measurable (F k)) ->
trivIset `I_n F ->
measurable (\big[setU/set0]_(k < n) F k) ->
mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Proof .
move => mF tF; apply : measure_semi_additive_ord.
by move => k; apply : mF.
by rewrite trivIset_comp// ?(image_eq [surjfun of val])//; apply : 'inj_val.
Qed .
Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) :
finite_set D ->
trivIset D F ->
(forall i , D i -> measurable (F i)) ->
measurable (\bigcup_(i in D) F i) ->
mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
Proof .
elim /choicePpointed: I => I in D F *.
by rewrite !emptyE => *; rewrite fsbig_set0 bigcup0.
move => [n /ppcard_eqP[f]] Ftriv Fm UFm.
rewrite -(image_eq [surjfun of f^-1 %FUN])/= in UFm Ftriv *.
rewrite bigcup_image fsbig_image//= bigcup_mkord -fsbig_ord/= in UFm *.
rewrite (@measure_semi_additive_ord_I (F \o f^-1 ))//= 1 ?trivIset_comp //.
by move => k kn; apply : Fm; exact : funS.
Qed .
Lemma measure_semi_additive2 : semi_additive2 mu.
Proof . exact /semi_additiveW. Qed .
Hint Resolve measure_semi_additive2 : core.
End content_on_semiring_of_sets .
Arguments measure0 {d R T} _.
#[global ] Hint Extern 0
(is_true (0 <= (_ : {content set _ -> \bar _}) _)%E) =>
solve [apply : measure_ge0] : core.
#[global ]
Hint Resolve measure0 measure_semi_additive2 measure_semi_additive : core.
Section content_on_ring_of_sets .
Context d (R : realFieldType)(T : ringOfSetsType d)
(mu : {content set T -> \bar R}).
Lemma measureU : additive2 mu.
Proof . by rewrite -semi_additive2E. Qed .
Lemma measure_bigsetU : additive mu.
Proof . by rewrite -semi_additiveE. Qed .
Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) :
finite_set D ->
trivIset D F ->
(forall i , D i -> measurable (F i)) ->
mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
Proof .
move => Dfin Ftriv Fm; rewrite content_fin_bigcup//.
exact : fin_bigcup_measurable.
Qed .
Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n -> set T) :
(forall i : 'I_n, P i -> measurable (F i)) -> trivIset P F ->
mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Proof .
move => mF tF; rewrite !(big_mkcond P)/= measure_semi_additive_ord//.
- by apply : eq_bigr => i _; rewrite (fun_if mu) measure0.
- by move => k; case : ifP => //; apply : mF.
- by rewrite -patch_pred trivIset_restr setIT.
- by apply : bigsetU_measurable=> k _; case : ifP => //; apply : mF.
Qed .
Lemma measure_bigsetU_ord n (P : {pred 'I_n}) (F : 'I_n -> set T) :
(forall i : 'I_n, measurable (F i)) -> trivIset setT F ->
mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Proof .
by move => mF tF; rewrite measure_bigsetU_ord_cond//; apply : sub_trivIset tF.
Qed .
Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I -> set T) :
(forall i , i \in A -> measurable (F i)) -> trivIset [set ` A] F ->
mu (\big[setU/set0]_(i <- A) F i) = (\sum_(i <- A) mu (F i))%E.
Proof .
by move => mF tF; rewrite -bigcup_fset measure_fin_bigcup// -fsbig_seq.
Qed .
End content_on_ring_of_sets .
#[global ]
Hint Resolve measureU measure_bigsetU : core.
HB.mixin Record isMeasure0 d
(R : numFieldType) (T : semiRingOfSetsType d)
mu of isContent d R T mu := {
measure_semi_sigma_additive : semi_sigma_additive mu }.
#[short(type=measure )]
HB.structure Definition Measure d
(R : numFieldType) (T : semiRingOfSetsType d) :=
{mu of isMeasure0 d R T mu & Content d mu}.
Notation "{ 'measure' 'set' T '->' '\bar' R }" := (measure R T)
(at level 36 , T, R at next level ,
format "{ 'measure' 'set' T '->' '\bar' R }" ) : ring_scope.
Section measure_signed .
Context d (R : numFieldType) (T : semiRingOfSetsType d).
Variable mu : {measure set T -> \bar R}.
Lemma measure_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).
Proof . exact : measure_ge0. Qed .
Canonical measure_snum S := Signed.mk (measure_snum_subproof S).
End measure_signed .
HB.factory Record isMeasure d
(R : realFieldType) (T : semiRingOfSetsType d) (mu : set T -> \bar R) := {
measure0 : mu set0 = 0 ;
measure_ge0 : forall x , 0 <= mu x ;
measure_semi_sigma_additive : semi_sigma_additive mu }.
HB.builders Context d (R : realFieldType) (T : semiRingOfSetsType d)
(mu : set T -> \bar R) of isMeasure d R T mu .
Let semi_additive_mu : semi_additive mu.
Proof .
apply : semi_sigma_additive_is_additive.
- exact : measure0.
- exact : measure_semi_sigma_additive.
Qed .
HB.instance Definition _ := isContent.Build d R T mu
measure_ge0 semi_additive_mu.
HB.instance Definition _ := isMeasure0.Build d R T mu measure_semi_sigma_additive.
HB.end .
Lemma eq_measure d (T : measurableType d) (R : realType)
(m1 m2 : {measure set T -> \bar R}) :
(m1 = m2 :> (set T -> \bar R)) -> m1 = m2.
Proof .
move : m1 m2 => [m1 [[m10 m1ge0 [m1sa]]]] [m2 [[+ + [+]]]] /= m1m2.
rewrite -{}m1m2 => m10' m1ge0' m1sa'; f_equal .
by rewrite (_ : m10' = m10)// (_ : m1ge0' = m1ge0)// (_ : m1sa' = m1sa).
Qed .
Section measure_lemmas .
Context d (R : realFieldType) (T : semiRingOfSetsType d).
Variable mu : {measure set T -> \bar R}.
Lemma measure_semi_bigcup A : (forall i : nat, measurable (A i)) ->
trivIset setT A -> measurable (\bigcup_n A n) ->
mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).
Proof . by move => Am Atriv /measure_semi_sigma_additive/cvg_lim<-//. Qed .
End measure_lemmas .
#[global ] Hint Extern 0 (_ set0 = 0 ) => solve [apply : measure0] : core.
#[global ] Hint Extern 0 (is_true (0 <= _)) => solve [apply : measure_ge0] : core.
Section measure_lemmas .
Context d (R : realFieldType) (T : measurableType d).
Variable mu : {measure set T -> \bar R}.
Lemma measure_sigma_additive : sigma_additive mu.
Proof .
by rewrite -semi_sigma_additiveE //; apply : measure_semi_sigma_additive.
Qed .
Lemma measure_bigcup (D : set nat) F : (forall i , D i -> measurable (F i)) ->
trivIset D F -> mu (\bigcup_(n in D) F n) = \sum_(i <oo | i \in D) mu (F i).
Proof .
move => mF tF; rewrite bigcup_mkcond measure_semi_bigcup.
- by rewrite [in RHS]eseries_mkcond; apply : eq_eseries => n _; case : ifPn.
- by move => i; case : ifPn => // /set_mem; exact : mF.
- by move /trivIset_mkcond : tF.
- by rewrite -bigcup_mkcond; apply : bigcup_measurable.
Qed .
End measure_lemmas .
Arguments measure_bigcup {d R T} _ _.
#[global ] Hint Extern 0 (sigma_additive _) =>
solve [apply : measure_sigma_additive] : core.
Definition finite_measure d (T : measurableType d) (R : numDomainType)
(mu : set T -> \bar R) :=
mu setT < +oo.
Lemma finite_measure_sigma_finite d (T : measurableType d) (R : realFieldType)
(mu : {measure set T -> \bar R}) :
finite_measure mu -> sigma_finite setT mu.
Proof .
exists (fun i => if i \in [set 0 %N] then setT else set0).
by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0 %N.
move => n; split ; first by case : ifPn.
by case : ifPn => // _; rewrite ?measure0 //; exact : finite_measure.
Qed .
HB.mixin Record isSigmaFinite d (R : numFieldType) (T : semiRingOfSetsType d)
(mu : set T -> \bar R) := {
sigma_finiteT : sigma_finite setT mu
}.
#[short(type="sigma_finite_content" )]
HB.structure Definition SigmaFiniteContent d R T :=
{mu of isSigmaFinite d R T mu & @Content d R T mu}.
Arguments sigma_finiteT {d R T} s.
Notation "{ 'sigma_finite_content' 'set' T '->' '\bar' R }" :=
(sigma_finite_content R T)
(at level 36 , T, R at next level ,
format "{ 'sigma_finite_content' 'set' T '->' '\bar' R }" )
: ring_scope.
#[global ]
Hint Resolve sigma_finiteT : core.
#[short(type="sigma_finite_measure" )]
HB.structure Definition SigmaFiniteMeasure d R T :=
{mu of isSigmaFinite d R T mu & @Measure d R T mu}.
Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" := (sigma_finite_measure R T)
(at level 36 , T, R at next level ,
format "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" ) : ring_scope.
Section pushforward_measure .
Local Open Scope ereal_scope.
Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2).
Variables (R : realFieldType) (m : {measure set T1 -> \bar R}).
Definition pushforward (mf : measurable_fun setT f) A := m (f @^-1 ` A).
Hypothesis mf : measurable_fun setT f.
Let pushforward0 : pushforward mf set0 = 0 .
Proof . by rewrite /pushforward preimage_set0 measure0. Qed .
Let pushforward_ge0 A : 0 <= pushforward mf A.
Proof . by apply : measure_ge0; rewrite -[X in measurable X]setIT; apply : mf. Qed .
Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf).
Proof .
move => F mF tF mUF; rewrite /pushforward preimage_bigcup.
apply : measure_semi_sigma_additive.
- by move => n; rewrite -[X in measurable X]setTI; exact : mf.
- apply /trivIsetP => /= i j _ _ ij; rewrite -preimage_setI.
by move /trivIsetP : tF => /(_ _ _ _ _ ij) ->//; rewrite preimage_set0.
- by rewrite -preimage_bigcup -[X in measurable X]setTI; exact : mf.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _
(pushforward mf) pushforward0 pushforward_ge0 pushforward_sigma_additive.
End pushforward_measure .
Section dirac_measure .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (a : T) (R : realFieldType).
Definition dirac (A : set T) : \bar R := (\1_ A a)%:E.
Let dirac0 : dirac set0 = 0 . Proof . by rewrite /dirac indic0. Qed .
Let dirac_ge0 B : 0 <= dirac B. Proof . by rewrite /dirac indicE. Qed .
Let dirac_sigma_additive : semi_sigma_additive dirac.
Proof .
move => F mF tF mUF; rewrite /dirac indicE; have [|aFn] /= := boolP (a \in _).
rewrite inE => -[n _ Fna].
have naF m : m != n -> a \notin F m.
move => mn; rewrite notin_set => Fma.
move /trivIsetP : tF => /(_ _ _ Logic.I Logic.I mn).
by rewrite predeqE => /(_ a)[+ _]; exact .
apply /cvg_ballP => _/posnumP[e]; near=> m.
have mn : (n < m)%N by near: m; exists n .+1 .
rewrite big_mkord (bigID (xpred1 (Ordinal mn)))//= big_pred1_eq/= big1/=.
by rewrite adde0 indicE mem_set//; exact : ballxx.
by move => j ij; rewrite indicE (negbTE (naF _ _)).
rewrite [X in X --> _](_ : _ = cst 0 ); first exact : cvg_cst.
apply /funext => n; rewrite big1// => i _; rewrite indicE; apply /eqP.
by rewrite eqe pnatr_eq0 eqb0; apply : contra aFn => /[!inE] aFn; exists i .
Unshelve . all : by end_near. Qed .
HB.instance Definition _ := isMeasure.Build _ _ _
dirac dirac0 dirac_ge0 dirac_sigma_additive.
End dirac_measure .
Arguments dirac {d T} _ {R}.
Notation "\d_ a" := (dirac a) : ring_scope.
Section dirac_lemmas_realFieldType .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realFieldType).
Lemma diracE a (A : set T) : \d_a A = (a \in A)%:R%:E :> \bar R.
Proof . by rewrite /dirac indicE. Qed .
Lemma dirac0 (a : T) : \d_a set0 = 0 :> \bar R.
Proof . by rewrite diracE in_set0. Qed .
Lemma diracT (a : T) : \d_a setT = 1 :> \bar R.
Proof . by rewrite diracE in_setT. Qed .
End dirac_lemmas_realFieldType .
Section dirac_lemmas .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Lemma finite_card_dirac (A : set T) : finite_set A ->
\esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.
Proof .
move => finA; rewrite esum_fset// (eq_fsbigr (cst 1 ))//.
by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite.
by move => i iA; rewrite diracE iA.
Qed .
Lemma infinite_card_dirac (A : set T) : infinite_set A ->
\esum_(i in A) \d_ i A = +oo :> \bar R.
Proof .
move => infA; apply /eqyP => r r0.
have [B BA Br] := infinite_set_fset `|ceil r| infA.
apply : esum_ge; exists [set ` B] => //; apply : (@le_trans _ _ `|ceil r|%:R%:E).
by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0 // ceil_ge.
move : Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply .
rewrite (eq_fsbigr (cst 1 ))/=; last first .
by move => i /[!inE] /BA /mem_set iA; rewrite diracE iA.
by rewrite fsbig_finite//= card_fset_sum1 sumEFin natr_sum// set_fsetK.
Qed .
End dirac_lemmas .
Section measure_sum .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m : {measure set T -> \bar R}^nat) (n : nat).
Definition msum (A : set T) : \bar R := \sum_(k < n) m k A.
Let msum0 : msum set0 = 0 . Proof . by rewrite /msum big1. Qed .
Let msum_ge0 B : 0 <= msum B. Proof . by rewrite /msum; apply : sume_ge0. Qed .
Let msum_sigma_additive : semi_sigma_additive msum.
Proof .
move => F mF tF mUF; rewrite [X in _ --> X](_ : _ =
lim (fun n => \sum_(0 <= i < n) msum (F i))).
by apply : is_cvg_ereal_nneg_natsum => k _; exact : sume_ge0.
rewrite nneseries_sum//; apply : eq_bigr => /= i _.
exact : measure_semi_bigcup.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ msum
msum0 msum_ge0 msum_sigma_additive.
End measure_sum .
Arguments msum {d T R}.
Section measure_zero .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Definition mzero (A : set T) : \bar R := 0 .
Let mzero0 : mzero set0 = 0 . Proof . by []. Qed .
Let mzero_ge0 B : 0 <= mzero B. Proof . by []. Qed .
Let mzero_sigma_additive : semi_sigma_additive mzero.
Proof .
move => F mF tF mUF; rewrite [X in X --> _](_ : _ = cst 0 ); first exact : cvg_cst.
by apply /funext => n; rewrite big1.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ mzero
mzero0 mzero_ge0 mzero_sigma_additive.
End measure_zero .
Arguments mzero {d T R}.
Lemma msum_mzero d (T : measurableType d) (R : realType)
(m_ : {measure set T -> \bar R}^nat) :
msum m_ 0 = mzero.
Proof . by apply /funext => A/=; rewrite /msum big_ord0. Qed .
Section measure_add .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m1 m2 : {measure set T -> \bar R}).
Definition measure_add := msum (fun n => if n is 0 %N then m1 else m2) 2 .
Lemma measure_addE A : measure_add A = m1 A + m2 A.
Proof . by rewrite /measure_add/= /msum 2 !big_ord_recl/= big_ord0 adde0. Qed .
End measure_add .
Section measure_scale .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realFieldType).
Variables (r : {nonneg R}) (m : {measure set T -> \bar R}).
Definition mscale (A : set T) : \bar R := r%:num%:E * m A.
Let mscale0 : mscale set0 = 0 . Proof . by rewrite /mscale measure0 mule0. Qed .
Let mscale_ge0 B : 0 <= mscale B.
Proof . by rewrite /mscale mule_ge0. Qed .
Let mscale_sigma_additive : semi_sigma_additive mscale.
Proof .
move => F mF tF mUF; rewrite [X in X --> _](_ : _ =
(fun n => (r%:num)%:E * \sum_(0 <= i < n) m (F i))); last first .
by apply /funext => k; rewrite ge0_sume_distrr.
rewrite /mscale; have [->|r0] := eqVneq r%:num 0 %R.
rewrite mul0e [X in X --> _](_ : _ = (fun => 0 )); first exact : cvg_cst.
by under eq_fun do rewrite mul0e.
by apply : cvgeMl => //; exact : measure_semi_sigma_additive.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ mscale
mscale0 mscale_ge0 mscale_sigma_additive.
End measure_scale .
Arguments mscale {d T R}.
Section measure_series .
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m : {measure set T -> \bar R}^nat) (n : nat).
Definition mseries (A : set T) : \bar R := \sum_(n <= k <oo) m k A.
Let mseries0 : mseries set0 = 0 .
Proof . by rewrite /mseries ereal_series eseries0. Qed .
Let mseries_ge0 B : 0 <= mseries B.
Proof .
by rewrite /mseries ereal_series nneseries_esum//; exact : esum_ge0.
Qed .
Let mseries_sigma_additive : semi_sigma_additive mseries.
Proof .
move => F mF tF mUF; rewrite [X in _ --> X](_ : _ =
lim (fun n => \sum_(0 <= i < n) mseries (F i))); last first .
rewrite [in LHS]/mseries.
transitivity (\sum_(n <= k <oo) \sum_(i <oo) m k (F i)).
rewrite 2 !ereal_series.
apply : (@eq_eseries _ (fun k => m k (\bigcup_n0 F n0))) => i ni.
exact : measure_semi_bigcup.
rewrite ereal_series nneseries_interchange//.
apply : (@eq_eseries R (fun j => \sum_(i <oo | (n <= i)%N) m i (F j))
(fun i => \sum_(n <= k <oo) m k (F i))).
by move => i _; rewrite ereal_series.
apply : is_cvg_ereal_nneg_natsum => k _.
by rewrite /mseries ereal_series; exact : nneseries_ge0.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ mseries
mseries0 mseries_ge0 mseries_sigma_additive.
End measure_series .
Arguments mseries {d T R}.
Definition mrestr d (T : measurableType d) (R : realFieldType) (D : set T)
(f : set T -> \bar R) (mD : measurable D) := fun X => f (X `&` D).
Section measure_restr .
Context d (T : measurableType d) (R : realFieldType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Local Notation restr := (mrestr mu mD).
Let restr0 : restr set0 = 0 %E. Proof . by rewrite /mrestr set0I measure0. Qed .
Let restr_ge0 (A : set _) : (0 <= restr A)%E.
Proof . by rewrite /restr; apply : measure_ge0; exact : measurableI. Qed .
Let restr_sigma_additive : semi_sigma_additive restr.
Proof .
move => F mF tF mU; pose FD i := F i `&` D.
have mFD i : measurable (FD i) by exact : measurableI.
have tFD : trivIset setT FD.
apply /trivIsetP => i j _ _ ij.
move /trivIsetP : tF => /(_ i j Logic.I Logic.I ij).
by rewrite /FD setIACA => ->; rewrite set0I.
by rewrite /restr setI_bigcupl; exact : measure_sigma_additive.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ restr
restr0 restr_ge0 restr_sigma_additive.
End measure_restr .
Section measure_count .
Context d (T : measurableType d) (R : realType).
Variables (D : set T) (mD : measurable D).
Definition counting (X : set T) : \bar R :=
if `[< finite_set X >] then (#|` fset_set X |)%:R%:E else +oo.
Let counting0 : counting set0 = 0 .
Proof . by rewrite /counting asboolT// fset_set0. Qed .
Let counting_ge0 (A : set _) : 0 <= counting A.
Proof . by rewrite /counting; case : ifPn; rewrite ?lee_fin // lee_pinfty. Qed .
Let counting_sigma_additive : semi_sigma_additive counting.
Proof .
move => F mF tF mU.
have [[i Fi]|infinF] := pselect (exists k , infinite_set (F k)).
have -> : counting (\bigcup_n F n) = +oo.
rewrite /counting asboolF//.
by apply : contra_not Fi; exact /sub_finite_set/bigcup_sup.
apply /cvgeyPge => M; near=> n.
have ni : (i < n)%N by near: n; exists i .+1 .
rewrite (bigID (xpred1 i))/= big_mkord (big_pred1 (Ordinal ni))//=.
rewrite [X in X + _]/counting asboolF// addye ?leey //.
by rewrite gt_eqF// (@lt_le_trans _ _ 0 )//; exact : sume_ge0.
have {infinF}finF : forall i , finite_set (F i) by exact /not_forallP.
pose u : nat^nat := fun n => #|` fset_set (F n) |.
have sumFE n : \sum_(i < n) counting (F i) =
#|` fset_set (\big[setU/set0]_(k < n) F k) |%:R%:E.
rewrite -trivIset_sum_card// natr_sum -sumEFin.
by apply : eq_bigr => // i _; rewrite /counting asboolT.
have [cvg_u|dvg_u] := pselect (cvg (nseries u)).
have [N _ Nu] : \forall n \near \oo, u n = 0 %N by apply : cvg_nseries_near.
rewrite [X in _ --> X](_ : _ = \sum_(i < N) counting (F i)); last first .
have -> : \bigcup_i (F i) = \big[setU/set0]_(i < N) F i.
rewrite (bigcupID (`I_N)) setTI bigcup_mkord.
rewrite [X in _ `|` X](_ : _ = set0) ?setU0 // bigcup0// => i [_ /negP].
by rewrite -leqNgt => /Nu/eqP/[!cardfs_eq0]/eqP/fset_set_set0 ->.
by rewrite /counting /= asboolT ?sumFE // -bigcup_mkord; exact : bigcup_finite.
rewrite -(cvg_shiftn N)/=.
rewrite (_ : (fun n => _) = (fun => \sum_(i < N) counting (F i))).
exact : cvg_cst.
apply /funext => n; rewrite /index_iota subn0 (addnC n) iotaD big_cat/=.
rewrite [X in _ + X](_ : _ = 0 ) ?adde0 .
by rewrite -{1 }(subn0 N) big_mkord.
rewrite add0n big_seq big1// => i /[!mem_iota] => /andP[NI iNn].
by rewrite /counting asboolT//= -/(u _) Nu.
have {dvg_u}cvg_F : (fun n => \sum_(i < n) counting (F i)) --> +oo.
rewrite (_ : (fun n => _) = [sequence (\sum_(0 <= i < n) (u i))%:R%:E]_n).
exact /cvgenyP/dvg_nseries.
apply /funext => n /=; under eq_bigr.
by rewrite /counting => i _; rewrite asboolT//; over .
by rewrite sumEFin natr_sum big_mkord.
have [UFoo|/contrapT[k UFk]] := pselect (infinite_set (\bigcup_n F n)).
rewrite /counting asboolF//.
by under eq_fun do rewrite big_mkord.
suff : false by [].
move : cvg_F =>/cvgeyPge/(_ k.+1 %:R) [K _] /(_ K (leqnn _)) /=; apply : contra_leT => _.
rewrite sumFE lte_fin ltr_nat ltnS.
have -> : k = #|` fset_set (\bigcup_n F n) |.
by apply /esym/card_eq_fsetP; rewrite fset_setK//; exists k .
apply /fsubset_leq_card; rewrite -fset_set_sub //.
- by move => /= t; rewrite -bigcup_mkord => -[m _ Fmt]; exists m .
- by rewrite -bigcup_mkord; exact : bigcup_finite.
- by exists k .
Unshelve . all : by end_near. Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ counting
counting0 counting_ge0 counting_sigma_additive.
End measure_count .
Lemma sigma_finite_counting (R : realType) :
sigma_finite [set : nat] (counting R).
Proof .
exists (fun n => `I_n.+1 ); first by apply /seteqP; split => //x _; exists x => /=.
by move => k; split => //; rewrite /counting/= asboolT// ltry.
Qed .
HB.instance Definition _ R :=
@isSigmaFinite.Build _ _ _ (counting R) (sigma_finite_counting R).
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 ->
\big[op/idx]_(i <- fset_set D) F (A i) =
\big[op/idx]_(X <- (A @` fset_set D)%fset) F X.
Proof .
elim /Pchoice: R => R in idx op F *.
move => Dfin Atriv F0; symmetry .
pose D' := [fset i in fset_set D | A i != set0]%fset.
transitivity (\big[op/idx]_(X <- (A @` D')%fset) F X).
apply : perm_big_supp; rewrite uniq_perm ?filter_uniq //=.
move => X; rewrite !mem_filter; case : (eqVneq (F X) idx) => //= FXNidx.
apply /imfsetP/imfsetP=> -[i/=]; rewrite ?(inE, in_fset_set)//=.
move => Di XAi; exists i ; rewrite // !(inE, in_fset_set)//=.
by rewrite (mem_set Di)/= -XAi; apply : contra_neq FXNidx => ->.
by move => /andP[Di AiN0] XAi; exists i ; rewrite ?in_fset_set .
rewrite big_imfset//=; last first .
move => i j; rewrite !(inE, in_fset_set)//= => /andP[+ +] /andP[+ +].
rewrite !inE => Di /set0P[x Aix] Dj _ Aij.
by apply : (Atriv _ _ Di Dj); exists x ; split => //; rewrite -Aij.
apply : perm_big_supp; rewrite uniq_perm ?filter_uniq //= => i.
rewrite !mem_filter; case : (eqVneq (F (A i)) idx) => //= FAiidx.
rewrite !(in_fset_set, inE)//=; case : (boolP (i \in D)) => //= Di.
by apply : contra_neq FAiidx => ->.
Qed .
Section covering .
Context {T : Type }.
Implicit Type (C : forall I , set (set I)).
Implicit Type (P : forall I , set I -> set (I -> set T)).
Definition covered_by C P :=
[set X : set T | exists I D A , [/\ C I D, P I D A & X = \bigcup_(i in D) A i]].
Lemma covered_bySr C P P' : (forall I D A , P I D A -> P' I D A) ->
covered_by C P `<=` covered_by C P'.
Proof .
by move => PP' X [I [D [A [CX PX ->]]]]; exists I , D, A; split => //; apply : PP'.
Qed .
Lemma covered_byP C P I D A : C I D -> P I D A ->
covered_by C P (\bigcup_(i in D) A i).
Proof . by move => CID PIDA; exists I , D, A. Qed .
Lemma covered_by_finite P :
(forall I (D : set I) A , (forall i , D i -> A i = set0) -> P I D A) ->
(forall (I : pointedType) D A , finite_set D -> P I D A ->
P nat `I_#|` fset_set D| (A \o nth point (fset_set D))) ->
covered_by (@finite_set) P =
[set X : set T | exists n A , [/\ P nat `I_n A & X = \bigcup_(i < n) A i]].
Proof .
move => P0 Pc; apply /predeqP=> X; rewrite /covered_by /cover/=; split ; last first .
by move => [n [A [Am ->]]]; exists nat , `I_n, A; split .
case ; elim /Ppointed=> I [D [A [Dfin Am ->]]].
exists 0 %N, (fun => set0); split ; first by rewrite II0; apply : P0.
by rewrite //= emptyE II0 !bigcup0.
exists #|`fset_set D|, (A \o nth point (fset_set D)).
split ; first exact : Pc.
by rewrite -bigsetU_fset_set// (big_nth point) big_mkord bigcup_mkord.
Qed .
Lemma covered_by_countable P :
(forall I (D : set I) A , (forall i , D i -> A i = set0) -> P I D A) ->
(forall (I : choiceType) (D : set I) (A : I -> set T) (f : nat -> I),
set_surj [set : nat] D f ->
P I D A -> P nat [set : nat] (A \o f)) ->
covered_by (@countable) P =
[set X : set T | exists A , [/\ P nat [set : nat] A & X = \bigcup_i A i]].
Proof .
move => P0 Pc; apply /predeqP=> X; rewrite /covered_by /cover/=; split ; last first .
by move => [A [Am ->]]; exists nat , [set : nat], A; split .
case ; elim /Ppointed=> I [D [A [Dcnt Am ->]]].
exists (fun => set0); split ; first exact : P0.
by rewrite emptyE bigcup_set0 bigcup0.
have /pfcard_geP[->|[f]] := Dcnt.
exists (fun => set0); split ; first exact : P0.
by rewrite !bigcup_set0 bigcup0.
pose g := [splitsurjfun of split f].
exists (A \o g); split => /=; first exact : Pc Am.
apply /predeqP=> x; split => [[i Di Aix]|[n _ Afnx]].
by exists (g ^-1 %FUN i) => //=; rewrite invK// inE.
by exists (g n ) => //; apply : funS.
Qed .
End covering .
Module SetRing .
Definition type (T : Type ) := T.
Definition display : measure_display -> measure_display. Proof . by []. Qed .
Section SetRing .
Context d {T : semiRingOfSetsType d}.
Notation rT := (type T).
Canonical ring_eqType := EqType rT ptclass.
Canonical ring_choiceType := ChoiceType rT ptclass.
Canonical ring_ptType := PointedType rT ptclass.
#[export]
HB.instance Definition _ := isRingOfSets.Build (display d) rT ptclass
(@setring0 T measurable) (@setringU T measurable) (@setringDI T measurable).
Local Notation "d .-ring" := (display d) (at level 1 , format "d .-ring" ).
Local Notation "d .-ring.-measurable" :=
((d%mdisp.-ring ).-measurable : set (set (type _))).
Local Definition measurable_fin_trivIset : set (set T) :=
[set A | exists B : set (set T),
[/\ A = \bigcup_(X in B) X, forall X : set T, B X -> measurable X,
finite_set B & trivIset B id]].
Lemma ring_measurableE : d.-ring .-measurable = measurable_fin_trivIset.
Proof .
apply /seteqP; split ; last first .
move => _ [B [-> Bm Bfin Btriv]]; apply : fin_bigcup_measurable => //.
by move => i Di; apply : sub_gen_smallest; apply : Bm.
have mdW A : measurable A -> measurable_fin_trivIset A.
move => Am; exists [set A]; split ; do ?by [rewrite bigcup_set1|move => ? ->|].
by move => ? ? -> ->.
have mdI : setI_closed measurable_fin_trivIset.
move => _ _ [A [-> Am Afin Atriv]] [B [-> Bm Bfin Btriv]].
rewrite setI_bigcupl; under eq_bigcupr do rewrite setI_bigcupr.
rewrite bigcup_bigcup -(bigcup_image _ _ id).
eexists ; split ; [reflexivity | | exact /finite_image/finite_setM |].
by move => _ [X [? ?] <-]; apply : measurableI; [apply : Am|apply : Bm].
apply : trivIset_sets => -[a b] [a' b']/= [Xa Xb] [Xa' Xb']; rewrite setIACA.
by move => [x [Ax Bx]]; rewrite (Atriv a a') 1 ?(Btriv b b')//; exists x .
have mdisj_bigcap : finN0_bigcap_closed measurable_fin_trivIset.
exact /finN0_bigcap_closedP/mdI.
have mDbigcup I (D : set I) (A : set T) (B : I -> set T) : finite_set D ->
measurable A -> (forall i , D i -> measurable (B i)) ->
measurable_fin_trivIset (A `\` \bigcup_(i in D) B i).
have [->|/set0P D0] := eqVneq D set0.
by rewrite bigcup0// setD0 => *; apply : mdW.
move => Dfin Am Bm; rewrite -bigcupDr//; apply : mdisj_bigcap=> // i Di.
by have [F [Ffin Fm -> ?]] := semi_measurableD A (B i) Am (Bm _ Di); exists F .
have mdU : fin_trivIset_closed measurable_fin_trivIset.
elim /Pchoice=> I D F Dfin Ftriv Fm.
have /(_ _ (set_mem _))/cid-/(all_sig_cond_dep (fun => set0))
[G /(_ _ (mem_set _))GP] := Fm _ _.
under eq_bigcupr => i Di do case : (GP i Di) => ->.
rewrite bigcup_bigcup_dep -(bigcup_image _ _ id); eexists ; split => //.
- by move => _ [i [Di Gi] <-]; have [_ + _ _] := GP i.1 Di; apply .
- by apply : finite_image; apply : finite_setMR=> // i Di; have [] := GP i Di.
apply : trivIset_sets => -[i X] [j Y] /= [Di Gi] [Dj Gj] XYN0.
suff eqij : i = j.
by rewrite {i}eqij in Di Gi *; have [_ _ _ /(_ _ _ _ _ XYN0)->] := GP j Dj.
apply : Ftriv => //; have [-> _ _ _] := GP j Dj; have [-> _ _ _] := GP i Di.
by case : XYN0 => [x [Xx Yx]]; exists x ; split ; [exists X |exists Y ].
have mdDI : setDI_closed measurable_fin_trivIset.
move => A B mA mB; have [F [-> Fm Ffin Ftriv]] := mA.
have [F' [-> F'm F'fin F'triv]] := mB.
have [->|/set0P F'N0] := eqVneq F' set0.
by rewrite bigcup_set0 setD0; exists F .
rewrite setD_bigcupl; apply : mdU => //; first by apply : trivIset_setIr.
move => X DX; rewrite -bigcupDr//; apply : mdisj_bigcap => //.
move => Y DY; case : (semi_measurableD X Y); [exact : Fm|exact : F'm|].
by move => G [Gfin Gm -> Gtriv]; exists G .
apply : smallest_sub => //; split => //; first by apply : mdW.
move => A B mA mB; rewrite -(setUIDK B A) setUA [X in X `|` _]setUidl//.
rewrite -bigcup2inE; apply : mdU => //; last by move => [|[]]// _; apply : mdDI.
by move => [|[]]// [|[]]//= _ _ []; rewrite setDE ?setIA => X [] []//.
Qed .
Lemma ring_finite_set (A : set rT) : measurable A -> exists B : set (set T),
[/\ finite_set B,
(forall X , B X -> X !=set0),
trivIset B id,
(forall X : set T, X \in B -> measurable X) &
A = \bigcup_(X in B) X].
Proof .
rewrite ring_measurableE => -[B [-> Bm Bfin Btriv]].
exists (B `&` [set X | X != set0]); split .
- by apply : sub_finite_set Bfin; exact : subIsetl.
- by move => ?/= [_ /set0P].
- by move => X Y/= [XB _] [YB _]; exact : Btriv.
- by move => X/= /[!inE] -[] /Bm.
rewrite bigcup_mkcondr; apply : eq_bigcupr => X Bx; case : ifPn => //.
by rewrite notin_set/= => /negP/negPn/eqP.
Qed .
Definition decomp (A : set rT) : set (set T) :=
if A == set0 then [set set0] else
if pselect (measurable A) is left mA then projT1 (cid (ring_finite_set mA))
else [set A].
Lemma decomp_finite_set (A : set rT) : finite_set (decomp A).
Proof .
rewrite /decomp; case : ifPn => // A0; case : pselect => // X.
by case : cid => /= ? [].
Qed .
Lemma decomp_triv (A : set rT) : trivIset (decomp A) id.
Proof .
rewrite /decomp; case : ifP => _; first by move => i j/= -> ->.
case : pselect => // Am; first by case : cid => //= ? [].
by move => i j /= -> ->.
Qed .
Hint Resolve decomp_triv : core.
Lemma all_decomp_neq0 (A : set rT) :
A !=set0 -> (forall X , decomp A X -> X !=set0).
Proof .
move => /set0P AN0; rewrite /decomp/= (negPf AN0).
case : pselect => //= Am; first by case : cid => //= ? [].
by move => X ->; exact /set0P.
Qed .
Lemma decomp_neq0 (A : set rT) X : A !=set0 -> X \in decomp A -> X !=set0.
Proof . by move => /all_decomp_neq0/(_ X) /[!inE]. Qed .
Lemma decomp_measurable (A : set rT) (X : set T) :
measurable A -> X \in decomp A -> measurable X.
Proof .
rewrite /decomp; case : ifP => _; first by rewrite inE => _ ->.
by case : pselect => // Am _; case : cid => //= ? [_ _ _ + _]; apply .
Qed .
Lemma cover_decomp (A : set rT) : \bigcup_(X in decomp A) X = A.
Proof .
rewrite /decomp; case : ifP => [/eqP->|_]; first by rewrite bigcup0.
case : pselect => // Am; first by case : cid => //= ? [].
by rewrite bigcup_set1.
Qed .
Lemma decomp_sub (A : set rT) (X : set T) : X \in decomp A -> X `<=` A.
Proof .
rewrite /decomp; case : ifP => _; first by rewrite inE/= => ->//.
case : pselect => //= Am; last by rewrite inE => ->.
by case : cid => //= D [_ _ _ _ ->] /[!inE] XD; apply : bigcup_sup.
Qed .
Lemma decomp_set0 : decomp set0 = [set set0].
Proof . by rewrite /decomp eqxx. Qed .
Lemma decompN0 (A : set rT) : decomp A != set0.
Proof .
rewrite /decomp; case : ifPn => [_|AN0]; first by apply /set0P; exists set0 .
case : pselect=> //= Am; last by apply /set0P; exists A .
case : cid=> //= D [_ _ _ _ Aeq]; apply : contra_neq AN0; rewrite Aeq => ->.
by rewrite bigcup_set0.
Qed .
Definition measure (R : numDomainType) (mu : set T -> \bar R)
(A : set rT) : \bar R := \sum_(X \in decomp A) mu X.
Section content .
Context {R : realFieldType} (mu : {content set T -> \bar R}).
Local Notation Rmu := (measure mu).
Arguments big_trivIset {I D T R idx op} A F.
Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) :
finite_set D -> trivIset D F -> (forall i , i \in D -> measurable (F i)) ->
Rmu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
Proof .
move => Dfin Ftriv Fm; rewrite /measure .
have mUD : measurable (\bigcup_(i in D) F i : set rT).
apply : fin_bigcup_measurable => // *; apply : sub_gen_smallest.
exact /Fm/mem_set.
have [->|/set0P[i0 Di0]] := eqVneq D set0.
by rewrite bigcup_set0 decomp_set0 fsbig_set0 fsbig_set1.
set E := decomp _; have Em X := decomp_measurable mUD X.
transitivity (\sum_(X \in E) \sum_(i \in D) mu (X `&` F i)).
apply : eq_fsbigr => /= X XE; have XDF : X = \bigcup_(i in D) (X `&` F i).
by rewrite -setI_bigcupr setIidl//; exact : decomp_sub.
rewrite [in LHS]XDF content_fin_bigcup//; first exact : trivIset_setIl.
- by move => i /mem_set Di; apply : measurableI; [exact : Em|exact : Fm].
- by rewrite -XDF; exact : Em.
rewrite exchange_fsbig //; last exact : decomp_finite_set.
apply : eq_fsbigr => i Di; have Feq : F i = \bigcup_(X in E) (X `&` F i).
rewrite -setI_bigcupl setIidr// cover_decomp.
by apply /bigcup_sup; exact : set_mem.
rewrite -content_fin_bigcup -?Feq //; [exact /decomp_finite_set| | |exact /Fm].
- exact /trivIset_setIr/decomp_triv.
- by move => X /= XE; apply : measurableI; [apply : Em; rewrite inE | exact : Fm].
Qed .
Lemma RmuE (A : set T) : measurable A -> Rmu A = mu A.
Proof .
move => Am; rewrite -[A in LHS](@bigcup_set1 _ unit _ tt).
by rewrite Rmu_fin_bigcup// ?fsbig_set1 // => -[].
Qed .
Let Rmu0 : Rmu set0 = 0 .
Proof .
rewrite -(bigcup_set0 (fun _ : void => set0)).
by rewrite Rmu_fin_bigcup// fsbig_set0.
Qed .
Lemma Rmu_ge0 A : Rmu A >= 0 .
Proof . by rewrite sume_ge0. Qed .
Lemma Rmu_additive : semi_additive Rmu.
Proof .
apply /(additive2P Rmu0) => // A B /ring_finite_set[/= {}A [? _ Atriv Am ->]].
move => /ring_finite_set[/= {}B [? _ Btriv Bm ->]].
rewrite -subset0 => coverAB0.
have AUBfin : finite_set (A `|` B) by rewrite finite_setU.
have AUBtriv : trivIset (A `|` B) id.
move => X Y [] ABX [] ABY; do ?by [exact : Atriv|exact : Btriv].
by move => [u [Xu Yu]]; case : (coverAB0 u); split ; [exists X |exists Y ].
by move => [u [Xu Yu]]; case : (coverAB0 u); split ; [exists Y |exists X ].
rewrite -bigcup_setU !Rmu_fin_bigcup//=.
- rewrite fsbigU//= => [X /= [XA XB]]; have [->//|/set0P[x Xx]] := eqVneq X set0.
by case : (coverAB0 x); split ; exists X .
- by move => X /set_mem [|] /mem_set ?; [exact : Am|exact : Bm].
Qed .
#[export]
HB.instance Definition _ := isContent.Build _ _ _ Rmu Rmu_ge0 Rmu_additive.
End content .
End SetRing .
Module Exports .
Canonical ring_eqType .
Canonical ring_choiceType .
Canonical ring_ptType .
HB.reexport SetRing.
End Exports .
End SetRing .
Export SetRing.Exports.
Notation "d .-ring" := (SetRing.display d)
(at level 1 , format "d .-ring" ) : measure_display_scope.
Notation "d .-ring.-measurable" :=
((d%mdisp.-ring ).-measurable : set (set (SetRing.type _))) : classical_set_scope.
Lemma le_measure d (R : realFieldType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}) :
{in measurable &, {homo mu : A B / A `<=` B >-> (A <= B)%E}}.
Proof .
move => A B; rewrite ?inE => mA mB AB; have [|muBfin] := leP +oo%E (mu B).
by rewrite leye_eq => /eqP ->; rewrite leey.
rewrite -[leRHS]SetRing.RmuE// -[B](setDUK AB) measureU/= ?setDIK //.
- by rewrite SetRing.RmuE ?lee_addl .
- exact : sub_gen_smallest.
- by apply : measurableD; exact : sub_gen_smallest.
Qed .
Lemma measure_le0 d (T : semiRingOfSetsType d) (R : realFieldType)
(mu : {content set T -> \bar R}) (A : set T) :
(mu A <= 0 )%E = (mu A == 0 )%E.
Proof . by case : ltgtP (measure_ge0 mu A). Qed .
Section more_content_semiring_lemmas .
Context d (R : realFieldType) (T : semiRingOfSetsType d).
Variable mu : {content set T -> \bar R}.
Lemma content_sub_additive : sub_additive mu.
Proof .
move => X A n Am Xm XA; pose B i := A\_`I_n i `&` X.
have XE : X = \big[setU/set0]_(i < n) B i.
rewrite -big_distrl/= setIidr// => x /XA/=.
by rewrite -!bigcup_mkord => -[k nk Ax]; exists k ; rewrite // patchT ?inE .
have Bm i : measurable (B i).
case : (ltnP i n) => ltin; last by rewrite /B patchC ?inE ?set0I //= leq_gtF.
by rewrite /B ?patchT ?inE //; apply : measurableI => //; apply : Am.
have subBA i : B i `<=` A i.
by rewrite /B/patch; case : ifP; rewrite // set0I//= => _ ?.
have subDUB i : seqDU B i `<=` A i by move => x [/subBA].
have DUBm i : measurable (seqDU B i : set (SetRing.type T)).
apply : measurableD; first exact : sub_gen_smallest.
by apply : bigsetU_measurable => ? _; apply : sub_gen_smallest.
have DU0 i : (i >= n)%N -> seqDU B i = set0.
move => leni; rewrite -subset0 => x []; rewrite /B patchC ?inE /= ?leq_gtF //.
by case .
rewrite -SetRing.RmuE// XE bigsetU_seqDU measure_bigsetU//.
rewrite [leRHS](big_ord_widen n (mu \o A))//= [leRHS]big_mkcond/=.
rewrite lee_sum => // i _; case : ltnP => ltin; last by rewrite DU0 ?measure0 .
rewrite -[leRHS]SetRing.RmuE; last exact : Am.
by rewrite le_measure ?inE //=; last by apply : sub_gen_smallest; apply : Am.
Qed .
Lemma content_sub_fsum (I : choiceType) D (A : set T) (A_ : I -> set T) :
finite_set D ->
(forall i , D i -> measurable (A_ i)) ->
measurable A ->
A `<=` \bigcup_(i in D) A_ i -> mu A <= \sum_(i \in D) mu (A_ i).
Proof .
elim /choicePpointed: I => I in A_ D *.
rewrite !emptyE bigcup_set0// subset0 => _ _ _ ->.
by rewrite measure0 fsbig_set0.
move => Dfin A_m Am Asub; have [n /ppcard_eqP[f]] := Dfin.
rewrite (reindex_fsbig f^-1 %FUN `I_n)//= -fsbig_ord.
rewrite (@content_sub_additive A (A_ \o f^-1 %FUN))//=.
by move => i ltin; apply : A_m; apply : funS.
rewrite (fsbig_ord _ _ (A_ \o f^-1 %FUN))/= -(reindex_fsbig _ _ D)//=.
by rewrite fsbig_setU.
Qed .
(* (* alternative proof *) *)
(* Theorem semi_Boole_inequality : sub_additive mu. *)
(* Proof. *)
(* move=> X A n Am Xm Xsub; rewrite -SetRing.RmuE//. *)
(* under eq_bigr => i do [rewrite -SetRing.RmuE; do ?by apply: Am=> /=]. *)
(* pose rT := SetRing.type T. *)
(* have {}Am i : `I_n i -> measurable (A i : set rT). *)
(* by move=> *; apply/SetRing.measurableW/Am => /=. *)
(* have {}Xm : measurable (X : set rT) by exact: SetRing.measurableW. *)
(* pose ammu := [additive_measure of SetRing.measure mu]. *)
(* rewrite (le_trans (le_measure ammu _ _ Xsub)) ?inE// {Xsub}. *)
(* by rewrite -bigcup_mkord; apply: fin_bigcup_measurable. *)
(* elim: n Am Xm => [|n IHn] Am Xm; first by rewrite !big_ord0 measure0. *)
(* have Anm : measurable (A n : set rT) by apply: Am => /=. *)
(* set B := \big[setU/set0]_(i < n) A i. *)
(* set C := \big[setU/set0]_(i < n.+1) A i. *)
(* have -> : C = B `|` (A n `\` B). *)
(* suff -> : A n `\` B = C `\` B by rewrite setDUK// /C big_ord_recr/=; left. *)
(* by rewrite /C big_ord_recr/= !setDE setIUl -!setDE setDv set0U. *)
(* have Bm : measurable (B : set rT). *)
(* by rewrite -[B]bigcup_mkord; apply: fin_bigcup_measurable => //= i /ltnW/Am. *)
(* rewrite measureU // ?setDIK//; last exact: measurableD. *)
(* rewrite (@le_trans _ _ (ammu B + ammu (A n))) // ?lee_add2l //; last first. *)
(* by rewrite big_ord_recr /= lee_add2r// IHn// => i /ltnW/Am. *)
(* by rewrite le_measure // ?inE// ?setDE//; exact: measurableD. *)
(* Qed. *)
End more_content_semiring_lemmas .
Section content_ring_lemmas .
Context d (R : realType) (T : ringOfSetsType d).
Variable mu : {content set T -> \bar R}.
Lemma content_ring_sup_sigma_additive (A : nat -> set T) :
(forall i , measurable (A i)) -> measurable (\bigcup_i A i) ->
trivIset [set : nat] A -> \sum_(i <oo) mu (A i) <= mu (\bigcup_i A i).
Proof .
move => Am UAm At; rewrite lime_le//; first exact : is_cvg_nneseries.
near=> n; rewrite big_mkord -measure_bigsetU//= le_measure ?inE //=.
- exact : bigsetU_measurable.
- by rewrite -bigcup_mkord; apply : bigcup_sub => i lein; apply : bigcup_sup.
Unshelve . all : by end_near. Qed .
Lemma content_ring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive mu.
Proof .
move => mu_sub A Am Atriv UAm.
suff <- : \sum_(i <oo) mu (A i) = mu (\bigcup_n A n) by exact : is_cvg_nneseries.
by apply /eqP; rewrite eq_le mu_sub// ?content_ring_sup_sigma_additive .
Qed .
End content_ring_lemmas .
Section ring_sigma_sub_additive_content .
Context d (R : realType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}).
Local Notation Rmu := (SetRing.measure mu).
Import SetRing.
Lemma ring_sigma_sub_additive : sigma_sub_additive mu -> sigma_sub_additive Rmu.
Proof .
move => muS; move => /= D A Am Dm Dsub.
rewrite /Rmu -(eq_eseries (fun _ _ => esum_fset _ _))//; last first .
by move => *; exact : decomp_finite_set.
rewrite nneseries_esum ?esum_esum //=; last by move => *; rewrite esum_ge0.
set K := _ `*`` _.
have /ppcard_eqP[f] : (K #= [set : nat])%card.
apply : cardMR_eq_nat => [|i].
by rewrite (_ : [set _ | true] = setT)//; exact /predeqP.
split ; first by apply /finite_set_countable; exact : decomp_finite_set.
exact /set0P/decompN0.
have {Dsub} : D `<=` \bigcup_(k in K) k.2 .
apply : (subset_trans Dsub); apply : bigcup_sub => i _.
rewrite -[A i]cover_decomp; apply : bigcup_sub => X/= XAi.
by move => x Xx; exists (i , X).
rewrite -(image_eq [bij of f^-1 %FUN])/=.
rewrite (esum_set_image _ f^-1 )//= bigcup_image => Dsub.
have DXsub X : X \in decomp D -> X `<=` \bigcup_i ((f^-1 %FUN i).2 `&` X).
move => XD; rewrite -setI_bigcupl -[Y in Y `<=` _](setIidr (decomp_sub XD)).
by apply : setSI.
have mf i : measurable ((f^-1 )%function i).2 .
have [_ /mem_set/decomp_measurable] := 'invS_f (I : setT i).
by apply ; exact : Am.
have mfD i X : X \in decomp D -> measurable (((f^-1 )%FUN i).2 `&` X : set T).
by move => XD; apply : measurableI; [exact : mf|exact : (decomp_measurable _ XD)].
apply : (@le_trans _ _
(\sum_(i <oo) \sum_(X <- fset_set (decomp D)) mu ((f^-1 %FUN i).2 `&` X))).
rewrite nneseries_sum// fsbig_finite/=; last exact : decomp_finite_set.
rewrite [leLHS]big_seq_cond [leRHS]big_seq_cond.
rewrite lee_sum// => X /[!(andbT,in_fset_set)]; last exact : decomp_finite_set.
move => XD; have Xm := decomp_measurable Dm XD.
by apply : muS => // [i|]; [exact : mfD|exact : DXsub].
apply : lee_lim => /=; do ?apply : is_cvg_nneseries=> //.
by move => n _; exact : sume_ge0.
near=> n; rewrite [n in _ <= n]big_mkcond; apply : lee_sum => i _.
rewrite ifT ?inE //.
under eq_big_seq.
move => x; rewrite in_fset_set=> [xD|]; last exact : decomp_finite_set.
rewrite -RmuE//; last exact : mfD.
over .
rewrite -fsbig_finite/=; last exact : decomp_finite_set.
rewrite -measure_fin_bigcup//=.
- rewrite -setI_bigcupr (cover_decomp D) -[leRHS]RmuE// ?le_measure ?inE //.
by apply : measurableI => //; apply : sub_gen_smallest; apply : mf.
by apply : sub_gen_smallest; apply : mf.
- exact : decomp_finite_set.
- by apply : trivIset_setIl; apply : decomp_triv.
- by move => X /= XD; apply : sub_gen_smallest; apply : mfD; rewrite inE.
Unshelve . all : by end_near. Qed .
Lemma ring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive Rmu.
Proof .
move => mu_sub; apply : content_ring_sigma_additive.
by apply : ring_sigma_sub_additive.
Qed .
End ring_sigma_sub_additive_content .
Section more_premeasure_ring_lemmas .
Context d (R : realType) (T : semiRingOfSetsType d).
Variable mu : {measure set T -> \bar R}.
Import SetRing.
Lemma measure_sigma_sub_additive : sigma_sub_additive mu.
Proof .
move => X A Am Xm XA; pose B i := A i `&` X.
have XE : X = \bigcup_i B i by rewrite -setI_bigcupl setIidr.
have Bm i : measurable (B i) by rewrite /B; apply : measurableI.
have subBA i : B i `<=` A i by rewrite /B.
have subDUB i : seqDU B i `<=` A i by move => x [/subBA].
have DUBm i : measurable (seqDU B i : set (SetRing.type T)).
by apply : measurableD => //;
do 1 ?apply : bigsetU_measurable => *; apply : sub_gen_smallest.
rewrite XE; move : (XE); rewrite seqDU_bigcup_eq.
under eq_bigcupr do rewrite -[seqDU B _]cover_decomp//.
rewrite bigcup_bigcup_dep; set K := _ `*`` _.
have /ppcard_eqP[f] : (K #= [set : nat])%card.
apply : cardMR_eq_nat=> // i; split ; last by apply /set0P; rewrite decompN0.
exact /finite_set_countable/decomp_finite_set.
pose f' := f^-1 %FUN; rewrite -(image_eq [bij of f'])/= bigcup_image/=.
pose g n := (f' n).2 ; have fVtriv : trivIset [set : nat] g.
move => i j _ _; rewrite /g.
have [/= _ f'iB] : K (f' i) by apply : funS.
have [/= _ f'jB] : K (f' j) by apply : funS.
have [f'ij|f'ij] := eqVneq (f' i).1 (f' j).1 .
move => /(decomp_triv f'iB)/=; rewrite f'ij => /(_ f'jB) f'ij2.
apply : 'inj_f'; rewrite ?inE //= -!/(f' _); move : f'ij f'ij2.
by case : (f' i) (f' j) => [? ?] [? ?]//= -> ->.
move => [x [f'ix f'jx]]; have Bij := @trivIset_seqDU _ B (f' i).1 (f' j).1 I I.
rewrite Bij ?eqxx // in f'ij; exists x ; split .
- by move /mem_set : f'iB => /decomp_sub; apply .
- by move /mem_set : f'jB => /decomp_sub; apply .
have g_inj : set_inj [set i | g i != set0] g.
by apply : trivIset_inj=> [i /set0P//|]; apply : sub_trivIset fVtriv.
move => XEbig; rewrite measure_semi_bigcup//= -?XEbig //; last first .
move => i; have [/= _ /mem_set] : K (f' i) by apply : funS.
exact : decomp_measurable.
rewrite [leLHS](_ : _ = \sum_(i <oo | g i != set0) mu (g i)); last first .
rewrite !nneseries_esum// esum_mkcond [RHS]esum_mkcond; apply : eq_esum.
move => i _; rewrite ifT ?inE //=; case : ifPn => //.
by rewrite notin_set /= -/(g _) => /negP/negPn/eqP ->.
rewrite -(esum_pred_image mu g)//.
rewrite [leLHS](_ : _ = \esum_(X in range g) mu X); last first .
rewrite esum_mkcond [RHS]esum_mkcond; apply : eq_esum.
move => Y _; case : ifPn; rewrite ?(inE, notin_set)/=.
by move => [i giN0 giY]; rewrite ifT// ?inE //=; exists i .
move => Ngx; case : ifPn; rewrite ?(inE, notin_set)//=.
move => [i _ giY]; apply : contra_not_eq Ngx; rewrite -giY => mugi.
by exists i => //; apply : contra_neq mugi => ->; rewrite measure0.
have -> : range g = \bigcup_i (decomp (seqDU B i)).
apply /predeqP => /= Y; split => [[n _ gnY]|[n _ /= YBn]].
have [/= _ f'nB] : K (f' n) by apply : funS.
by exists (f' n ).1 => //=; rewrite -gnY.
by exists (f (n, Y)) => //; rewrite /g /f' funK//= inE.
rewrite esum_bigcup//; last first .
move => i j /=.
have [->|/set0P DUBiN0] := eqVneq (seqDU B i) set0.
rewrite decomp_set0 ?set_fset1 => /negP[].
apply /eqP/predeqP=> x; split => [[Y/=->]|->]//; first by rewrite measure0.
by exists set0 .
have [->|/set0P DUBjN0] := eqVneq (seqDU B j) set0.
rewrite decomp_set0 ?set_fset1 => _ /negP[].
apply /eqP/predeqP=> x; split => [[Y/=->]|->]//=; first by rewrite measure0.
by exists set0 .
move => _ _ [Y /= [/[dup] +]].
move => /mem_set /decomp_sub YBi /mem_set + /mem_set /decomp_sub YBj.
move => /(decomp_neq0 DUBiN0) [y Yy].
apply : (@trivIset_seqDU _ B) => //; exists y .
by split => //; [exact : YBi|exact : YBj].
rewrite nneseries_esum// set_true le_esum// => i _.
rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j); last first .
by rewrite esum_fset//; exact : decomp_finite_set.
rewrite -SetRing.Rmu_fin_bigcup//=; last 3 first .
exact : decomp_finite_set.
exact : decomp_triv.
by move => ?; exact : decomp_measurable.
rewrite -[leRHS]SetRing.RmuE// le_measure//; last by rewrite cover_decomp.
- rewrite inE; apply : fin_bigcup_measurable; first exact : decomp_finite_set.
move => j /mem_set jdec; apply : sub_gen_smallest.
exact : decomp_measurable jdec.
- by rewrite inE; apply : sub_gen_smallest; exact : Am.
Qed .
End more_premeasure_ring_lemmas .
Section ring_sigma_content .
Context d (R : realType) (T : semiRingOfSetsType d)
(mu : {measure set T -> \bar R}).
Local Notation Rmu := (SetRing.measure mu).
Import SetRing.
Let ring_sigma_content : semi_sigma_additive Rmu.
Proof . exact /ring_sigma_additive/measure_sigma_sub_additive. Qed .
HB.instance Definition _ := isMeasure0.Build _ _ _ Rmu
ring_sigma_content.
End ring_sigma_content .
Lemma measureIl d (R : realFieldType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}) (A B : set T) :
measurable A -> measurable B -> (mu (A `&` B) <= mu A)%E.
Proof . by move => mA mB; rewrite le_measure ?inE //; apply : measurableI. Qed .
Lemma measureIr d (R : realFieldType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}) (A B : set T) :
measurable A -> measurable B -> (mu (A `&` B) <= mu B)%E.
Proof . by move => mA mB; rewrite le_measure ?inE //; apply : measurableI. Qed .
Lemma subset_measure0 d (T : semiRingOfSetsType d) (R : realType)
(mu : {content set T -> \bar R}) (A B : set T) :
measurable A -> measurable B -> A `<=` B ->
mu B = 0 %E -> mu A = 0 %E.
Proof .
move => mA mB AB B0; apply /eqP; rewrite eq_le measure_ge0// ?andbT -?B0 .
by apply : le_measure; rewrite ?inE .
Qed .
Section measureD .
Context d (R : realFieldType) (T : ringOfSetsType d).
Variable mu : {measure set T -> \bar R}.
Lemma measureDI A B : measurable A -> measurable B ->
mu A = mu (A `\` B) + mu (A `&` B).
Proof .
move => mA mB; rewrite -measure_semi_additive2.
- by rewrite -setDDr setDv setD0.
- exact : measurableD.
- exact : measurableI.
- by apply : measurableU; [exact : measurableD |exact : measurableI].
- by rewrite setDE setIACA setICl setI0.
Qed .
Lemma measureD A B : measurable A -> measurable B ->
mu A < +oo -> mu (A `\` B) = mu A - mu (A `&` B).
Proof .
move => mA mB mAoo.
rewrite (measureDI mA mB) addeK// fin_numE 1 ?gt_eqF 1 ?lt_eqF //.
- by rewrite (le_lt_trans _ mAoo)// le_measure // ?inE //; exact : measurableI.
- by rewrite (lt_le_trans _ (measure_ge0 _ _)).
Qed .
End measureD .
Lemma measureUfinr d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
(mu : {measure set T -> \bar R}):
measurable A -> measurable B -> (mu B < +oo)%E ->
mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
Proof .
move => Am Bm mBfin; rewrite -[B in LHS](setDUK (@subIsetl _ _ A)) setUA.
rewrite [A `|` _]setUidl; last exact : subIsetr.
rewrite measureU//=; do ?by apply :measurableD; do ?apply : measurableI.
rewrite measureD//; do ?exact : measurableI.
by rewrite addeA setIA setIid setIC.
by rewrite setDE setCI setIUr -!setDE setDv set0U setDIK.
Qed .
Lemma measureUfinl d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
(mu : {measure set T -> \bar R}):
measurable A -> measurable B -> (mu A < +oo)%E ->
mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
Proof . by move => *; rewrite setUC measureUfinr// setIC [(mu B + _)%E]addeC. Qed .
Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
(mu mu' : {measure set T -> \bar R}):
measurable A -> measurable B ->
mu A = mu' A -> mu B = mu' B -> mu (A `&` B) = mu' (A `&` B) ->
mu (A `|` B) = mu' (A `|` B).
Proof .
move => mA mB muA muB muAB; have [mu'ANoo|] := ltP (mu' A) +oo.
by rewrite !measureUfinl ?muA ?muB ?muAB .
rewrite leye_eq => /eqP mu'A; transitivity (+oo : \bar R); apply /eqP.
by rewrite -leye_eq -mu'A -muA le_measure ?inE //=; apply : measurableU.
by rewrite eq_sym -leye_eq -mu'A le_measure ?inE //=; apply : measurableU.
Qed .
Lemma null_set_setU d (R : realFieldType) (T : ringOfSetsType d)
(mu : {measure set T -> \bar R}) (A B : set T) :
measurable A -> measurable B -> mu A = 0 %E -> mu B = 0 %E -> mu (A `|` B) = 0 %E.
Proof .
move => mA mB A0 B0; rewrite measureUfinl ?A0 //= ?B0 ?add0e .
apply /eqP; rewrite oppe_eq0 -measure_le0/=; do ?exact : measurableI.
by rewrite -A0 measureIl.
Qed .
Lemma nondecreasing_cvg_mu d (R : realFieldType) (T : ringOfSetsType d)
(mu : {measure set T -> \bar R}) (F : (set T) ^nat) :
(forall i , measurable (F i)) -> measurable (\bigcup_n F n) ->
nondecreasing_seq F ->
mu \o F --> mu (\bigcup_n F n).
Proof .
move => mF mbigcupF ndF.
have Binter : trivIset setT (seqD F) := trivIset_seqD ndF.
have FBE : forall n , F n.+1 = F n `|` seqD F n.+1 := setU_seqD ndF.
have FE n : F n = \big[setU/set0]_(i < n.+1 ) (seqD F) i := eq_bigsetU_seqD n ndF.
rewrite eq_bigcup_seqD.
have mB i : measurable (seqD F i) by elim : i => * //=; apply : measurableD.
apply : cvg_trans (measure_semi_sigma_additive _ mB Binter _); last first .
by rewrite -eq_bigcup_seqD.
apply : (@cvg_trans _ [filter of (fun n => \sum_(i < n.+1 ) mu (seqD F i))]).
rewrite [X in _ --> X](_ : _ = mu \o F) // funeqE => n.
by rewrite -measure_semi_additive // -?FE // => -[|k].
move => S [n _] nS; exists n => // m nm.
under eq_fun do rewrite -(big_mkord predT (mu \o seqD F)).
exact /(nS m.+1 )/(leq_trans nm).
Qed .
Section boole_inequality .
Context d (R : realFieldType) (T : ringOfSetsType d).
Variable mu : {content set T -> \bar R}.
Theorem Boole_inequality (A : (set T) ^nat) n :
(forall i , `I_n i -> measurable (A i)) ->
mu (\big[setU/set0]_(i < n) A i) <= \sum_(i < n) mu (A i).
Proof .
move => Am; rewrite content_sub_additive// -bigcup_mkord.
exact : fin_bigcup_measurable.
Qed .
End boole_inequality .
Notation le_mu_bigsetU := Boole_inequality.
Section sigma_finite_lemma .
Context d (R : realFieldType) (T : ringOfSetsType d) (A : set T)
(mu : {content set T -> \bar R}).
Lemma sigma_finiteP : sigma_finite A mu ->
exists2 F, A = \bigcup_i F i &
nondecreasing_seq F /\ forall i , measurable (F i) /\ mu (F i) < +oo.
Proof .
move => [S AS moo]; exists (fun n => \big[setU/set0]_(i < n.+1 ) S i).
rewrite AS predeqE => t; split => [[i _ Sit]|[i _]].
by exists i => //; rewrite big_ord_recr /=; right .
by rewrite -bigcup_mkord => -[j /= ji Sjt]; exists j .
split => [|i].
- apply /nondecreasing_seqP => i; rewrite [in leRHS]big_ord_recr /=.
by apply /subsetPset; left .
- split ; first by apply : bigsetU_measurable => j _; exact : (moo j).1 .
rewrite (@le_lt_trans _ _ (\sum_(j < i.+1 ) mu (S j)))//.
by apply : Boole_inequality => j _; exact : (moo j).1 .
by apply /lte_sum_pinfty => j _; exact : (moo j).2 .
Qed .
End sigma_finite_lemma .
Section generalized_boole_inequality .
Context d (R : realType) (T : ringOfSetsType d).
Variable (mu : {measure set T -> \bar R}).
Theorem generalized_Boole_inequality (A : (set T) ^nat) :
(forall i , measurable (A i)) -> measurable (\bigcup_n A n) ->
mu (\bigcup_n A n) <= \sum_(i <oo) mu (A i).
Proof . by move => Am UAm; rewrite measure_sigma_sub_additive. Qed .
End generalized_boole_inequality .
Notation le_mu_bigcup := generalized_Boole_inequality.
Section negligible .
Context d (R : realFieldType) (T : ringOfSetsType d).
Definition negligible (mu : set T -> \bar R) (N : set T) :=
exists A : set T, [/\ measurable A, mu A = 0 & N `<=` A].
Local Notation "mu .-negligible" := (negligible mu).
Lemma negligibleP (mu : {content set _ -> \bar _}) A :
measurable A -> mu.-negligible A <-> mu A = 0 .
Proof .
move => mA; split => [[B [mB mB0 AB]]|mA0]; last by exists A ; split .
apply /eqP; rewrite eq_le measure_ge0 // andbT -mB0.
by apply : (le_measure mu) => //; rewrite in_setE.
Qed .
Lemma negligible_set0 (mu : {content set _ -> \bar _}) : mu.-negligible set0.
Proof . exact /negligibleP. Qed .
Lemma measure_negligible (mu : {content set T -> \bar R}) (A : set T) :
measurable A -> mu.-negligible A -> mu A = 0 %E.
Proof . by move => mA /negligibleP ->. Qed .
Definition almost_everywhere (mu : set T -> \bar R) (P : T -> Prop )
& (phantom Prop (forall x , P x)) :=
mu.-negligible (~` [set x | P x]).
Local Notation "{ 'ae' m , P }" :=
(almost_everywhere m (inPhantom P)) : type_scope.
Lemma aeW (mu : {measure set _ -> \bar _}) (P : T -> Prop ) :
(forall x , P x) -> {ae mu, forall x , P x}.
Proof .
move => aP; have -> : P = setT by rewrite predeqE => t; split .
by apply /negligibleP; [rewrite setCT|rewrite setCT measure0].
Qed .
End negligible .
Notation "mu .-negligible" := (negligible mu) : type_scope.
Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) : type_scope.
Definition sigma_subadditive (R : numFieldType) (T : Type )
(mu : set T -> \bar R) := forall (F : (set T) ^nat),
mu (\bigcup_n (F n)) <= \sum_(i <oo) mu (F i).
HB.mixin Record isOuterMeasure
(R : numFieldType) (T : Type ) (mu : set T -> \bar R) := {
outer_measure0 : mu set0 = 0 ;
outer_measure_ge0 : forall x , 0 <= mu x ;
le_outer_measure : {homo mu : A B / A `<=` B >-> A <= B} ;
outer_measure_sigma_subadditive : sigma_subadditive mu }.
#[short(type=outer_measure)]
HB.structure Definition OuterMeasure (R : numFieldType) (T : Type ) :=
{mu & isOuterMeasure R T mu}.
Notation "{ 'outer_measure' 'set' T '->' '\bar' R }" := (outer_measure R T)
(at level 36 , T, R at next level ,
format "{ 'outer_measure' 'set' T '->' '\bar' R }" ) : ring_scope.
#[global ] Hint Extern 0 (_ set0 = 0 ) => solve [apply : outer_measure0] : core.
#[global ] Hint Extern 0 (sigma_subadditive _) =>
solve [apply : outer_measure_sigma_subadditive] : core.
Arguments outer_measure0 {R T} _.
Arguments outer_measure_ge0 {R T} _.
Arguments le_outer_measure {R T} _.
Arguments outer_measure_sigma_subadditive {R T} _.
Lemma le_outer_measureIC (R : realFieldType) T
(mu : {outer_measure set T -> \bar R}) (A X : set T) :
mu X <= mu (X `&` A) + mu (X `&` ~` A).
Proof .
pose B : (set T) ^nat := bigcup2 (X `&` A) (X `&` ~` A).
have cvg_mu : (fun n => \sum_(i < n) mu (B i)) --> mu (B 0 %N) + mu (B 1 %N).
rewrite -2 !cvg_shiftS /=.
rewrite [X in X --> _](_ : _ = (fun => mu (B 0 %N) + mu (B 1 %N))); last first .
rewrite funeqE => i; rewrite 2 !big_ord_recl /= big1 ?adde0 // => j _.
by rewrite /B /bigcup2 /=.
exact : cvg_cst.
have := outer_measure_sigma_subadditive mu B.
suff : \bigcup_n B n = X.
move => -> /le_trans; apply ; under eq_fun do rewrite big_mkord.
by rewrite (cvg_lim _ cvg_mu).
transitivity (\big[setU/set0]_(i < 2 ) B i).
by rewrite (bigcup_splitn 2 ) // -bigcup_mkord setUidl// => t -[].
by rewrite 2 !big_ord_recl big_ord0 setU0 /= -setIUr setUCr setIT.
Unshelve . all : by end_near. Qed .
Definition caratheodory_measurable (R : realType) (T : Type )
(mu : set T -> \bar R) (A : set T) := forall X ,
mu X = mu (X `&` A) + mu (X `&` ~` A).
Local Notation "mu .-caratheodory" :=
(caratheodory_measurable mu) : classical_set_scope.
Lemma le_caratheodory_measurable (R : realType) T
(mu : {outer_measure set T -> \bar R}) (A : set T) :
(forall X , mu (X `&` A) + mu (X `&` ~` A) <= mu X) ->
mu.-caratheodory A.
Proof .
move => suf X; apply /eqP; rewrite eq_le; apply /andP; split ;
[exact : le_outer_measureIC | exact : suf].
Qed .
Section caratheodory_theorem_sigma_algebra .
Variables (R : realType) (T : Type ) (mu : {outer_measure set T -> \bar R}).
Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X :
mu (X `&` \bigcup_k A k) <= \sum_(k <oo) mu (X `&` A k).
Proof .
apply : (le_trans _ (outer_measure_sigma_subadditive mu (fun n => X `&` A n))).
by apply /le_outer_measure; rewrite setI_bigcupr.
Qed .
Let M := mu.-caratheodory.
Lemma caratheodory_measurable_set0 : M set0.
Proof . by move => X /=; rewrite setI0 outer_measure0 add0e setC0 setIT. Qed .
Lemma caratheodory_measurable_setC A : M A -> M (~` A).
Proof . by move => MA X; rewrite setCK addeC -MA. Qed .
Lemma caratheodory_measurable_setU_le (X A B : set T) :
mu.-caratheodory A -> mu.-caratheodory B ->
mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <= mu X.
Proof .
move => mA mB; pose Y := X `&` A `|` X `&` B `&` ~` A.
have /(lee_add2r (mu (X `&` ~` (A `|` B)))) :
mu Y <= mu (X `&` A) + mu (X `&` B `&` ~` A).
pose Z := bigcup2 (X `&` A) (X `&` B `&` ~` A).
have -> : Y = \bigcup_k Z k.
rewrite predeqE => t; split => [[?|?]|[]]; [by exists O |by exists 1 %N|].
by move => [_ ?|[_ ?|//]]; [left |right ].
rewrite (le_trans (outer_measure_sigma_subadditive mu Z)) //.
suff : ((fun n => \sum_(i < n) mu (Z i)) -->
mu (X `&` A) + mu (X `&` B `&` ~` A)).
move /cvg_lim => /=; under [in leLHS]eq_fun do rewrite big_mkord.
by move => ->.
rewrite -(cvg_shiftn 2 ) /=; set l := (X in _ --> X).
rewrite [X in X --> _](_ : _ = cst l); first exact : cvg_cst.
rewrite funeqE => i; rewrite addn2 2 !big_ord_recl big1 ?adde0 //.
by move => ? _; exact : outer_measure0.
have /le_trans : mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <=
mu Y + mu (X `&` ~` (A `|` B)).
rewrite setIUr (_ : X `&` A `|` X `&` B = Y) //.
rewrite /Y -[in LHS](setIT B) -(setUCr A) 2 !setIUr setUC -[in RHS]setIA.
rewrite setUC setUA; congr (_ `|` _).
by rewrite setUidPl setICA; apply : subIset; right .
suff -> : mu (X `&` A) + mu (X `&` B `&` ~` A) +
mu (X `&` (~` (A `|` B))) = mu X by exact .
by rewrite setCU setIA -(setIA X) setICA (setIC B) -addeA -mB -mA.
Qed .
Lemma caratheodory_measurable_setU A B : M A -> M B -> M (A `|` B).
Proof .
move => mA mB X; apply /eqP; rewrite eq_le.
by rewrite le_outer_measureIC andTb caratheodory_measurable_setU_le.
Qed .
Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) : (forall n , M (A n)) ->
forall n , M (\big[setU/set0]_(i < n) A i).
Proof .
move => MA; elim => [|n ih]; first by rewrite big_ord0; exact : caratheodory_measurable_set0.
by rewrite big_ord_recr; apply : caratheodory_measurable_setU.
Qed .
Lemma caratheodory_measurable_setI A B : M A -> M B -> M (A `&` B).
Proof .
move => mA mB; rewrite -(setCK A) -(setCK B) -setCU.
by apply /caratheodory_measurable_setC/caratheodory_measurable_setU;
exact /caratheodory_measurable_setC.
Qed .
Lemma caratheodory_measurable_setD A B : M A -> M B -> M (A `\` B).
Proof .
move => mA mB; rewrite setDE; apply : caratheodory_measurable_setI => //.
exact : caratheodory_measurable_setC.
Qed .
Section additive_ext_lemmas .
Variable A B : set T.
Hypothesis (mA : M A) (mB : M B).
Let caratheodory_decomp X :
mu X = mu (X `&` A `&` B) + mu (X `&` A `&` ~` B) +
mu (X `&` ~` A `&` B) + mu (X `&` ~` A `&` ~` B).
Proof . by rewrite mA mB [X in _ + _ + X = _]mB addeA. Qed .
Let caratheorody_decompIU X : mu (X `&` (A `|` B)) =
mu (X `&` A `&` B) + mu (X `&` ~` A `&` B) + mu (X `&` A `&` ~` B).
Proof .
rewrite caratheodory_decomp -!addeA; congr (mu _ + _).
rewrite -!setIA; congr (_ `&` _).
by rewrite setIC; apply /setIidPl; apply : subIset; left ; left .
rewrite addeA addeC [X in mu X + _](_ : _ = set0); last first .
by rewrite -setIA -setCU -setIA setICr setI0.
rewrite outer_measure0 add0e addeC -!setIA; congr (mu (X `&` _) + mu (X `&` _)).
by rewrite setIC; apply /setIidPl; apply : subIset; right ; right .
by rewrite setIC; apply /setIidPl; apply : subIset; left ; left .
Qed .
Lemma disjoint_caratheodoryIU X : [disjoint A & B] ->
mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B).
Proof .
move => /eqP AB; rewrite caratheodory_decomp -setIA AB setI0 outer_measure0.
rewrite add0e addeC -setIA -setCU -setIA setICr setI0 outer_measure0 add0e.
rewrite -!setIA; congr (mu (X `&` _ ) + mu (X `&` _)).
rewrite (setIC A) setIA setIC; apply /setIidPl.
- by rewrite setIUl setICr setU0 subsetI; move /disjoints_subset in AB; split .
- rewrite setIA setIC; apply /setIidPl; rewrite setIUl setICr set0U.
by move : AB; rewrite setIC => /disjoints_subset => AB; rewrite subsetI; split .
Qed .
End additive_ext_lemmas .
Lemma caratheodory_additive (A : (set T) ^nat) : (forall n , M (A n)) ->
trivIset setT A -> forall n X ,
mu (X `&` \big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (X `&` A i).
Proof .
move => MA ta; elim => [|n ih] X; first by rewrite !big_ord0 setI0 outer_measure0.
rewrite big_ord_recr /= disjoint_caratheodoryIU // ?ih ?big_ord_recr //.
- exact : caratheodory_measurable_bigsetU.
- by apply /eqP/(@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE.
Qed .
Lemma caratheodory_lime_le (A : (set T) ^nat) : (forall n , M (A n)) ->
trivIset setT A -> forall X ,
\sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` \bigcup_k A k) <= mu X.
Proof .
move => MA tA X.
set A' := \bigcup_k A k; set B := fun n => \big[setU/set0]_(k < n) (A k).
suff : forall n , \sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X.
move => XA; rewrite (_ : lim _ = ereal_sup
((fun n => \sum_(k < n) mu (X `&` A k)) @` setT)); last first .
under eq_fun do rewrite big_mkord.
apply /cvg_lim => //; apply /ereal_nondecreasing_cvg.
apply : (lee_sum_nneg_ord (fun n => mu (X `&` A n)) xpredT) => n _.
exact : outer_measure_ge0.
move XAx : (mu (X `&` ~` A')) => [x| |].
- rewrite -lee_subr_addr //; apply : ub_ereal_sup => /= _ [n _] <-.
by rewrite EFinN lee_subr_addr // -XAx XA.
- suff : mu X = +oo by move => ->; rewrite leey.
by apply /eqP; rewrite -leye_eq -XAx le_outer_measure.
- by rewrite addeC /= leNye.
move => n.
apply : (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))).
apply /lee_add2l/le_outer_measure; apply : setIS; apply : subsetC => t.
by rewrite /B -bigcup_mkord => -[i ? ?]; exists i .
rewrite [in leRHS](caratheodory_measurable_bigsetU MA n) lee_add2r //.
by rewrite caratheodory_additive.
Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" ,
note="renamed `caratheodory_lime_le`" )]
Notation caratheodory_lim_lee := caratheodory_lime_le.
Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) :
(forall n , M (A n)) -> trivIset setT A -> M (\bigcup_k (A k)).
Proof .
move => MA tA; apply : le_caratheodory_measurable => X /=.
have /(lee_add2r (mu (X `&` ~` \bigcup_k A k))) := outer_measure_bigcup_lim A X.
by move /le_trans; apply ; exact : caratheodory_lime_le.
Qed .
Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (forall n , M (A n)) ->
M (\bigcup_k (A k)).
Proof .
move => MA; rewrite -eq_bigcup_seqD_bigsetU.
apply /caratheodory_measurable_trivIset_bigcup; last first .
apply : (@trivIset_seqD _ (fun n => \big[setU/set0]_(i < n.+1 ) A i)).
by move => n m nm; exact /subsetPset/subset_bigsetU.
by case => [|n /=]; [| apply /caratheodory_measurable_setD => //];
exact /caratheodory_measurable_bigsetU.
Qed .
End caratheodory_theorem_sigma_algebra .
Definition caratheodory_type (R : realType) (T : Type )
(mu : set T -> \bar R) := T.
Definition caratheodory_display R T : (set T -> \bar R) -> measure_display.
Proof . exact . Qed .
Section caratheodory_sigma_algebra .
Variables (R : realType) (T : pointedType) (mu : {outer_measure set T -> \bar R}).
HB.instance Definition _ := @isMeasurable.Build (caratheodory_display mu)
(caratheodory_type mu) (Pointed.class T) mu.-caratheodory
(caratheodory_measurable_set0 mu)
(@caratheodory_measurable_setC _ _ mu)
(@caratheodory_measurable_bigcup _ _ mu).
End caratheodory_sigma_algebra .
Notation "mu .-cara" := (caratheodory_display mu) : measure_display_scope.
Notation "mu .-cara.-measurable" :=
(measurable : set (set (caratheodory_type mu))) : classical_set_scope.
Definition measure_is_complete d (R : realType) (T : measurableType d)
(mu : set T -> \bar R) :=
forall X , mu.-negligible X -> measurable X.
Section caratheodory_measure .
Variables (R : realType) (T : pointedType).
Variable (mu : {outer_measure set T -> \bar R}).
Let U := caratheodory_type mu.
Lemma caratheodory_measure0 : mu (set0 : set U) = 0 .
Proof . exact : outer_measure0. Qed .
Lemma caratheodory_measure_ge0 (A : set U) : 0 <= mu A.
Proof . exact : outer_measure_ge0. Qed .
Lemma caratheodory_measure_sigma_additive :
semi_sigma_additive (mu : set U -> _).
Proof .
move => A mA tA mbigcupA; set B := \bigcup_k A k.
suff : forall X , mu X = \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` B).
move /(_ B); rewrite setICr outer_measure0 adde0.
rewrite (_ : (fun n => _) = fun n => \sum_(k < n) mu (A k)); last first .
rewrite funeqE => n; rewrite big_mkord; apply : eq_bigr => i _; congr (mu _).
by rewrite setIC; apply /setIidPl => t Ait; exists i .
move => ->; have := fun n (_ : xpredT n) => outer_measure_ge0 mu (A n).
move /is_cvg_nneseries => /cvg_ex[l] hl.
under [in X in _ --> X]eq_fun do rewrite -(big_mkord xpredT (mu \o A)).
by move /(@cvg_lim _ (@ereal_hausdorff R)) : (hl) => ->.
move => X.
have mB : mu.-cara.-measurable B := caratheodory_measurable_bigcup mA.
apply /eqP; rewrite eq_le (caratheodory_lime_le mA tA X) andbT.
have /(lee_add2r (mu (X `&` ~` B))) := outer_measure_bigcup_lim mu A X.
by rewrite -le_caratheodory_measurable // => ?; rewrite -mB.
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ (mu : set (caratheodory_type mu) -> _)
caratheodory_measure0 caratheodory_measure_ge0
caratheodory_measure_sigma_additive.
Lemma measure_is_complete_caratheodory :
measure_is_complete (mu : set (caratheodory_type mu) -> _).
Proof .
move => B [A [mA muA0 BA]]; apply : le_caratheodory_measurable => X.
suff -> : mu (X `&` B) = 0 .
by rewrite add0e le_outer_measure //; apply : subIset; left .
have muB0 : mu B = 0 .
apply /eqP; rewrite eq_le outer_measure_ge0 andbT.
by apply : (le_trans (le_outer_measure mu _ _ BA)); rewrite -muA0.
apply /eqP; rewrite eq_le outer_measure_ge0 andbT.
have : X `&` B `<=` B by apply : subIset; right .
by move /(le_outer_measure mu); rewrite muB0 => ->.
Qed .
End caratheodory_measure .
Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) e
(P : pred nat) : (forall n , 0 <= A n) -> (0 <= e)%R ->
\sum_(i <oo | P i) (A i + (e / (2 ^ i.+1 )%:R)%:E) <=
\sum_(i <oo | P i) A i + e%:E.
Proof .
move => A0 /nonnegP[{}e].
rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) +
\sum_(0 <= i < n) (e%:num / (2 ^ i.+1 )%:R)%:E))) //.
rewrite nneseriesD // limeD //.
- rewrite lee_add2l //; apply : lee_lim => //.
+ exact : is_cvg_nneseries.
+ exact : is_cvg_nneseries.
+ by near=> n; exact : lee_sum_nneg_subset.
- exact : is_cvg_nneseries.
- exact : is_cvg_nneseries.
- exact : adde_def_nneseries.
suff cvggeo : (fun n => \sum_(0 <= i < n) (e%:num / (2 ^ i.+1 )%:R)%:E) -->
e%:num%:E.
rewrite limeD //.
- by rewrite lee_add2l // (cvg_lim _ cvggeo).
- exact : is_cvg_nneseries.
- by apply : is_cvg_nneseries => ?; rewrite lee_fin divr_ge0.
- by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_defl.
rewrite (_ : (fun n => _) = EFin \o
(fun n => \sum_(0 <= i < n) (e%:num / (2 ^ (i + 1 ))%:R))%R); last first .
rewrite funeqE => n /=; rewrite (@big_morph _ _ EFin 0 adde)//.
by under [in RHS]eq_bigr do rewrite addn1.
apply : cvg_comp; last by apply cvg_refl.
have := cvg_geometric_series_half e%:num O.
by rewrite expr0 divr1; apply : cvg_trans.
Unshelve . all : by end_near. Qed .
Section measurable_cover .
Context d (T : semiRingOfSetsType d).
Implicit Types (X : set T) (F : (set T)^nat).
Definition measurable_cover X := [set F : (set T)^nat |
(forall i , measurable (F i)) /\ X `<=` \bigcup_k (F k)].
Lemma cover_measurable X F : measurable_cover X F -> forall k , measurable (F k).
Proof . by move => + k; rewrite /measurable_cover => -[] /(_ k). Qed .
Lemma cover_subset X F : measurable_cover X F -> X `<=` \bigcup_k (F k).
Proof . by case . Qed .
End measurable_cover .
Lemma measurable_uncurry (T1 T2 : Type ) d (T : semiRingOfSetsType d)
(G : T1 -> T2 -> set T) (x : T1 * T2) :
measurable (G x.1 x.2 ) <-> measurable (uncurry G x).
Proof . by case : x. Qed .
Section measure_extension .
Context (R : realType) d (T : semiRingOfSetsType d).
Variable mu : set T -> \bar R.
Hypothesis measure0 : mu set0 = 0 .
Hypothesis measure_ge0 : forall X , mu X >= 0 .
Hint Resolve measure_ge0 measure0 : core.
Definition mu_ext (X : set T) : \bar R :=
ereal_inf [set \sum_(i <oo) mu (A i) | A in measurable_cover X].
Local Notation "mu^*" := mu_ext.
Lemma le_mu_ext : {homo mu^* : A B / A `<=` B >-> A <= B}.
Proof .
move => A B AB; apply /le_ereal_inf => x [B' [mB' BB']].
by move => <-{x}; exists B' => //; split => //; apply : subset_trans AB BB'.
Qed .
Lemma mu_ext_ge0 A : 0 <= mu^* A.
Proof .
apply : lb_ereal_inf => x [B [mB AB] <-{x}]; rewrite lime_ge //=.
exact : is_cvg_nneseries.
by near=> n; rewrite sume_ge0.
Unshelve . all : by end_near. Qed .
Lemma mu_ext0 : mu^* set0 = 0 .
Proof .
apply /eqP; rewrite eq_le; apply /andP; split ; last exact /mu_ext_ge0.
rewrite /mu_ext; apply : ereal_inf_lb; exists (fun _ => set0); first by split .
by apply : (@lim_near_cst _ _ _ _ _ 0 ) => //; near=> n => /=; rewrite big1.
Unshelve . all : by end_near. Qed .
Lemma mu_ext_sigma_subadditive : sigma_subadditive mu^*.
Proof .
move => A; have [[i ioo]|] := pselect (exists i , mu^* (A i) = +oo).
rewrite (eseries_pinfty _ _ ioo)// ?leey // => n _.
by rewrite gt_eqF// (lt_le_trans _ (mu_ext_ge0 _)).
rewrite -forallNE => Aoo.
suff add2e : forall e : {posnum R},
mu^* (\bigcup_n A n) <= \sum_(i <oo) mu^* (A i) + e%:num%:E.
by apply : lee_adde => e.
move => e; rewrite (le_trans _ (epsilon_trick _ _ _))//; last first .
by move => n; apply : mu_ext_ge0.
pose P n (B : (set T)^nat) := measurable_cover (A n) B /\
\sum_(k <oo) mu (B k) <= mu^* (A n) + (e%:num / (2 ^ n.+1 )%:R)%:E.
have [G PG] : {G : ((set T)^nat)^nat & forall n , P n (G n)}.
apply : (@choice _ _ P) => n; rewrite /P /mu_ext.
set S := (X in ereal_inf X); move infS : (ereal_inf S) => iS.
case : iS infS => [r Sr|Soo|Soo].
- have en1 : (0 < e%:num / (2 ^ n.+1 )%:R)%R.
by rewrite divr_gt0 // ltr0n expn_gt0.
have /(lb_ereal_inf_adherent en1) : ereal_inf S \is a fin_num by rewrite Sr.
move => [x [B [mB AnB muBx] xS]].
exists B ; split => //; rewrite muBx -Sr; apply /ltW.
by rewrite (lt_le_trans xS) // lee_add2l //= lee_fin ler_pmul.
- by have := Aoo n; rewrite /mu^* Soo.
- suff : lbound S 0 by move /lb_ereal_inf; rewrite Soo.
by move => /= _ [B [mB AnB] <-]; exact : nneseries_ge0.
have muG_ge0 x : 0 <= (mu \o uncurry G) x by exact /measure_ge0.
apply : (@le_trans _ _ (\esum_(i in setT) (mu \o uncurry G) i)).
rewrite /mu_ext; apply : ereal_inf_lb => /=.
have /card_esym/ppcard_eqP[f] := card_nat2.
exists (uncurry G \o f).
split => [i|]; first exact /measurable_uncurry/(PG (f i).1 ).1 .1 .
apply : (@subset_trans _ (\bigcup_n \bigcup_k G n k)) => [t [i _]|].
by move => /(cover_subset (PG i).1 ) -[j _ ?]; exists i => //; exists j .
move => t [i _ [j _ Bijt]]; exists (f ^-1 %FUN (i, j)) => //=.
by rewrite invK ?inE .
rewrite -(esum_pred_image (mu \o uncurry G) _ xpredT) ?[fun => _]set_true//.
congr esum.
by rewrite -[RHS](image_eq f)predeqE=> -[a b]/=; split => -[n _ <-]; exists n .
rewrite (_ : esum _ _ = \sum_(i <oo) \sum_(j <oo ) mu (G i j)); last first .
pose J : nat -> set (nat * nat) := fun i => [set (i, j) | j in setT].
rewrite (_ : setT = \bigcup_k J k); last first .
by rewrite predeqE => -[a b]; split => // _; exists a => //; exists b .
rewrite esum_bigcupT /=; last 2 first .
- apply /trivIsetP => i j _ _ ij.
rewrite predeqE => -[n m] /=; split => //= -[] [_] _ [<-{n} _].
by move => [m' _] [] /esym/eqP; rewrite (negbTE ij).
- by move => /= [n m]; apply /measure_ge0; exact : (cover_measurable (PG n).1 ).
rewrite (_ : setT = id @` xpredT); last first .
by rewrite image_id funeqE => x; rewrite trueE.
rewrite esum_pred_image //; last by move => n _; exact : esum_ge0.
apply : eq_eseries => /= j _.
rewrite -(esum_pred_image (mu \o uncurry G) (pair j) predT)//=; last first .
by move => ? ? _ _; exact : (@can_inj _ _ _ snd).
by congr esum; rewrite predeqE => -[a b]; split ; move => [i _ <-]; exists i .
apply : lee_lim.
- apply : is_cvg_nneseries => n _.
by apply : nneseries_ge0 => m _; exact : (muG_ge0 (n, m)).
- by apply : is_cvg_nneseries => n _; apply : adde_ge0 => //; exact : mu_ext_ge0.
- by near=> n; apply : lee_sum => i _; exact : (PG i).2 .
Unshelve . all : by end_near. Qed .
End measure_extension .
Declare Scope measure_scope.
Delimit Scope measure_scope with mu.
Notation "mu ^*" := (mu_ext mu) : measure_scope.
Local Open Scope measure_scope.
Section measure_extension .
Context d (R : realType) (T : semiRingOfSetsType d).
Variable mu : {content set T -> \bar R}.
HB.instance Definition _ := isOuterMeasure.Build
R T _ (@mu_ext0 _ _ _ _ (measure0 mu) (measure_ge0 mu))
(mu_ext_ge0 (measure_ge0 mu))
(le_mu_ext mu)
(mu_ext_sigma_subadditive (measure_ge0 mu)).
End measure_extension .
Section g_salgebra_measure_unique_trace .
Context d (R : realType) (T : measurableType d).
Variables (G : set (set T)) (D : set T) (mD : measurable D).
Let H := [set X | G X /\ X `<=` D] (* "trace" of G wrt D *) .
Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H) (HD : H D).
Variables m1 m2 : {measure set T -> \bar R}.
Hypotheses (m1m2 : forall A , H A -> m1 A = m2 A) (m1oo : (m1 D < +oo)%E).
Lemma g_salgebra_measure_unique_trace :
(forall X , (<<s D, H >>) X -> X `<=` D) -> forall X , <<s D, H >> X ->
m1 X = m2 X.
Proof .
move => sDHD; set E := [set A | [/\ measurable A, m1 A = m2 A & A `<=` D] ].
have HE : H `<=` E.
by move => X HX; rewrite /E /=; split ; [exact : Hm|exact : m1m2|case : HX].
have setDE : setD_closed E.
move => A B BA [mA m1m2A AD] [mB m1m2B BD]; split ; first exact : measurableD.
- rewrite measureD//; last first .
by rewrite (le_lt_trans _ m1oo)//; apply : le_measure => // /[!inE].
rewrite setIidr// m1m2A m1m2B measureD// ?setIidr //.
by rewrite (le_lt_trans _ m1oo)// -m1m2A; apply : le_measure => // /[!inE].
- by rewrite setDE; apply : subIset; left .
have ndE : ndseq_closed E.
move => A ndA EA; split ; have mA n : measurable (A n) by have [] := EA n.
- exact : bigcupT_measurable.
- transitivity (lim (m1 \o A)).
apply /esym/cvg_lim=>//.
exact /(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable.
transitivity (lim (m2 \o A)).
by congr (lim _); rewrite funeqE => n; have [] := EA n.
apply /cvg_lim => //.
exact /(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable.
- by apply : bigcup_sub => n; have [] := EA n.
have sDHE : <<s D, H >> `<=` E.
by apply : monotone_class_subset => //; split => //; [move => A []|exact /HE].
by move => X /sDHE[mX ?] _.
Qed .
End g_salgebra_measure_unique_trace .
Section g_salgebra_measure_unique .
Context d (R : realType) (T : measurableType d).
Variable G : set (set T).
Hypothesis Gm : G `<=` measurable.
Variable g : (set T)^nat.
Hypotheses Gg : forall i , G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T -> \bar R}.
Lemma g_salgebra_measure_unique_cover :
(forall n A , <<s G >> A -> m1 (g n `&` A) = m2 (g n `&` A)) ->
forall A , <<s G >> A -> m1 A = m2 A.
Proof .
pose GT := [the ringOfSetsType _ of salgebraType G].
move => sGm1m2; pose g' k := \bigcup_(i < k) g i.
have sGm := smallest_sub (@sigma_algebra_measurable _ T) Gm.
have Gg' i : <<s G >> (g' i).
apply : (@fin_bigcup_measurable _ GT) => //.
by move => n _; apply : sub_sigma_algebra.
have sG'm1m2 n A : <<s G >> A -> m1 (g' n `&` A) = m2 (g' n `&` A).
move => sGA; rewrite setI_bigcupl bigcup_mkord.
elim : n => [|n IHn] in A sGA *; rewrite (big_ord0, big_ord_recr) ?measure0 //=.
have sGgA i : <<s G >> (g i `&` A).
by apply : (@measurableI _ GT) => //; exact : sub_sigma_algebra.
apply : eq_measureU; rewrite ?sGm1m2 ?IHn //; last first .
- by rewrite -big_distrl -setIA big_distrl/= IHn// setICA setIid.
- exact /sGm.
- by apply : bigsetU_measurable => i _; apply /sGm.
have g'_cover : \bigcup_k (g' k) = setT.
by rewrite -subTset -g_cover => x [k _ gx]; exists k .+1 => //; exists k => /=.
have nd_g' : nondecreasing_seq g'.
move => m n lemn; rewrite subsetEset => x [k km gx]; exists k => //=.
exact : leq_trans lemn.
move => A gA.
have -> : A = \bigcup_n (g' n `&` A) by rewrite -setI_bigcupl g'_cover setTI.
transitivity (lim (fun n => m1 (g' n `&` A))).
apply /esym/cvg_lim => //; apply : nondecreasing_cvg_mu.
- by move => n; apply : measurableI; exact /sGm.
- by apply : bigcupT_measurable => k; apply : measurableI; exact /sGm.
- by move => ? ? ?; apply /subsetPset; apply : setSI; exact /subsetPset/nd_g'.
transitivity (lim (fun n => m2 (g' n `&` A))).
by congr (lim _); rewrite funeqE => x; apply : sG'm1m2 => //; exact /sGm.
apply /cvg_lim => //; apply : nondecreasing_cvg_mu.
- by move => k; apply : measurableI => //; exact /sGm.
- by apply : bigcupT_measurable => k; apply : measurableI; exact /sGm.
- by move => a b ab; apply /subsetPset; apply : setSI; exact /subsetPset/nd_g'.
Qed .
Hypothesis setIG : setI_closed G.
Hypothesis m1m2 : forall A , G A -> m1 A = m2 A.
Hypothesis m1goo : forall k , (m1 (g k) < +oo)%E.
Lemma g_salgebra_measure_unique : forall E , <<s G >> E -> m1 E = m2 E.
Proof .
pose G_ n := [set X | G X /\ X `<=` g n]. (* "trace" *)
have G_E n : G_ n = [set g n `&` C | C in G].
rewrite eqEsubset; split .
by move => X [GX Xgn] /=; exists X => //; rewrite setIidr.
by rewrite /G_ => X [Y GY <-{X}]; split ; [exact : setIG|apply : subIset; left ].
have gIsGE n : [set g n `&` A | A in <<s G >>] =
<<s g n, preimage_class (g n) id G >>.
rewrite sigma_algebra_preimage_classE eqEsubset; split .
by move => _ /= [Y sGY <-]; exists Y => //; rewrite preimage_id setIC.
by move => _ [Y mY <-] /=; exists Y => //; rewrite preimage_id setIC.
have preimg_gGE n : preimage_class (g n) id G = G_ n.
rewrite eqEsubset; split => [_ [Y GY <-]|].
by rewrite preimage_id G_E /=; exists Y => //; rewrite setIC.
by move => X [GX Xgn]; exists X => //; rewrite preimage_id setIidr.
apply : g_salgebra_measure_unique_cover => //.
move => n A sGA; apply : (@g_salgebra_measure_unique_trace _ _ _ G (g n)) => //.
- exact : Gm.
- by move => ? [? _]; exact /Gm.
- by move => ? ? [? ?] [? ?]; split ; [exact : setIG|apply : subIset; tauto ].
- by split .
- by move => ? [? ?]; exact : m1m2.
- move => X; rewrite -/(G_ n) -preimg_gGE -gIsGE.
by case => B sGB <-{X}; apply : subIset; left .
- by rewrite -/(G_ n) -preimg_gGE -gIsGE; exists A .
Qed .
End g_salgebra_measure_unique .
Section measure_unique .
Context d (R : realType) (T : measurableType d).
Variables (G : set (set T)) (g : (set T)^nat).
Hypotheses (mG : measurable = <<s G >>) (setIG : setI_closed G).
Hypothesis Gg : forall i , G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T -> \bar R}.
Hypothesis m1m2 : forall A , G A -> m1 A = m2 A.
Hypothesis m1goo : forall k , (m1 (g k) < +oo)%E.
Lemma measure_unique A : measurable A -> m1 A = m2 A.
Proof .
move => mA; apply : (@g_salgebra_measure_unique _ _ _ G); rewrite -?mG //.
by rewrite mG; exact : sub_sigma_algebra.
Qed .
End measure_unique .
Arguments measure_unique {d R T} G g.
Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}) X :
sigma_sub_additive mu ->
measurable X -> mu^* X = mu X.
Proof .
move => muS mX; apply /eqP; rewrite eq_le; apply /andP; split .
apply : ereal_inf_lb; exists (fun n => if n is 0 %N then X else set0).
by split => [[]// _|t Xt]; exists 0 %N.
apply /cvg_lim => //; rewrite -cvg_shiftS.
rewrite (_ : [sequence _]_n = cst (mu X)); first exact : cvg_cst.
by rewrite funeqE => n /=; rewrite big_nat_recl//= big1 ?adde0 .
apply /lb_ereal_inf => x [A [mA XA] <-{x}].
have XUA : X = \bigcup_n (X `&` A n).
rewrite predeqE => t; split => [Xt|[i _ []//]].
by have [i _ Ait] := XA _ Xt; exists i ; split .
apply : (@le_trans _ _ (\sum_(i <oo) mu (X `&` A i))).
by rewrite muS//= -?XUA => // i; apply : measurableI.
apply : lee_lim; [exact : is_cvg_nneseries|exact : is_cvg_nneseries|].
apply : nearW => n; apply : lee_sum => i _; apply : le_measure => // /[!inE]//=.
exact : measurableI.
Qed .
Section Rmu_ext .
Import SetRing.
Lemma Rmu_ext d (R : realType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}) :
(measure mu)^* = mu^*.
Proof .
apply /funeqP => /= X; rewrite /mu_ext/=; apply /eqP; rewrite eq_le.
rewrite ?lb_ereal_inf // => _ [F [Fm XS] <-]; rewrite ereal_inf_lb//; last first .
exists F ; first by split => // i; apply : sub_gen_smallest.
by rewrite (eq_eseries (fun _ _ => RmuE _ (Fm _))).
pose K := [set : nat] `*`` fun i => decomp (F i).
have /ppcard_eqP[f] : (K #= [set : nat])%card.
apply : cardMR_eq_nat => // i; split ; last by apply /set0P; rewrite decompN0.
by apply : finite_set_countable => //; exact : decomp_finite_set.
pose g i := (f^-1 %FUN i).2 ; exists g ; first split .
- move => k; have [/= _ /mem_set] : K (f^-1 %FUN k) by apply : funS.
exact : decomp_measurable.
- move => i /XS [k _]; rewrite -[F k]cover_decomp => -[D /= DFk Di].
by exists (f (k, D)) => //; rewrite /g invK// inE.
rewrite !nneseries_esum//= /measure ?set_true .
transitivity (\esum_(i in setT) \sum_(X0 \in decomp (F i)) mu X0); last first .
by apply : eq_esum => /= k _; rewrite fsbig_finite//; exact : decomp_finite_set.
rewrite -(eq_esum (fun _ _ => esum_fset _ _))//; last first .
by move => ? _; exact : decomp_finite_set.
rewrite esum_esum//= (reindex_esum K setT f) => //=.
by apply : eq_esum => i Ki; rewrite /g funK ?inE .
Qed .
End Rmu_ext .
Lemma measurable_Rmu_extE d (R : realType) (T : semiRingOfSetsType d)
(mu : {content set T -> \bar R}) X :
sigma_sub_additive mu ->
d.-ring .-measurable X -> mu^* X = SetRing.measure mu X.
Proof .
move => mu_sub Xm/=; rewrite -Rmu_ext/= measurable_mu_extE//.
exact : ring_sigma_sub_additive.
Qed .
Section Hahn_extension .
Context d (R : realType) (T : semiRingOfSetsType d).
Variable mu : {content set T -> \bar R}.
Hypothesis mu_sub : sigma_sub_additive mu.
Let Rmu := SetRing.measure mu.
Notation rT := (SetRing.type T).
Lemma sub_caratheodory :
(d.-measurable).-sigma.-measurable `<=` mu^*.-cara.-measurable.
Proof .
suff : <<s d.-ring .-measurable >> `<=` mu^*.-cara.-measurable.
apply : subset_trans; apply : sub_smallest2r => //.
by apply : sub_smallest.
apply : smallest_sub.
split => //; [by move => X mX; rewrite setTD; exact : measurableC |
by move => u_ mu_; exact : bigcupT_measurable].
move => A mA; apply le_caratheodory_measurable => // X.
apply lb_ereal_inf => _ [B [mB XB] <-].
rewrite -(eq_eseries (fun _ _ => SetRing.RmuE _ (mB _)))=> //.
have RmB i : measurable (B i : set rT) by exact : sub_gen_smallest.
set BA := eseries (fun n => Rmu (B n `&` A)).
set BNA := eseries (fun n => Rmu (B n `&` ~` A)).
apply : (@le_trans _ _ (lim BA + lim BNA)); [apply : lee_add|].
- rewrite (_ : BA = eseries (fun n => mu_ext mu (B n `&` A))); last first .
rewrite funeqE => n; apply : eq_bigr => k _.
by rewrite /= measurable_Rmu_extE //; exact : measurableI.
apply : (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `&` A)))).
by apply : le_mu_ext; rewrite -setI_bigcupl; exact : setISS.
exact : outer_measure_sigma_subadditive.
- rewrite (_ : BNA = eseries (fun n => mu_ext mu (B n `\` A))); last first .
rewrite funeqE => n; apply : eq_bigr => k _.
rewrite /= measurable_Rmu_extE //; exact : measurableD.
apply : (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `\` A)))).
by apply : le_mu_ext; rewrite -setI_bigcupl; exact : setISS.
exact : outer_measure_sigma_subadditive.
have ? : cvg BNA.
apply /is_cvg_nneseries => n _.
by rewrite -setDE; apply : measure_ge0 => //; exact : measurableD.
have ? : cvg BA.
by apply /is_cvg_nneseries => n _; apply : measure_ge0 =>//; apply : measurableI.
have ? : cvg (eseries (Rmu \o B)) by exact /is_cvg_nneseries.
have [def|] := boolP (adde_def (lim BA) (lim BNA)); last first .
rewrite /adde_def negb_and !negbK=> /orP[/andP[BAoo BNAoo]|/andP[BAoo BNAoo]].
- suff -> : lim (eseries (Rmu \o B)) = +oo by rewrite leey.
apply /eqP; rewrite -leye_eq -(eqP BAoo); apply /lee_lim => //.
near=> n; apply : lee_sum => m _; apply : le_measure; rewrite /mkset; by
[rewrite inE; exact : measurableI | rewrite inE | apply : subIset; left ].
- suff -> : lim (eseries (Rmu \o B)) = +oo by rewrite leey.
apply /eqP; rewrite -leye_eq -(eqP BNAoo); apply /lee_lim => //.
by near=> n; apply : lee_sum => m _; rewrite -setDE; apply : le_measure;
rewrite /mkset ?inE //; apply : measurableD.
rewrite -limeD // (_ : (fun _ => _) =
eseries (fun k => Rmu (B k `&` A) + Rmu (B k `&` ~` A))); last first .
by rewrite funeqE => n; rewrite -big_split /=; apply : eq_bigr.
apply /lee_lim => //.
apply /is_cvg_nneseries => // n _; apply /adde_ge0.
by apply : measure_ge0 => //; exact : measurableI.
by rewrite -setDE; apply : measure_ge0; exact : measurableD.
near=> n; apply : lee_sum => i _; rewrite -measure_semi_additive2.
- apply : le_measure; rewrite /mkset ?inE //; [|by rewrite -setIUr setUCr setIT].
by apply : measurableU; [exact :measurableI|rewrite -setDE; exact :measurableD].
- exact : measurableI.
- by rewrite -setDE; exact : measurableD.
- by apply : measurableU; [exact :measurableI|rewrite -setDE; exact :measurableD].
- by rewrite setIACA setICr setI0.
Unshelve . all : by end_near. Qed .
Let I := [the measurableType _ of salgebraType (@measurable _ T)].
Definition Hahn_ext : set I -> \bar R := mu^*.
Local Lemma Hahn_ext0 : Hahn_ext set0 = 0 .
Proof . exact : mu_ext0. Qed .
Local Lemma Hahn_ext_ge0 (A : set I) : 0 <= Hahn_ext A.
Proof . exact : mu_ext_ge0. Qed .
Local Lemma Hahn_ext_sigma_additive : semi_sigma_additive Hahn_ext.
Proof .
move => F mF tF mUF; rewrite /Hahn_ext.
apply : caratheodory_measure_sigma_additive => //; last first .
exact : sub_caratheodory.
by move => i; exact : (sub_caratheodory (mF i)).
Qed .
HB.instance Definition _ := isMeasure.Build _ _ _ Hahn_ext
Hahn_ext0 Hahn_ext_ge0 Hahn_ext_sigma_additive.
Lemma Hahn_ext_sigma_finite : @sigma_finite _ _ T setT mu ->
@sigma_finite _ _ _ setT Hahn_ext.
Proof .
move => -[S setTS mS]; exists S => //; move => i; split .
by have := (mS i).1 ; exact : sub_sigma_algebra.
by rewrite /Hahn_ext /= measurable_mu_extE //;
[exact : (mS i).2 | exact : (mS i).1 ].
Qed .
Lemma Hahn_ext_unique : sigma_finite [set : T] mu ->
(forall mu' : {measure set I -> \bar R},
(forall X , d.-measurable X -> mu X = mu' X) ->
(forall X , (d.-measurable).-sigma.-measurable X -> Hahn_ext X = mu' X)).
Proof .
move => [F TF /all_and2[Fm muF]] mu' mu'mu X mX.
apply : (@measure_unique _ _ [the measurableType _ of I] d.-measurable F) => //.
- by move => A B Am Bm; apply : measurableI.
- by move => A Am; rewrite /= /Hahn_ext measurable_mu_extE// mu'mu.
- by move => k; rewrite /= /Hahn_ext measurable_mu_extE.
Qed .
End Hahn_extension .
Lemma caratheodory_measurable_mu_ext d (R : realType) (T : measurableType d)
(mu : {measure set T -> \bar R}) A :
d.-measurable A -> mu^*.-cara.-measurable A.
Proof .
by move => Am; apply : sub_caratheodory => //;
[exact : measure_sigma_sub_additive|exact : sub_sigma_algebra].
Qed .
Definition preimage_classes d1 d2
(T1 : measurableType d1) (T2 : measurableType d2) (T : Type )
(f1 : T -> T1) (f2 : T -> T2) :=
<<s preimage_class setT f1 measurable `|`
preimage_class setT f2 measurable >>.
Section product_lemma .
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
Variables (T : pointedType) (f1 : T -> T1) (f2 : T -> T2).
Variables (T3 : Type ) (g : T3 -> T).
Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) =
preimage_class setT g (preimage_classes f1 f2).
Proof .
rewrite {1 }/preimage_classes -sigma_algebra_preimage_classE; congr (<<s _ >>).
rewrite predeqE => C; split .
- move => [[A mA <-{C}]|[A mA <-{C}]].
+ by exists (f1 @^-1 ` A) => //; left ; exists A => //; rewrite setTI.
+ by exists (f2 @^-1 ` A) => //; right ; exists A => //; rewrite setTI.
- move => [A [[B mB <-{A} <-{C}]|[B mB <-{A} <-{C}]]].
+ by left ; rewrite !setTI; exists B => //; rewrite setTI.
+ by right ; rewrite !setTI; exists B => //; rewrite setTI.
Qed .
End product_lemma .
Definition measure_prod_display :
(measure_display * measure_display) -> measure_display.
Proof . exact . Qed .
Section product_salgebra_instance .
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
Let f1 := @fst T1 T2.
Let f2 := @snd T1 T2.
Lemma prod_salgebra_set0 : preimage_classes f1 f2 (set0 : set (T1 * T2)).
Proof . exact : sigma_algebra0. Qed .
Lemma prod_salgebra_setC A : preimage_classes f1 f2 A ->
preimage_classes f1 f2 (~` A).
Proof . exact : sigma_algebraC. Qed .
Lemma prod_salgebra_bigcup (F : _^nat) : (forall i , preimage_classes f1 f2 (F i)) ->
preimage_classes f1 f2 (\bigcup_i (F i)).
Proof . exact : sigma_algebra_bigcup. Qed .
HB.instance Definition prod_salgebra_mixin :=
@isMeasurable.Build (measure_prod_display (d1, d2))
(T1 * T2)%type (Pointed.class _) (preimage_classes f1 f2)
(prod_salgebra_set0) (prod_salgebra_setC) (prod_salgebra_bigcup).
End product_salgebra_instance .
Notation "p .-prod" := (measure_prod_display p) : measure_display_scope.
Notation "p .-prod.-measurable" :=
((p.-prod).-measurable : set (set (_ * _))) :
classical_set_scope.
Lemma measurableM d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
(A : set T1) (B : set T2) :
measurable A -> measurable B -> measurable (A `*` B).
Proof .
move => mA mB.
have -> : A `*` B = (A `*` setT) `&` (setT `*` B) :> set (T1 * T2).
by rewrite -{1 }(setIT A) -{1 }(setTI B) setMI.
rewrite setMT setTM; apply : measurableI.
- by apply : sub_sigma_algebra; left ; exists A => //; rewrite setTI.
- by apply : sub_sigma_algebra; right ; exists B => //; rewrite setTI.
Qed .
Section product_salgebra_measurableType .
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
Let M1 := @measurable _ T1.
Let M2 := @measurable _ T2.
Let M1xM2 := [set A `*` B | A in M1 & B in M2].
Lemma measurable_prod_measurableType :
(d1, d2).-prod.-measurable = <<s M1xM2 >>.
Proof .
rewrite eqEsubset; split .
apply : smallest_sub; first exact : smallest_sigma_algebra.
rewrite subUset; split .
- have /subset_trans : preimage_class setT fst M1 `<=` M1xM2.
by move => _ [X MX <-]; exists X => //; exists setT ; rewrite /M2 // setIC//.
by apply ; exact : sub_sigma_algebra.
- have /subset_trans : preimage_class setT snd M2 `<=` M1xM2.
by move => _ [Y MY <-]; exists setT ; rewrite /M1 //; exists Y .
by apply ; exact : sub_sigma_algebra.
apply : smallest_sub; first exact : smallest_sigma_algebra.
by move => _ [A MA] [B MB] <-; apply : measurableM => //; exact : sub_sigma_algebra.
Qed .
End product_salgebra_measurableType .
Section product_salgebra_g_measurableTypeR .
Context d1 (T1 : measurableType d1) (T2 : pointedType) (C2 : set (set T2)).
Hypothesis setTC2 : setT `<=` C2.
(* NB: useful? *)
Lemma measurable_prod_g_measurableTypeR :
@measurable _ [the measurableType _ of T1 * salgebraType C2 : Type ]
= <<s [set A `*` B | A in measurable & B in C2] >>.
Proof .
rewrite measurable_prod_measurableType //; congr (<<s _ >>).
rewrite predeqE => X; split => [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}].
by exists A => //; exists B => //; exact : setTC2.
by exists A => //; exists B => //; exact : sub_sigma_algebra.
Qed .
End product_salgebra_g_measurableTypeR .
Section product_salgebra_g_measurableType .
Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)).
Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2).
Lemma measurable_prod_g_measurableType :
@measurable _ [the measurableType _ of salgebraType C1 * salgebraType C2 : Type ]
= <<s [set A `*` B | A in C1 & B in C2] >>.
Proof .
rewrite measurable_prod_measurableType //; congr (<<s _ >>).
rewrite predeqE => X; split => [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}].
by exists A ; [exact : setTC1|exists B => //; exact : setTC2].
by exists A ; [exact : sub_sigma_algebra|exists B => //; exact : sub_sigma_algebra].
Qed .
End product_salgebra_g_measurableType .
Section prod_measurable_fun .
Context d d1 d2 (T : measurableType d) (T1 : measurableType d1)
(T2 : measurableType d2).
Lemma prod_measurable_funP (h : T -> T1 * T2) : measurable_fun setT h <->
measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h).
Proof .
apply : (@iff_trans _ (preimage_classes (fst \o h) (snd \o h) `<=` measurable)).
- rewrite preimage_classes_comp; split => [mf A [C HC <-]|f12]; first exact : mf.
by move => _ A mA; apply : f12; exists A .
- split => [h12|[mf1 mf2]].
split => _ A mA; apply : h12; apply : sub_sigma_algebra;
by [left ; exists A |right ; exists A ].
apply : smallest_sub; first exact : sigma_algebra_measurable.
by rewrite subUset; split => [|] A [C mC <-]; [exact : mf1|exact : mf2].
Qed .
Lemma measurable_fun_pair (f : T -> T1) (g : T -> T2) :
measurable_fun setT f -> measurable_fun setT g ->
measurable_fun setT (fun x => (f x, g x)).
Proof . by move => mf mg; apply /prod_measurable_funP. Qed .
End prod_measurable_fun .
Section prod_measurable_proj .
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
Lemma measurable_fun_fst : measurable_fun setT (@fst T1 T2).
Proof .
by have /prod_measurable_funP[] :=
@measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT.
Qed .
Lemma measurable_fun_snd : measurable_fun setT (@snd T1 T2).
Proof .
by have /prod_measurable_funP[] :=
@measurable_fun_id _ [the measurableType _ of (T1 * T2)%type] setT.
Qed .
Lemma measurable_fun_swap : measurable_fun [set : T1 * T2] (@swap T1 T2).
Proof .
by apply /prod_measurable_funP => /=; split ;
[exact : measurable_fun_snd|exact : measurable_fun_fst].
Qed .
End prod_measurable_proj .
Lemma measurable_fun_if_pair d d' (X : measurableType d)
(Y : measurableType d') (x y : X -> Y) :
measurable_fun setT x -> measurable_fun setT y ->
measurable_fun setT (fun tb => if tb.2 then x tb.1 else y tb.1 ).
Proof .
move => mx my.
have {}mx : measurable_fun [set : X * bool] (x \o fst).
by apply : measurable_funT_comp => //; exact : measurable_fun_fst.
have {}my : measurable_fun [set : X * bool] (y \o fst).
by apply : measurable_funT_comp => //; exact : measurable_fun_fst.
by apply : measurable_fun_ifT => //=; exact : measurable_fun_snd.
Qed .
Section partial_measurable_fun .
Context d d1 d2 (T : measurableType d) (T1 : measurableType d1)
(T2 : measurableType d2).
Variable f : T1 * T2 -> T.
Lemma measurable_fun_prod1 x :
measurable_fun setT f -> measurable_fun setT (fun y => f (x, y)).
Proof .
move => mf; pose pairx := fun y : T2 => (x, y).
have m1pairx : measurable_fun setT (fst \o pairx) by exact /measurable_fun_cst.
have m2pairx : measurable_fun setT (snd \o pairx) by exact /measurable_fun_id.
have ? : measurable_fun setT pairx by exact /(proj2 (prod_measurable_funP _)).
exact : (measurable_fun_comp _ _ mf).
Qed .
Lemma measurable_fun_prod2 y :
measurable_fun setT f -> measurable_fun setT (fun x => f (x, y)).
Proof .
move => mf; pose pairy := fun x : T1 => (x, y).
have m1pairy : measurable_fun setT (fst \o pairy) by exact /measurable_fun_id.
have m2pairy : measurable_fun setT (snd \o pairy) by exact /measurable_fun_cst.
have : measurable_fun setT pairy by exact /(proj2 (prod_measurable_funP _)).
exact : (measurable_fun_comp _ _ mf).
Qed .
End partial_measurable_fun .
HB.mixin Record isProbability d (T : measurableType d)
(R : realType) (P : set T -> \bar R) of isMeasure d R T P :=
{ probability_setT : P setT = 1 %E }.
#[short(type=probability)]
HB.structure Definition Probability d (T : measurableType d) (R : realType) :=
{P of isProbability d T R P & isMeasure d R T P }.
Section probability_lemmas .
Context d (T : measurableType d) (R : realType) (P : probability T R).
Lemma probability_le1 (A : set T) : measurable A -> (P A <= 1 )%E.
Proof .
move => mA; rewrite -(@probability_setT _ _ _ P).
by apply : le_measure => //; rewrite ?in_setE .
Qed .
End probability_lemmas .