Module mathcomp.analysis.measure_theory.measurable_structure

From HB Require Import structures.
From mathcomp Require Import boot order algebra finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions cardinality reals.

# 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. pmeasurableType == the type of pointed sigma-algebras The HB class is PMeasurable. ``` ## 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 ``` 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 ``` ## 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. ```

Unset 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 := .
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 {} ( : set_system T -> Prop) ( : set T) ( : set_system T).

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

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

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

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

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

Lemma : 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 , nondecreasing_seq F -> (forall , G (F i)) -> G (\bigcup_ (F i)).

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

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

Definition :=
  forall ( : set I) ( : I -> set T), finite_set D -> trivIset D F ->
   (forall , D i -> G (F i)) -> G (\bigcup_( in D) F k).

Definition := [/\ G set0, setU_closed G & setD_closed].

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

Definition :=
  [/\ G set0, (forall , G A -> G (D `\` A)) &
     (forall : (set T)^nat, (forall , G (A n)) -> G (\bigcup_ 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 , 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 := setD_closed (only parsing).
#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_semi_setD_closed`")]
Notation := setD_semi_setD_closed (only parsing).

Lemma ( : Type) ( : set T) :
sigma_ring [set | 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 ( : Type) ( : set T) :
lambda_system D [set | X `<=` D].

Proof.

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

Notation := (smallest (lambda_system D) G) :
classical_set_scope.
Notation := (<<l setT, G>>) : classical_set_scope.
Notation := (smallest dynkin G) : classical_set_scope.
Notation := (smallest (sigma_algebra D) G) :
classical_set_scope.
Notation := (<<s setT, G>>) : classical_set_scope.
Notation := (smallest setring G) : classical_set_scope.
Notation := (smallest sigma_ring G) : classical_set_scope.
Notation := (smallest monotone G) : classical_set_scope.

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

Lemma : 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 ( : set_system 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 ( : set_system 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 ( : set_system 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 := setD_closed (only parsing).

Lemma ( : choiceType) ( : set T)
    ( : I -> set_system T) ( : set I) :
  (forall , J n -> sigma_algebra D (F n)) ->
  sigma_algebra D (\bigcap_( 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 ( : set_system T) :
  (forall , 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)); last first.
    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))); last first.
    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_ \big[setU/set0]_( < i.+1) F j).
    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.
  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))).
      by rewrite setDIr// !setDD (setIidr (C_subU _ DA)) (setIidr (C_subU _ _)).
    apply DC => //; last by apply: DI; apply: DC => //; exact: C_subU.
    by apply: subIset; left; apply: subIset; left.
  by rewrite big_ord_recr; exact: CU.
Qed.

Section generated_sigma_algebra.
Context { : Type} ( : set T) ( : set_system T).
Implicit Type M : set_system T.

Lemma : 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 : M `<=` <<s D, G>> -> <<s D, M >> `<=` <<s D, G >>.

Proof.

move=> MsG A + H [sH GH]; apply; split => //; apply: (subset_trans MsG).
exact: bigcap_inf.
Qed.

Lemma : M `<=` G -> <<s D, M >> `<=` <<s D, G >>.

Proof.

exact: sub_smallest2r. Qed.

Lemma : sigma_algebra D G -> <<s D, G >> = G.

Proof.

by move=> /smallest_id->. Qed.

Lemma : G `<=` <<s D, G >>

Proof.

exact: sub_smallest. Qed.

Lemma : <<s D, G >> set0.

Proof.

by case: smallest_sigma_algebra. Qed.

Lemma : forall , <<s D, G >> A -> <<s D, G >> (D `\` A).

Proof.

by case: smallest_sigma_algebra. Qed.

Lemma ( : (set T)^nat) :
(forall , <<s D, G >> (A i)) -> <<s D, G >> (\bigcup_ (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 { : Type} ( : set_system T).
Implicit Type M : set_system T.

Lemma : 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 : M `<=` G -> <<r M >> `<=` <<r G >>.

Proof.

exact: sub_smallest2r. Qed.

Lemma : setring G -> <<r G >> = G.

Proof.

by move=> /smallest_id->. Qed.

Lemma : G `<=` <<r G >>

Proof.

exact: sub_smallest. Qed.

Lemma : <<r G >> set0.

Proof.

by case: smallest_setring. Qed.

Lemma : setD_closed <<r G>>.

Proof.

by case: smallest_setring. Qed.

Lemma : setU_closed <<r G>>.

Proof.

by case: smallest_setring. Qed.

Lemma : 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 := setringD (only parsing).

Lemma ( : set_system T) ( : set T) :
(forall , <<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 ( : set_system 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 ( : set_system 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 ( : set_system T) : monotone <<sr G >>.

Proof.

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

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

Proof.

exact: sub_smallest. Qed.

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

Lemma ( : set_system 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 ( : set_system 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 ( : Type) ( : set_system T).
Hypothesis : setring G.

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

Lemma : setring <<M G>>.

Proof.

pose M := <<M G>>.
pose K := [set | [/\ 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 : <<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 ( : set_system 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 ( : Type) ( : set_system T) ( : setI_closed G) ( : set T).
Hypothesis : lambda_system D <<l D, G >>.

Lemma : (forall , <<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_ := [set | 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)).
    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 ( : Type) ( : set_system T) ( : setI_closed G) ( : set T).
Variables ( : set_system T) ( : lambda_system D H) ( : G `<=` H).

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

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

Proof.

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

End lambda_system_subset.

Section dynkin.
Variable : Type.
Implicit Types G D : set_system T.

Lemma : dynkin G -> G setT

Proof.

by case. Qed.

Lemma : dynkin G -> setC_closed G

Proof.

by case. Qed.

Lemma : dynkin G -> (forall : (set T)^nat, trivIset setT F ->
(forall , G (F n)) -> G (\bigcup_ F k))

Proof.

by case. Qed.

End dynkin.

Section dynkin_lemmas.
Variable : Type.
Implicit Types D G : set_system T.

Lemma : 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 := \big[setU/set0]_( < 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)).
    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 <<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 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 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 -> <<d G >> = <<s G >>.

Proof.

move=> GI; rewrite eqEsubset; split.
  by apply: sub_smallest2l; exact: sigma_algebra_dynkin.
pose delta ( : set T) := [set | <<d G >> (E `&` D)].
have ddelta ( : 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 ( : Type).
Implicit Types (G : set_system T) (A D : set T).

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

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

Proof.

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

Lemma : <<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 : 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 := sval (cid2 (GAF n)).
  pose Hf := (svalP (cid2 (GAF n))).1.
  pose H := (svalP (cid2 (GAF n))).2.
  exists (\bigcup_ 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 : strace <<sr G >> A = <<sr strace G A >>.

Proof.

pose D := [set B `|` (C `\` A) | in <<sr strace G A>> & 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 := sval (cid2 (DF n)).
    pose Hf := (svalP (cid2 (DF n))).1.
    pose g := sval (cid2 (svalP (cid2 (DF n))).2).
    pose Hg := (svalP (cid2 (svalP (cid2 (DF n))).2)).1.
    exists (\bigcup_ f n).
      have [_ _] := smallest_sigma_ring (strace G A).
      by apply => n; exact: Hf.
    exists (\bigcup_ g n).
      have [_ _] := smallest_sigma_ring G.
      by apply => n; exact: Hg.
    pose H := (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 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 , exists , G A /\ S n = A `&` D.
    by move=> n; have [A mA ADSn] := mS n; exists A.
  exists (\bigcup_ (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.

. () T := {
  measurable : set_system T ;
  measurable0 : measurable set0 ;
  measurableI : setI_closed measurable;
  semi_measurableD : semi_setD_closed measurable;
}.

()
.
  { of Choice T & isSemiRingOfSets d T}.

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

Lemma ( : Type) ( : semiRingOfSetsType d)
    ( : T1 * T2 -> set T) ( : T1 * T2) :
  measurable (G x) <-> measurable (curry G x.1 x.2).

Proof.

by case: x. Qed.

Notation := (@measurable d%mdisp) : classical_set_scope.
Notation :=
  (@measurable default_measure_display) : classical_set_scope.

. d T := {
  measurableU : @setU_closed T measurable
}.

()
.
  { of SemiRingOfSets d T & SemiRingOfSets_isRingOfSets d T }.

. d T := {
  measurableT : measurable [set: T]
}.

()
.
  { of RingOfSets d T & RingOfSets_isAlgebraOfSets d T }.

. d T := {
  bigcupT_measurable : forall : (set T)^nat, (forall , measurable (F i)) ->
    measurable (\bigcup_ (F i))
}.

. d T.

Let : @setU_closed T measurable.

Proof.

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

..Build d T mU.

..

()
.
  { of SemiRingOfSets d T & hasMeasurableCountableUnion d T}.

. () T & Choice T := {
  measurable : set_system T ;
  measurable0 : measurable set0 ;
  measurableD : setD_closed measurable ;
  bigcupT_measurable : forall : (set T)^nat, (forall , measurable (F i)) ->
    measurable (\bigcup_ (F i))
}.

. d T.

Let : measurable set0

Proof.

exact: measurable0. Qed.

Let : setI_closed measurable.

Proof.

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

Let : semi_setD_closed measurable.

Proof.

by apply: setD_semi_setD_closed; exact: measurableD. Qed.

..Build d T m0 mI mD.

..Build d T bigcupT_measurable.

..

()
.
  { of AlgebraOfSets d T & hasMeasurableCountableUnion d T }.

()
. of Pointed T & Measurable d T}.

. () T & Choice T := {
  measurable : set_system T ;
  measurable0 : measurable set0 ;
  measurableU : setU_closed measurable;
  measurableD : setD_closed measurable;
}.

. d T.
Implicit Types (A B C D : set T).

Lemma : setI_closed measurable.

Proof.

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

Lemma : semi_setD_closed measurable.

Proof.

by apply: setD_semi_setD_closed; exact: measurableD. Qed.

.
  .Build d T measurable measurable0 mI mD.

..Build d T measurableU.

..

. () T
    & Choice T := {
  measurable : set_system T ;
  measurable_nonempty : measurable !=set0 ;
  measurable_setY : setY_closed measurable ;
  measurable_setI : setI_closed measurable }.

. d T.

Let : measurable set0.

Proof.

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

Let : setU_closed measurable.

Proof.

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

Let : setD_closed measurable.

Proof.

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

..Build d T m0 mU mD.

..

. () T & Choice T := {
  measurable : set_system T ;
  measurable0 : measurable set0 ;
  measurableU : setU_closed measurable;
  measurableC : setC_closed measurable
}.

. d T.

Lemma : setD_closed measurable.

Proof.

move=> A B mA mB; rewrite setDE -[A]setCK -setCU.
by do ?[apply: measurableU | apply: measurableC].
Qed.

..Build d T
measurable measurable0 measurableU mD.

Lemma : measurable [set: T].

Proof.

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

..Build d T measurableT.

..

. () T & Choice T := {
  measurable : set_system T ;
  measurableT : measurable [set: T] ;
  measurableD : setD_closed measurable
}.

. d T.

Let : measurable set0.

Proof.

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

Let : 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.

..Build d T m0 mU measurableD.

..Build d T measurableT.

..

. () T & Choice T := {
  measurable : set_system T ;
  measurable0 : measurable set0 ;
  measurableC : forall , measurable A -> measurable (~` A) ;
  measurable_bigcup : forall : (set T)^nat, (forall , measurable (F i)) ->
    measurable (\bigcup_ (F i))
}.

