Module mathcomp.analysis.measure_theory.measurable_structure

From HB Require Import structures.
From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions cardinality reals.
From mathcomp Require Import ereal topology normedtype sequences.

# Measure Theory NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. References: - R. Affeldt, C. Cohen. Measure construction by extension in dependent type theory with application to integration. JAR 2023 - Daniel Li. Intégration et applications. 2016 - Achim Klenke. Probability Theory. 2014 ## Mathematical structures ``` semiRingOfSetsType d == the type of semirings of sets The carrier is a set of sets A_i such that "measurable A_i" holds. "measurable A" is printed as "d.-measurable A" where d is a "display parameter" whose purpose is to distinguish different "measurable" predicates in the same context. The HB class is SemiRingOfSets. ringOfSetsType d == the type of rings of sets The HB class is RingOfSets. sigmaRingType d == the type of sigma-rings (of sets) The HB class is SigmaRing. algebraOfSetsType d == the type of algebras of sets The HB class is AlgebraOfsets. measurableType == the type of sigma-algebras The HB class is Measurable. ``` ## Instances of mathematical structures ``` discrete_measurable T == alias for the sigma-algebra [set: set T] setring G == the set of sets G contains the empty set, is closed by union, and difference (it is a ring of sets in the sense of ringOfSetsType) <<r G >> := smallest setring G <<r G >> is equipped with a structure of ring of sets. sigma_ring G == the set of sets G forms a sigma-ring <<sr G >> == sigma-ring generated by G := smallest sigma_ring 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 >> <<s G >> is equipped with a structure of sigma-algebra G.-sigma.-measurable A == A is measurable for the sigma-algebra <<s G >> g_sigma_algebraType G == the measurableType corresponding to <<s G >> This is an HB alias. ``` ## About sets of sets ``` setC_closed G == the set of sets G is closed under complement setSD_closed G == the set of sets G is closed under proper difference setD_closed G == the set of sets G is closed under difference setY_closed G == the set of sets G is closed under symmetric difference ndseq_closed G == the set of sets G is closed under non-decreasing countable union niseq_closed G == the set of sets G is closed under non-increasing countable intersection trivIset_closed G == the set of sets G is closed under pairwise-disjoint countable union lambda_system D G == G is a lambda_system of subsets of D <<l D, G >> == lambda-system generated by G on D <<l G >> := <<m setT, G >> monotone G == G is a monotone set system <<M G >> == monotone set system generated by G := smallest monotone G dynkin G == G is a set of sets that form a Dynkin system (or a d-system) <<d G >> == Dynkin system generated by G, i.e., smallest dynkin G strace G D := [set x `&` D | x in G] ``` ## Other measure-theoretic definitions ``` preimage_set_system D f G == set system of the preimages by f of sets in G g_sigma_algebra_preimage f == sigma-algebra generated by the function f g_sigma_algebra_preimageType f == the measurableType corresponding to g_sigma_algebra_preimage f This is an HB alias. f.-preimage.-measurable A == A is measurable for g_sigma_algebra_preimage f image_set_system D f G == set system of the sets with a preimage by f in G subset_sigma_subadditive mu == alternative predicate defining sigma-subadditivity ``` ## Product of measurable spaces ``` g_sigma_preimageU 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 semiRingOfSetsType's (d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra generated from T1 x T2, with T1 and T2 semiRingOfSetsType's with resp. display d1 and d2 g_sigma_preimage n (f : 'I_n -> aT -> rT) == the sigma-algebra over aT generated by the projections f n.-tuple T is equipped with a measurableType using g_sigma_preimage and the tnth projections. ```

Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import ProperNotations.
Import Order.TTheory GRing.Theory 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 .-measurable" (format "mu .-measurable").
Reserved Notation "G .-sigma" (format "G .-sigma").
Reserved Notation "G .-sigma.-measurable" (format "G .-sigma.-measurable").
Reserved Notation "f .-preimage" (format "f .-preimage").
Reserved Notation "f .-preimage.-measurable" (format "f .-preimage.-measurable").
Reserved Notation "'<<l' D , G '>>'" (format "'<<l' D , G '>>'").
Reserved Notation "'<<l' G '>>'" (format "'<<l' G '>>'").
Reserved Notation "'<<d' G '>>'" (format "'<<d' G '>>'").
Reserved Notation "'<<s' D , G '>>'" (format "'<<s' D , G '>>'").
Reserved Notation "'<<s' G '>>'" (format "'<<s' G '>>'").
Reserved Notation "'<<r' G '>>'" (format "'<<r' G '>>'").
Reserved Notation "'<<sr' G '>>'" (format "'<<sr' G '>>'").
Reserved Notation "'<<M' G '>>'" (format "'<<M' G '>>'").
Reserved Notation "p .-prod" (format "p .-prod").
Reserved Notation "p .-prod.-measurable" (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 set_systems.
Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)).

Definition := forall A, G A -> G (~` A).
Definition := forall A B, B `<=` A -> G A -> G B -> G (A `\` B).
Definition := forall A B, G A -> G B -> G (A `\` B).
Definition := forall A B, G A -> G B -> G (A `+` B).

Definition :=
    forall I (D : set I) A_, finite_set D -> (forall i, D i -> G (A_ i)) ->
  G (\bigcap_(i in D) (A_ i)).

Definition :=
    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 :=
    forall I (D : set I) A_, finite_set D -> (forall i, D i -> G (A_ i)) ->
  G (\bigcup_(i in D) (A_ i)).

Definition := forall A B, G A -> G B -> exists D,
  [/\ finite_set D, D `<=` G, A `\` B = \bigcup_(X in D) X & trivIset D id].

Lemma setD_semi_setD_closed : setD_closed -> semi_setD_closed.

Proof.

move=> mD A B Am Bm; exists [set A `\` B]; split; rewrite ?bigcup_set1//.
by move=> X ->; apply: mD.
by move=> X Y -> ->.
Qed.

Definition :=
  forall F, nondecreasing_seq F -> (forall i, G (F i)) -> G (\bigcup_i (F i)).

Definition :=
  forall F, nonincreasing_seq F -> (forall i, G (F i)) -> G (\bigcap_i (F i)).

Definition :=
  forall F : (set T)^nat, trivIset setT F -> (forall n, G (F n)) ->
                    G (\bigcup_k F k).

Definition :=
  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 := [/\ G set0, setU_closed G & setD_closed].

Definition := [/\ G set0, setD_closed &
   (forall A : (set T)^nat, (forall n, G (A n)) -> G (\bigcup_k A k))].

Definition :=
  [/\ 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 := [/\ G setT, setC_closed & trivIset_closed].

Until MathComp-Analysis 1.1.0, the identifier was `monotone_class` because this definition corresponds to "classe monotone" in several French references, e.g., the definition of "classe monotone" on the French wikipedia.

Definition :=
[/\ forall A, G A -> A `<=` D, G D, setSD_closed & ndseq_closed].

Definition := ndseq_closed /\ niseq_closed.

End set_systems.
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_closed`")]
Notation setDI_closed := setD_closed (only parsing).
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_semi_setD_closed`")]
Notation setDI_semi_setD_closed := setD_semi_setD_closed (only parsing).

Lemma powerset_sigma_ring (T : Type) (D : set T) :
sigma_ring [set X | X `<=` D].

Proof.

split => //; last first.
by move=> F FA/=; apply: bigcup_sub => i _; exact: FA.
by move=> U V + VA; apply: subset_trans; exact: subDsetl.
Qed.

Lemma powerset_lambda_system (T : Type) (D : set T) :
lambda_system D [set X | X `<=` D].

Proof.

split => //.
- by move=> A B BA + BD; apply: subset_trans; exact: subDsetl.
- by move=> /= F _ FD; exact: bigcup_sub.
Qed.

Notation "'<<l' D , G '>>'" := (smallest (lambda_system D) G) :
classical_set_scope.
Notation "'<<l' G '>>'" := (<<l 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.
Notation "'<<sr' G '>>'" := (smallest sigma_ring G) : classical_set_scope.
Notation "'<<M' G '>>'" := (smallest monotone G) : classical_set_scope.

Section lambda_system_smallest.
Variables (T : Type) (D : set T) (G : set (set T)).
Hypothesis GD : forall A, G A -> A `<=` D.

Lemma lambda_system_smallest : lambda_system D <<l D , G >>.

Proof.

split => [A MA | E [monoE] | A B BA MA MB E [[EsubD ED setDE ndE] GE] |].
- have monoH := powerset_lambda_system D.
by case: (monoH) => + _ _ _; apply; exact: MA.
- by case: monoE.
- by apply setDE => //; [exact: MA|exact: MB].
- by move=> F ndF MF E [[EsubD ED setDE ndE] CE]; apply ndE=> // n; exact: MF.
Qed.

End lambda_system_smallest.

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 setD_closedP T (G : set (set T)) :
setD_closed G <-> (setI_closed G /\ setSD_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.

#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_closed`")]
Notation sedDI_closedP := setD_closed (only parsing).

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, setSD_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 setringD : setD_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.
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setringD`")]
Notation setringDI := setringD (only parsing).

Lemma g_sigma_algebra_lambda_system T (G : set (set T)) (D : set T) :
(forall X, <<s D, G >> X -> X `<=` D) ->
lambda_system D <<s D, G >>.

Proof.

move=> sDGD; have := smallest_sigma_algebra D G.
by move=> /(sigma_algebraP sDGD) [sT sD snd sI]; split.
Qed.

Lemma smallest_sigma_ring T (G : set (set T)) : sigma_ring <<sr G >>.

Proof.

split=> [B [[]]//|A B GA GB C [[? CDI ?]] GC|A GA C [[? ? CU]] GC] /=.
- by apply: (CDI); [exact: GA|exact: GB].
- by apply: (CU) => n; exact: GA.
Qed.

see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.A(1), p.27

Lemma sigma_ring_monotone T (G : set (set T)) : sigma_ring G -> monotone G.

Proof.

move=> [G0 GDI GU]; split => [F ndF GF|F icF GF]; first exact: GU.
rewrite -(@setD_bigcup _ _ F _ O)//; apply: (GDI); first exact: GF.
by rewrite bigcup_mkcond; apply: GU => n; case: ifPn => // _; exact: GDI.
Qed.

Lemma g_sigma_ring_monotone T (G : set (set T)) : monotone <<sr G >>.

Proof.

by apply: sigma_ring_monotone => //; exact: smallest_sigma_ring. Qed.

Lemma sub_g_sigma_ring T (G : set (set T)) : G `<=` <<sr G >>.

Proof.

exact: sub_smallest. Qed.

see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.A(2), p.27

Lemma setring_monotone_sigma_ring T (G : set (set T)) :
setring G -> monotone G -> sigma_ring G.

Proof.

move=> [G0 GU GD] [ndG niG]; split => // F GF.
rewrite -bigcup_bigsetU_bigcup; apply: ndG.
by move=> *; exact/subsetPset/subset_bigsetU.
by elim=> [|n ih]; rewrite big_ord_recr/= ?big_ord0 ?set0U//; exact: GU.
Qed.

Lemma g_monotone_monotone T (G : set (set T)) : monotone <<M G>>.

Proof.

split=> /= F ndF GF C [[ndC niC] GC];
have {}GC : <<M G >> `<=` C by exact: smallest_sub.
- by apply: (ndC) => // i; apply: (GC); exact: GF.
- by apply: (niC) => // i; apply: (GC); exact: GF.
Qed.

Section g_monotone_g_sigma_ring.
Variables (T : Type) (G : set (set T)).
Hypothesis ringG : setring G.

see Paul Halmos' Measure Theory, Ch.1, sec.6, thm.B, p.27

Lemma g_monotone_setring : setring <<M G>>.

Proof.

pose M := <<M G>>.
pose K F := [set E | [/\ M (E `\` F), M (F `\` E) & M (E `|` F)] ].
have KP E F : K(F) E -> K(E) F by move=> [] *; split; rewrite 1?setUC.
have K_monotone F : monotone (K(F)).
  split.
    move=> /= H ndH KFH; split.
    - rewrite setD_bigcupl; apply: (g_monotone_monotone G).1.
        by move=> m n mn; apply/subsetPset; apply: setSD; exact/subsetPset/ndH.
      by move=> i; have [] := KFH i.
    - rewrite setDE setC_bigcup -bigcapIr//; apply: (g_monotone_monotone G).2.
        move=> m n mn; apply/subsetPset.
        by apply: setDS; exact/subsetPset/ndH.
      by move=> i; have [] := KFH i.
    - rewrite -bigcupUl//; apply: (g_monotone_monotone G).1.
        move=> m n mn; apply/subsetPset.
        by apply: setSU; exact/subsetPset/ndH.
      by move=> i; have [] := KFH i.
  move=> /= H niH KFH; split.
  - rewrite setDE -bigcapIl//; apply: (g_monotone_monotone G).2.
      move=> m n mn; apply/subsetPset; apply: setSI; exact/subsetPset/niH.
    by move=> i; have [] := KFH i.
  - rewrite setDE setC_bigcap setI_bigcupr; apply: (g_monotone_monotone G).1.
      move=> m n mn; apply/subsetPset.
      by apply: setIS; apply: subsetC; exact/subsetPset/niH.
    by move=> i; have [] := KFH i.
  - rewrite setU_bigcapl//; apply: (g_monotone_monotone G).2.
      move=> m n mn; apply/subsetPset.
      by apply: setSU; exact/subsetPset/niH.
    by move=> i; have [] := KFH i.
have G_KF F : G F -> G `<=` K(F).
  case: ringG => _ GU GDI GF A GA; split.
  - by apply: sub_gen_smallest; exact: GDI.
  - by apply: sub_gen_smallest; exact: GDI.
  - by apply: sub_gen_smallest; exact: GU.
have GM_KF F : G F -> M `<=` K(F).
  by move=> GF; apply: smallest_sub => //; exact: G_KF.
have MG_KF F : M F -> G `<=` K(F).
  by move=> MF A GA; rewrite /K/=; split; have /KP[] := GM_KF _ GA _ MF.
have MM_KF F : M F -> M `<=` K(F).
  by move=> MF; apply: smallest_sub => //; exact: MG_KF.
split.
- by apply: sub_gen_smallest; case: ringG.
- by move=> A B GA GB; have [] := MM_KF _ GB _ GA.
- by move=> A B GA GB; have [] := MM_KF _ GB _ GA.
Qed.

Lemma g_monotone_g_sigma_ring : <<M G >> = <<sr G >>.

Proof.

rewrite eqEsubset; split.
by apply: smallest_sub; [exact: g_sigma_ring_monotone|
exact: sub_g_sigma_ring].
apply: smallest_sub; last exact: sub_smallest.
apply: setring_monotone_sigma_ring; last exact: g_monotone_monotone.
exact: g_monotone_setring.
Qed.

End g_monotone_g_sigma_ring.

Corollary monotone_setring_sub_g_sigma_ring T (G R : set (set T)) : monotone G ->
setring R -> R `<=` G -> <<sr R>> `<=` G.

Proof.

by move=> mG rR RG; rewrite -g_monotone_g_sigma_ring//; exact: smallest_sub.
Qed.

Section smallest_lambda_system.
Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T).
Hypothesis lambdaDG : lambda_system D <<l D, G >>.

Lemma smallest_lambda_system : (forall X, <<s D, G >> X -> X `<=` D) ->
<<l D, G >> = <<s D, G >>.

Proof.

move=> sDGD; rewrite eqEsubset; split.
  apply: smallest_sub; first exact: g_sigma_algebra_lambda_system.
  exact: sub_sigma_algebra.
suff: setI_closed <<l D, G >>.
  move=> IH; apply: smallest_sub => //.
  by apply/sigma_algebraP; case: lambdaDG.
pose H := <<l D, G >>.
pose H_ A := [set X | H X /\ H (X `&` A)].
have setDH_ A : setSD_closed (H_ A).
  move=> X Y XY [HX HXA] [HY HYA]; case: lambdaDG => 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: lambdaDG => h _ _; apply => // => n; have [] := H_AF n.
  rewrite setI_bigcupl; case: lambdaDG => 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.
  move=> GX; rewrite /H_ => A GA; split; first exact: sub_smallest GA.
  by apply: (@sub_smallest _ _ _ G) => //; exact: setIG.
have HD X : H X -> X `<=` D by move=> ?; case: lambdaDG => + _ _ _; apply.
have GHH_ X : G X -> H `<=` H_ X.
  move=> GX; apply: smallest_sub; last exact: GGH_.
  split => //; first by move=> A [HA _]; case: lambdaDG => + _ _ _; exact.
  have XD : X `<=` D by apply: HD; exact: (@sub_smallest _ _ _ G).
  rewrite /H_ /= setIidr//; split; [by case: lambdaDG|].
  exact: (@sub_smallest _ _ _ G).
have HGH_ X : H X -> G `<=` H_ X.
  move=> *; split; [|by rewrite setIC; apply GHH_].
  exact: (@sub_smallest _ _ _ G).
have HHH_ X : H X -> H `<=` H_ X.
  move=> HX; apply: smallest_sub; last exact: HGH_.
  split=> //.
  - by move=> ? [? ?]; case: lambdaDG => + _ _ _; exact.
  - have XD : X `<=` D := HD _ HX.
    by rewrite /H_/= setIidr//; split => //; case: lambdaDG.
by move=> *; apply HHH_.
Qed.

End smallest_lambda_system.

Section lambda_system_subset.
Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T).
Variables (H : set (set T)) (DH : lambda_system D H) (GH : G `<=` H).

a.k.a. Sierpiński–Dynkin's pi-lambda theorem

Lemma lambda_system_subset : (forall X, (<<s D, G >>) X -> X `<=` D) ->
<<s D, G >> `<=` H.

Proof.

move=> sDGD; set M := <<l D, G >>.
rewrite -(@smallest_lambda_system _ _ setIG D) //.
- exact: smallest_sub.
- apply: lambda_system_smallest => A GA.
by apply: sDGD; exact: sub_sigma_algebra.
Qed.

End lambda_system_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_lambda_system G : dynkin G <-> lambda_system 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_bigsetU_bigcup.
  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 g_dynkin_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_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.
  apply: big_ind => //; first by case: dG.
  by move=> i _; exact/(dynkinC dG).
Qed.

Lemma setI_closed_g_dynkin_g_sigma_algebra G :
setI_closed G -> <<d G >> = <<s G >>.

Proof.

move=> GI; rewrite eqEsubset; split.
  by apply: sub_smallest2l; exact: 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: g_dynkin_dynkin.
Qed.

End dynkin_lemmas.

Section trace.
Variable (T : Type).
Implicit Types (G : set (set T)) (A D : set T).

Definition G D := [set x `&` D | x in G].

Lemma subset_strace G C : G `<=` C -> forall D, strace G D `<=` strace C D.

Proof.

by move=> GC D _ [A GA <-]; exists A => //; exact: GC. Qed.

Lemma g_sigma_ring_strace G A B : <<sr strace G A >> B -> B `<=` A.

Proof.

move=> H; apply H => /=; split; first exact: powerset_sigma_ring.
by move=> X [A0 GA0 <-]; exact: subIsetr.
Qed.

Lemma strace_sigma_ring G A : sigma_ring (strace <<sr G>> A).

Proof.

split.
- by exists set0; rewrite ?set0I//; have [] := smallest_sigma_ring G.
- move=> _ _ [A0 GA0] <- [A1 GA1] <-.
  exists (A0 `\` A1); first by have [_ + _] := smallest_sigma_ring G; exact.
  by rewrite -setIDA setDIr setDv setU0 setIDAC setIDA.
- move=> F GAF.
  pose f n := sval (cid2 (GAF n)).
  pose Hf n := (svalP (cid2 (GAF n))).1.
  pose H n := (svalP (cid2 (GAF n))).2.
  exists (\bigcup_k f k).
    by have [_ _] := smallest_sigma_ring G; apply => n; exact: Hf.
  by rewrite setI_bigcupl; apply: eq_bigcupr => i _; exact: H.
Qed.

see Paul Halmos' Measure Theory, Ch.1, sec.5, thm.E, p.25

Lemma setI_g_sigma_ring G A : strace <<sr G >> A = <<sr strace G A >>.

Proof.

pose D := [set B `|` (C `\` A) | B in <<sr strace G A>> & C in <<sr G >>].
have D_sigma_ring : sigma_ring D.
  split.
  - exists set0; first by have [] := smallest_sigma_ring (strace G A).
    exists set0; first by have [] := smallest_sigma_ring G.
    by rewrite set0D setU0.
  - move=> _ _ [B0 GAB0] [C0 GC0] <- [B1 GAB1] [C1 GC1] <-.
    exists (B0 `\` B1).
      by have [_ + _] := smallest_sigma_ring (strace G A); exact.
    exists (C0 `\` C1); first by have [_ + _] := smallest_sigma_ring G; exact.
    apply/esym; rewrite setDUD.
    transitivity (((B0 `\` B1) `&` (B0 `\` (C1 `\` A))) `|`
                  ((C0 `\` (A `|` B1)) `&` (C0 `\` C1))).
      congr setU; first by rewrite setDUr.
      apply/seteqP; split => [x [[C0x Ax]]|x].
        move=> /not_orP[B1x /not_andP[C1x|//]].
        by split=> //; split => // -[].
      move=> [[C0x /not_orP[Ax B1x] [_ C1x]]].
      by split=> // -[//|[]].
    transitivity (((B0 `\` B1) `&` B0) `|`
                  ((C0 `\` A ) `&` (C0 `\` C1))).
      apply/seteqP; split => [x [[[B0x B1x] [_ /not_andP[C1x|]]]|
                                 [[C0x /not_orP[Ax B1x]] [_ C1x]]]|
                              x [[[B0x B1x] _]|[[C0x Ax] [_ C1x]]]].
      + by left; split.
      + by move=> /contrapT Ax; left.
      + by right; split.
      + left; split => //; split => // -[] _; apply.
        exact: (g_sigma_ring_strace GAB0).
      + right; split => //; split => // -[//|B1x]; apply: Ax.
        exact: (g_sigma_ring_strace GAB1).
      + congr setU; first by rewrite setDE setIAC setIid.
        by rewrite setDDl setDUr setIC.
  - move=> F DF.
    pose f n := sval (cid2 (DF n)).
    pose Hf n := (svalP (cid2 (DF n))).1.
    pose g n := sval (cid2 (svalP (cid2 (DF n))).2).
    pose Hg n := (svalP (cid2 (svalP (cid2 (DF n))).2)).1.
    exists (\bigcup_n f n).
      have [_ _] := smallest_sigma_ring (strace G A).
      by apply => n; exact: Hf.
    exists (\bigcup_n g n).
      have [_ _] := smallest_sigma_ring G.
      by apply => n; exact: Hg.
    pose H n := (svalP (cid2 (svalP (cid2 (DF n))).2)).2.
    by rewrite setD_bigcupl -bigcupU; apply: eq_bigcupr => k _; exact: H.
apply/seteqP; split => [|].
  have GD : G `<=` D.
    move=> E GE; exists (E `&` A).
      by apply: sub_g_sigma_ring; exists E.
    by exists E; [exact: sub_g_sigma_ring|exact: setUIDK].
  have {}GD : <<sr G >> `<=` D by exact: smallest_sub GD.
  have GDA : strace <<sr G >> A `<=` strace D A by exact: subset_strace.
  suff: strace D A = <<sr strace G A >> by move=> <-.
  apply/seteqP; split.
    move=> _ [_ [gA HgA [g Hg] <-] <-].
    by rewrite setIUl setDKI setU0 setIidl//; exact: (g_sigma_ring_strace HgA).
  move=> X HX; exists X.
    exists X => //; exists set0; rewrite ?set0D ?setU0//.
    by have [] := smallest_sigma_ring G.
  by rewrite setIidl//; exact: (g_sigma_ring_strace HX).
have : strace G A `<=` strace <<sr G>> A.
  by move=> X [Y GY <-]; exists Y => //; exact: sub_smallest GY.
by apply: smallest_sub; exact: strace_sigma_ring.
Qed.

Lemma sigma_algebra_strace G D :
sigma_algebra setT G -> sigma_algebra D (strace G D).

Proof.

move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I.
- move=> S [A mA ADS]; have mCA := GC _ mA.
  have : strace G D (D `&` ~` A).
    by rewrite setIC; exists (setT `\` A) => //; rewrite setTD.
  rewrite -setDE => trDA.
  have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0.
  by rewrite DADS in trDA.
- move=> S mS; have /choice[M GM] : forall n, exists A, G A /\ S n = A `&` D.
    by move=> n; have [A mA ADSn] := mS n; exists A.
  exists (\bigcup_i (M i)); first by apply GU => i; exact: (GM i).1.
  by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2.
Qed.

End trace.

HB.mixin Record isSemiRingOfSets (d : measure_display) 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 Pointed T & isSemiRingOfSets d T}.

Arguments measurable {d}%_measure_display_scope {s} _%_classical_set_scope.

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 SemiRingOfSets_isRingOfSets d T & SemiRingOfSets d T := {
  measurableU : @setU_closed T measurable
}.

#[short(type="ringOfSetsType")]
HB.structure Definition RingOfSets d :=
  {T of SemiRingOfSets d T & SemiRingOfSets_isRingOfSets d T }.

HB.mixin Record RingOfSets_isAlgebraOfSets d T & RingOfSets d T := {
  measurableT : measurable [set: T]
}.

#[short(type="algebraOfSetsType")]
HB.structure Definition AlgebraOfSets d :=
  {T of RingOfSets d T & RingOfSets_isAlgebraOfSets d T }.

HB.mixin Record hasMeasurableCountableUnion d T & SemiRingOfSets d T := {
  bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) ->
    measurable (\bigcup_i (F i))
}.

HB.builders Context d T & hasMeasurableCountableUnion d T.

Let mU : @setU_closed T measurable.

Proof.

move=> A B mA mB; rewrite -bigcup2E.
by apply: bigcupT_measurable => -[//|[//|/= _]]; exact: measurable0.
Qed.

HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T mU.

HB.end.

#[short(type="sigmaRingType")]
HB.structure Definition SigmaRing d :=
  {T of SemiRingOfSets d T & hasMeasurableCountableUnion d T}.

HB.factory Record isSigmaRing (d : measure_display) T & Pointed T := {
  measurable : set (set T) ;
  measurable0 : measurable set0 ;
  measurableD : setD_closed measurable ;
  bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) ->
    measurable (\bigcup_i (F i))
}.

HB.builders Context d T & isSigmaRing d T.

Let m0 : measurable set0

Proof.

exact: measurable0. Qed.

Let mI : setI_closed measurable.

Proof.

by have [] := (setD_closedP measurable).1 measurableD. Qed.

Let mD : semi_setD_closed measurable.

Proof.

by apply: setD_semi_setD_closed; exact: measurableD. Qed.

HB.instance Definition _ := isSemiRingOfSets.Build d T m0 mI mD.

HB.instance Definition _ := hasMeasurableCountableUnion.Build d T bigcupT_measurable.

HB.end.

#[short(type="measurableType")]
HB.structure Definition Measurable d :=
  {T of AlgebraOfSets d T & hasMeasurableCountableUnion d T }.

HB.factory Record isRingOfSets (d : measure_display) T & Pointed T := {
  measurable : set (set T) ;
  measurable0 : measurable set0 ;
  measurableU : setU_closed measurable;
  measurableD : setD_closed measurable;
}.

HB.builders Context d T & isRingOfSets d T.
Implicit Types (A B C D : set T).

Lemma mI : setI_closed measurable.

Proof.

by have [] := (setD_closedP measurable).1 measurableD. Qed.

Lemma mD : semi_setD_closed measurable.

Proof.

by apply: setD_semi_setD_closed; exact: measurableD. Qed.

HB.instance Definition _ :=
  @isSemiRingOfSets.Build d T measurable measurable0 mI mD.

HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU.

HB.end.

HB.factory Record isRingOfSets_setY (d : measure_display) T
    & Pointed T := {
  measurable : set (set T) ;
  measurable_nonempty : measurable !=set0 ;
  measurable_setY : setY_closed measurable ;
  measurable_setI : setI_closed measurable }.

HB.builders Context d T & isRingOfSets_setY d T.

Let m0 : measurable set0.

Proof.

have [A mA] := measurable_nonempty.
have := measurable_setY mA mA.
by rewrite setYK.
Qed.

Let mU : setU_closed measurable.

Proof.

move=> A B mA mB; rewrite -setYU.
by apply: measurable_setY; [exact: measurable_setY|exact: measurable_setI].
Qed.

Let mD : setD_closed measurable.

Proof.

move=> A B mA mB; rewrite -setYD.
by apply: measurable_setY => //; exact: measurable_setI.
Qed.

HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD.

HB.end.

HB.factory Record isAlgebraOfSets (d : measure_display) T & Pointed T := {
  measurable : set (set T) ;
  measurable0 : measurable set0 ;
  measurableU : setU_closed measurable;
  measurableC : setC_closed measurable
}.

HB.builders Context d T & isAlgebraOfSets d T.

Lemma mD : setD_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
measurable measurable0 measurableU mD.

Lemma measurableT : measurable [set: T].

Proof.

by rewrite -setC0; apply: measurableC; exact: measurable0. Qed.

HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.

HB.end.

HB.factory Record isAlgebraOfSets_setD (d : measure_display) T & Pointed T := {
  measurable : set (set T) ;
  measurableT : measurable [set: T] ;
  measurableD : setD_closed measurable
}.

HB.builders Context d T & isAlgebraOfSets_setD d T.

Let m0 : measurable set0.

Proof.

by rewrite -(setDT setT); apply: measurableD; exact: measurableT. Qed.

Let mU : setU_closed measurable.

Proof.

move=> A B mA mB.
rewrite -(setCK A) -setCD -!setTD; apply: measurableD; first exact: measurableT.
by do 2 apply: measurableD => //; exact: measurableT.
Qed.

HB.instance Definition _ := isRingOfSets.Build d T m0 mU measurableD.

HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.

HB.end.

HB.factory Record isMeasurable (d : measure_display) T & Pointed 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 & 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 _ := @isAlgebraOfSets.Build d T
  measurable measurable0 mU mC.

HB.instance Definition _ :=
  @hasMeasurableCountableUnion.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 : setD_closed (@measurable d T).

Proof.

move=> A B mA mB; case: (semi_measurableD A B) => // [D [Dfin Dl -> _]].
by apply: fin_bigcup_measurable.
Qed.

Lemma seqDU_measurable (F : sequence (set T)) :
(forall n, measurable (F n)) -> forall n, measurable (seqDU F n).

Proof.

by move=> Fmeas n; apply/measurableD/bigsetU_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.

Lemma measurableID A B : measurable A -> measurable (A `&` B) ->
measurable (A `\` B).

Proof.

move=> mA /measurableC; rewrite setCI => /(measurableI A) => /(_ mA).
by rewrite setIUr setICr set0U.
Qed.

End algebraofsets_lemmas.

Section sigmaring_lemmas.
Context d (T : sigmaRingType d).
Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat).

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 : P !=set0 ->
(forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i).

Proof.

move=> [j Pj] PF; rewrite -(setD_bigcup F Pj).
apply: measurableD; first exact: PF.
by apply: bigcup_measurable => k/= [Pk kj]; apply: measurableD; exact: PF.
Qed.

Lemma bigcapT_measurable F :
(forall k, measurable (F k)) -> measurable (\bigcap_i F i).

Proof.

by move=> PF; apply: bigcap_measurable => //; exists 1. Qed.

End sigmaring_lemmas.

Lemma dynkin_induction d {T : measurableType d} (G : set (set T))
    (P : set_system T) :
  @measurable _ T = <<s G >> ->
  setI_closed G ->
  P [set: T] ->
  G `<=` P ->
  (forall S, measurable S -> P S -> P (~` S)) ->
  (forall F : (set T)^nat,
    (forall n, measurable (F n)) ->
    trivIset [set: nat] F ->
    (forall n, P (F n)) -> P (\bigcup_k F k)) ->
  (forall S, <<s G >> S -> P S).