. d T.

Obligation Tactic := idtac.

Lemma : setU_closed measurable.

Proof.

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

Lemma : setC_closed measurable

Proof.

by move=> *; apply: measurableC. Qed.

..Build d T
  measurable measurable0 mU mC.

.
  .Build d T measurable_bigcup.

..

#[global] Hint Extern 0 (measurable set0) => solve [apply: measurable0] : core.
#[global] Hint Extern 0 (measurable setT) => solve [apply: measurableT] : core.

Section ringofsets_lemmas.
Context ( : ringOfSetsType d).
Implicit Types A B : set T.

Lemma ( : pred I) ( : I -> set T) :
  (forall , P i -> measurable (F i)) ->
  measurable (\big[setU/set0]_( <- r | P i) F i).

Proof.

by move=> mF; elim/big_ind : _ => //; exact: measurableU. Qed.

Lemma ( : set I) ( : I -> set T) :
    finite_set D ->
    (forall , D i -> measurable (F i)) ->
  measurable (\bigcup_( 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 : 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 ( : sequence (set T)) :
(forall , measurable (F n)) -> forall , measurable (seqDU F n).

Proof.

by move=> Fmeas n; apply/measurableD/bigsetU_measurable. Qed.

End ringofsets_lemmas.

Section algebraofsets_lemmas.
Context ( : algebraOfSetsType d).
Implicit Types A B : set T.

Lemma : measurable A -> measurable (~` A).

Proof.

by move=> mA; rewrite -setTD; exact: measurableD. Qed.

Lemma ( : pred I) ( : I -> set T) :
(forall , P i -> measurable (F i)) ->
measurable (\big[setI/setT]_( <- 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 ( : set I) ( : I -> set T) :
    finite_set D ->
    (forall , D i -> measurable (F i)) ->
  measurable (\bigcap_( 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 : 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 ( : sigmaRingType d).
Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat).

Lemma :
(forall , P k -> measurable (F k)) -> measurable (\bigcup_( in P) F i).

Proof.

move=> PF; rewrite bigcup_mkcond; apply: bigcupT_measurable => k.
by case: ifP => //; rewrite inE; exact: PF.
Qed.

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

Proof.

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

Lemma {} { : U -> set T}
{ : set U} : countable P -> (forall , P i -> measurable (F i)) ->
measurable (\bigcup_( in P) F i).

Proof.

move=>/[dup] cP /pfcard_geP =>[[-> _|/surjfunPex [f ->] mF]].
by rewrite bigcup0.
by rewrite bigcup_image; apply: bigcupT_measurable=>// i; exact: mF.
Qed.

Lemma {} { : U -> set T} ( : set U) :
P !=set0 -> countable P -> (forall , P k -> measurable (F k)) ->
measurable (\bigcap_( in P) F i).

Proof.

move=> [j Pj] /pfcard_geP=>[[P0|/surjfunPex [f ->] mF]].
by rewrite P0/= in Pj.
by rewrite bigcap_image; apply: bigcap_measurable=>// k _; exact: mF.
Qed.

End sigmaring_lemmas.

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

Proof.

move=> GE GI PsetT GP PsetC Pbigcup A sGA.
suff: <<s G >> `<=` [set | 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 ( : sigmaRingType d) ( : set T) :
(forall : 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_( in f @` A) [set 'pinv_(cst r) A f x]).
by rewrite eqEsubset; split=> [_ [_ [s As <-]] <-|_ [_ [s As <-]] ->];
exists (f s).
by apply: bigcup_measurable => _ /= [s As <-].
Qed.

Section sigma_ring_lambda_system.
Context ( : sigmaRingType d).

Lemma ( : set T) : measurable D ->
lambda_system D [set | 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 ( : sigmaRingType d)
( : U -> set T) : countable [set: U] ->
(forall , measurable (F i)) -> measurable (\bigcup_ 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)//=; last exact: bigcupT_measurable.
exact: (@subl_surj _ _ B).
Qed.

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

Proof.

exact/countable_bigcupT_measurable. Qed.

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

Lemma : measurable D ->
sigma_algebra D (@measurable d T).

Proof.

by move=> mD; split=> // [A|]; [exact: measurableD|exact: bigcupT_measurable].
Qed.

Lemma :
(forall , P k -> measurable (F k)) -> measurable (\bigcap_( 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 { : Type}.

Definition : set_system T := [set: set T].

Lemma : discrete_measurable set0

Proof.

by []. Qed.

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

End discrete_measurable.

..Build default_measure_display
  unit discrete_measurable discrete_measurable0
  discrete_measurableC discrete_measurableU.

..Build default_measure_display
  bool discrete_measurable discrete_measurable0
  discrete_measurableC discrete_measurableU.

..Build default_measure_display
  nat discrete_measurable discrete_measurable0
  discrete_measurableC discrete_measurableU.

Definition {} : set_system T -> measure_display.

Proof.

exact. Qed.

Definition {} ( : set_system T) := T.

Section g_salgebra_instance.
Variables ( : choiceType) ( : set_system T).

Lemma ( : set T) : <<s G >> A -> <<s G >> (~` A).

Proof.

by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed.

..on (g_sigma_algebraType G).
..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.

. (G : set_system T) :=
  Pointed.on (g_sigma_algebraType G).

Notation := (sigma_display G) : measure_display_scope.
Notation :=
  (measurable : set_system (g_sigma_algebraType G)) : classical_set_scope.

Lemma ( : choiceType) ( : set_system T) :
  sigma_algebra setT G -> G.-sigma.-measurable = G.

Proof.

exact: sigma_algebra_id. Qed.

Section measurability.

Lemma ( : Type) ( : set_system rT)
( : set aT) ( : 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 , G x /\ D `&` f @^-1` x = F n.
    by have := mF n => -[B mB <-]; exists B.
  have [F' mF'] := @choice _ _ (fun => G y /\ D `&` f @^-1` y = F x) mF.
  exists (\bigcup_ (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') -> measure_display.

Proof.

exact. Qed.

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

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

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

Let : g_sigma_algebra_preimage f set0.

Proof.

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

Let :
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 ( : (set T)^nat) :
(forall , g_sigma_algebra_preimage f (F i)) ->
g_sigma_algebra_preimage f (\bigcup_ (F i)).

Proof.

move=> mF; rewrite /g_sigma_algebra_preimage /preimage_set_system/=.
pose g := fun => sval (cid2 (mF i)).
pose mg := fun => svalP (cid2 (mF i)).
exists (\bigcup_ 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.

..on (g_sigma_algebra_preimageType f).

..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 := (preimage_display f) : measure_display_scope.
Notation :=
  (measurable : set_system (g_sigma_algebra_preimageType f)) : classical_set_scope.

Lemma ( : Type) ( : set aT) ( : aT -> rT)
    ( : set_system 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)); last 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 ( : choiceType) ( : set aT)
    ( : aT -> rT) ( : set_system 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_system 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.

Lemma ( : choiceType) ( : Type) ( : R)
   ( : Monoid.com_law idx) ( : I -> set T) ( : set T -> R) :
    finite_set D -> trivIset D A -> F set0 = idx ->
  \big[op/idx]_( <- fset_set D) F (A i) =
  \big[op/idx]_( <- (A @` fset_set D)%fset) F X.

Proof.

elim/Pchoice: R => R in idx op F *.
move=> Dfin Atriv F0; symmetry.
pose D' := [fset in fset_set D | A i != set0]%fset.
transitivity (\big[op/idx]_( <- (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//=.
  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 { : Type}.
Implicit Type (C : forall , set_system I).
Implicit Type (P : forall , set I -> set (I -> set T)).

Definition :=
[set : set T | exists , [/\ C I D, P I D A & X = \bigcup_( in D) A i]].

Lemma : (forall , 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 : C I D -> P I D A ->
covered_by C P (\bigcup_( in D) A i).

Proof.

by move=> CID PIDA; exists I, D, A. Qed.

Lemma :
    (forall ( : set I) , (forall , D i -> A i = set0) -> P I D A) ->
    (forall ( : pointedType) , 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 : set T | exists , [/\ P nat `I_n A & X = \bigcup_( < 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 :
    (forall ( : set I) , (forall , D i -> A i = set0) -> P I D A) ->
    (forall ( : choiceType) ( : set I) ( : I -> set T) ( : nat -> I),
       set_surj [set: nat] D f ->
       P I D A -> P nat [set: nat] (A \o f)) ->
  covered_by (@countable) P =
    [set : set T | exists , [/\ P nat [set: nat] A & X = \bigcup_ 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 ( : Type) ( : semiRingOfSetsType d)
( : T1 -> T2 -> set T) ( : T1 * T2) :
measurable (G x.1 x.2) <-> measurable (uncurry G x).

Proof.

by case: x. Qed.

Section g_sigma_algebra_cross.

Yoneda Lemma: two elements in a poset are equal if and only if they share the same set of upper bounds

Let {} ( : set_system T) :
  sigma_algebra [set: T] A -> sigma_algebra [set: T] B ->
  (forall , sigma_algebra [set: T] Z -> A `<=` Z <-> B `<=` Z)
  <-> A = B.

Proof.

move=> sA sB; split=> [AB|AB]; last by rewrite AB.
by apply/seteqP; split; exact/AB.
Qed.

Lemma { : choiceType} ( : set_system T1)
( : set_system T2) :
<<s X `x` <<s Y >> >> = <<s X `x` Y >>.

Proof.

apply/forall_subset_eq; [exact: smallest_sigma_algebra..|].
move=> Z mZ.
rewrite smallest_sub_iff//=.
rewrite {1}/cross12/= subUset -g_sigma_preimageE//.
rewrite smallest_sub_iff//= -subUset -[_ `|` _]/(cross12 X Y)//.
by rewrite smallest_sub_iff.
Qed.

End g_sigma_algebra_cross.

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

Section product_lemma.
Context ( : semiRingOfSetsType d1) ( : semiRingOfSetsType d2).
Variables ( : choiceType) ( : T -> T1) ( : T -> T2).
Variables ( : Type) ( : T3 -> T).

Lemma : 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 := g_sigma_preimageU_comp (only parsing).

Definition :
(measure_display * measure_display) -> measure_display.

Proof.

exact. Qed.

Section product_salgebra_instance.
Context {} {} { : semiRingOfSetsType d1} { : semiRingOfSetsType d2}.
Let := @fst T1 T2.
Let := @snd T1 T2.

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

Proof.

exact: sigma_algebra0. Qed.

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

Proof.

exact: sigma_algebraC. Qed.

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

Proof.

exact: sigma_algebra_bigcup. Qed.

.
  .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 := (measure_prod_display p) : measure_display_scope.
Notation :=
  ((p.-prod).-measurable : set_system (_ * _)) :
    classical_set_scope.

.
     ( d) (Y : pmeasurableType d') :=
  Measurable.on (X * Y)%type.

Lemma
     ( : semiRingOfSetsType d1) ( : semiRingOfSetsType d2)
    ( : set T1) ( : set T2) :
  measurable A -> measurable B -> measurable (A `*` B).

Proof.

move=> mA mB.
rewrite -(setIT A) -(setTI B) setXI 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.

Lemma { : choiceType} ( : set_system T1)
( : set_system T2) : X [set: T1] -> Y [set: T2] ->
<<s rectangle X Y >> = <<s X `x` Y >>.

Proof.

move=> sX sY; apply/seteqP; split.
- rewrite smallest_sub_iff//= => _ [A1 X1] [A2 X2] <-.
  rewrite (_ : _ `*` _ = fst @^-1` A1 `&` snd @^-1` A2)//.
  apply: (@measurableI _ (@g_sigma_algebraType _ (X `x` Y))).
  + by apply: sub_sigma_algebra; left; exists A1 => //; rewrite setTI.
  + by apply: sub_sigma_algebra; right; exists A2 => //; rewrite setTI.
- apply: sigma_algebra_sub => A [|].
  + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}].
    by rewrite -setXT setTI; exact: rectangle_setX.
  + rewrite /preimage_set_system/= => -[A1 XA1 <-{A}].
    by rewrite -setTX setTI; exact: rectangle_setX.
Qed.

Section product_salgebra_algebraOfSetsType.
Context ( : algebraOfSetsType d1) ( : algebraOfSetsType d2).
Let := @measurable _ T1.
Let := @measurable _ T2.

Lemma :
(d1, d2).-prod.-measurable = <<s rectangle M1 M2 >>.

Proof.

by rewrite g_sigma_algebra_rectangle//; exact: measurableT. Qed.

End product_salgebra_algebraOfSetsType.
#[deprecated(since="mathcomp-analysis 1.17.0", use=prod_measurable_rectangle)]
Notation := prod_measurable_rectangle (only parsing).

Section product_salgebra_g_measurableTypeR.
Context ( : algebraOfSetsType d1) ( : choiceType) ( : set_system T2).
Hypothesis : setT `<=` C2.

#[deprecated(since="mathcomp-analysis 1.17.0")]
Lemma :
@measurable _ (T1 * g_sigma_algebraType C2)%type
= <<s rectangle (@measurable _ T1) C2 >>.

Proof.

rewrite prod_measurable_rectangle//; 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 ( : choiceType) ( : set_system T1) ( : set_system T2).
Hypotheses ( : setT `<=` C1) ( : setT `<=` C2).

#[deprecated(since="mathcomp-analysis 1.17.0")]
Lemma :
@measurable _ (g_sigma_algebraType C1 * g_sigma_algebraType C2)%type =
<<s rectangle C1 C2 >>.

Proof.

rewrite prod_measurable_rectangle//; 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 ( : semiRingOfSetsType d) ( : Type)
    ( : nat) ( : 'I_n -> aT -> rT) : set_system aT :=
  <<s \big[setU/set0]_( < n) preimage_set_system setT (f i) measurable >>.

Lemma { : semiRingOfSetsType d1}
    { : choiceType} ( : 'I_n -> T -> T1) { : Type} ( : T2 -> T) :
  g_sigma_preimage (fun => 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 {} { : sigmaRingType d}.
Variable : nat.

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

Let : g_sigma_preimage coors set0.

Proof.

exact: sigma_algebra0. Qed.

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

Proof.

exact: sigma_algebraC. Qed.

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

Proof.

exact: sigma_algebra_bigcup. Qed.

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