Proof.

move=> GE GI PsetT GP PsetC Pbigcup A sGA.
suff: <<s G >> `<=` [set A | measurable A /\ P A] by move=> /(_ _ sGA)[].
apply: lambda_system_subset; [by []| | |by []].
- apply/dynkin_lambda_system; split => //.
  + by move=> B [mB PB]; split; [exact: measurableC|exact: PsetC].
  + move=> F tF Hm; split.
      by apply: bigcup_measurable => k _; apply Hm.
    by apply: Pbigcup => //; apply Hm.
- move=> B GB; split; last exact: GP.
  by rewrite GE; exact: sub_gen_smallest.
Qed.

Lemma countable_measurable d (T : sigmaRingType d) (A : set T) :
(forall t : T, measurable [set t]) -> countable A -> measurable A.

Proof.

move=> m1; have [->//|/set0P[r Ar]/countable_injP[f injf]] := eqVneq A set0.
rewrite -(injpinv_image (cst r) injf).
rewrite [X in _ X](_ : _ = \bigcup_(x in f @` A) [set 'pinv_(cst r) A f x]).
by apply: bigcup_measurable => _ /= [s As <-].
by rewrite eqEsubset; split=> [_ [_ [s As <-]] <-|_ [_ [s As <-]] ->];
exists (f s).
Qed.

Section sigma_ring_lambda_system.
Context d (T : sigmaRingType d).

Lemma sigmaRingType_lambda_system (D : set T) : measurable D ->
lambda_system D [set X | measurable X /\ X `<=` D].

Proof.

move=> mD; split.
- by move=> A /=[].
- by split.
- move=> B A AB/= [mB BD] [mA AD]; split; first exact: measurableD.
  by apply: subset_trans BD; exact: subDsetl.
- move=> /= F _ mFD; split.
    by apply: bigcup_measurable => i _; exact: (mFD _).1.
  by apply: bigcup_sub => i _; exact: (mFD _).2.
Qed.

End sigma_ring_lambda_system.

Lemma countable_bigcupT_measurable d (T : sigmaRingType d) U
(F : U -> set T) : countable [set: U] ->
(forall i, measurable (F i)) -> measurable (\bigcup_i F i).

Proof.

elim/Ppointed: U => U in F *; first by move=> *; rewrite empty_eq0 bigcup0.
move=> /countable_bijP[B] /ppcard_eqP[f] Fm.
rewrite (reindex_bigcup f^-1%FUN setT)//=; first exact: bigcupT_measurable.
exact: (@subl_surj _ _ B).
Qed.

Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) :
(forall i, measurable (F i)) -> measurable (\bigcup_i F i).

Proof.

exact/countable_bigcupT_measurable. Qed.

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

End measurable_lemmas.

Section discrete_measurable.
Context {T : Type}.

Definition : set (set T) := [set: set T].

Lemma discrete_measurable0 : discrete_measurable set0

Proof.

by []. Qed.

Lemma discrete_measurableC X :
discrete_measurable X -> discrete_measurable (~` X).

Proof.

by []. Qed.

Lemma discrete_measurableU (F : (set T)^nat) :
(forall i, discrete_measurable (F i)) ->
discrete_measurable (\bigcup_i F i).

Proof.

by []. Qed.

Proof.

exact. Qed.

Definition {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.

HB.instance Definition _ := Pointed.on (g_sigma_algebraType G).
HB.instance Definition _ := @isMeasurable.Build (sigma_display G)
  (g_sigma_algebraType G)
  <<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 (g_sigma_algebraType 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.

Section measurability.

Definition {aT rT : Type} (D : set aT) (f : aT -> rT)
    (G : set_system rT) : set (set aT) :=
  [set D `&` f @^-1` B | B in G].

Lemma preimage_set_system0 {aT rT : Type} (D : set aT) (f : aT -> rT) :
  preimage_set_system D f set0 = set0.

Proof.

exact: image_set0. Qed.

Lemma preimage_set_systemU {aT rT : Type} (D : set aT) (f : aT -> rT) :
{morph preimage_set_system D f : x y / x `|` y >-> x `|` y}.

Proof.

exact: image_setU. Qed.

Lemma preimage_set_system_comp {aT bT rT : Type} (D : set aT)
    (f : aT -> bT) (g : bT -> rT) (F : set_system rT) :
  preimage_set_system D (g \o f) F
    = preimage_set_system D f (preimage_set_system setT g F).

Proof.

apply/seteqP; split=> [_ [B FB] <-|_ [_ [C FC <-] <-]].
by exists (g @^-1` B) => //; exists B => //; rewrite setTI.
by exists C => //; rewrite setTI comp_preimage.
Qed.

Lemma preimage_set_system_id {aT : Type} (D : set aT) (F : set (set aT)) :
preimage_set_system D idfun F = setI D @` F.

Proof.

by []. Qed.

Lemma sigma_algebra_preimage (aT rT : Type) (G : set (set rT))
(D : set aT) (f : aT -> rT) :
sigma_algebra setT G -> sigma_algebra D (preimage_set_system D f G).

Proof.

case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0.
- move=> A; rewrite /preimage_set_system /= => -[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_set_system /= => 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 {T T'} : (T -> T') -> measure_display.

Proof.

exact. Qed.

Definition d' (T : pointedType)
  (T' : measurableType d') (f : T -> T') : Type := T.

Definition d' (T : pointedType)
    (T' : measurableType d') (f : T -> T') :=
  preimage_set_system setT f (@measurable _ T').

Section preimage_generated_sigma_algebra.
Context {d'} (T : pointedType) (T' : measurableType d').
Variable f : T -> T'.

Let preimage_set0 : g_sigma_algebra_preimage f set0.

Proof.

rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
by exists set0 => //; rewrite preimage_set0 setI0.
Qed.

Let preimage_setC A :
g_sigma_algebra_preimage f A -> g_sigma_algebra_preimage f (~` A).

Proof.

rewrite /g_sigma_algebra_preimage /preimage_set_system/= => -[B mB] <-{A}.
by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC].
Qed.

Let preimage_bigcup (F : (set T)^nat) :
(forall i, g_sigma_algebra_preimage f (F i)) ->
g_sigma_algebra_preimage f (\bigcup_i (F i)).

Proof.

move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
pose g := fun i => sval (cid2 (mF i)).
pose mg := fun i => svalP (cid2 (mF i)).
exists (\bigcup_i g i).
by apply: bigcup_measurable => k; case: (mg k).
rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _.
by case: (mg k) => _; rewrite setTI.
Qed.

HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f).

HB.instance Definition _ := @isMeasurable.Build (preimage_display f)
  (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f)
  preimage_set0 preimage_setC preimage_bigcup.

End preimage_generated_sigma_algebra.

Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
Notation "f .-preimage.-measurable" :=
  (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.

Definition (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 (aT rT : Type) (D : set aT) (f : aT -> rT)
    (G : set (set aT)) :
  sigma_algebra D G -> sigma_algebra setT (image_set_system D f G).

Proof.

move=> [G0 GC GU]; split; rewrite /image_set_system.
- 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 g_sigma_preimageE aT (rT : pointedType) (D : set aT)
    (f : aT -> rT) (G' : set (set rT)) :
  <<s D, preimage_set_system D f G' >> =
    preimage_set_system D f (G'.-sigma.-measurable).

Proof.

rewrite eqEsubset; split.
  have mG : sigma_algebra D
      (preimage_set_system D f (G'.-sigma.-measurable)).
    exact/sigma_algebra_preimage/sigma_algebra_measurable.
  have subset_preimage : preimage_set_system D f G' `<=`
                         preimage_set_system D f (G'.-sigma.-measurable).
    by move=> A [B CCB <-{A}]; exists B => //; exact: sub_sigma_algebra.
  exact: smallest_sub.
have G'pre A' : G' A' -> (preimage_set_system D f G') (D `&` f @^-1` A').
  by move=> ?; exists A'.
pose I : set (set aT) := <<s D, preimage_set_system D f G' >>.
have G'sfun : G' `<=` image_set_system D f I.
  by move=> A' /G'pre[B G'B h]; apply: sub_sigma_algebra; exists B.
have sG'sfun : <<s G' >> `<=` image_set_system D f I.
  apply: smallest_sub => //; apply: sigma_algebra_image.
  exact: smallest_sigma_algebra.
by move=> _ [B mB <-]; exact: sG'sfun.
Qed.

End measurability.
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system`")]
Notation preimage_class := preimage_set_system (only parsing).
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `image_set_system`")]
Notation image_class := image_set_system (only parsing).
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_preimage`")]
Notation sigma_algebra_preimage_class := sigma_algebra_preimage (only parsing).
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_image`")]
Notation sigma_algebra_image_class := sigma_algebra_image (only parsing).

#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")]
Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing).

This predicate is used also by `measure_function.v`

Definition {T} {R : numFieldType}
  (mu : set T -> \bar R) (A : set T) (F : nat -> set T) :=
  A `<=` \bigcup_n F n -> (mu A <= \sum_(n <oo) mu (F n))%E.

Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R)
   (op : Monoid.com_law idx) (A : I -> set T) (F : set T -> R) :
    finite_set D -> trivIset D A -> F set0 = idx ->
  \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 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.

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.

Definition d1 d2
    (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2) (T : Type)
    (f1 : T -> T1) (f2 : T -> T2) :=
  <<s preimage_set_system setT f1 measurable `|`
      preimage_set_system setT f2 measurable >>.
#[deprecated(since="mathcomp-analysis 1.9.0",
  note="renamed to `g_sigma_preimageU`")]
Notation preimage_classes := g_sigma_preimageU (only parsing).

Section product_lemma.
Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2).
Variables (T : pointedType) (f1 : T -> T1) (f2 : T -> T2).
Variables (T3 : Type) (g : T3 -> T).

Lemma g_sigma_preimageU_comp : g_sigma_preimageU (f1 \o g) (f2 \o g) =
  preimage_set_system setT g (g_sigma_preimageU f1 f2).

Proof.

rewrite {1}/g_sigma_preimageU -g_sigma_preimageE; 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.
#[deprecated(since="mathcomp-analysis 1.9.0",
note="renamed to `g_sigma_preimageU_comp`")]
Notation preimage_classes_comp := g_sigma_preimageU_comp (only parsing).

Definition :
(measure_display * measure_display) -> measure_display.

Proof.

exact. Qed.

Section product_salgebra_instance.
Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2).
Let f1 := @fst T1 T2.
Let f2 := @snd T1 T2.

Let prod_salgebra_set0 : g_sigma_preimageU f1 f2 (set0 : set (T1 * T2)).

Proof.

exact: sigma_algebra0. Qed.

Let prod_salgebra_setC A : g_sigma_preimageU f1 f2 A ->
g_sigma_preimageU f1 f2 (~` A).

Proof.

exact: sigma_algebraC. Qed.

Let prod_salgebra_bigcup (F : _^nat) :
(forall i, g_sigma_preimageU f1 f2 (F i)) ->
g_sigma_preimageU f1 f2 (\bigcup_i (F i)).

Proof.

exact: sigma_algebra_bigcup. Qed.

HB.instance Definition _ := Pointed.on (T1 * T2)%type.
HB.instance Definition prod_salgebra_mixin :=
  @isMeasurable.Build (measure_prod_display (d1, d2))
    (T1 * T2)%type (g_sigma_preimageU 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 measurableX d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType 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) setXI.
rewrite setXT setTX; 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_algebraOfSetsType.
Context d1 d2 (T1 : algebraOfSetsType d1) (T2 : algebraOfSetsType 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_set_system 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_set_system 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 ?] [B ?] <-; apply: measurableX => //; exact: sub_sigma_algebra.
Qed.

End product_salgebra_algebraOfSetsType.

Section product_salgebra_g_measurableTypeR.
Context d1 (T1 : algebraOfSetsType d1) (T2 : pointedType) (C2 : set (set T2)).
Hypothesis setTC2 : setT `<=` C2.

Lemma measurable_prod_g_measurableTypeR :
@measurable _ (T1 * g_sigma_algebraType 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 _ (g_sigma_algebraType C1 * g_sigma_algebraType 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.

Definition d (rT : semiRingOfSetsType d) (aT : Type)
    (n : nat) (f : 'I_n -> aT -> rT) : set (set aT) :=
  <<s \big[setU/set0]_(i < n) preimage_set_system setT (f i) measurable >>.

Lemma g_sigma_preimage_comp d1 {T1 : semiRingOfSetsType d1} n
    {T : pointedType} (f : 'I_n -> T -> T1) {T2 : Type} (g : T2 -> T) :
  g_sigma_preimage (fun i => f i \o g) =
  preimage_set_system [set: T2] g (g_sigma_preimage f).

Proof.

rewrite -[RHS]g_sigma_preimageE; congr (<<s _ >>).
case: n => [|n] in f *; first by rewrite !big_ord0 preimage_set_system0.
rewrite predeqE => B; split.
- rewrite -bigcup_mkord_ord => -[i Ii [A mA <-{B}]].
  have iE : Ordinal Ii = inord i by apply/val_inj => /=; rewrite inordK.
  exists (f (inord i) @^-1` A) => //.
  rewrite -bigcup_mkord_ord; exists i => //.
  by exists A => //; rewrite -iE setTI.
- move=> [C].
  rewrite -bigcup_mkord_ord => -[i Ii [A mA <-{C}]] <-{B}.
  rewrite -bigcup_mkord_ord; exists i => //.
  by exists A => //; rewrite !setTI -comp_preimage.
Qed.

Definition : measure_display -> measure_display.

Proof.

exact. Qed.

Section measurable_tuple.
Context {d} {T : sigmaRingType d}.
Variable n : nat.

Let coors : 'I_n -> n.-tuple T -> T := fun i x => @tnth n T x i.

Let tuple_set0 : g_sigma_preimage coors set0.

Proof.

exact: sigma_algebra0. Qed.

Let tuple_setC A : g_sigma_preimage coors A -> g_sigma_preimage coors (~` A).

Proof.

exact: sigma_algebraC. Qed.

Let tuple_bigcup (F : _^nat) : (forall i, g_sigma_preimage coors (F i)) ->
g_sigma_preimage coors (\bigcup_i (F i)).

Proof.

exact: sigma_algebra_bigcup. Qed.

HB.instance Definition _ := @isMeasurable.Build (measure_tuple_display d)
(n.-tuple T) (g_sigma_preimage coors) tuple_set0 tuple_setC tuple_bigcup.

End measurable_tuple.

Files

Module mathcomp.analysis.measure_theory.measurable_structure