measure.v

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect all_algebra finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop .
Require Import reals ereal signed topology normedtype sequences esum numfun.
From HB Require Import structures.

(******************************************************************************)
(*                            Measure Theory                                  *)
(*                                                                            *)
(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.   *)
(*                                                                            *)
(* This files provides a formalization of the basics of measure theory. This  *)
(* includes the formalization of mathematical structures and of measures, as  *)
(* well as standard theorems such as the Measure Extension theorem.           *)
(*                                                                            *)
(* References:                                                                *)
(* - Daniel Li, Intégration et applications, 2016                             *)
(* - Achim Klenke, Probability Theory 2nd edition, 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.                     *)
(*     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_unit == the measurableType corresponding to            *)
(*                             [set: set unit]                                *)
(* discrete_measurable_bool == the measurableType corresponding to            *)
(*                             [set: set bool]                                *)
(*  discrete_measurable_nat == the measurableType corresponding to            *)
(*                             [set: set nat]                                 *)
(*                setring G == the set of sets G contains the empty set, is   *)
(*                             closed by union, and difference                *)
(*                 <<r G >> := smallest setring G                             *)
(*                             <<r G >> is equipped with a structure of ring  *)
(*                             of sets.                                       *)
(*    G.-ring.-measurable A == A belongs for the ring of sets <<r 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 >> *)
(*           salgebraType G == the measurableType corresponding to <<s G >>   *)
(*                             This is an HB alias.                           *)
(*    mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets  *)
(*                                                                            *)
(* * Structures for functions on classes of sets                              *)
(*   (There are a few details about mixins/factories to highlight             *)
(*   implementations peculiarities.)                                          *)
(* {content set T -> \bar R} == type of contents                              *)
(*                            T is expected to be a semiring of sets and R a  *)
(*                            numFieldType.                                   *)
(*                            The HB class is Content.                        *)
(* {measure set T -> \bar R} == type of (non-negative) measures               *)
(*                            T is expected to be a semiring of sets and R a  *)
(*                            numFieldType.                                   *)
(*                            The HB class is Measure.                        *)
(* Content_SubSigmaAdditive_isMeasure ==                                      *)
(*                      mixin that extends a content to a measure with the    *)
(*                      proof that it is semi_sigma_additive                  *)
(* Content_isMeasure == factory that extends a content to a measure with      *)
(*                      the proof that it is sub_sigma_additive               *)
(*                 isMeasure == factory corresponding to the "textbook        *)
(*                            definition" of measures                         *)
(*           sfinite_measure == predicate for s-finite measure functions      *)
(* {sfinite_measure set T -> \bar R} == type of s-finite measures             *)
(*                            The HB class is SFiniteMeasure.                 *)
(*    sfinite_measure_seq mu == the sequence of finite measures of the        *)
(*                            s-finite measure mu                             *)
(*  Measure_isSFinite_subdef == mixin for s-finite measures                   *)
(*         Measure_isSFinite == factory for s-finite measures                 *)
(* {sigma_finite_content set T -> \bar R} == contents that are also sigma     *)
(*                            finite                                          *)
(*                            The HB class is SigmaFiniteContent.             *)
(* {sigma_finite_measure set T -> \bar R} == measures that are also sigma     *)
(*                            finite                                          *)
(*                            The HB class is SigmaFiniteMeasure.             *)
(*          sigma_finite A f == the measure function f is sigma-finite on the *)
(*                            A : set T with T a semiring of sets             *)
(*               fin_num_fun == predicate for finite function over measurable *)
(*                            sets                                            *)
(*            FinNumFun.type == type of functions over semiring of sets       *)
(*                            returning a fin_num                             *)
(*                            The HB class is FinNumFun.                      *)
(* {finite_measure set T -> \bar R} == finite measures                        *)
(*                            The HB class is FiniteMeasure.                  *)
(*      SigmaFinite_isFinite == mixin for finite measures                     *)
(*          Measure_isFinite == factory for finite measures                   *)
(*       subprobability T R == subprobability measure over the measurableType *)
(*                            T with values in \bar R with R : realType       *)
(*                            The HB class is SubProbability.                 *)
(*         probability T R == probability measure over the measurableType T   *)
(*                            with values in \bar with R : realType           *)
(*               probability == type of probability measures                  *)
(*                            The HB class is Probability.                    *)
(*     Measure_isProbability == factor for probability measures               *)
(*              mnormalize mu == normalization of a measure to a probability  *)
(* {outer_measure set T -> \bar R} == type of an outer measure over sets      *)
(*                            of elements of type T : Type where R is         *)
(*                            expected to be a numFieldType                   *)
(*                            The HB class is OuterMeasure.                   *)
(*                                                                            *)
(* * Instances of measures                                                    *)
(*  pushforward mf m == pushforward/image measure of m by f, where mf is a    *)
(*                      proof that f is measurable                            *)
(*              \d_a == Dirac measure                                         *)
(*         msum mu n == the measure corresponding to the sum of the measures  *)
(*                      mu_0, ..., mu_{n-1}                                   *)
(*        @mzero T R == the zero measure                                      *)
(* measure_add m1 m2 == the measure corresponding to the sum of the           *)
(*                      measures m1 and m2                                    *)
(*        mscale r m == the measure of corresponding to fun A => r * m A      *)
(*                      where r has type {nonneg R}                           *)
(*      mseries mu n == the measure corresponding to the sum of the           *)
(*                      measures mu_n, mu_{n+1}, ...                          *)
(*      mrestr mu mD == restriction of the measure mu to a set D; mD is a     *)
(*                      proof that D is measurable                            *)
(*      counting T R == counting measure                                      *)
(*                                                                            *)
(*      setI_closed G == the set of sets G is closed under finite             *)
(*                       intersection                                         *)
(*      setU_closed G == the set of sets G is closed under finite union       *)
(*      setC_closed G == the set of sets G is closed under complement         *)
(*      setD_closed G == the set of sets G is closed under difference         *)
(*     ndseq_closed G == the set of sets G is closed under non-decreasing     *)
(*                       countable union                                      *)
(*  trivIset_closed G == the set of sets G is closed under pairwise-disjoint  *)
(*                       countable union                                      *)
(*                                                                            *)
(* * Hierarchy of s-finite, sigma-finite, finite measures:                    *)
(*     sfinite_measure == predicate for s-finite measure functions            *)
(*     Measure_isSFinite_subdef == mixin for s-finite measures                *)
(*     SFiniteMeasure == structure of s-finite measures                       *)
(*     {sfinite_measure set T -> \bar R} == type of s-finite measures         *)
(*     Measure_isSFinite == factory for s-finite measures                     *)
(*     sfinite_measure_seq mu == the sequence of finite measures of the       *)
(*                               s-finite measure mu                          *)
(*                                                                            *)
(*     sigma_finite A f == the measure function f is sigma-finite on the set  *)
(*                         A : set T  with T : semiRingOfSetsType             *)
(*     isSigmaFinite == mixin corresponding to sigma finiteness               *)
(*     {sigma_finite_content set T -> \bar R} == contents that are also sigma *)
(*                                               finite                       *)
(*     {sigma_finite_measure set T -> \bar R} == measures that are also sigma *)
(*                                               finite                       *)
(*                                                                            *)
(*     fin_num_fun == predicate for finite function over measurable sets      *)
(*     SigmaFinite_isFinite == mixin for finite measures                      *)
(*     FiniteMeasure == structure of finite measures                          *)
(*     Measure_isFinite == factory for finite measures                        *)
(*                                                                            *)
(*     mfrestr mD muDoo == finite measure corresponding to the restriction of *)
(*                         the measure mu over D with mu D < +oo,             *)
(*                         mD : measurable D, muDoo : mu D < +oo              *)
(*                                                                            *)
(*     FiniteMeasure_isSubProbability = mixin corresponding to subprobability *)
(*     SubProbability = structure of subprobability                           *)
(*     subprobability T R == subprobability measure over the measurableType T *)
(*                           with value in R : realType                       *)
(*     Measure_isSubProbability == factory for subprobability measures        *)
(*                                                                            *)
(*     isProbability == mixin corresponding to probability measures           *)
(*     Probability == structure of probability measures                       *)
(*     probability T R == probability measure over the measurableType T with  *)
(*                        value in R : realType                               *)
(*     Measure_isProbability == factor for probability measures               *)
(*                                                                            *)
(*      monotone_class D G == G is a monotone class of subsets of D           *)
(*             <<m D, G >> == monotone class generated by G on D              *)
(*                <<m G >> := <<m setT, G >>                                  *)
(*                dynkin G == G is a set of sets that form a Dynkin           *)
(*                            (or a lambda) system                            *)
(*                <<d G >> == Dynkin system generated by G, i.e.,             *)
(*                            smallest dynkin G                               *)
(*                                                                            *)
(*      measurable_fun D f == the function f with domain D is measurable      *)
(*    preimage_class D f G == class of the preimages by f of sets in G        *)
(*       image_class D f G == class of the sets with a preimage by f in G     *)
(*                                                                            *)
(*        mu.-negligible A == A is mu negligible                              *)
(*  measure_is_complete mu == the measure mu is complete                      *)
(*  {ae mu, forall x, P x} == P holds almost everywhere for the measure mu,   *)
(*                            declared as an instance of the type of filters  *)
(*                                                                            *)
(* * From a premeasure to an outer measure (Measure Extension Theorem part 1) *)
(*   measurable_cover X == the set of sequences F such that                   *)
(*                         - forall k, F k is measurable                      *)
(*                         - X `<=` \bigcup_k (F k)                           *)
(*                 mu^* == extension of the measure mu over a semiring of     *)
(*                         sets (it is an outer measure)                      *)
(* * From an outer measure to a measure (Measure Extension Theorem part 2):   *)
(*        mu.-caratheodory == the set of Caratheodory measurable sets for the *)
(*                         outer measure mu, i.e., sets A such that           *)
(*                         forall B, mu A = mu (A `&` B) + mu (A `&` ~` B)    *)
(*    caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R}   *)
(*                         It is a canonical mesurableType copy of T.         *)
(*                         The restriction of the outer measure mu to the     *)
(*                         sigma algebra of Caratheodory measurable sets is a *)
(*                         measure.                                           *)
(*                         Remark: sets that are negligible for               *)
(*                         this measure are Caratheodory measurable.          *)
(* * Measure Extension Theorem:                                               *)
(*    measure_extension mu == extension of the content mu over a semiring of  *)
(*                         sets to a measure over the generated sigma algebra *)
(*                         (requires a proof of sigma-sub-additivity)         *)
(*                                                                            *)
(* * Product of measurable spaces:                                            *)
(*   preimage_classes f1 f2 == sigma-algebra generated by the union of the    *)
(*                             preimages by f1 and the preimages by f2 with   *)
(*                             f1 : T -> T1 and f : T -> T2, T1 and T2 being  *)
(*                             measurableType's                               *)
(*   (d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra    *)
(*                             generated from T1 x T2, with T1 and T2         *)
(*                             measurableType's with resp. display d1 and d2  *)
(*                                                                            *)
(*  m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1     *)
(*  ess_sup f == essential supremum of the function f : T -> R where T is a   *)
(*               measurableType and R is a realType                           *)
(*                                                                            *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Reserved Notation "'s<|' D , G '|>'" (at level 40, G, D at next level).
Reserved Notation "'s<<' A '>>'".
Reserved Notation "'d<<' D '>>'".
Reserved Notation "mu .-negligible" (at level 2, format "mu .-negligible").
Reserved Notation "{ 'ae' m , P }" (at level 0, format "{ 'ae'  m ,  P }").
Reserved Notation "mu .-measurable" (at level 2, format "mu .-measurable").
Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a").
Reserved Notation "G .-sigma" (at level 1, format "G .-sigma").
Reserved Notation "G .-sigma.-measurable"
 (at level 2, format "G .-sigma.-measurable").
Reserved Notation "d .-ring" (at level 1, format "d .-ring").
Reserved Notation "d .-ring.-measurable"
 (at level 2, format "d .-ring.-measurable").
Reserved Notation "mu .-cara" (at level 1, format "mu .-cara").
Reserved Notation "mu .-cara.-measurable"
 (at level 2, format "mu .-cara.-measurable").
Reserved Notation "mu .-caratheodory"
  (at level 2, format "mu .-caratheodory").
Reserved Notation "'<<m' D , G '>>'"
  (at level 2, format "'<<m'  D ,  G  '>>'").
Reserved Notation "'<<m' G '>>'"
  (at level 2, format "'<<m'  G  '>>'").
Reserved Notation "'<<d' G '>>'"
  (at level 2, format "'<<d'  G '>>'").
Reserved Notation "'<<s' D , G '>>'"
  (at level 2, format "'<<s'  D ,  G  '>>'").
Reserved Notation "'<<s' G '>>'"
  (at level 2, format "'<<s'  G  '>>'").
Reserved Notation "'<<r' G '>>'"
  (at level 2, format "'<<r'  G '>>'").
Reserved Notation "{ 'content' fUV }" (at level 0, format "{ 'content'  fUV }").
Reserved Notation "[ 'content' 'of' f 'as' g ]"
  (at level 0, format "[ 'content'  'of'  f  'as'  g ]").
Reserved Notation "[ 'content' 'of' f ]"
  (at level 0, format "[ 'content'  'of'  f ]").
Reserved Notation "{ 'measure' fUV }"
  (at level 0, format "{ 'measure'  fUV }").
Reserved Notation "[ 'measure' 'of' f 'as' g ]"
  (at level 0, format "[ 'measure'  'of'  f  'as'  g ]").
Reserved Notation "[ 'measure' 'of' f ]"
  (at level 0, format "[ 'measure'  'of'  f ]").
Reserved Notation "{ 'outer_measure' fUV }"
  (at level 0, format "{ 'outer_measure'  fUV }").
Reserved Notation "[ 'outer_measure' 'of' f 'as' g ]"
  (at level 0, format "[ 'outer_measure'  'of'  f  'as'  g ]").
Reserved Notation "[ 'outer_measure' 'of' f ]"
  (at level 0, format "[ 'outer_measure'  'of'  f ]").
Reserved Notation "p .-prod" (at level 1, format "p .-prod").
Reserved Notation "p .-prod.-measurable"
 (at level 2, format "p .-prod.-measurable").
Reserved Notation "m1 `<< m2" (at level 51).

Inductive measure_display := default_measure_display.
Declare Scope measure_display_scope.
Delimit Scope measure_display_scope with mdisp.
Bind Scope measure_display_scope with measure_display.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section classes.
Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)).

Definition setC_closed := forall A, G A -> G (~` A).
Definition setI_closed := forall A B, G A -> G B -> G (A `&` B).
Definition setU_closed := forall A B, G A -> G B -> G (A `|` B).
Definition setD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B).
Definition setDI_closed := forall A B, G A -> G B -> G (A `\` B).

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

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

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

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

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

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

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

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

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

Definition dynkin := [/\ G setT, setC_closed & trivIset_closed].

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

End classes.

Notation "'<<m' D , G '>>'" := (smallest (monotone_class D) G) :
  classical_set_scope.
Notation "'<<m' G '>>'" := (<<m setT, G>>) : classical_set_scope.
Notation "'<<d' G '>>'" := (smallest dynkin G) : classical_set_scope.
Notation "'<<s' D , G '>>'" := (smallest (sigma_algebra D) G) :
  classical_set_scope.
Notation "'<<s' G '>>'" := (<<s setT, G>>) : classical_set_scope.
Notation "'<<r' G '>>'" := (smallest setring G) : classical_set_scope.

Lemma fin_bigcup_closedP T (G : set (set T)) :
  (G set0 /\ setU_closed G) <-> fin_bigcup_closed G.
Proof.
split=> [[G0 GU] I D A DF GA|GU]; last first.
  have G0 : G set0 by have := GU void set0 point; rewrite bigcup0//; apply.
  by split=> // A B GA GB; rewrite -bigcup2inE; apply: GU => // -[|[|[]]].
elim/Pchoice: I => I in D DF A GA *; rewrite -bigsetU_fset_set// big_seq.
by elim/big_ind: _ => // i; rewrite in_fset_set// inE => /GA.
Qed.

Lemma finN0_bigcap_closedP T (G : set (set T)) :
  setI_closed G <-> finN0_bigcap_closed G.
Proof.
split=> [GI I D A DF [i Di] GA|GI A B GA GB]; last first.
  by rewrite -bigcap2inE; apply: GI => // [|[|[|[]]]]; first by exists 0%N.
elim/Pchoice: I => I in D DF i Di A GA *.
have finDDi : finite_set (D `\ i) by exact: finite_setD.
rewrite (bigcap_setD1 i)// -bigsetI_fset_set// big_seq.
elim/big_rec: _ => // [|j B]; first by rewrite setIT; apply: GA.
rewrite in_fset_set// inE => -[Dj /eqP nij] GAB.
by rewrite setICA; apply: GI => //; apply: GA.
Qed.

Lemma sedDI_closedP T (G : set (set T)) :
  setDI_closed G <-> (setI_closed G /\ setD_closed G).
Proof.
split=> [GDI|[GI GD]].
  by split=> A B => [|AB] => GA GB; rewrite -?setDD//; do ?apply: (GDI).
move=> A B GA GB; suff <- : A `\` (A `&` B) = A `\` B.
  by apply: GD => //; apply: GI.
by rewrite setDE setCI setIUr -setDE setDv set0U.
Qed.

Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T)
    (F : I -> set (set T)) (J : set I) :
  (forall n, J n -> sigma_algebra D (F n)) ->
  sigma_algebra D (\bigcap_(i in J) F i).
Proof.
move=> mG; split=> [i Ji|A AJ i Ji|H GH i Ji]; first by have [] := mG i.
- by have [_ mGiC _] := mG i Ji; exact/mGiC/AJ.
- by have [_ _ mGiU] := mG i Ji; apply: mGiU => j; exact: GH.
Qed.

Lemma sigma_algebraP T U (C : set (set T)) :
  (forall X, C X -> X `<=` U) ->
  sigma_algebra U C <->
  [/\ C U, setD_closed C, ndseq_closed C & setI_closed C].
Proof.
move=> C_subU; split => [[C0 CD CU]|[DT DC DU DI]]; split.
- by rewrite -(setD0 U); apply: CD.
- move=> A B BA CA CB; rewrite (_ : A `\` B = U `\` ((U `\` A) `|` B)).
    by apply CD; rewrite -bigcup2E; apply: CU => -[|[|[|]]] //=; exact: CD.
  rewrite setDUr setDD [in RHS]setDE setIACA setIid -setDE setIidr//.
  by rewrite setDE; apply: subIset; left; apply: C_subU.
- by move=> F ndF DF; exact: CU.
- move=> A B DA DB; rewrite (_ : A `&` B = U `\` ((U `\` A) `|` (U `\` B))).
    by apply CD; rewrite -bigcup2E; apply: CU => -[|[|[|]]] //; exact: CD.
  rewrite setDUr !setDD setIACA setIid (@setIidr _ U)//.
  by apply: subIset; left; exact: C_subU.
- by rewrite -(setDv U); exact: DC.
- by move=> A CA; apply: DC => //; exact: C_subU.
- move=> F DF.
  rewrite [X in C X](_ : _ = \bigcup_i \big[setU/set0]_(j < i.+1) F j).
    apply: DU; first by move=> *; exact/subsetPset/subset_bigsetU.
    elim=> [|n ih]; first by rewrite big_ord_recr /= big_ord0 set0U; exact: DF.
    have CU : setU_closed C.
      move=> A B DA DB; rewrite (_ : A `|` B = U `\` ((U `\` A) `&` (U `\` B))).
        apply DC => //; last by apply: DI; apply: DC => //; exact: C_subU.
        by apply: subIset; left; apply: subIset; left.
      by rewrite setDIr// !setDD (setIidr (C_subU _ DA)) (setIidr (C_subU _ _)).
    by rewrite big_ord_recr; exact: CU.
  rewrite predeqE => x; split => [[n _ Fnx]|[n _]].
    by exists n => //; rewrite big_ord_recr /=; right.
  by rewrite -bigcup_mkord => -[m /=]; rewrite ltnS => _ Fmx; exists m.
Qed.

Section generated_sigma_algebra.
Context {T : Type} (D : set T) (G : set (set T)).
Implicit Types (M : set (set T)).

Lemma smallest_sigma_algebra : sigma_algebra D <<s D, G >>.
Proof.
split=> [|A GA|A GA] P [[P0 PD PU]] GP //.
  by apply: (PD); apply: GA.
by apply: (PU) => n; apply: GA.
Qed.
Hint Resolve smallest_sigma_algebra : core.

Lemma sub_sigma_algebra2 M : M `<=` G -> <<s D, M >> `<=` <<s D, G >>.
Proof. exact: sub_smallest2r. Qed.

Lemma sigma_algebra_id : sigma_algebra D G -> <<s D, G >> = G.
Proof. by move=> /smallest_id->. Qed.

Lemma sub_sigma_algebra : G `<=` <<s D, G >>. Proof. exact: sub_smallest. Qed.

Lemma sigma_algebra0 : <<s D, G >> set0.
Proof. by case: smallest_sigma_algebra. Qed.

Lemma sigma_algebraCD : forall A, <<s D, G >> A -> <<s D, G >> (D `\` A).
Proof. by case: smallest_sigma_algebra. Qed.

Lemma sigma_algebra_bigcup (A : (set T)^nat) :
  (forall i, <<s D, G >> (A i)) ->  <<s D, G >> (\bigcup_i (A i)).
Proof. by case: smallest_sigma_algebra A. Qed.

End generated_sigma_algebra.
#[global] Hint Resolve smallest_sigma_algebra : core.

Section generated_setring.
Context {T : Type} (G : set (set T)).
Implicit Types (M : set (set T)).

Lemma smallest_setring : setring <<r G >>.
Proof.
split=> [|A B GA GB|A B GA GB] P [[P0 PU PDI]] GP //.
  by apply: (PU); [apply: GA|apply: GB].
by apply: (PDI); [apply: GA|apply: GB].
Qed.
Hint Resolve smallest_setring : core.

Lemma sub_setring2 M : M `<=` G -> <<r M >> `<=` <<r G >>.
Proof. exact: sub_smallest2r. Qed.

Lemma setring_id : setring G -> <<r G >> = G.
Proof. by move=> /smallest_id->. Qed.

Lemma sub_setring : G `<=` <<r G >>. Proof. exact: sub_smallest. Qed.

Lemma setring0 : <<r G >> set0.
Proof. by case: smallest_setring. Qed.

Lemma setringDI : setDI_closed <<r G>>.
Proof. by case: smallest_setring. Qed.

Lemma setringU : setU_closed <<r G>>.
Proof. by case: smallest_setring. Qed.

Lemma setring_fin_bigcup : fin_bigcup_closed <<r G>>.
Proof.
by apply/fin_bigcup_closedP; split; [apply: setring0|apply: setringU].
Qed.

End generated_setring.
#[global] Hint Resolve smallest_setring setring0 : core.

Lemma monotone_class_g_salgebra T (G : set (set T)) (D : set T) :
  (forall X, <<s D, G >> X -> X `<=` D) -> G D ->
  monotone_class D (<<s D, G >>).
Proof.
move=> sDGD GD; have := smallest_sigma_algebra D G.
by move=> /(sigma_algebraP sDGD) [sT sD snd sI]; split.
Qed.

Section smallest_monotone_classE.
Variables (T : Type) (G : set (set T)) (setIG : setI_closed G).
Variables (D : set T) (GD : G D).
Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H).

Lemma smallest_monotone_classE : (forall X, <<s D, G >> X -> X `<=` D) ->
  (forall E, monotone_class D E -> G `<=` E -> H `<=` E) ->
  H = <<s D, G >>.
Proof.
move=> sDGD smallestH; rewrite eqEsubset; split.
  apply: (smallestH _ _ (@sub_sigma_algebra _ D G)).
  exact: monotone_class_g_salgebra.
suff: setI_closed H.
  move=> IH; apply: smallest_sub => //.
  by apply/sigma_algebraP; by case: monoH.
pose H_ A := [set X | H X /\ H (X `&` A)].
have setDH_ A : setD_closed (H_ A).
  move=> X Y XY [HX HXA] [HY HYA]; case: monoH => h _ setDH _; split.
    exact: setDH.
  rewrite (_ : _ `&` _ = (X `&` A) `\` (Y `&` A)); last first.
    rewrite predeqE => x; split=> [[[? ?] ?]|]; first by split => // -[].
    by move=> [[? ?] YAx]; split => //; split => //; apply: contra_not YAx.
  by apply: setDH => //; exact: setSI.
have ndH_ A : ndseq_closed (H_ A).
  move=> F ndF H_AF; split.
    by case: monoH => h _ _; apply => // => n; have [] := H_AF n.
  rewrite setI_bigcupl; case: monoH => h _ _; apply => //.
    by move=> m n mn; apply/subsetPset; apply: setSI; apply/subsetPset/ndF.
  by move=> n; have [] := H_AF n.
have GGH_ X : G X -> G `<=` H_ X.
  by move=> *; split; [exact: GH | apply: GH; exact: setIG].
have GHH_ X : G X -> H `<=` H_ X.
  move=> CX; apply: smallestH; [split => //; last exact: GGH_|exact: GGH_].
  by move=> ? [? ?]; case: monoH => + _ _ _; exact.
have HGH_ X : H X -> G `<=` H_ X.
  by move=> *; split; [exact: GH|rewrite setIC; apply GHH_].
have HHH_ X : H X -> H `<=` H_ X.
  move=> HX; apply: (smallestH _ _ (HGH_ _ HX)); split=> //.
  - by move=> ? [? ?]; case: monoH => + _ _ _; exact.
  - exact: HGH_.
by move=> *; apply HHH_.
Qed.

End smallest_monotone_classE.

Section monotone_class_subset.
Variables (T : Type) (G : set (set T)) (setIG : setI_closed G).
Variables (D : set T) (GD : G D).
Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H).

Lemma monotone_class_subset : (forall X, (<<s D, G >>) X -> X `<=` D) ->
  <<s D, G >> `<=` H.
Proof.
move=> sDGD; set M := <<m D, G >>.
rewrite -(@smallest_monotone_classE _ _ setIG _ _ M) //.
- exact: smallest_sub.
- split => [A MA | E [monoE] | A B BA MA MB E [[EsubD ED setDE ndE] GE] |].
  + by case: monoH => + _ _ _; apply; exact: MA.
  + exact.
  + by apply setDE => //; [exact: MA|exact: MB].
  + by move=> F ndF MF E [[EsubD ED setDE ndE] CE]; apply ndE=> // n; exact: MF.
- exact: sub_smallest.
- by move=> ? ? ?; exact: smallest_sub.
Qed.

End monotone_class_subset.

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

Lemma dynkinT G : dynkin G -> G setT. Proof. by case. Qed.

Lemma dynkinC G : dynkin G -> setC_closed G. Proof. by case. Qed.

Lemma dynkinU G : dynkin G -> (forall F : (set T)^nat, trivIset setT F ->
  (forall n, G (F n)) -> G (\bigcup_k F k)). Proof. by case. Qed.

End dynkin.

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

Lemma dynkin_monotone G : dynkin G <-> monotone_class setT G.
Proof.
split => [[GT setCG trG]|[_ GT setDG ndG]]; split => //.
- move=> A B BA GA GB; rewrite setDE -(setCK (_ `&` _)) setCI; apply: (setCG).
  rewrite setCK -bigcup2E; apply trG.
  + by rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint.
  + by move=> [|[//|n]]; [exact: setCG|rewrite /bigcup2 -setCT; apply: setCG].
- move=> F ndF GF; rewrite eq_bigcup_seqD; apply: (trG).
    exact: trivIset_seqD.
  move=> [/=|n]; first exact: GF.
  rewrite /seqD setDE -(setCK (_ `&` _)) setCI; apply: (setCG).
  rewrite setCK -bigcup2E; apply: trG.
  + rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint.
    exact/subsetPset/ndF/ltnW.
  + move=> [|[|]]; rewrite /bigcup2 /=; [exact/setCG/GF|exact/GF|].
    by move=> _; rewrite -setCT; apply: setCG.
- by move=> A B; rewrite -setTD; apply: setDG.
- move=> F tF GF; pose A i := \big[setU/set0]_(k < i.+1) F k.
  rewrite (_ : bigcup _ _ = \bigcup_i A i); last first.
    rewrite predeqE => t; split => [[n _ Fn]|[n _]].
      by exists n => //; rewrite /A -bigcup_mkord; exists n=> //=; rewrite ltnS.
    by rewrite /A -bigcup_mkord => -[m /=]; rewrite ltnS => mn Fmt; exists m.
  apply: ndG; first by move=> a b ab; exact/subsetPset/subset_bigsetU.
  elim=> /= => [|n ih].
    by rewrite /A big_ord_recr /= big_ord0 set0U; exact: GF.
  rewrite /A /= big_ord_recr /= -/(A n).
  rewrite (_ : _ `|` _ = ~` (~` A n `\` F n.+1)); last first.
    by rewrite setDE setCI !setCK.
  rewrite -setTD; apply: (setDG) => //; apply: (setDG) => //; last first.
    by rewrite -setTD; apply: setDG.
  apply/disjoints_subset; rewrite setIC.
  by apply: (@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE.
Qed.

Lemma dynkin_g_dynkin G : dynkin (<<d G >>).
Proof.
split=> [D /= [] []//| | ].
- by move=> Y sGY D /= [dD GD]; exact/(dynkinC dD)/(sGY D).
- by move=> F tF gGF D /= [dD GD]; apply dD => // k; exact: gGF.
Qed.

Lemma sigma_algebra_dynkin G : sigma_algebra setT G -> dynkin G.
Proof.
case=> ? DC DU; split => [| |? ? ?]; last exact: DU.
- by rewrite -setC0 -setTD; exact: DC.
- by move=> A GA; rewrite -setTD; apply: DC.
Qed.

Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G -> setI_closed G ->
  (forall n, G (F n)) -> forall n, G (\big[setI/setT]_(i < n) F i).
Proof.
move=> dG GI GF; elim => [|n ih]; last by rewrite big_ord_recr /=; apply: GI.
by rewrite big_ord0; exact: (dynkinT dG).
Qed.

Lemma dynkin_setI_sigma_algebra G : dynkin G -> setI_closed G ->
  sigma_algebra setT G.
Proof.
move=> dG GI; split => [|//|F DF].
- by rewrite -setCT; exact/(dynkinC dG)/(dynkinT dG).
- by move=> A GA; rewrite setTD; exact: (dynkinC dG).
- rewrite seqDU_bigcup_eq; apply/(dynkinU dG) => //.
  move=> n; rewrite /seqDU setDE; apply GI => //.
  rewrite -bigcup_mkord setC_bigcup bigcap_mkord.
  by apply: (@dynkin_setI_bigsetI _ (fun x => ~` F x)) => // ?; exact/(dynkinC dG).
Qed.

Lemma setI_closed_gdynkin_salgebra G : setI_closed G -> <<d G >> = <<s G >>.
Proof.
move=> GI; rewrite eqEsubset; split.
  by apply: sub_smallest2l; apply: sigma_algebra_dynkin.
pose delta (D : set T) := [set E | <<d G >> (E `&` D)].
have ddelta (D : set T) : <<d G >> D -> dynkin (delta D).
  move=> dGD; split; first by rewrite /delta /= setTI.
  - move=> E DE; rewrite /delta /=.
    have -> : (~` E) `&` D = ~` ((E `&` D) `|` (~` D)).
      by rewrite -[LHS]setU0 -(setICl D) -setIUl -setCI -{2}(setCK D) -setCU.
    have : <<d G >> ((E `&` D) `|` ~` D).
      rewrite -bigcup2E => S [dS GS]; apply: (dynkinU dS).
        move=> [|[|i]] [|[|j]] => // _ _; rewrite /bigcup2 /=.
        + by rewrite -setIA setICr setI0 => /set0P; rewrite eqxx.
        + by rewrite setI0 => /set0P; rewrite eqxx.
        + by rewrite setICA setICl setI0 => /set0P; rewrite eqxx.
        + by rewrite setI0 => /set0P; rewrite eqxx.
        + by rewrite set0I => /set0P; rewrite eqxx.
        + by rewrite set0I => /set0P; rewrite eqxx.
        + by rewrite set0I => /set0P; rewrite eqxx.
      move=> [|[|n]] //; rewrite /bigcup2 /=; [exact: DE| |].
      + suff: <<d G >> (~` D) by exact.
        by move=> F [dF GF]; apply: (dynkinC dF) => //; exact: dGD.
      + by rewrite -setCT; apply/(dynkinC dS)/(dynkinT dS).
    by move=> dGEDD S /= [+ GS] => dS; apply/(dynkinC dS); exact: dGEDD.
  - move=> F tF deltaDF; rewrite /delta /= => S /= [dS GS].
    rewrite setI_bigcupl; apply: (dynkinU dS) => //.
      by under eq_fun do rewrite setIC; exact: trivIset_setIl.
    by move=> n; exact: deltaDF.
have GdG : G `<=` <<d G >> by move=> ? ? ? [_]; apply.
have Gdelta A : G A -> G `<=` delta A.
  by move=> ? ? ?; rewrite /delta /= => ? [?]; apply; exact/GI.
have GdGdelta A : G A -> <<d G >> `<=` delta A.
  move=> ?; apply: smallest_sub => //; last exact: Gdelta.
  by apply/ddelta; exact: GdG.
have dGGI A B : <<d G >> A -> G B -> <<d G >> (A `&` B).
  by move=> ? ?; apply: GdGdelta.
have dGGdelta A : <<d G >> A -> G `<=` delta A.
  by move=> ? ? ?; rewrite /delta /= setIC; exact: dGGI.
have dGdGdelta A : <<d G >> A -> <<d G >> `<=` delta A.
  by move=> ?; exact: smallest_sub (ddelta _ _) (dGGdelta _ _).
have dGdGdG A B : <<d G >> A -> <<d G >> B -> <<d G >> (A `&` B).
  by move=> ? ?; exact: dGdGdelta.
apply: smallest_sub => //; apply: dynkin_setI_sigma_algebra => //.
exact: dynkin_g_dynkin.
Qed.

End dynkin_lemmas.

HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
  ptclass : Pointed.class_of T;
  measurable : set (set T) ;
  measurable0 : measurable set0 ;
  measurableI : setI_closed measurable;
  semi_measurableD : semi_setD_closed measurable;
}.

#[short(type=semiRingOfSetsType)]
HB.structure Definition SemiRingOfSets d := {T of isSemiRingOfSets d T}.

Canonical semiRingOfSets_eqType d (T : semiRingOfSetsType d) := EqType T ptclass.
Canonical semiRingOfSets_choiceType d (T : semiRingOfSetsType d) :=
  ChoiceType T ptclass.
Canonical semiRingOfSets_ptType d (T : semiRingOfSetsType d) :=
  PointedType T ptclass.

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

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

HB.mixin Record SemiRingOfSets_isRingOfSets d T of isSemiRingOfSets d T := {
  measurableU : setU_closed (@measurable d [the semiRingOfSetsType d of T]) }.

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

Canonical ringOfSets_eqType d (T : ringOfSetsType d) := EqType T ptclass.
Canonical ringOfSets_choiceType d (T : ringOfSetsType d) := ChoiceType T ptclass.
Canonical ringOfSets_ptType d (T : ringOfSetsType d) := PointedType T ptclass.

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

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

Canonical algebraOfSets_eqType d (T : algebraOfSetsType d) := EqType T ptclass.
Canonical algebraOfSets_choiceType d (T : algebraOfSetsType d) :=
  ChoiceType T ptclass.
Canonical algebraOfSets_ptType d (T : algebraOfSetsType d) :=
  PointedType T ptclass.

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

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

Canonical measurable_eqType d (T : measurableType d) := EqType T ptclass.
Canonical measurable_choiceType d (T : measurableType d) := ChoiceType T ptclass.
Canonical measurable_ptType d (T : measurableType d) := PointedType T ptclass.

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

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

Lemma mI : setI_closed measurable.
Proof. by move=> A B mA mB; rewrite -setDD; do ?apply: measurableD. Qed.

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

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

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

HB.end.

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

HB.builders Context d T of isAlgebraOfSets d T.

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

HB.instance Definition _ :=
  @isRingOfSets.Build d T ptclass measurable measurable0 measurableU mD.

Lemma measurableT : measurable [set: T].
Proof. by rewrite -setC0; apply: measurableC; exact: measurable0. Qed.

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

HB.end.

HB.factory Record isMeasurable (d : measure_display) T := {
  ptclass : Pointed.class_of T;
  measurable : set (set T) ;
  measurable0 : measurable set0 ;
  measurableC : forall A, measurable A -> measurable (~` A) ;
  measurable_bigcup : forall F : (set T)^nat, (forall i, measurable (F i)) ->
    measurable (\bigcup_i (F i))
}.

HB.builders Context d T of isMeasurable d T.

Obligation Tactic := idtac.

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

Lemma mC : setC_closed measurable. Proof. by move=> *; apply: measurableC. Qed.

HB.instance Definition _ :=
  @isAlgebraOfSets.Build d T ptclass measurable measurable0 mU mC.

HB.instance Definition _ :=
  @AlgebraOfSets_isMeasurable.Build d T measurable_bigcup.

HB.end.

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

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

Lemma bigsetU_measurable I r (P : pred I) (F : I -> set T) :
  (forall i, P i -> measurable (F i)) ->
  measurable (\big[setU/set0]_(i <- r | P i) F i).
Proof. by move=> mF; elim/big_ind : _ => //; exact: measurableU. Qed.

Lemma fin_bigcup_measurable I (D : set I) (F : I -> set T) :
    finite_set D ->
    (forall i, D i -> measurable (F i)) ->
  measurable (\bigcup_(i in D) F i).
Proof.
elim/Pchoice: I => I in D F * => Dfin Fm.
rewrite -bigsetU_fset_set// big_seq; apply: bigsetU_measurable => i.
by rewrite in_fset_set ?inE// => *; apply: Fm.
Qed.

Lemma measurableD : setDI_closed (@measurable d T).
Proof.
move=> A B mA mB; case: (semi_measurableD A B) => // [D [Dfin Dl -> _]].
by apply: fin_bigcup_measurable.
Qed.

End ringofsets_lemmas.

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

Lemma measurableC A : measurable A -> measurable (~` A).
Proof. by move=> mA; rewrite -setTD; exact: measurableD. Qed.

Lemma bigsetI_measurable I r (P : pred I) (F : I -> set T) :
  (forall i, P i -> measurable (F i)) ->
  measurable (\big[setI/setT]_(i <- r | P i) F i).
Proof.
move=> mF; rewrite -[X in measurable X]setCK setC_bigsetI; apply: measurableC.
by apply: bigsetU_measurable => i Pi; apply/measurableC/mF.
Qed.

Lemma fin_bigcap_measurable I (D : set I) (F : I -> set T) :
    finite_set D ->
    (forall i, D i -> measurable (F i)) ->
  measurable (\bigcap_(i in D) F i).
Proof.
elim/Pchoice: I => I in D F * => Dfin Fm.
rewrite -bigsetI_fset_set// big_seq; apply: bigsetI_measurable => i.
by rewrite in_fset_set ?inE// => *; apply: Fm.
Qed.

End algebraofsets_lemmas.

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

Lemma sigma_algebra_measurable : sigma_algebra setT (@measurable d T).
Proof. by split=> // [A|]; [exact: measurableD|exact: bigcupT_measurable]. Qed.

Lemma bigcup_measurable F P :
  (forall k, P k -> measurable (F k)) -> measurable (\bigcup_(i in P) F i).
Proof.
move=> PF; rewrite bigcup_mkcond; apply: bigcupT_measurable => k.
by case: ifP => //; rewrite inE; exact: PF.
Qed.

Lemma bigcap_measurable F P :
  (forall k, P k -> measurable (F k)) -> measurable (\bigcap_(i in P) F i).
Proof.
move=> PF; rewrite -[X in measurable X]setCK setC_bigcap; apply: measurableC.
by apply: bigcup_measurable => k Pk; exact/measurableC/PF.
Qed.

Lemma bigcapT_measurable F : (forall i, measurable (F i)) ->
  measurable (\bigcap_i (F i)).
Proof. by move=> ?; exact: bigcap_measurable. Qed.

End measurable_lemmas.

Lemma bigcupT_measurable_rat d (T : measurableType d) (F : rat -> set T) :
  (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
Proof.
move=> Fm; have /ppcard_eqP[f] := card_rat.
by rewrite (reindex_bigcup f^-1%FUN setT)//=; exact: bigcupT_measurable.
Qed.

Section discrete_measurable_unit.

Definition discrete_measurable_unit : set (set unit) := [set: set unit].

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

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

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

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

End discrete_measurable_unit.

Section discrete_measurable_bool.

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

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

Let discrete_measurableC X :
  discrete_measurable_bool X -> discrete_measurable_bool (~` X).
Proof. by []. Qed.

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

HB.instance Definition _ := @isMeasurable.Build default_measure_display bool
  (Pointed.class _) discrete_measurable_bool discrete_measurable0
  discrete_measurableC discrete_measurableU.

End discrete_measurable_bool.

Section discrete_measurable_nat.

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

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

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

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

HB.instance Definition _ := @isMeasurable.Build default_measure_display nat
  (Pointed.class _) discrete_measurable_nat discrete_measurable_nat0
  discrete_measurable_natC discrete_measurable_natU.

End discrete_measurable_nat.

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

Definition salgebraType {T} (G : set (set T)) := T.

Section g_salgebra_instance.
Variables (T : pointedType) (G : set (set T)).

Lemma sigma_algebraC (A : set T) : <<s G >> A -> <<s G >> (~` A).
Proof. by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed.

Canonical salgebraType_eqType := EqType (salgebraType G) (Equality.class T).
Canonical salgebraType_choiceType := ChoiceType (salgebraType G) (Choice.class T).
Canonical salgebraType_ptType := PointedType (salgebraType G) (Pointed.class T).
HB.instance Definition _ := @isMeasurable.Build (sigma_display G)
  (salgebraType G) (Pointed.class T)
  <<s G >> (@sigma_algebra0 _ setT G) (@sigma_algebraC)
  (@sigma_algebra_bigcup _ setT G).

End g_salgebra_instance.

Notation "G .-sigma" := (sigma_display G) : measure_display_scope.
Notation "G .-sigma.-measurable" :=
  (measurable : set (set (salgebraType G))) : classical_set_scope.

Lemma measurable_g_measurableTypeE (T : pointedType) (G : set (set T)) :
  sigma_algebra setT G -> G.-sigma.-measurable = G.
Proof. exact: sigma_algebra_id. Qed.

Definition measurable_fun d d' (T : measurableType d) (U : measurableType d')
    (D : set T) (f : T -> U) :=
  measurable D -> forall Y, measurable Y -> measurable (D `&` f @^-1` Y).

Section measurable_fun.
Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2)
        (T3 : measurableType d3).
Implicit Type D E : set T1.

Lemma measurable_id D : measurable_fun D id.
Proof. by move=> mD A mA; apply: measurableI. Qed.

Lemma measurable_comp F (f : T2 -> T3) E (g : T1 -> T2) :
  measurable F -> g @` E `<=` F ->
  measurable_fun F f -> measurable_fun E g -> measurable_fun E (f \o g).
Proof.
move=> mF FgE mf mg /= mE A mA.
rewrite comp_preimage.
rewrite (_ : _ `&` _ = E `&` g @^-1` (F `&` f @^-1` A)); last first.
  apply/seteqP; split=> [|? [?] []//].
  by move=> x/= [Ex Afgx]; split => //; split => //; exact: FgE.
by apply/mg => //; exact: mf.
Qed.

Lemma measurableT_comp (f : T2 -> T3) E (g : T1 -> T2) :
  measurable_fun setT f -> measurable_fun E g -> measurable_fun E (f \o g).
Proof. exact: measurable_comp. Qed.

Lemma eq_measurable_fun D (f g : T1 -> T2) :
  {in D, f =1 g} -> measurable_fun D f -> measurable_fun D g.
Proof.
by move=> fg mf mD A mA; rewrite [X in measurable X](_ : _ = D `&` f @^-1` A);
  [exact: mf|exact/esym/eq_preimage].
Qed.

Lemma measurable_cst D (r : T2) : measurable_fun D (cst r : T1 -> _).
Proof.
by move=> mD /= Y mY; rewrite preimage_cst; case: ifPn; rewrite ?setIT ?setI0.
Qed.

Lemma measurable_fun_bigcup (E : (set T1)^nat) (f : T1 -> T2) :
  (forall i, measurable (E i)) ->
  measurable_fun (\bigcup_i E i) f <-> (forall i, measurable_fun (E i) f).
Proof.
move=> mE; split => [|mf /= _ A mA]; last first.
  by rewrite setI_bigcupl; apply: bigcup_measurable => i _; exact: mf.
move=> mf i _ A /mf => /(_ (bigcup_measurable (fun k _ => mE k))).
move=> /(measurableI (E i))-/(_ (mE i)).
by rewrite setICA setIA (@setIidr _ _ (E i))//; exact: bigcup_sup.
Qed.

Lemma measurable_funU D E (f : T1 -> T2) : measurable D -> measurable E ->
  measurable_fun (D `|` E) f <-> measurable_fun D f /\ measurable_fun E f.
Proof.
move=> mD mE; rewrite -bigcup2E; apply: (iff_trans (measurable_fun_bigcup _ _)).
  by move=> [//|[//|//=]].
split=> [mf|[Df Dg] [//|[//|/= _ _ Y mY]]]; last by rewrite set0I.
by split; [exact: (mf 0%N)|exact: (mf 1%N)].
Qed.

Lemma measurable_funS E D (f : T1 -> T2) :
    measurable E -> D `<=` E -> measurable_fun E f ->
  measurable_fun D f.
Proof.
move=> mE DE mf mD; have mC : measurable (E `\` D) by exact: measurableD.
move: (mD).
have := measurable_funU f mD mC.
suff -> : D `|` (E `\` D) = E by move=> [[]] //.
by rewrite setDUK.
Qed.

Lemma measurable_funTS D (f : T1 -> T2) :
  measurable_fun setT f -> measurable_fun D f.
Proof. exact: measurable_funS. Qed.

Lemma measurable_restrict D E (f : T1 -> T2) :
  measurable D -> measurable E -> D `<=` E ->
  measurable_fun D f <-> measurable_fun E (f \_ D).
Proof.
move=> mD mE DE; split => mf _ /= X mX.
- rewrite preimage_restrict; apply/measurableI => //.
  by apply/measurableU/mf => //; case: ifP => // _; apply: measurableC.
- have := mf mE _ mX; rewrite preimage_restrict.
  case: ifP => ptX; last first.
    rewrite set0U => /(measurableI _ _ mD).
    by rewrite (setIA D) (setIidl DE) setIA setIid.
  rewrite setUIr setvU setTI => /(measurableI _ _ mD).
  by rewrite setIA (setIidl DE) setIUr setICr set0U.
Qed.

Lemma measurable_fun_if (g h : T1 -> T2) D (mD : measurable D)
    (f : T1 -> bool) (mf : measurable_fun D f) :
  measurable_fun (D `&` (f @^-1` [set true])) g ->
  measurable_fun (D `&` (f @^-1` [set false])) h ->
  measurable_fun D (fun t => if f t then g t else h t).
Proof.
move=> mx my /= _ B mB; rewrite (_ : _ @^-1` B =
    ((f @^-1` [set true]) `&` (g @^-1` B)) `|`
    ((f @^-1` [set false]) `&` (h @^-1` B))).
  rewrite setIUr; apply: measurableU.
  - by rewrite setIA; apply: mx => //; exact: mf.
  - by rewrite setIA; apply: my => //; exact: mf.
apply/seteqP; split=> [t /=| t /= [] [] ->//].
by case: ifPn => ft; [left|right].
Qed.

Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool)
    (mf : measurable_fun setT f) :
  measurable_fun setT g -> measurable_fun setT h ->
  measurable_fun setT (fun t => if f t then g t else h t).
Proof.
by move=> mx my; apply: measurable_fun_if => //;
  [exact: measurable_funS mx|exact: measurable_funS my].
Qed.

Lemma measurable_fun_bool D (f : T1 -> bool) b :
  measurable (f @^-1` [set b]) -> measurable_fun D f.
Proof.
have FNT : [set false] = [set~ true] by apply/seteqP; split => -[]//=.
wlog {b}-> : b / b = true.
  case: b => [|h]; first exact.
  by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact: h.
move=> mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT.
have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
- by rewrite preimage0 ?setI0.
- by apply: measurableI => //; exact: mfT.
- rewrite -[X in measurable X]setCK; apply: measurableC; rewrite setCI.
  apply: measurableU; first exact: measurableC.
  by rewrite FNT preimage_setC setCK; exact: mfT.
- by rewrite -setT_bool preimage_setT setIT.
Qed.

End measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
  solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ (cst _)) =>
  solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ id) =>
  solve [apply: measurable_id] : core.
Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_bool {d1 T1 D f} b.
#[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")]
Notation measurable_fun_ext := eq_measurable_fun (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")]
Notation measurable_fun_id := measurable_id (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_cst`")]
Notation measurable_fun_cst := measurable_cst (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_comp`")]
Notation measurable_fun_comp := measurable_comp (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurableT_comp`")]
Notation measurable_funT_comp := measurableT_comp (only parsing).

Section measurability.

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

(* f is measurable on the sigma-algebra generated by itself *)
Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d)
  (D : set aT) (f : aT -> rT) :
  measurable_fun (D : set (salgebraType (preimage_class D f measurable))) f.
Proof. by move=> mD A mA; apply: sub_sigma_algebra; exists A. Qed.

Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT))
    (D : set aT) (f : aT -> rT) :
  sigma_algebra setT G -> sigma_algebra D (preimage_class D f G).
Proof.
case=> h0 hC hU; split; first by exists set0 => //; rewrite preimage_set0 setI0.
- move=> A; rewrite /preimage_class /= => -[B mB <-{A}].
  exists (~` B); first by rewrite -setTD; exact: hC.
  rewrite predeqE => x; split=> [[Dx Bfx]|[Dx]]; first by split => // -[] _ /Bfx.
  by move=> /not_andP[].
- move=> F; rewrite /preimage_class /= => mF.
  have {}mF n : exists x, G x /\ D `&` f @^-1` x = F n.
    by have := mF n => -[B mB <-]; exists B.
  have [F' mF'] := @choice _ _ (fun x y => G y /\ D `&` f @^-1` y = F x) mF.
  exists (\bigcup_k (F' k)); first by apply: hU => n; exact: (mF' n).1.
  rewrite preimage_bigcup setI_bigcupr; apply: eq_bigcupr => i _.
  exact: (mF' i).2.
Qed.

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

Lemma sigma_algebra_image_class (aT rT : Type) (D : set aT) (f : aT -> rT)
    (G : set (set aT)) :
  sigma_algebra D G -> sigma_algebra setT (image_class D f G).
Proof.
move=> [G0 GC GU]; split; rewrite /image_class.
- by rewrite /= preimage_set0 setI0.
- move=> A /= GfAD; rewrite setTD -preimage_setC -setDE.
  rewrite (_ : _ `\` _ = D `\` (D `&` f @^-1` A)); first exact: GC.
  rewrite predeqE => x; split=> [[Dx fAx]|[Dx fADx]].
    by split => // -[] _ /fAx.
  by split => //; exact: contra_not fADx.
- by move=> F /= mF; rewrite preimage_bigcup setI_bigcupr; exact: GU.
Qed.

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

Lemma measurability d d' (aT : measurableType d) (rT : measurableType d')
    (D : set aT) (f : aT -> rT)
    (G' : set (set rT)) :
  @measurable _ rT = <<s G' >> -> preimage_class D f G' `<=` @measurable _ aT ->
  measurable_fun D f.
Proof.
move=> sG_rT fG_aT mD.
suff h : preimage_class D f (@measurable _ rT) `<=` @measurable _ aT.
  by move=> A mA; apply: h; exists A.
have -> : preimage_class D f (@measurable _ rT) =
         <<s D , (preimage_class D f G')>>.
  by rewrite [in LHS]sG_rT [in RHS]sigma_algebra_preimage_classE.
apply: smallest_sub => //; split => //.
- by move=> A mA; exact: measurableD.
- by move=> F h; exact: bigcupT_measurable.
Qed.

End measurability.

Local Open Scope ereal_scope.

Section additivity.
Context d (R : numFieldType) (T : semiRingOfSetsType d)
        (mu : set T -> \bar R).

Definition semi_additive2 := forall A B, measurable A -> measurable B ->
  measurable (A `|` B) ->
  A `&` B = set0 -> mu (A `|` B) = mu A + mu B.

Definition semi_additive := forall F n,
 (forall k : nat, measurable (F k)) -> trivIset setT F ->
  measurable (\big[setU/set0]_(k < n) F k) ->
  mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).

Definition semi_sigma_additive :=
  forall F, (forall i : nat, measurable (F i)) -> trivIset setT F ->
  measurable (\bigcup_n F n) ->
  (fun n => \sum_(0 <= i < n) mu (F i)) --> mu (\bigcup_n F n).

Definition additive2 := forall A B, measurable A -> measurable B ->
  A `&` B = set0 -> mu (A `|` B) = mu A + mu B.

Definition additive :=
  forall F, (forall i : nat, measurable (F i)) -> trivIset setT F ->
  forall n, mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).

Definition sigma_additive :=
  forall F, (forall i : nat, measurable (F i)) -> trivIset setT F ->
  (fun n => \sum_(0 <= i < n) mu (F i)) --> mu (\bigcup_n F n).

Definition sub_additive := forall (A : set T) (F : nat -> set T) n,
 (forall k, `I_n k -> measurable (F k)) -> measurable A ->
  A `<=` \big[setU/set0]_(k < n) F k ->
  mu A <= \sum_(k < n) mu (F k).

Definition sigma_sub_additive := forall (A : set T) (F : nat -> set T),
 (forall n, measurable (F n)) -> measurable A ->
  A `<=` \bigcup_n F n ->
  mu A <= \sum_(n <oo) mu (F n).

Lemma semi_additiveW : mu set0 = 0 -> semi_additive -> semi_additive2.
Proof.
move=> mu0 amx A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord.
move=> /(amx (bigcup2 A B))->.
- by rewrite !(big_ord_recl, big_ord0)/= adde0.
- by move=> [|[|[]]]//=.
- by move=> [|[|i]] [|[|j]]/= _ _; rewrite ?(AB, setI0, set0I, setIC) => -[].
Qed.

End additivity.

Section ring_additivity.
Context d (R : numFieldType) (T : ringOfSetsType d) (mu : set T -> \bar R).

Lemma semi_additiveE : semi_additive mu = additive mu.
Proof.
rewrite propeqE; split=> [sa A mA tA n|+ A m mA tA UAm]; last by move->.
by rewrite sa //; exact: bigsetU_measurable.
Qed.

Lemma semi_additive2E : semi_additive2 mu = additive2 mu.
Proof.
rewrite propeqE; split=> [amu A B ? ? ?|amu A B ? ? _ ?]; last by rewrite amu.
by rewrite amu //; exact: measurableU.
Qed.

Lemma additive2P : mu set0 = 0 -> semi_additive mu <-> additive2 mu.
Proof.
move=> mu0; rewrite -semi_additive2E; split; first exact: semi_additiveW.
rewrite semi_additiveE semi_additive2E => muU A Am Atriv n.
elim: n => [|n IHn]; rewrite ?(big_ord_recr, big_ord0) ?mu0//=.
rewrite muU ?IHn//=; first by apply: bigsetU_measurable.
rewrite -bigcup_mkord -subset0 => x [[/= m + Amx] Anx].
by rewrite (Atriv m n) ?ltnn//=; exists x.
Qed.

End ring_additivity.

(* NB: realFieldType cannot be weakened to numFieldType in the current
   state because cvg_lim requires a topology for \bar R which is
   defined for at least realFieldType *)
Lemma semi_sigma_additive_is_additive d (T : semiRingOfSetsType d)
    (R : realFieldType) (mu : set T -> \bar R) :
  mu set0 = 0 -> semi_sigma_additive mu -> semi_additive mu.
Proof.
move=> mu0 samu A n Am Atriv UAm.
have := samu (fun i => if (i < n)%N then A i else set0).
rewrite (bigcup_splitn n) bigcup0 ?setU0; last first.
  by move=> i _; rewrite -ltn_subRL subnn.
under eq_bigr do rewrite ltn_ord.
move=> /(_ _ _ UAm)/(@cvg_lim _) <-//; last 2 first.
- by move=> i; case: ifP.
- move=> i j _ _; do 2![case: ifP] => ? ?; do ?by rewrite (setI0, set0I) => -[].
  by move=> /Atriv; apply.
apply: lim_near_cst => //=; near=> i.
have /subnKC<- : (n <= i)%N by near: i; exists n.
transitivity (\sum_(j < n + (i - n)) mu (if (j < n)%N then A j else set0)).
  by rewrite big_mkord.
rewrite big_split_ord/=; under eq_bigr do rewrite ltn_ord.
by rewrite [X in _ + X]big1 ?adde0// => ?; rewrite -ltn_subRL subnn.
Unshelve. all: by end_near. Qed.

Lemma semi_sigma_additiveE
  (R : numFieldType) d (T : measurableType d) (mu : set T -> \bar R) :
  semi_sigma_additive mu = sigma_additive mu.
Proof.
rewrite propeqE; split=> [amu A mA tA|amu A mA tA mbigcupA]; last exact: amu.
by apply: amu => //; exact: bigcupT_measurable.
Qed.

Lemma sigma_additive_is_additive
  (R : realFieldType) d (T : measurableType d) (mu : set T -> \bar R) :
  mu set0 = 0 -> sigma_additive mu -> additive mu.
Proof.
move=> mu0; rewrite -semi_sigma_additiveE -semi_additiveE.
exact: semi_sigma_additive_is_additive.
Qed.

HB.mixin Record isContent d
    (T : semiRingOfSetsType d) (R : numFieldType) (mu : set T -> \bar R) := {
  measure_ge0 : forall x, 0 <= mu x ;
  measure_semi_additive : semi_additive mu }.

HB.structure Definition Content d
    (T : semiRingOfSetsType d) (R : numFieldType) := {
  mu & isContent d T R mu }.

Notation content := Content.type.
Notation "{ 'content' 'set' T '->' '\bar' R }" :=
  (content T R) (at level 36, T, R at next level,
    format "{ 'content'  'set'  T  '->'  '\bar'  R }") : ring_scope.

Arguments measure_ge0 {d T R} _.

Section content_signed.
Context d (T : semiRingOfSetsType d) (R : numFieldType).

Variable mu : {content set T -> \bar R}.

Lemma content_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).
Proof. exact: measure_ge0. Qed.

Canonical content_snum S := Signed.mk (content_snum_subproof S).

End content_signed.

Section content_on_semiring_of_sets.
Context d (T : semiRingOfSetsType d) (R : numFieldType)
        (mu : {content set T -> \bar R}).

Lemma measure0 : mu set0 = 0.
Proof.
have /[!big_ord0] ->// := @measure_semi_additive _ _ _ mu (fun=> set0) 0%N.
exact: trivIset_set0.
Qed.

Hint Resolve measure0 : core.

Hint Resolve measure_ge0 : core.

Hint Resolve measure_semi_additive : core.

Lemma measure_semi_additive_ord (n : nat) (F : 'I_n -> set T) :
  (forall (k : 'I_n), measurable (F k)) ->
  trivIset setT F ->
  measurable (\big[setU/set0]_(k < n) F k) ->
  mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Proof.
move=> mF tF mUF; pose F' (i : nat) := oapp F set0 (insub i).
have FE (i : 'I_n) : F i = (F' \o val) i by rewrite /F'/= valK/=.
rewrite (eq_bigr (F' \o val))// (eq_bigr (mu \o F' \o val))//; last first.
  by move=> i _; rewrite FE.
rewrite -measure_semi_additive//.
- by move=> k; rewrite /F'; case: insubP => /=.
- apply/trivIsetP=> i j _ _; rewrite /F'.
  do 2?[case: insubP; rewrite ?(set0I, setI0)//= => ? _ <-].
  by move/trivIsetP: tF; apply.
- by rewrite (eq_bigr (F' \o val)) in mUF.
Qed.

Lemma measure_semi_additive_ord_I (F : nat -> set T) (n : nat) :
  (forall k, (k < n)%N -> measurable (F k)) ->
  trivIset `I_n F ->
  measurable (\big[setU/set0]_(k < n) F k) ->
  mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Proof.
move=> mF tF; apply: measure_semi_additive_ord.
  by move=> k; apply: mF.
by rewrite trivIset_comp// ?(image_eq [surjfun of val])//; apply: 'inj_val.
Qed.

Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) :
    finite_set D ->
    trivIset D F ->
    (forall i, D i -> measurable (F i)) ->
    measurable (\bigcup_(i in D) F i) ->
  mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
Proof.
elim/choicePpointed: I => I in D F *.
  by rewrite !emptyE => *; rewrite fsbig_set0 bigcup0.
move=> [n /ppcard_eqP[f]] Ftriv Fm UFm.
rewrite -(image_eq [surjfun of f^-1%FUN])/= in UFm Ftriv *.
rewrite bigcup_image fsbig_image//= bigcup_mkord -fsbig_ord/= in UFm *.
rewrite (@measure_semi_additive_ord_I (F \o f^-1))//= 1?trivIset_comp//.
by move=> k kn; apply: Fm; exact: funS.
Qed.

Lemma measure_semi_additive2 : semi_additive2 mu.
Proof. exact/semi_additiveW. Qed.
Hint Resolve measure_semi_additive2 : core.

End content_on_semiring_of_sets.
Arguments measure0 {d T R} _.

#[global] Hint Extern 0
  (is_true (0 <= (_ : {content set _ -> \bar _}) _)%E) =>
  solve [apply: measure_ge0] : core.

#[global]
Hint Resolve measure0 measure_semi_additive2 measure_semi_additive : core.

Section content_on_ring_of_sets.
Context d (R : realFieldType)(T : ringOfSetsType d)
        (mu : {content set T -> \bar R}).

Lemma measureU : additive2 mu.
Proof. by rewrite -semi_additive2E. Qed.

Lemma measure_bigsetU : additive mu.
Proof. by rewrite -semi_additiveE. Qed.

Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) :
    finite_set D ->
    trivIset D F ->
    (forall i, D i -> measurable (F i)) ->
  mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
Proof.
move=> Dfin Ftriv Fm; rewrite content_fin_bigcup//.
exact: fin_bigcup_measurable.
Qed.

Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n -> set T) :
  (forall i : 'I_n, P i -> measurable (F i)) -> trivIset P F ->
  mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Proof.
move=> mF tF; rewrite !(big_mkcond P)/= measure_semi_additive_ord//.
- by apply: eq_bigr => i _; rewrite (fun_if mu) measure0.
- by move=> k; case: ifP => //; apply: mF.
- by rewrite -patch_pred trivIset_restr setIT.
- by apply: bigsetU_measurable=> k _; case: ifP => //; apply: mF.
Qed.

Lemma measure_bigsetU_ord n (P : {pred 'I_n}) (F : 'I_n -> set T) :
  (forall i : 'I_n, measurable (F i)) -> trivIset setT F ->
  mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Proof.
by move=> mF tF; rewrite measure_bigsetU_ord_cond//; apply: sub_trivIset tF.
Qed.

Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I -> set T) :
  (forall i, i \in A -> measurable (F i)) -> trivIset [set` A] F ->
  mu (\big[setU/set0]_(i <- A) F i) = (\sum_(i <- A) mu (F i))%E.
Proof.
by move=> mF tF; rewrite -bigcup_fset measure_fin_bigcup// -fsbig_seq.
Qed.

End content_on_ring_of_sets.

#[global]
Hint Resolve measureU measure_bigsetU : core.

HB.mixin Record Content_isMeasure d (T : semiRingOfSetsType d)
    (R : numFieldType) (mu : set T -> \bar R) of Content d mu := {
  measure_semi_sigma_additive : semi_sigma_additive mu }.

#[short(type=measure)]
HB.structure Definition Measure d (T : semiRingOfSetsType d)
    (R : numFieldType) :=
  {mu of Content_isMeasure d T R mu & Content d mu}.

Notation "{ 'measure' 'set' T '->' '\bar' R }" := (measure T%type R)
  (at level 36, T, R at next level,
    format "{ 'measure'  'set'  T  '->'  '\bar'  R }") : ring_scope.

Section measure_signed.
Context d (R : numFieldType) (T : semiRingOfSetsType d).

Variable mu : {measure set T -> \bar R}.

Lemma measure_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).
Proof. exact: measure_ge0. Qed.

Canonical measure_snum S := Signed.mk (measure_snum_subproof S).

End measure_signed.

HB.factory Record isMeasure d (T : semiRingOfSetsType d) (R : realFieldType)
    (mu : set T -> \bar R) := {
  measure0 : mu set0 = 0 ;
  measure_ge0 : forall x, 0 <= mu x ;
  measure_semi_sigma_additive : semi_sigma_additive mu }.

HB.builders Context d (T : semiRingOfSetsType d) (R : realFieldType)
  (mu : set T -> \bar R) of isMeasure _ T R mu.

Let semi_additive_mu : semi_additive mu.
Proof.
apply: semi_sigma_additive_is_additive.
- exact: measure0.
- exact: measure_semi_sigma_additive.
Qed.

HB.instance Definition _ := isContent.Build d T R mu
  measure_ge0 semi_additive_mu.
HB.instance Definition _ := Content_isMeasure.Build d T R mu
  measure_semi_sigma_additive.
HB.end.

Lemma eq_measure d (T : measurableType d) (R : realFieldType)
  (m1 m2 : {measure set T -> \bar R}) :
  (m1 = m2 :> (set T -> \bar R)) -> m1 = m2.
Proof.
move: m1 m2 => [m1 [[m10 m1ge0 [m1sa]]]] [m2 [[+ + [+]]]] /= m1m2.
rewrite -{}m1m2 => m10' m1ge0' m1sa'; f_equal.
by rewrite (_ : m10' = m10)// (_ : m1ge0' = m1ge0)// (_ : m1sa' = m1sa).
Qed.

Section measure_lemmas.
Context d (R : realFieldType) (T : semiRingOfSetsType d).

Variable mu : {measure set T -> \bar R}.

Lemma measure_semi_bigcup A : (forall i : nat, measurable (A i)) ->
    trivIset setT A -> measurable (\bigcup_n A n) ->
  mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).
Proof. by move=> Am Atriv /measure_semi_sigma_additive/cvg_lim<-//. Qed.

End measure_lemmas.

#[global] Hint Extern 0 (_ set0 = 0) => solve [apply: measure0] : core.
#[global] Hint Extern 0 (is_true (0 <= _)) => solve [apply: measure_ge0] : core.

Section measure_lemmas.
Context d (R : realFieldType) (T : measurableType d).
Variable mu : {measure set T -> \bar R}.

Lemma measure_sigma_additive : sigma_additive mu.
Proof.
by rewrite -semi_sigma_additiveE //; apply: measure_semi_sigma_additive.
Qed.

Lemma measure_bigcup (D : set nat) F : (forall i, D i -> measurable (F i)) ->
  trivIset D F -> mu (\bigcup_(n in D) F n) = \sum_(i <oo | i \in D) mu (F i).
Proof.
move=> mF tF; rewrite bigcup_mkcond measure_semi_bigcup.
- by rewrite [in RHS]eseries_mkcond; apply: eq_eseriesr => n _; case: ifPn.
- by move=> i; case: ifPn => // /set_mem; exact: mF.
- by move/trivIset_mkcond : tF.
- by rewrite -bigcup_mkcond; apply: bigcup_measurable.
Qed.

End measure_lemmas.
Arguments measure_bigcup {d R T} _ _.

#[global] Hint Extern 0 (sigma_additive _) =>
  solve [apply: measure_sigma_additive] : core.

Section pushforward_measure.
Local Open Scope ereal_scope.
Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2).
Variables (R : realFieldType) (m : {measure set T1 -> \bar R}).

Definition pushforward (mf : measurable_fun setT f) A := m (f @^-1` A).

Hypothesis mf : measurable_fun setT f.

Let pushforward0 : pushforward mf set0 = 0.
Proof. by rewrite /pushforward preimage_set0 measure0. Qed.

Let pushforward_ge0 A : 0 <= pushforward mf A.
Proof. by apply: measure_ge0; rewrite -[X in measurable X]setIT; apply: mf. Qed.

Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf).
Proof.
move=> F mF tF mUF; rewrite /pushforward preimage_bigcup.
apply: measure_semi_sigma_additive.
- by move=> n; rewrite -[X in measurable X]setTI; exact: mf.
- apply/trivIsetP => /= i j _ _ ij; rewrite -preimage_setI.
  by move/trivIsetP : tF => /(_ _ _ _ _ ij) ->//; rewrite preimage_set0.
- by rewrite -preimage_bigcup -[X in measurable X]setTI; exact: mf.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _
  (pushforward mf) pushforward0 pushforward_ge0 pushforward_sigma_additive.

End pushforward_measure.

Section dirac_measure.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (a : T) (R : realFieldType).

Definition dirac (A : set T) : \bar R := (\1_A a)%:E.

Let dirac0 : dirac set0 = 0. Proof. by rewrite /dirac indic0. Qed.

Let dirac_ge0 B : 0 <= dirac B. Proof. by rewrite /dirac indicE. Qed.

Let dirac_sigma_additive : semi_sigma_additive dirac.
Proof.
move=> F mF tF mUF; rewrite /dirac indicE; have [|aFn] /= := boolP (a \in _).
  rewrite inE => -[n _ Fna].
  have naF m : m != n -> a \notin F m.
    move=> mn; rewrite notin_set => Fma.
    move/trivIsetP : tF => /(_ _ _ Logic.I Logic.I mn).
    by rewrite predeqE => /(_ a)[+ _]; exact.
  apply/cvg_ballP => _/posnumP[e]; near=> m.
  have mn : (n < m)%N by near: m; exists n.+1.
  rewrite big_mkord (bigID (xpred1 (Ordinal mn)))//= big_pred1_eq/= big1/=.
    by rewrite adde0 indicE mem_set//; exact: ballxx.
  by move=> j ij; rewrite indicE (negbTE (naF _ _)).
rewrite [X in X --> _](_ : _ = cst 0); first exact: cvg_cst.
apply/funext => n; rewrite big1// => i _; rewrite indicE; apply/eqP.
by rewrite eqe pnatr_eq0 eqb0; apply: contra aFn => /[!inE] aFn; exists i.
Unshelve. all: by end_near. Qed.

HB.instance Definition _ := isMeasure.Build _ _ _
  dirac dirac0 dirac_ge0 dirac_sigma_additive.

End dirac_measure.
Arguments dirac {d T} _ {R}.

Notation "\d_ a" := (dirac a) : ring_scope.

Section dirac_lemmas_realFieldType.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realFieldType).

Lemma diracE a (A : set T) : \d_a A = (a \in A)%:R%:E :> \bar R.
Proof. by rewrite /dirac indicE. Qed.

Lemma dirac0 (a : T) : \d_a set0 = 0 :> \bar R.
Proof. by rewrite diracE in_set0. Qed.

Lemma diracT (a : T) : \d_a setT = 1 :> \bar R.
Proof. by rewrite diracE in_setT. Qed.

End dirac_lemmas_realFieldType.

Section dirac_lemmas.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).

Lemma finite_card_sum (A : set T) : finite_set A ->
  \esum_(i in A) 1 = (#|` fset_set A|%:R)%:E :> \bar R.
Proof.
move=> finA; rewrite esum_fset// (eq_fsbigr (cst 1))//.
by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite.
Qed.

Lemma finite_card_dirac (A : set T) : finite_set A ->
  \esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.
Proof.
move=> finA; rewrite esum_fset// (eq_fsbigr (cst 1))//.
  by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite.
by move=> i iA; rewrite diracE iA.
Qed.

Lemma infinite_card_dirac (A : set T) : infinite_set A ->
  \esum_(i in A) \d_ i A = +oo :> \bar R.
Proof.
move=> infA; apply/eqyP => r r0.
have [B BA Br] := infinite_set_fset `|ceil r| infA.
apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E).
  by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge.
move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.
rewrite (eq_fsbigr (cst 1))/=; last first.
  by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA.
by rewrite fsbig_finite//= card_fset_sum1 sumEFin natr_sum// set_fsetK.
Qed.

End dirac_lemmas.

Section measure_sum.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m : {measure set T -> \bar R}^nat) (n : nat).

Definition msum (A : set T) : \bar R := \sum_(k < n) m k A.

Let msum0 : msum set0 = 0. Proof. by rewrite /msum big1. Qed.

Let msum_ge0 B : 0 <= msum B. Proof. by rewrite /msum; apply: sume_ge0. Qed.

Let msum_sigma_additive : semi_sigma_additive msum.
Proof.
move=> F mF tF mUF; rewrite [X in _ --> X](_ : _ =
    lim (fun n => \sum_(0 <= i < n) msum (F i))).
  by apply: is_cvg_ereal_nneg_natsum => k _; exact: sume_ge0.
rewrite nneseries_sum//; apply: eq_bigr => /= i _.
exact: measure_semi_bigcup.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ msum
  msum0 msum_ge0 msum_sigma_additive.

End measure_sum.
Arguments msum {d T R}.

Section measure_zero.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).

Definition mzero (A : set T) : \bar R := 0.

Let mzero0 : mzero set0 = 0. Proof. by []. Qed.

Let mzero_ge0 B : 0 <= mzero B. Proof. by []. Qed.

Let mzero_sigma_additive : semi_sigma_additive mzero.
Proof.
move=> F mF tF mUF; rewrite [X in X --> _](_ : _ = cst 0); first exact: cvg_cst.
by apply/funext => n; rewrite big1.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ mzero
  mzero0 mzero_ge0 mzero_sigma_additive.

End measure_zero.
Arguments mzero {d T R}.

Lemma msum_mzero d (T : measurableType d) (R : realType)
    (m_ : {measure set T -> \bar R}^nat) :
  msum m_ 0 = mzero.
Proof. by apply/funext => A/=; rewrite /msum big_ord0. Qed.

Section measure_add.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m1 m2 : {measure set T -> \bar R}).

Definition measure_add := msum (fun n => if n is 0%N then m1 else m2) 2.

Lemma measure_addE A : measure_add A = m1 A + m2 A.
Proof. by rewrite /measure_add/= /msum 2!big_ord_recl/= big_ord0 adde0. Qed.

End measure_add.

Section measure_scale.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realFieldType).
Variables (r : {nonneg R}) (m : {measure set T -> \bar R}).

Definition mscale (A : set T) : \bar R := r%:num%:E * m A.

Let mscale0 : mscale set0 = 0. Proof. by rewrite /mscale measure0 mule0. Qed.

Let mscale_ge0 B : 0 <= mscale B.
Proof. by rewrite /mscale mule_ge0. Qed.

Let mscale_sigma_additive : semi_sigma_additive mscale.
Proof.
move=> F mF tF mUF; rewrite [X in X --> _](_ : _ =
    (fun n => (r%:num)%:E * \sum_(0 <= i < n) m (F i))); last first.
  by apply/funext => k; rewrite ge0_sume_distrr.
rewrite /mscale; have [->|r0] := eqVneq r%:num 0%R.
  rewrite mul0e [X in X --> _](_ : _ = (fun=> 0)); first exact: cvg_cst.
  by under eq_fun do rewrite mul0e.
by apply: cvgeMl => //; exact: measure_semi_sigma_additive.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ mscale
  mscale0 mscale_ge0 mscale_sigma_additive.

End measure_scale.
Arguments mscale {d T R}.

Section measure_series.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (m : {measure set T -> \bar R}^nat) (n : nat).

Definition mseries (A : set T) : \bar R := \sum_(n <= k <oo) m k A.

Let mseries0 : mseries set0 = 0.
Proof. by rewrite /mseries ereal_series eseries0. Qed.

Let mseries_ge0 B : 0 <= mseries B.
Proof.
by rewrite /mseries ereal_series nneseries_esum//; exact: esum_ge0.
Qed.

Let mseries_sigma_additive : semi_sigma_additive mseries.
Proof.
move=> F mF tF mUF; rewrite [X in _ --> X](_ : _ =
  lim (fun n => \sum_(0 <= i < n) mseries (F i))); last first.
  rewrite [in LHS]/mseries.
  transitivity (\sum_(n <= k <oo) \sum_(i <oo) m k (F i)).
    rewrite 2!ereal_series.
    apply: (@eq_eseriesr _ (fun k => m k (\bigcup_n0 F n0))) => i ni.
    exact: measure_semi_bigcup.
  rewrite ereal_series nneseries_interchange//.
  apply: (@eq_eseriesr _ (fun j => \sum_(i <oo | (n <= i)%N) m i (F j))
    (fun i => \sum_(n <= k <oo) m k (F i))).
  by move=> i _; rewrite ereal_series.
apply: is_cvg_ereal_nneg_natsum => k _.
by rewrite /mseries ereal_series; exact: nneseries_ge0.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ mseries
  mseries0 mseries_ge0 mseries_sigma_additive.

End measure_series.
Arguments mseries {d T R}.

Definition mrestr d (T : measurableType d) (R : realFieldType) (D : set T)
  (f : set T -> \bar R) (mD : measurable D) := fun X => f (X `&` D).

Section measure_restr.
Context d (T : measurableType d) (R : realFieldType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).

Local Notation restr := (mrestr mu mD).

Let restr0 : restr set0 = 0%E. Proof. by rewrite /mrestr set0I measure0. Qed.

Let restr_ge0 (A : set _) : (0 <= restr A)%E.
Proof. by rewrite /restr; apply: measure_ge0; exact: measurableI. Qed.

Let restr_sigma_additive : semi_sigma_additive restr.
Proof.
move=> F mF tF mU; pose FD i := F i `&` D.
have mFD i : measurable (FD i) by exact: measurableI.
have tFD : trivIset setT FD.
  apply/trivIsetP => i j _ _ ij.
  move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij).
  by rewrite /FD setIACA => ->; rewrite set0I.
by rewrite /restr setI_bigcupl; exact: measure_sigma_additive.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ restr
  restr0 restr_ge0 restr_sigma_additive.

End measure_restr.

Definition counting (T : choiceType) (R : realType) (X : set T) : \bar R :=
  if `[< finite_set X >] then (#|` fset_set X |)%:R%:E else +oo.
Arguments counting {T R}.

Section measure_count.
Context d (T : measurableType d) (R : realType).
Variables (D : set T) (mD : measurable D).

Local Notation counting := (@counting [choiceType of T] R).

Let counting0 : counting set0 = 0.
Proof. by rewrite /counting asboolT// fset_set0. Qed.

Let counting_ge0 (A : set T) : 0 <= counting A.
Proof. by rewrite /counting; case: ifPn; rewrite ?lee_fin// lee_pinfty. Qed.

Let counting_sigma_additive : semi_sigma_additive counting.
Proof.
move=> F mF tF mU.
have [[i Fi]|infinF] := pselect (exists k, infinite_set (F k)).
  have -> : counting (\bigcup_n F n) = +oo.
    rewrite /counting asboolF//.
    by apply: contra_not Fi; exact/sub_finite_set/bigcup_sup.
  apply/cvgeyPge => M; near=> n.
  have ni : (i < n)%N by near: n; exists i.+1.
  rewrite (bigID (xpred1 i))/= big_mkord (big_pred1 (Ordinal ni))//=.
  rewrite [X in X + _]/(counting _) asboolF// addye ?leey//.
  by rewrite gt_eqF// (@lt_le_trans _ _ 0)//; exact: sume_ge0.
have {infinF}finF : forall i, finite_set (F i) by exact/not_forallP.
pose u : nat^nat := fun n => #|` fset_set (F n) |.
have sumFE n : \sum_(i < n) counting (F i) =
               #|` fset_set (\big[setU/set0]_(k < n) F k) |%:R%:E.
  rewrite -trivIset_sum_card// natr_sum -sumEFin.
  by apply: eq_bigr => // i _; rewrite /counting asboolT.
have [cvg_u|dvg_u] := pselect (cvg (nseries u)).
  have [N _ Nu] : \forall n \near \oo, u n = 0%N by apply: cvg_nseries_near.
  rewrite [X in _ --> X](_ : _ = \sum_(i < N) counting (F i)); last first.
    have -> : \bigcup_i (F i) = \big[setU/set0]_(i < N) F i.
      rewrite (bigcupID (`I_N)) setTI bigcup_mkord.
      rewrite [X in _ `|` X](_ : _ = set0) ?setU0// bigcup0// => i [_ /negP].
      by rewrite -leqNgt => /Nu/eqP/[!cardfs_eq0]/eqP/fset_set_set0 ->.
    by rewrite /counting /= asboolT ?sumFE// -bigcup_mkord; exact: bigcup_finite.
  rewrite -(cvg_shiftn N)/=.
  rewrite (_ : (fun n => _) = (fun=> \sum_(i < N) counting (F i))).
    exact: cvg_cst.
  apply/funext => n; rewrite /index_iota subn0 (addnC n) iotaD big_cat/=.
  rewrite [X in _ + X](_ : _ = 0) ?adde0.
    by rewrite -{1}(subn0 N) big_mkord.
  rewrite add0n big_seq big1// => i /[!mem_iota] => /andP[NI iNn].
  by rewrite /counting asboolT//= -/(u _) Nu.
have {dvg_u}cvg_F : (fun n => \sum_(i < n) counting (F i)) --> +oo.
  rewrite (_ : (fun n => _) = [sequence (\sum_(0 <= i < n) (u i))%:R%:E]_n).
    exact/cvgenyP/dvg_nseries.
  apply/funext => n /=; under eq_bigr.
    by rewrite /counting => i _; rewrite asboolT//; over.
  by rewrite sumEFin natr_sum big_mkord.
have [UFoo|/contrapT[k UFk]] := pselect (infinite_set (\bigcup_n F n)).
  rewrite /counting asboolF//.
  by under eq_fun do rewrite big_mkord.
suff: false by [].
move: cvg_F =>/cvgeyPge/(_ k.+1%:R) [K _] /(_ K (leqnn _)) /=; apply: contra_leT => _.
rewrite sumFE lte_fin ltr_nat ltnS.
have -> : k = #|` fset_set (\bigcup_n F n) |.
  by apply/esym/card_eq_fsetP; rewrite fset_setK//; exists k.
apply/fsubset_leq_card; rewrite -fset_set_sub //.
- by move=> /= t; rewrite -bigcup_mkord => -[m _ Fmt]; exists m.
- by rewrite -bigcup_mkord; exact: bigcup_finite.
- by exists k.
Unshelve. all: by end_near. Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ counting
  counting0 counting_ge0 counting_sigma_additive.

End measure_count.

Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R)
   (op : Monoid.com_law idx) (A : I -> set T) (F : set T -> R) :
    finite_set D -> trivIset D A -> F set0 = idx ->
  \big[op/idx]_(i <- fset_set D) F (A i) =
  \big[op/idx]_(X <- (A @` fset_set D)%fset) F X.
Proof.
elim/Pchoice: R => R in idx op F *.
move=> Dfin Atriv F0; symmetry.
pose D' := [fset i in fset_set D | A i != set0]%fset.
transitivity (\big[op/idx]_(X <- (A @` D')%fset) F X).
  apply: perm_big_supp; rewrite uniq_perm ?filter_uniq//=.
  move=> X; rewrite !mem_filter; case: (eqVneq (F X) idx) => //= FXNidx.
  apply/imfsetP/imfsetP=> -[i/=]; rewrite ?(inE, in_fset_set)//=.
    move=> Di XAi; exists i; rewrite // !(inE, in_fset_set)//=.
    by rewrite (mem_set Di)/= -XAi; apply: contra_neq FXNidx => ->.
  by move=> /andP[Di AiN0] XAi; exists i; rewrite ?in_fset_set.
rewrite big_imfset//=; last first.
  move=> i j; rewrite !(inE, in_fset_set)//= => /andP[+ +] /andP[+ +].
  rewrite !inE => Di /set0P[x Aix] Dj _ Aij.
  by apply: (Atriv _ _ Di Dj); exists x; split=> //; rewrite -Aij.
apply: perm_big_supp; rewrite uniq_perm ?filter_uniq//= => i.
rewrite !mem_filter; case: (eqVneq (F (A i)) idx) => //= FAiidx.
rewrite !(in_fset_set, inE)//=; case: (boolP (i \in D)) => //= Di.
by apply: contra_neq FAiidx => ->.
Qed.

Section covering.
Context {T : Type}.
Implicit Type (C : forall I, set (set I)).
Implicit Type (P : forall I, set I -> set (I -> set T)).

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

Lemma covered_bySr C P P' : (forall I D A, P I D A -> P' I D A) ->
  covered_by C P `<=` covered_by C P'.
Proof.
by move=> PP' X [I [D [A [CX PX ->]]]]; exists I, D, A; split=> //; apply: PP'.
Qed.

Lemma covered_byP C P I D A : C I D -> P I D A ->
  covered_by C P (\bigcup_(i  in D) A i).
Proof. by move=> CID PIDA; exists I, D, A. Qed.

Lemma covered_by_finite P :
    (forall I (D : set I) A, (forall i, D i -> A i = set0) -> P I D A) ->
    (forall (I : pointedType) D A, finite_set D -> P I D A ->
       P nat `I_#|` fset_set D| (A \o nth point (fset_set D))) ->
  covered_by (@finite_set) P =
    [set X : set T | exists n A, [/\ P nat `I_n A & X = \bigcup_(i < n) A i]].
Proof.
move=> P0 Pc; apply/predeqP=> X; rewrite /covered_by /cover/=; split; last first.
  by move=> [n [A [Am ->]]]; exists nat, `I_n, A; split.
case; elim/Ppointed=> I [D [A [Dfin Am ->]]].
  exists 0%N, (fun=> set0); split; first by rewrite II0; apply: P0.
  by rewrite //= emptyE II0 !bigcup0.
exists #|`fset_set D|, (A \o nth point (fset_set D)).
split; first exact: Pc.
by rewrite -bigsetU_fset_set// (big_nth point) big_mkord bigcup_mkord.
Qed.

Lemma covered_by_countable P :
    (forall I (D : set I) A, (forall i, D i -> A i = set0) -> P I D A) ->
    (forall (I : choiceType) (D : set I) (A : I -> set T) (f : nat -> I),
       set_surj [set: nat] D f ->
       P I D A -> P nat [set: nat] (A \o f)) ->
  covered_by (@countable) P =
    [set X : set T | exists A, [/\ P nat [set: nat] A & X = \bigcup_i A i]].
Proof.
move=> P0 Pc; apply/predeqP=> X; rewrite /covered_by /cover/=; split; last first.
  by move=> [A [Am ->]]; exists nat, [set: nat], A; split.
case; elim/Ppointed=> I [D [A [Dcnt Am ->]]].
  exists (fun=> set0); split; first exact: P0.
  by rewrite emptyE bigcup_set0 bigcup0.
have /pfcard_geP[->|[f]] := Dcnt.
  exists (fun=> set0); split; first exact: P0.
  by rewrite !bigcup_set0 bigcup0.
pose g := [splitsurjfun of split f].
exists (A \o g); split=> /=; first exact: Pc Am.
apply/predeqP=> x; split=> [[i Di Aix]|[n _ Afnx]].
  by exists (g^-1%FUN i) => //=; rewrite invK// inE.
by exists (g n) => //; apply: funS.
Qed.

End covering.

Module SetRing.
Definition type (T : Type) := T.
Definition display : measure_display -> measure_display. Proof. by []. Qed.

Section SetRing.
Context d {T : semiRingOfSetsType d}.

Notation rT := (type T).
Canonical ring_eqType := EqType rT ptclass.
Canonical ring_choiceType := ChoiceType rT ptclass.
Canonical ring_ptType := PointedType rT ptclass.
#[export]
HB.instance Definition _ := isRingOfSets.Build (display d) rT ptclass
  (@setring0 T measurable) (@setringU T measurable) (@setringDI T measurable).

Local Notation "d .-ring" := (display d) (at level 1, format "d .-ring").
Local Notation "d .-ring.-measurable" :=
  ((d%mdisp.-ring).-measurable : set (set (type _))).

Local Definition measurable_fin_trivIset : set (set T) :=
  [set A | exists B : set (set T),
    [/\ A = \bigcup_(X in B) X, forall X : set T, B X -> measurable X,
      finite_set B & trivIset B id]].

Lemma ring_measurableE : d.-ring.-measurable = measurable_fin_trivIset.
Proof.
apply/seteqP; split; last first.
  move=> _ [B [-> Bm Bfin Btriv]]; apply: fin_bigcup_measurable => //.
  by move=> i Di; apply: sub_gen_smallest; apply: Bm.
have mdW A : measurable A -> measurable_fin_trivIset A.
  move=> Am; exists [set A]; split; do ?by [rewrite bigcup_set1|move=> ? ->|].
  by move=> ? ? -> ->.
have mdI : setI_closed measurable_fin_trivIset.
  move=> _ _ [A [-> Am Afin Atriv]] [B [-> Bm Bfin Btriv]].
  rewrite setI_bigcupl; under eq_bigcupr do rewrite setI_bigcupr.
  rewrite -bigcup_setM -(bigcup_image _ _ id).
  eexists; split; [reflexivity | | exact/finite_image/finite_setM |].
    by move=> _ [X [? ?] <-]; apply: measurableI; [apply: Am|apply: Bm].
  apply: trivIset_sets => -[a b] [a' b']/= [Xa Xb] [Xa' Xb']; rewrite setIACA.
  by move=> [x [Ax Bx]]; rewrite (Atriv a a') 1?(Btriv b b')//; exists x.
have mdisj_bigcap : finN0_bigcap_closed measurable_fin_trivIset.
   exact/finN0_bigcap_closedP/mdI.
have mDbigcup I (D : set I) (A : set T) (B : I -> set T) : finite_set D ->
    measurable A -> (forall i, D i -> measurable (B i)) ->
    measurable_fin_trivIset (A `\` \bigcup_(i in D) B i).
  have [->|/set0P D0] := eqVneq D set0.
    by rewrite bigcup0// setD0 => *; apply: mdW.
  move=> Dfin Am Bm; rewrite -bigcupDr//; apply: mdisj_bigcap=> // i Di.
  by have [F [Ffin Fm -> ?]] := semi_measurableD A (B i) Am (Bm _ Di); exists F.
have mdU : fin_trivIset_closed measurable_fin_trivIset.
  elim/Pchoice=> I D F Dfin Ftriv Fm.
  have /(_ _ (set_mem _))/cid-/(all_sig_cond_dep (fun=> set0))
       [G /(_ _ (mem_set _))GP] := Fm _ _.
  under eq_bigcupr => i Di do case: (GP i Di) => ->.
  rewrite -bigcup_setM_dep -(bigcup_image _ _ id); eexists; split=> //.
  - by move=> _ [i [Di Gi] <-]; have [_ + _ _] := GP i.1 Di; apply.
  - by apply: finite_image; apply: finite_setMR=> // i Di; have [] := GP i Di.
  apply: trivIset_sets => -[i X] [j Y] /= [Di Gi] [Dj Gj] XYN0.
  suff eqij : i = j.
    by rewrite {i}eqij in Di Gi *; have [_ _ _ /(_ _ _ _ _ XYN0)->] := GP j Dj.
  apply: Ftriv => //; have [-> _ _ _] := GP j Dj; have [-> _ _ _] := GP i Di.
  by case: XYN0 => [x [Xx Yx]]; exists x; split; [exists X|exists Y].
have mdDI : setDI_closed measurable_fin_trivIset.
  move=> A B mA mB; have [F [-> Fm Ffin Ftriv]] := mA.
  have [F' [-> F'm F'fin F'triv]] := mB.
  have [->|/set0P F'N0] := eqVneq F' set0.
    by rewrite bigcup_set0 setD0; exists F.
  rewrite setD_bigcupl; apply: mdU => //; first by apply: trivIset_setIr.
  move=> X DX; rewrite -bigcupDr//; apply: mdisj_bigcap => //.
  move=> Y DY; case: (semi_measurableD X Y); [exact: Fm|exact: F'm|].
  by move=> G [Gfin Gm -> Gtriv]; exists G.
apply: smallest_sub => //; split=> //; first by apply: mdW.
move=> A B mA mB; rewrite -(setUIDK B A) setUA [X in X `|` _]setUidl//.
rewrite -bigcup2inE; apply: mdU => //; last by move=> [|[]]// _; apply: mdDI.
by move=> [|[]]// [|[]]//= _ _ []; rewrite setDE ?setIA => X [] []//.
Qed.

Lemma measurable_subring : (d.-measurable : set (set T)) `<=` d.-ring.-measurable.
Proof. by rewrite /measurable => X Xmeas /= M /= [_]; apply. Qed.

Lemma ring_finite_set (A : set rT) : measurable A -> exists B : set (set T),
  [/\ finite_set B,
      (forall X, B X -> X !=set0),
      trivIset B id,
      (forall X : set T, X \in B -> measurable X) &
      A = \bigcup_(X in B) X].
Proof.
rewrite ring_measurableE => -[B [-> Bm Bfin Btriv]].
exists (B `&` [set X | X != set0]); split.
- by apply: sub_finite_set Bfin; exact: subIsetl.
- by move=> ?/= [_ /set0P].
- by move=> X Y/= [XB _] [YB _]; exact: Btriv.
- by move=> X/= /[!inE] -[] /Bm.
rewrite bigcup_mkcondr; apply: eq_bigcupr => X Bx; case: ifPn => //.
by rewrite notin_set/= => /negP/negPn/eqP.
Qed.

Definition decomp (A : set rT) : set (set T) :=
  if A == set0 then [set set0] else
  if pselect (measurable A) is left mA then projT1 (cid (ring_finite_set mA))
  else [set A].

Lemma decomp_finite_set (A : set rT) : finite_set (decomp A).
Proof.
rewrite /decomp; case: ifPn => // A0; case: pselect => // X.
by case: cid => /= ? [].
Qed.

Lemma decomp_triv (A : set rT) : trivIset (decomp A) id.
Proof.
rewrite /decomp; case: ifP => _; first by move=> i j/= -> ->.
case: pselect => // Am; first by case: cid => //= ? [].
by move=> i j /= -> ->.
Qed.
Hint Resolve decomp_triv : core.

Lemma all_decomp_neq0 (A : set rT) :
  A !=set0 -> (forall X, decomp A X -> X !=set0).
Proof.
move=> /set0P AN0; rewrite /decomp/= (negPf AN0).
case: pselect => //= Am; first by case: cid => //= ? [].
by move=> X ->; exact/set0P.
Qed.

Lemma decomp_neq0 (A : set rT) X : A !=set0 -> X \in decomp A -> X !=set0.
Proof. by move=> /all_decomp_neq0/(_ X) /[!inE]. Qed.

Lemma decomp_measurable (A : set rT) (X : set T) :
  measurable A -> X \in decomp A -> measurable X.
Proof.
rewrite /decomp; case: ifP => _; first by rewrite inE => _ ->.
by case: pselect => // Am _; case: cid => //= ? [_ _ _ + _]; apply.
Qed.

Lemma cover_decomp (A : set rT) : \bigcup_(X in decomp A) X = A.
Proof.
rewrite /decomp; case: ifP => [/eqP->|_]; first by rewrite bigcup0.
case: pselect => // Am; first by case: cid => //= ? [].
by rewrite bigcup_set1.
Qed.

Lemma decomp_sub (A : set rT) (X : set T) : X \in decomp A -> X `<=` A.
Proof.
rewrite /decomp; case: ifP => _; first by rewrite inE/= => ->//.
case: pselect => //= Am; last by rewrite inE => ->.
by case: cid => //= D [_ _ _ _ ->] /[!inE] XD; apply: bigcup_sup.
Qed.

Lemma decomp_set0 : decomp set0 = [set set0].
Proof. by rewrite /decomp eqxx. Qed.

Lemma decompN0 (A : set rT) : decomp A != set0.
Proof.
rewrite /decomp; case: ifPn => [_|AN0]; first by apply/set0P; exists set0.
case: pselect=> //= Am; last by apply/set0P; exists A.
case: cid=> //= D [_ _ _ _ Aeq]; apply: contra_neq AN0; rewrite Aeq => ->.
by rewrite bigcup_set0.
Qed.

Definition measure (R : numDomainType) (mu : set T -> \bar R)
  (A : set rT) : \bar R := \sum_(X \in decomp A) mu X.

Section content.
Context {R : realFieldType} (mu : {content set T -> \bar R}).
Local Notation Rmu := (measure mu).
Arguments big_trivIset {I D T R idx op} A F.

Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) :
    finite_set D -> trivIset D F -> (forall i, i \in D -> measurable (F i)) ->
  Rmu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).
Proof.
move=> Dfin Ftriv Fm; rewrite /measure.
have mUD : measurable (\bigcup_(i in D) F i : set rT).
  apply: fin_bigcup_measurable => // *; apply: sub_gen_smallest.
  exact/Fm/mem_set.
have [->|/set0P[i0 Di0]] := eqVneq D set0.
  by rewrite bigcup_set0 decomp_set0 fsbig_set0 fsbig_set1.
set E := decomp _; have Em X := decomp_measurable mUD X.
transitivity (\sum_(X \in E) \sum_(i \in D) mu (X `&` F i)).
  apply: eq_fsbigr => /= X XE; have XDF : X = \bigcup_(i in D) (X `&` F i).
    by rewrite -setI_bigcupr setIidl//; exact: decomp_sub.
  rewrite [in LHS]XDF content_fin_bigcup//; first exact: trivIset_setIl.
  - by move=> i /mem_set Di; apply: measurableI; [exact: Em|exact: Fm].
  - by rewrite -XDF; exact: Em.
rewrite exchange_fsbig //; last exact: decomp_finite_set.
apply: eq_fsbigr => i Di; have Feq : F i = \bigcup_(X in E) (X `&` F i).
  rewrite -setI_bigcupl setIidr// cover_decomp.
  by apply/bigcup_sup; exact: set_mem.
rewrite -content_fin_bigcup -?Feq//; [exact/decomp_finite_set| | |exact/Fm].
- exact/trivIset_setIr/decomp_triv.
- by move=> X /= XE; apply: measurableI; [apply: Em; rewrite inE | exact: Fm].
Qed.

Lemma RmuE (A : set T) : measurable A -> Rmu A = mu A.
Proof.
move=> Am; rewrite -[A in LHS](@bigcup_set1 _ unit _ tt).
by rewrite Rmu_fin_bigcup// ?fsbig_set1// => -[].
Qed.

Let Rmu0 : Rmu set0 = 0.
Proof.
rewrite -(bigcup_set0 (fun _ : void => set0)).
by rewrite Rmu_fin_bigcup// fsbig_set0.
Qed.

Lemma Rmu_ge0 A : Rmu A >= 0.
Proof. by rewrite sume_ge0. Qed.

Lemma Rmu_additive : semi_additive Rmu.
Proof.
apply/(additive2P Rmu0) => // A B /ring_finite_set[/= {}A [? _ Atriv Am ->]].
move=> /ring_finite_set[/= {}B [? _ Btriv Bm ->]].
rewrite -subset0 => coverAB0.
have AUBfin : finite_set (A `|` B) by rewrite finite_setU.
have AUBtriv : trivIset (A `|` B) id.
  move=> X Y [] ABX [] ABY; do ?by [exact: Atriv|exact: Btriv].
    by move=> [u [Xu Yu]]; case: (coverAB0 u); split; [exists X|exists Y].
  by move=> [u [Xu Yu]]; case: (coverAB0 u); split; [exists Y|exists X].
rewrite -bigcup_setU !Rmu_fin_bigcup//=.
- rewrite fsbigU//= => [X /= [XA XB]]; have [->//|/set0P[x Xx]] := eqVneq X set0.
  by case: (coverAB0 x); split; exists X.
- by move=> X /set_mem [|] /mem_set ?; [exact: Am|exact: Bm].
Qed.

#[export]
HB.instance Definition _ := isContent.Build _ _ _ Rmu Rmu_ge0 Rmu_additive.

End content.

End SetRing.
Module Exports.
Canonical ring_eqType.
Canonical ring_choiceType.
Canonical ring_ptType.
HB.reexport SetRing.
End Exports.
End SetRing.
Export SetRing.Exports.

Notation "d .-ring" := (SetRing.display d)
  (at level 1, format "d .-ring") : measure_display_scope.
Notation "d .-ring.-measurable" :=
  ((d%mdisp.-ring).-measurable : set (set (SetRing.type _))) : classical_set_scope.

Lemma le_measure d (R : realFieldType) (T : semiRingOfSetsType d)
    (mu : {content set T -> \bar R}) :
  {in measurable &, {homo mu : A B / A `<=` B >-> (A <= B)%E}}.
Proof.
move=> A B; rewrite ?inE => mA mB AB; have [|muBfin] := leP +oo%E (mu B).
  by rewrite leye_eq => /eqP ->; rewrite leey.
rewrite -[leRHS]SetRing.RmuE// -[B](setDUK AB) measureU/= ?setDIK//.
- by rewrite SetRing.RmuE ?lee_addl.
- exact: sub_gen_smallest.
- by apply: measurableD; exact: sub_gen_smallest.
Qed.

Lemma measure_le0 d (T : semiRingOfSetsType d) (R : realFieldType)
  (mu : {content set T -> \bar R}) (A : set T) :
  (mu A <= 0)%E = (mu A == 0)%E.
Proof. by case: ltgtP (measure_ge0 mu A). Qed.

Section more_content_semiring_lemmas.
Context d (R : realFieldType) (T : semiRingOfSetsType d).
Variable mu : {content set T -> \bar R}.

Lemma content_sub_additive : sub_additive mu.
Proof.
move=> X A n Am Xm XA; pose B i := A\_`I_n i `&` X.
have XE : X = \big[setU/set0]_(i < n) B i.
  rewrite -big_distrl/= setIidr// => x /XA/=.
  by rewrite -!bigcup_mkord => -[k nk Ax]; exists k; rewrite // patchT ?inE.
have Bm i : measurable (B i).
  case: (ltnP i n) => ltin; last by rewrite /B patchC ?inE ?set0I//= leq_gtF.
  by rewrite /B ?patchT ?inE//; apply: measurableI => //; apply: Am.
have subBA i : B i `<=` A i.
  by rewrite /B/patch; case: ifP; rewrite // set0I//= => _ ?.
have subDUB i : seqDU B i `<=` A i by  move=> x [/subBA].
have DUBm i : measurable (seqDU B i : set (SetRing.type T)).
  apply: measurableD; first exact: sub_gen_smallest.
  by apply: bigsetU_measurable => ? _; apply: sub_gen_smallest.
have DU0 i : (i >= n)%N -> seqDU B i = set0.
  move=> leni; rewrite -subset0 => x []; rewrite /B patchC ?inE/= ?leq_gtF//.
  by case.
rewrite -SetRing.RmuE// XE bigsetU_seqDU measure_bigsetU//.
rewrite [leRHS](big_ord_widen n (mu \o A))//= [leRHS]big_mkcond/=.
rewrite lee_sum => // i _; case: ltnP => ltin; last by rewrite DU0 ?measure0.
rewrite -[leRHS]SetRing.RmuE; last exact: Am.
by rewrite le_measure ?inE//=; last by apply: sub_gen_smallest; apply: Am.
Qed.

Lemma content_sub_fsum (I : choiceType) D (A : set T) (A_ : I -> set T) :
  finite_set D ->
  (forall i, D i -> measurable (A_ i)) ->
  measurable A ->
  A `<=` \bigcup_(i in D) A_ i -> mu A <= \sum_(i \in D) mu (A_ i).
Proof.
elim/choicePpointed: I => I in A_ D *.
  rewrite !emptyE bigcup_set0// subset0 => _ _ _ ->.
  by rewrite measure0 fsbig_set0.
move=> Dfin A_m Am Asub; have [n /ppcard_eqP[f]] := Dfin.
rewrite (reindex_fsbig f^-1%FUN `I_n)//= -fsbig_ord.
rewrite (@content_sub_additive A (A_ \o f^-1%FUN))//=.
  by move=> i ltin; apply: A_m; apply: funS.
rewrite (fsbig_ord _ _ (A_ \o f^-1%FUN))/= -(reindex_fsbig _ _ D)//=.
by rewrite fsbig_setU.
Qed.

(* (* alternative proof *) *)
(* Theorem semi_Boole_inequality : sub_additive mu. *)
(* Proof. *)
(* move=> X A n Am Xm Xsub; rewrite -SetRing.RmuE//. *)
(* under eq_bigr => i do [rewrite -SetRing.RmuE; do ?by apply: Am=> /=]. *)
(* pose rT := SetRing.type T. *)
(* have {}Am i : `I_n i -> measurable (A i : set rT). *)
(*   by move=> *; apply/SetRing.measurableW/Am => /=. *)
(* have {}Xm : measurable (X : set rT) by exact: SetRing.measurableW. *)
(* pose ammu := [additive_measure of SetRing.measure mu]. *)
(* rewrite (le_trans (le_measure ammu  _ _ Xsub)) ?inE// {Xsub}. *)
(*   by rewrite -bigcup_mkord; apply: fin_bigcup_measurable. *)
(* elim: n Am Xm => [|n IHn] Am Xm; first by rewrite !big_ord0 measure0. *)
(* have Anm : measurable (A n : set rT) by apply: Am => /=. *)
(* set B := \big[setU/set0]_(i < n) A i. *)
(* set C := \big[setU/set0]_(i < n.+1) A i. *)
(* have -> : C = B `|` (A n `\` B). *)
(*   suff -> : A n `\` B = C `\` B by rewrite setDUK// /C big_ord_recr/=; left. *)
(*   by rewrite /C big_ord_recr/= !setDE setIUl -!setDE setDv set0U. *)
(* have Bm : measurable (B : set rT). *)
(*   by rewrite -[B]bigcup_mkord; apply: fin_bigcup_measurable => //= i /ltnW/Am. *)
(* rewrite measureU // ?setDIK//; last exact: measurableD. *)
(* rewrite (@le_trans _ _ (ammu B + ammu (A n))) // ?lee_add2l //; last first. *)
(*   by rewrite big_ord_recr /= lee_add2r// IHn// => i /ltnW/Am. *)
(* by rewrite le_measure // ?inE// ?setDE//; exact: measurableD. *)
(* Qed. *)

End more_content_semiring_lemmas.

Section content_ring_lemmas.
Context d (R : realType) (T : ringOfSetsType d).
Variable mu : {content set T -> \bar R}.

Lemma content_ring_sup_sigma_additive (A : nat -> set T) :
  (forall i, measurable (A i)) -> measurable (\bigcup_i A i) ->
  trivIset [set: nat] A -> \sum_(i <oo) mu (A i) <= mu (\bigcup_i A i).
Proof.
move=> Am UAm At; rewrite lime_le//; first exact: is_cvg_nneseries.
near=> n; rewrite big_mkord -measure_bigsetU//= le_measure ?inE//=.
- exact: bigsetU_measurable.
- by rewrite -bigcup_mkord; apply: bigcup_sub => i lein; apply: bigcup_sup.
Unshelve. all: by end_near. Qed.

Lemma content_ring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive mu.
Proof.
move=> mu_sub A Am Atriv UAm.
suff <- : \sum_(i <oo) mu (A i) = mu (\bigcup_n A n) by exact: is_cvg_nneseries.
by apply/eqP; rewrite eq_le mu_sub// ?content_ring_sup_sigma_additive.
Qed.

End content_ring_lemmas.

Section ring_sigma_sub_additive_content.
Context d (R : realType) (T : semiRingOfSetsType d)
        (mu : {content set T -> \bar R}).
Local Notation Rmu := (SetRing.measure mu).
Import SetRing.

Lemma ring_sigma_sub_additive : sigma_sub_additive mu -> sigma_sub_additive Rmu.
Proof.
move=> muS; move=> /= D A Am Dm Dsub.
rewrite /Rmu -(eq_eseriesr (fun _ _ => esum_fset _ _))//; last first.
  by move=> *; exact: decomp_finite_set.
rewrite nneseries_esum ?esum_esum//=; last by move=> *; rewrite esum_ge0.
set K := _ `*`` _.
have /ppcard_eqP[f] : (K #= [set: nat])%card.
  apply: cardMR_eq_nat => [|i].
    by rewrite (_ : [set _ | true] = setT)//; exact/predeqP.
  split; first by apply/finite_set_countable; exact: decomp_finite_set.
  exact/set0P/decompN0.
have {Dsub} : D `<=` \bigcup_(k in K) k.2.
  apply: (subset_trans Dsub); apply: bigcup_sub => i _.
  rewrite -[A i]cover_decomp; apply: bigcup_sub => X/= XAi.
  by move=> x Xx; exists (i, X).
rewrite -(image_eq [bij of f^-1%FUN])/=.
rewrite (esum_set_image _ f^-1)//= bigcup_image => Dsub.
have DXsub X : X \in decomp D -> X `<=` \bigcup_i ((f^-1%FUN i).2 `&` X).
  move=> XD; rewrite -setI_bigcupl -[Y in Y `<=` _](setIidr (decomp_sub XD)).
  by apply: setSI.
have mf i : measurable ((f^-1)%function i).2.
  have [_ /mem_set/decomp_measurable] := 'invS_f (I : setT i).
  by apply; exact: Am.
have mfD i X : X \in decomp D -> measurable (((f^-1)%FUN i).2 `&` X : set T).
  by move=> XD; apply: measurableI; [exact: mf|exact: (decomp_measurable _ XD)].
apply: (@le_trans _ _
    (\sum_(i <oo) \sum_(X <- fset_set (decomp D)) mu ((f^-1%FUN i).2 `&` X))).
  rewrite nneseries_sum// fsbig_finite/=; last exact: decomp_finite_set.
  rewrite [leLHS]big_seq_cond [leRHS]big_seq_cond.
  rewrite lee_sum// => X /[!(andbT,in_fset_set)]; last exact: decomp_finite_set.
  move=> XD; have Xm := decomp_measurable Dm XD.
  by apply: muS => // [i|]; [exact: mfD|exact: DXsub].
apply: lee_lim => /=; do ?apply: is_cvg_nneseries=> //.
  by move=> n _; exact: sume_ge0.
near=> n; rewrite [n in _ <= n]big_mkcond; apply: lee_sum => i _.
rewrite ifT ?inE//.
under eq_big_seq.
  move=> x; rewrite in_fset_set=> [xD|]; last exact: decomp_finite_set.
  rewrite -RmuE//; last exact: mfD.
  over.
rewrite -fsbig_finite/=; last exact: decomp_finite_set.
rewrite -measure_fin_bigcup//=.
- rewrite -setI_bigcupr (cover_decomp D) -[leRHS]RmuE// ?le_measure ?inE//.
    by apply: measurableI => //; apply: sub_gen_smallest; apply: mf.
  by apply: sub_gen_smallest; apply: mf.
- exact: decomp_finite_set.
- by apply: trivIset_setIl; apply: decomp_triv.
- by move=> X /= XD; apply: sub_gen_smallest; apply: mfD; rewrite inE.
Unshelve. all: by end_near. Qed.

Lemma ring_semi_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive Rmu.
Proof.
move=> mu_sub; apply: content_ring_sigma_additive.
by apply: ring_sigma_sub_additive.
Qed.

Lemma semiring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive mu.
Proof.
move=> /ring_semi_sigma_additive Rmu_sigmadd F Fmeas Ftriv cupFmeas.
have Fringmeas i : d.-ring.-measurable (F i) by apply: measurable_subring.
have := Rmu_sigmadd F Fringmeas Ftriv (measurable_subring cupFmeas).
rewrite SetRing.RmuE//.
by under eq_fun do under eq_bigr do rewrite SetRing.RmuE//=.
Qed.

End ring_sigma_sub_additive_content.

#[key="mu"]
HB.factory Record Content_SubSigmaAdditive_isMeasure d
    (R : realType) (T : semiRingOfSetsType d) (mu : set T -> \bar R) of Content d mu := {
  measure_sigma_sub_additive : sigma_sub_additive mu }.

HB.builders Context d (R : realType) (T : semiRingOfSetsType d)
  (mu : set T -> \bar R) of Content_SubSigmaAdditive_isMeasure d R T mu.
  HB.instance Definition _ := Content_isMeasure.Build d T R mu
    (semiring_sigma_additive (measure_sigma_sub_additive)).
HB.end.

Section more_premeasure_ring_lemmas.
Context d (R : realType) (T : semiRingOfSetsType d).
Variable mu : {measure set T -> \bar R}.
Import SetRing.

Lemma measure_sigma_sub_additive : sigma_sub_additive mu.
Proof.
move=> X A Am Xm XA; pose B i := A i `&` X.
have XE : X = \bigcup_i B i by rewrite -setI_bigcupl setIidr.
have Bm i : measurable (B i) by rewrite /B; apply: measurableI.
have subBA i : B i `<=` A i by rewrite /B.
have subDUB i : seqDU B i `<=` A i by  move=> x [/subBA].
have DUBm i : measurable (seqDU B i : set (SetRing.type T)).
  by apply: measurableD => //;
     do 1?apply: bigsetU_measurable => *; apply: sub_gen_smallest.
rewrite XE; move: (XE); rewrite seqDU_bigcup_eq.
under eq_bigcupr do rewrite -[seqDU B _]cover_decomp//.
rewrite -bigcup_setM_dep; set K := _ `*`` _.
have /ppcard_eqP[f] : (K #= [set: nat])%card.
  apply: cardMR_eq_nat=> // i; split; last by apply/set0P; rewrite decompN0.
  exact/finite_set_countable/decomp_finite_set.
pose f' := f^-1%FUN; rewrite -(image_eq [bij of f'])/= bigcup_image/=.
pose g n := (f' n).2; have fVtriv : trivIset [set: nat] g.
  move=> i j _ _; rewrite /g.
  have [/= _ f'iB] : K (f' i) by apply: funS.
  have [/= _ f'jB] : K (f' j) by apply: funS.
  have [f'ij|f'ij] := eqVneq (f' i).1 (f' j).1.
    move=> /(decomp_triv f'iB)/=; rewrite f'ij => /(_ f'jB) f'ij2.
    apply: 'inj_f'; rewrite ?inE//= -!/(f' _); move: f'ij f'ij2.
    by case: (f' i) (f' j) => [? ?] [? ?]//= -> ->.
  move=> [x [f'ix f'jx]]; have Bij := @trivIset_seqDU _ B (f' i).1 (f' j).1 I I.
  rewrite Bij ?eqxx// in f'ij; exists x; split.
  - by move/mem_set : f'iB => /decomp_sub; apply.
  - by move/mem_set : f'jB => /decomp_sub; apply.
have g_inj : set_inj [set i | g i != set0] g.
  by apply: trivIset_inj=> [i /set0P//|]; apply: sub_trivIset fVtriv.
move=> XEbig; rewrite measure_semi_bigcup//= -?XEbig//; last first.
  move=> i; have [/= _ /mem_set] : K (f' i) by apply: funS.
  exact: decomp_measurable.
rewrite [leLHS](_ : _ = \sum_(i <oo | g i != set0) mu (g i)); last first.
  rewrite !nneseries_esum// esum_mkcond [RHS]esum_mkcond; apply: eq_esum.
  move=> i _; rewrite ifT ?inE//=; case: ifPn => //.
  by rewrite notin_set /= -/(g _) => /negP/negPn/eqP ->.
rewrite -(esum_pred_image mu g)//.
rewrite [leLHS](_ : _ = \esum_(X in range g) mu X); last first.
  rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum.
  move=> Y _; case: ifPn; rewrite ?(inE, notin_set)/=.
    by move=> [i giN0 giY]; rewrite ifT// ?inE//=; exists i.
  move=> Ngx; case: ifPn; rewrite ?(inE, notin_set)//=.
  move=> [i _ giY]; apply: contra_not_eq Ngx; rewrite -giY => mugi.
  by exists i => //; apply: contra_neq mugi => ->; rewrite measure0.
have -> : range g = \bigcup_i (decomp (seqDU B i)).
  apply/predeqP => /= Y; split => [[n _ gnY]|[n _ /= YBn]].
  have [/= _ f'nB] : K (f' n) by apply: funS.
    by exists (f' n).1 => //=; rewrite -gnY.
  by exists (f (n, Y)) => //; rewrite /g /f' funK//= inE.
rewrite esum_bigcup//; last first.
   move=> i j /=.
   have [->|/set0P DUBiN0] := eqVneq (seqDU B i) set0.
     rewrite decomp_set0 ?set_fset1 => /negP[].
     apply/eqP/predeqP=> x; split=> [[Y/=->]|->]//; first by rewrite measure0.
     by exists set0.
   have [->|/set0P DUBjN0] := eqVneq (seqDU B j) set0.
     rewrite decomp_set0 ?set_fset1 => _ /negP[].
     apply/eqP/predeqP=> x; split=> [[Y/=->]|->]//=; first by rewrite measure0.
     by exists set0.
   move=> _ _ [Y /= [/[dup] +]].
   move=> /mem_set /decomp_sub YBi /mem_set + /mem_set /decomp_sub YBj.
   move=> /(decomp_neq0 DUBiN0) [y Yy].
   apply: (@trivIset_seqDU _ B) => //; exists y.
   by split => //; [exact: YBi|exact: YBj].
rewrite nneseries_esum// set_true le_esum// => i _.
rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j); last first.
  by rewrite esum_fset//; exact: decomp_finite_set.
rewrite -SetRing.Rmu_fin_bigcup//=; last 3 first.
  exact: decomp_finite_set.
  exact: decomp_triv.
  by move=> ?; exact: decomp_measurable.
rewrite -[leRHS]SetRing.RmuE// le_measure//; last by rewrite cover_decomp.
- rewrite inE; apply: fin_bigcup_measurable; first exact: decomp_finite_set.
  move=> j /mem_set jdec; apply: sub_gen_smallest.
  exact: decomp_measurable jdec.
- by rewrite inE; apply: sub_gen_smallest; exact: Am.
Qed.

End more_premeasure_ring_lemmas.

Section ring_sigma_content.
Context d (R : realType) (T : semiRingOfSetsType d)
        (mu : {measure set T -> \bar R}).
Local Notation Rmu := (SetRing.measure mu).
Import SetRing.

Let ring_sigma_content : semi_sigma_additive Rmu.
Proof. exact/ring_semi_sigma_additive/measure_sigma_sub_additive. Qed.

HB.instance Definition _ := Content_isMeasure.Build _ _ _ Rmu
  ring_sigma_content.

End ring_sigma_content.

Definition fin_num_fun d (T : semiRingOfSetsType d) (R : numDomainType)
  (mu : set T -> \bar R) := forall U, measurable U -> mu U \is a fin_num.

Lemma fin_num_fun_lty d (T : algebraOfSetsType d) (R : realFieldType)
  (mu : set T -> \bar R) : fin_num_fun mu -> mu setT < +oo.
Proof. by move=> h; rewrite ltey_eq h. Qed.

Lemma lty_fin_num_fun d (T : algebraOfSetsType d)
    (R : realFieldType) (mu : {measure set T -> \bar R}) :
  mu setT < +oo -> fin_num_fun mu.
Proof.
move=> h U mU; rewrite fin_real// (lt_le_trans _ (measure_ge0 mu U))//=.
by rewrite (le_lt_trans _ h)//= le_measure// inE.
Qed.

Definition sfinite_measure d (T : measurableType d) (R : realType)
    (mu : set T -> \bar R) :=
  exists2 s : {measure set T -> \bar R}^nat,
    forall n, fin_num_fun (s n) &
    forall U, measurable U -> mu U = mseries s 0 U.

Definition sigma_finite d (T : semiRingOfSetsType d) (R : numDomainType)
    (A : set T) (mu : set T -> \bar R) :=
  exists2 F : (set T)^nat, A = \bigcup_(i : nat) F i &
      forall i, measurable (F i) /\ mu (F i) < +oo.

Lemma fin_num_fun_sigma_finite d (T : algebraOfSetsType d)
    (R : realFieldType) (mu : set T -> \bar R) : mu set0 < +oo ->
  fin_num_fun mu -> sigma_finite setT mu.
Proof.
move=> muoo; exists (fun i => if i \in [set 0%N] then setT else set0).
  by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N.
by move=> n; split; case: ifPn => // _; rewrite fin_num_fun_lty.
Qed.

Lemma sfinite_measure_sigma_finite d (T : measurableType d)
    (R : realType) (mu : {measure set T -> \bar R}) :
  sigma_finite setT mu -> sfinite_measure mu.
Proof.
move=> [F UF mF]; rewrite /sfinite_measure.
have mDF k : measurable (seqDU F k).
  apply: measurableD; first exact: (mF k).1.
  by apply: bigsetU_measurable => i _; exact: (mF i).1.
exists (fun k => [the measure _ _ of mrestr mu (mDF k)]) => [n|U mU].
- apply: lty_fin_num_fun => //=.
  rewrite /mrestr setTI (@le_lt_trans _ _ (mu (F n)))//.
  + apply: le_measure; last exact: subDsetl.
    * rewrite inE; apply: measurableD; first exact: (mF n).1.
      by apply: bigsetU_measurable => i _; exact: (mF i).1.
    * by rewrite inE; exact: (mF n).1.
  + exact: (mF n).2.
rewrite /mseries/= /mrestr/=; apply/esym/cvg_lim => //.
rewrite -[X in _ --> mu X]setIT UF seqDU_bigcup_eq setI_bigcupr.
apply: (@measure_sigma_additive _ _ _ mu (fun k => U `&` seqDU F k)).
  by move=> i; exact: measurableI.
exact/trivIset_setIl/trivIset_seqDU.
Qed.

HB.mixin Record Measure_isSFinite_subdef d (T : measurableType d)
    (R : realType) (mu : set T -> \bar R) := {
  sfinite_measure_subdef : sfinite_measure mu }.

HB.structure Definition SFiniteMeasure
    d (T : measurableType d) (R : realType) :=
  {mu of @Measure _ T R mu & Measure_isSFinite_subdef _ T R mu }.
Arguments sfinite_measure_subdef {d T R} _.

Notation "{ 'sfinite_measure' 'set' T '->' '\bar' R }" :=
  (SFiniteMeasure.type T R) (at level 36, T, R at next level,
    format "{ 'sfinite_measure'  'set'  T  '->'  '\bar'  R }") : ring_scope.

HB.mixin Record isSigmaFinite d (T : semiRingOfSetsType d) (R : numFieldType)
  (mu : set T -> \bar R) := { sigma_finiteT : sigma_finite setT mu }.

#[short(type="sigma_finite_content")]
HB.structure Definition SigmaFiniteContent d T R :=
  { mu of isSigmaFinite d T R mu & @Content d T R mu }.

Arguments sigma_finiteT {d T R} s.
#[global] Hint Resolve sigma_finiteT : core.

Notation "{ 'sigma_finite_content' 'set' T '->' '\bar' R }" :=
  (sigma_finite_content T R) (at level 36, T, R at next level,
    format "{ 'sigma_finite_content'  'set'  T  '->'  '\bar'  R }")
  : ring_scope.

#[short(type="sigma_finite_measure")]
HB.structure Definition SigmaFiniteMeasure d T R :=
  { mu of @SFiniteMeasure d T R mu & isSigmaFinite d T R mu }.

Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" :=
  (sigma_finite_measure T R) (at level 36, T, R at next level,
    format "{ 'sigma_finite_measure'  'set'  T  '->'  '\bar'  R }")
  : ring_scope.

HB.factory Record Measure_isSigmaFinite d (T : measurableType d) (R : realType)
    (mu : set T -> \bar R) of isMeasure _ _ _ mu :=
  { sigma_finiteT : sigma_finite setT mu }.

HB.builders Context d (T : measurableType d) (R : realType)
  mu of @Measure_isSigmaFinite d T R mu.

Lemma sfinite : sfinite_measure mu.
Proof. by apply: sfinite_measure_sigma_finite; exact: sigma_finiteT. Qed.

HB.instance Definition _ := @Measure_isSFinite_subdef.Build _ _ _ mu sfinite.

HB.instance Definition _ := @isSigmaFinite.Build _ _ _ mu sigma_finiteT.

HB.end.

Lemma sigma_finite_mzero d (T : measurableType d) (R : realType) :
  sigma_finite setT (@mzero d T R).
Proof. by apply: fin_num_fun_sigma_finite => //; rewrite measure0. Qed.

HB.instance Definition _ d (T : measurableType d) (R : realType) :=
  @isSigmaFinite.Build d T R mzero (@sigma_finite_mzero d T R).

Lemma sfinite_mzero d (T : measurableType d) (R : realType) :
  sfinite_measure (@mzero d T R).
Proof. by apply: sfinite_measure_sigma_finite; exact: sigma_finite_mzero. Qed.

HB.instance Definition _ d (T : measurableType d) (R : realType) :=
  @Measure_isSFinite_subdef.Build d T R mzero (@sfinite_mzero d T R).

HB.mixin Record SigmaFinite_isFinite d (T : semiRingOfSetsType d)
    (R : numDomainType) (k : set T -> \bar R) :=
  { fin_num_measure : fin_num_fun k }.

HB.structure Definition FinNumFun d (T : semiRingOfSetsType d)
    (R : numFieldType) := { k of SigmaFinite_isFinite _ T R k }.

HB.structure Definition FiniteMeasure d (T : measurableType d) (R : realType) :=
  { k of @SigmaFiniteMeasure _ _ _ k & SigmaFinite_isFinite _ T R k }.
Arguments fin_num_measure {d T R} _.

Notation "{ 'finite_measure' 'set' T '->' '\bar' R }" :=
  (FiniteMeasure.type T R) (at level 36, T, R at next level,
    format "{ 'finite_measure'  'set'  T  '->'  '\bar'  R }") : ring_scope.

HB.factory Record Measure_isFinite d (T : measurableType d)
    (R : realType) (k : set T -> \bar R)
  of isMeasure _ _ _ k := { fin_num_measure : fin_num_fun k }.

HB.builders Context d (T : measurableType d) (R : realType) k
  of Measure_isFinite d T R k.

Let sfinite : sfinite_measure k.
Proof.
apply: sfinite_measure_sigma_finite.
by apply: fin_num_fun_sigma_finite; [rewrite measure0|exact: fin_num_measure].
Qed.

HB.instance Definition _ := @Measure_isSFinite_subdef.Build d T R k sfinite.

Let sigma_finite : sigma_finite setT k.
Proof.
by apply: fin_num_fun_sigma_finite; [rewrite measure0|exact: fin_num_measure].
Qed.

HB.instance Definition _ := @isSigmaFinite.Build d T R k sigma_finite.

Let finite : fin_num_fun k. Proof. exact: fin_num_measure. Qed.

HB.instance Definition _ := @SigmaFinite_isFinite.Build d T R k finite.

HB.end.

HB.factory Record Measure_isSFinite d (T : measurableType d)
    (R : realType) (k : set T -> \bar R) of isMeasure _ _ _ k := {
  sfinite_measure_subdef : exists s : {finite_measure set T -> \bar R}^nat,
    forall U, measurable U -> k U = mseries s 0 U }.

HB.builders Context d (T : measurableType d) (R : realType)
  k of Measure_isSFinite d T R k.

Let sfinite : sfinite_measure k.
Proof.
have [s sE] := sfinite_measure_subdef.
by exists s => //=> n; exact: fin_num_measure.
Qed.

HB.instance Definition _ := @Measure_isSFinite_subdef.Build d T R k sfinite.

HB.end.

Section sfinite_measure.
Context d (T : measurableType d) (R : realType)
        (mu : {sfinite_measure set T -> \bar R}).

Let s : (set T -> \bar R)^nat :=
  let: exist2 x _ _ := cid2 (sfinite_measure_subdef mu) in x.

Let s0 n : s n set0 = 0.
Proof. by rewrite /s; case: cid2. Qed.

Let s_ge0 n x : 0 <= s n x.
Proof. by rewrite /s; case: cid2. Qed.

Let s_semi_sigma_additive n : semi_sigma_additive (s n).
Proof.
by rewrite /s; case: cid2 => s' s'1 s'2; exact: measure_semi_sigma_additive.
Qed.

HB.instance Definition _ n := @isMeasure.Build _ _ _ (s n) (s0 n) (s_ge0 n)
  (@s_semi_sigma_additive n).

Let s_fin n : fin_num_fun (s n).
Proof. by rewrite /s; case: cid2 => F finF muE; exact: finF. Qed.

HB.instance Definition _ n := @Measure_isFinite.Build d T R (s n) (s_fin n).

Definition sfinite_measure_seq : {finite_measure set T -> \bar R}^nat :=
  fun n => [the {finite_measure set T -> \bar R} of s n].

Lemma sfinite_measure_seqP U : measurable U ->
  mu U = mseries sfinite_measure_seq O U.
Proof.
by move=> mU; rewrite /mseries /= /s; case: cid2 => // x xfin ->.
Qed.

End sfinite_measure.

Definition mfrestr d (T : measurableType d) (R : realFieldType) (D : set T)
    (f : set T -> \bar R) (mD : measurable D) of f D < +oo :=
  mrestr f mD.

Section measure_frestr.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Hypothesis moo : mu D < +oo.

Local Notation restr := (mfrestr mD moo).

HB.instance Definition _ := Measure.on restr.

Let restr_fin : fin_num_fun restr.
Proof.
move=> U mU; rewrite /restr /mrestr ge0_fin_numE ?measure_ge0//.
by rewrite (le_lt_trans _ moo)// le_measure// ?inE//; exact: measurableI.
Qed.

HB.instance Definition _ := Measure_isFinite.Build _ _ _ restr
  restr_fin.

End measure_frestr.

HB.mixin Record FiniteMeasure_isSubProbability d (T : measurableType d)
    (R : realType) (P : set T -> \bar R) :=
  { sprobability_setT : P setT <= 1%E }.

#[short(type=subprobability)]
HB.structure Definition SubProbability d (T : measurableType d) (R : realType)
  := {mu of @FiniteMeasure d T R mu & FiniteMeasure_isSubProbability d T R mu }.

HB.factory Record Measure_isSubProbability d (T : measurableType d)
    (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P :=
  { sprobability_setT : P setT <= 1%E }.

HB.builders Context d (T : measurableType d) (R : realType)
  P of Measure_isSubProbability d T R P.

Let finite : @Measure_isFinite d T R P.
Proof.
split; apply: lty_fin_num_fun.
by rewrite (le_lt_trans (@sprobability_setT))// ltey.
Qed.

HB.instance Definition _ := finite.

HB.instance Definition _ :=
  @FiniteMeasure_isSubProbability.Build _ _ _ P sprobability_setT.

HB.end.

HB.mixin Record isProbability d (T : measurableType d) (R : realType)
  (P : set T -> \bar R) := { probability_setT : P setT = 1%E }.

#[short(type=probability)]
HB.structure Definition Probability d (T : measurableType d) (R : realType) :=
  {P of @SubProbability d T R P & isProbability d T R P }.

Section probability_lemmas.
Context d (T : measurableType d) (R : realType) (P : probability T R).

Lemma probability_le1 (A : set T) : measurable A -> (P A <= 1)%E.
Proof.
move=> mA; rewrite -(@probability_setT _ _ _ P).
by apply: le_measure => //; rewrite ?in_setE.
Qed.

End probability_lemmas.

HB.factory Record Measure_isProbability d (T : measurableType d)
    (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P :=
  { probability_setT : P setT = 1%E }.

HB.builders Context d (T : measurableType d) (R : realType)
  P of Measure_isProbability d T R P.

Let subprobability : @Measure_isSubProbability d T R P.
Proof. by split; rewrite probability_setT. Qed.

HB.instance Definition _ := subprobability.

HB.instance Definition _ := @isProbability.Build _ _ _ P probability_setT.

HB.end.

Section mnormalize.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (P : probability T R).

Definition mnormalize :=
  let evidence := mu [set: T] in
  if (evidence == 0) || (evidence == +oo) then fun U => P U
  else fun U => mu U * (fine evidence)^-1%:E.

Let mnormalize0 : mnormalize set0 = 0.
Proof.
by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e.
Qed.

Let mnormalize_ge0 U : 0 <= mnormalize U.
Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed.

Let mnormalize_sigma_additive : semi_sigma_additive mnormalize.
Proof.
move=> F mF tF mUF; rewrite /mnormalize/=.
case: ifPn => [_|_]; first exact: measure_semi_sigma_additive.
rewrite [X in X --> _](_ : _ = (fun n => \sum_(0 <= i < n) mu (F i)) \*
                               cst (fine (mu setT))^-1%:E); last first.
  by apply/funext => n; rewrite -ge0_sume_distrl.
by apply: cvgeMr => //; exact: measure_semi_sigma_additive.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ mnormalize
  mnormalize0 mnormalize_ge0 mnormalize_sigma_additive.

Let mnormalize1 : mnormalize [set: T] = 1.
Proof.
rewrite /mnormalize; case: ifPn; first by rewrite probability_setT.
rewrite negb_or => /andP[ft0 ftoo].
have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey.
by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0.
Qed.

HB.instance Definition _ :=
  Measure_isProbability.Build _ _ _ mnormalize mnormalize1.

End mnormalize.

Section pdirac.
Context d (T : measurableType d) (R : realType).

HB.instance Definition _ x :=
  Measure_isProbability.Build _ _ _ (@dirac _ T x R) (diracT R x).

End pdirac.

Lemma sigma_finite_counting (R : realType) :
  sigma_finite [set: nat] (@counting _ R).
Proof.
exists (fun n => `I_n.+1); first by apply/seteqP; split=> //x _; exists x => /=.
by move=> k; split => //; rewrite /counting/= asboolT// ltry.
Qed.
HB.instance Definition _ R :=
  @isSigmaFinite.Build _ _ _ (@counting _ R) (sigma_finite_counting R).

Section content_semiRingOfSetsType.
Context d (T : semiRingOfSetsType d) (R : realFieldType).
Variables (mu : {content set T -> \bar R}) (A B : set T).
Hypotheses (mA : measurable A) (mB : measurable B).

Lemma measureIl : mu (A `&` B) <= mu A.
Proof. by rewrite le_measure ?inE//; apply: measurableI. Qed.

Lemma measureIr : mu (A `&` B) <= mu B.
Proof. by rewrite le_measure ?inE//; apply: measurableI. Qed.

Lemma subset_measure0 : A `<=` B -> mu B = 0 -> mu A = 0.
Proof.
by move=> AB B0; apply/eqP; rewrite eq_le measure_ge0// -B0 le_measure// inE.
Qed.

End content_semiRingOfSetsType.

Section content_ringOfSetsType.
Context d (T : ringOfSetsType d) (R : realFieldType).
Variable mu : {content set T -> \bar R}.
Implicit Types A B : set T.

Lemma measureDI A B : measurable A -> measurable B ->
  mu A = mu (A `\` B) + mu (A `&` B).
Proof.
move=> mA mB; rewrite -measure_semi_additive2.
- by rewrite -setDDr setDv setD0.
- exact: measurableD.
- exact: measurableI.
- by apply: measurableU; [exact: measurableD |exact: measurableI].
- by rewrite setDE setIACA setICl setI0.
Qed.

Lemma measureD A B : measurable A -> measurable B ->
  mu A < +oo -> mu (A `\` B) = mu A - mu (A `&` B).
Proof.
move=> mA mB mAoo.
rewrite (measureDI mA mB) addeK// fin_numE 1?gt_eqF 1?lt_eqF//.
- by rewrite (le_lt_trans _ mAoo)// le_measure // ?inE//; exact: measurableI.
- by rewrite (lt_le_trans _ (measure_ge0 _ _)).
Qed.

Lemma measureU2 A B : measurable A -> measurable B ->
  mu (A `|` B) <= mu A + mu B.
Proof.
move=> ? ?; rewrite -bigcup2inE bigcup_mkord.
rewrite (le_trans (@content_sub_additive _ _ _ mu _ (bigcup2 A B) 2%N _ _ _))//.
by move=> -[//|[//|[|]]].
by apply: bigsetU_measurable => -[] [//|[//|[|]]].
by rewrite big_ord_recr/= big_ord_recr/= big_ord0 add0e.
Qed.

End content_ringOfSetsType.

Section measureU.
Context d (T : ringOfSetsType d) (R : realFieldType).
Variable mu : {measure set T -> \bar R}.

Lemma measureUfinr A B : measurable A -> measurable B -> mu B < +oo ->
  mu (A `|` B) = mu A + mu B - mu (A `&` B).
Proof.
move=> Am Bm mBfin; rewrite -[B in LHS](setDUK (@subIsetl _ _ A)) setUA.
rewrite [A `|` _]setUidl; last exact: subIsetr.
rewrite measureU//=; [|rewrite setDIr setDv set0U ?setDIK//..].
- by rewrite measureD// ?setIA ?setIid 1?setIC ?addeA//; exact: measurableI.
- exact: measurableD.
Qed.

Lemma measureUfinl A B : measurable A -> measurable B -> mu A < +oo ->
  mu (A `|` B) = mu A + mu B - mu (A `&` B).
Proof. by move=> *; rewrite setUC measureUfinr// setIC [mu B + _]addeC. Qed.

Lemma null_set_setU A B : measurable A -> measurable B ->
  mu A = 0 -> mu B = 0 -> mu (A `|` B) = 0.
Proof.
move=> mA mB A0 B0; rewrite measureUfinl/= ?A0//= ?B0 ?add0e.
by apply/eqP; rewrite oppe_eq0 -measure_le0/= -A0 measureIl.
Qed.

Lemma measureU0 A B : measurable A -> measurable B -> mu B = 0 ->
  mu (A `|` B) = mu A.
Proof.
move=> mA mB B0; rewrite measureUfinr/= ?B0// adde0.
by rewrite (@subset_measure0 _ _ _ _ (A `&` B) B) ?sube0//; exact: measurableI.
Qed.

End measureU.

Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
   (mu mu' : {measure set T -> \bar R}):
    measurable A -> measurable B ->
  mu A = mu' A -> mu B = mu' B -> mu (A `&` B) = mu' (A `&` B) ->
  mu (A `|` B) = mu' (A `|` B).
Proof.
move=> mA mB muA muB muAB; have [mu'ANoo|] := ltP (mu' A) +oo.
  by rewrite !measureUfinl/= ?muA ?muB ?muAB.
rewrite leye_eq => /eqP mu'A; transitivity (+oo : \bar R); apply/eqP.
  by rewrite -leye_eq -mu'A -muA le_measure ?inE//=; apply: measurableU.
by rewrite eq_sym -leye_eq -mu'A le_measure ?inE//=; apply: measurableU.
Qed.

Section measure_continuity.

Local Open Scope ereal_scope.

Lemma nondecreasing_cvg_mu d (T : ringOfSetsType d) (R : realFieldType)
  (mu : {measure set T -> \bar R}) (F : (set T) ^nat) :
  (forall i, measurable (F i)) -> measurable (\bigcup_n F n) ->
  nondecreasing_seq F ->
  mu \o F --> mu (\bigcup_n F n).
Proof.
move=> mF mbigcupF ndF.
have Binter : trivIset setT (seqD F) := trivIset_seqD ndF.
have FBE : forall n, F n.+1 = F n `|` seqD F n.+1 := setU_seqD ndF.
have FE n : F n = \big[setU/set0]_(i < n.+1) (seqD F) i := eq_bigsetU_seqD n ndF.
rewrite eq_bigcup_seqD.
have mB i : measurable (seqD F i) by elim: i => * //=; apply: measurableD.
apply: cvg_trans (measure_semi_sigma_additive _ mB Binter _); last first.
  by rewrite -eq_bigcup_seqD.
apply: (@cvg_trans _ [filter of (fun n => \sum_(i < n.+1) mu (seqD F i))]).
  rewrite [X in _ --> X](_ : _ = mu \o F) // funeqE => n.
  by rewrite -measure_semi_additive // -?FE// => -[|k].
move=> S [n _] nS; exists n => // m nm.
under eq_fun do rewrite -(big_mkord predT (mu \o seqD F)).
exact/(nS m.+1)/(leq_trans nm).
Qed.

Lemma nonincreasing_cvg_mu d (T : algebraOfSetsType d) (R : realFieldType)
  (mu : {measure set T -> \bar R}) (F : (set T) ^nat) :
  mu (F 0%N) < +oo ->
  (forall i, measurable (F i)) -> measurable (\bigcap_n F n) ->
  nonincreasing_seq F -> mu \o F --> mu (\bigcap_n F n).
Proof.
move=> F0pos mF mbigcapF niF; pose G n := F O `\` F n.
have ? : mu (F 0%N) \is a fin_num by rewrite ge0_fin_numE.
have F0E r : mu (F 0%N) - (mu (F 0%N) - r) = r.
  by rewrite oppeB ?addeA ?subee ?add0e// fin_num_adde_defr.
rewrite -[x in _ --> x] F0E.
have -> : mu \o F = fun n => mu (F 0%N) - (mu (F 0%N) - mu (F n)).
  by apply:funext => n; rewrite F0E.
apply: cvgeB; rewrite ?fin_num_adde_defr//; first exact: cvg_cst.
have -> : \bigcap_n F n = F 0%N `&` \bigcap_n F n.
  by rewrite setIidr//; exact: bigcap_inf.
rewrite -measureD // setDE setC_bigcap setI_bigcupr -[x in bigcup _ x]/G.
have -> : (fun n => mu (F 0%N) - mu (F n)) = mu \o G.
  by apply: funext => n /=; rewrite measureD// setIidr//; exact/subsetPset/niF.
apply: nondecreasing_cvg_mu.
- by move=> ?; apply: measurableD; exact: mF.
- rewrite -setI_bigcupr; apply: measurableI; first exact: mF.
  by rewrite -@setC_bigcap; exact: measurableC.
- by move=> n m NM; apply/subsetPset; apply: setDS; apply/subsetPset/niF.
Qed.

End measure_continuity.

Section boole_inequality.
Context d (R : realFieldType) (T : ringOfSetsType d).
Variable mu : {content set T -> \bar R}.

Theorem Boole_inequality (A : (set T) ^nat) n :
    (forall i, `I_n i -> measurable (A i)) ->
  mu (\big[setU/set0]_(i < n) A i) <= \sum_(i < n) mu (A i).
Proof.
move=> Am; rewrite content_sub_additive// -bigcup_mkord.
exact: fin_bigcup_measurable.
Qed.

End boole_inequality.
Notation le_mu_bigsetU := Boole_inequality.

Section sigma_finite_lemma.
Context d (T : ringOfSetsType d) (R : realFieldType) (A : set T)
        (mu : {content set T -> \bar R}).

Lemma sigma_finiteP : sigma_finite A mu ->
  exists2 F, A = \bigcup_i F i &
    nondecreasing_seq F /\ forall i, measurable (F i) /\ mu (F i) < +oo.
Proof.
move=> [S AS moo]; exists (fun n => \big[setU/set0]_(i < n.+1) S i).
  rewrite AS predeqE => t; split => [[i _ Sit]|[i _]].
    by exists i => //; rewrite big_ord_recr /=; right.
  by rewrite -bigcup_mkord => -[j /= ji Sjt]; exists j.
split=> [|i].
- apply/nondecreasing_seqP => i; rewrite [in leRHS]big_ord_recr /=.
  by apply/subsetPset; left.
- split; first by apply: bigsetU_measurable => j _; exact: (moo j).1.
  rewrite (@le_lt_trans _ _ (\sum_(j < i.+1) mu (S j)))//.
    by apply: Boole_inequality => j _; exact: (moo j).1.
  by apply/lte_sum_pinfty => j _; exact: (moo j).2.
Qed.

End sigma_finite_lemma.

Section generalized_boole_inequality.
Context d (T : ringOfSetsType d) (R : realType).
Variable mu : {measure set T -> \bar R}.

Theorem generalized_Boole_inequality (A : (set T) ^nat) :
  (forall i, measurable (A i)) -> measurable (\bigcup_n A n) ->
  mu (\bigcup_n A n) <= \sum_(i <oo) mu (A i).
Proof. by move=> Am UAm; rewrite measure_sigma_sub_additive. Qed.

End generalized_boole_inequality.
Notation le_mu_bigcup := generalized_Boole_inequality.

Section negligible.
Context d (T : semiRingOfSetsType d) (R : realFieldType).

Definition negligible (mu : set T -> \bar R) N :=
  exists A, [/\ measurable A, mu A = 0 & N `<=` A].

Local Notation "mu .-negligible" := (negligible mu).

Variable mu : {content set T -> \bar R}.

Lemma negligibleP A : measurable A -> mu.-negligible A <-> mu A = 0.
Proof.
move=> mA; split => [[B [mB mB0 AB]]|mA0]; last by exists A; split.
apply/eqP; rewrite eq_le measure_ge0 // andbT -mB0.
by apply: (le_measure mu) => //; rewrite in_setE.
Qed.

Lemma negligible_set0 : mu.-negligible set0.
Proof. exact/negligibleP. Qed.

Lemma measure_negligible (A : set T) :
  measurable A -> mu.-negligible A -> mu A = 0%E.
Proof. by move=> mA /negligibleP ->. Qed.

Lemma negligibleS A B : B `<=` A -> mu.-negligible A -> mu.-negligible B.
Proof.
by move=> BA [N [mN N0 AN]]; exists N; split => //; exact: subset_trans AN.
Qed.

Lemma negligibleI A B :
  mu.-negligible A -> mu.-negligible B -> mu.-negligible (A `&` B).
Proof.
move=> [N [mN N0 AN]] [M [mM M0 BM]]; exists (N `&` M); split => //.
- exact: measurableI.
- apply/eqP; rewrite eq_le measure_ge0 andbT -N0 le_measure// inE//.
  exact: measurableI.
- exact: setISS.
Qed.

End negligible.
Notation "mu .-negligible" := (negligible mu) : type_scope.

Definition measure_is_complete d (T : semiRingOfSetsType d) (R : realFieldType)
    (mu : set T -> \bar R) :=
  mu.-negligible `<=` measurable.

Section negligible_ringOfSetsType.
Context d (T : ringOfSetsType d) (R : realFieldType).
Variable mu : {content set T -> \bar R}.

Lemma negligibleU A B :
  mu.-negligible A -> mu.-negligible B -> mu.-negligible (A `|` B).
Proof.
move=> [N [mN N0 AN]] [M [mM M0 BM]]; exists (N `|` M); split => //.
- exact: measurableU.
- apply/eqP; rewrite eq_le measure_ge0 andbT.
  rewrite -N0 -[leRHS]adde0 -M0 -bigsetU_bigcup2; apply: le_trans.
  + apply: (@content_sub_additive _ _ _ _ _ (bigcup2 N M) 2%N) => //.
    * by move=> [|[|[|]]].
    * apply: bigsetU_measurable => // i _; rewrite /bigcup2.
      by case: ifPn => // i0; case: ifPn.
  + by rewrite big_ord_recr/= big_ord_recr/= big_ord0 add0e.
- exact: setUSS.
Qed.

Lemma negligible_bigsetU (F : (set T)^nat) s (P : pred nat) :
  (forall k, P k -> mu.-negligible (F k)) ->
  mu.-negligible (\big[setU/set0]_(k <- s | P k) F k).
Proof.
by move=> PF; elim/big_ind : _ => //;
  [exact: negligible_set0|exact: negligibleU].
Qed.

End negligible_ringOfSetsType.

Lemma negligible_bigcup d (T : measurableType d) (R : realFieldType)
    (mu : {measure set T -> \bar R}) (F : (set T)^nat) :
  (forall k, mu.-negligible (F k)) -> mu.-negligible (\bigcup_k F k).
Proof.
move=> mF; exists (\bigcup_k sval (cid (mF k))); split.
- by apply: bigcupT_measurable => // k; have [] := svalP (cid (mF k)).
- rewrite seqDU_bigcup_eq measure_bigcup//; last first.
    move=> k _; apply: measurableD; first by case: cid => //= A [].
    by apply: bigsetU_measurable => i _; case: cid => //= A [].
  rewrite eseries0// => k _.
  have [mFk mFk0 ?] := svalP (cid (mF k)).
  rewrite measureD//=.
  + rewrite mFk0 sub0e eqe_oppLRP oppe0.
    apply/eqP; rewrite eq_le measure_ge0 andbT.
    rewrite -[leRHS]mFk0 le_measure//= ?inE//; apply: measurableI => //.
    by apply: bigsetU_measurable => i _; case: cid => // A [].
  + by apply: bigsetU_measurable => i _; case: cid => // A [].
  + by rewrite mFk0.
- by apply: subset_bigcup => k _; rewrite /sval/=; by case: cid => //= A [].
Qed.

Section ae.

Definition almost_everywhere d (T : semiRingOfSetsType d) (R : realFieldType)
  (mu : set T -> \bar R) (P : T -> Prop) := mu.-negligible (~` [set x | P x]).

Let almost_everywhereT d (T : semiRingOfSetsType d) (R : realFieldType)
    (mu : {content set T -> \bar R}) : almost_everywhere mu setT.
Proof. by rewrite /almost_everywhere setCT; exact: negligible_set0. Qed.

Let almost_everywhereS d (T : semiRingOfSetsType d) (R : realFieldType)
    (mu : {measure set T -> \bar R}) A B : A `<=` B ->
  almost_everywhere mu A -> almost_everywhere mu B.
Proof. by move=> AB; apply: negligibleS; exact: subsetC. Qed.

Let almost_everywhereI d (T : ringOfSetsType d) (R : realFieldType)
    (mu : {measure set T -> \bar R}) A B :
  almost_everywhere mu A -> almost_everywhere mu B ->
  almost_everywhere mu (A `&` B).
Proof.
by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU.
Qed.

#[global]
Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType)
  (mu : {measure set T -> \bar R}) : Filter (almost_everywhere mu).
Proof.
by split; [exact: almost_everywhereT|exact: almost_everywhereI|
  exact: almost_everywhereS].
Qed.

#[global]
Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d}
    (R : realFieldType) (mu : {measure set T -> \bar R}) :
  mu [set: T] > 0 -> ProperFilter (almost_everywhere mu).
Proof.
move=> muT; split=> [|]; last exact: ae_filter_ringOfSetsType.
rewrite /almost_everywhere setC0 => /(measure_negligible measurableT).
by apply/eqP; rewrite eq_le negb_and measure_ge0 orbF -ltNge.
Qed.

End ae.

#[global] Hint Extern 0 (Filter (almost_everywhere _)) =>
  (apply: ae_filter_ringOfSetsType) : typeclass_instances.

#[global] Hint Extern 0 (ProperFilter (almost_everywhere _)) =>
  (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances.

Definition almost_everywhere_notation d (T : semiRingOfSetsType d)
    (R : realFieldType) (mu : set T -> \bar R) (P : T -> Prop)
  & (phantom Prop (forall x, P x)) := almost_everywhere mu P.
Notation "{ 'ae' m , P }" :=
  (almost_everywhere_notation m (inPhantom P)) : type_scope.

Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType}
    (mu : {measure set _ -> \bar R}) (P : T -> Prop) :
  (forall x, P x) -> {ae mu, forall x, P x}.
Proof.
move=> aP; have -> : P = setT by rewrite predeqE => t; split.
by apply/negligibleP; [rewrite setCT|rewrite setCT measure0].
Qed.

Definition sigma_subadditive {T} {R : numFieldType}
  (mu : set T -> \bar R) := forall (F : (set T) ^nat),
  mu (\bigcup_n (F n)) <= \sum_(i <oo) mu (F i).

HB.mixin Record isOuterMeasure
    (R : numFieldType) (T : Type) (mu : set T -> \bar R) := {
  outer_measure0 : mu set0 = 0 ;
  outer_measure_ge0 : forall x, 0 <= mu x ;
  le_outer_measure : {homo mu : A B / A `<=` B >-> A <= B} ;
  outer_measure_sigma_subadditive : sigma_subadditive mu }.

#[short(type=outer_measure)]
HB.structure Definition OuterMeasure (R : numFieldType) (T : Type) :=
  {mu & isOuterMeasure R T mu}.

Notation "{ 'outer_measure' 'set' T '->' '\bar' R }" := (outer_measure R T)
  (at level 36, T, R at next level,
    format "{ 'outer_measure'  'set'  T  '->'  '\bar'  R }") : ring_scope.

#[global] Hint Extern 0 (_ set0 = 0) => solve [apply: outer_measure0] : core.
#[global] Hint Extern 0 (sigma_subadditive _) =>
  solve [apply: outer_measure_sigma_subadditive] : core.

Arguments outer_measure0 {R T} _.
Arguments outer_measure_ge0 {R T} _.
Arguments le_outer_measure {R T} _.
Arguments outer_measure_sigma_subadditive {R T} _.

Section outer_measureU.
Context d (T : semiRingOfSetsType d) (R : realType).
Variable mu : {outer_measure set T -> \bar R}.
Local Open Scope ereal_scope.

Lemma outer_measure_subadditive (F : nat -> set T) n :
  mu (\big[setU/set0]_(i < n) F i) <= \sum_(i < n) mu (F i).
Proof.
pose F' := fun k => if (k < n)%N then F k else set0.
rewrite -(big_mkord xpredT F) big_nat (eq_bigr F')//; last first.
  by move=> k /= kn; rewrite /F' kn.
rewrite -big_nat big_mkord.
have := outer_measure_sigma_subadditive mu F'.
rewrite (bigcup_splitn n) (_ : bigcup _ _ = set0) ?setU0; last first.
  by rewrite bigcup0 // => k _; rewrite /F' /= ltnNge leq_addr.
move/le_trans; apply.
rewrite (nneseries_split n); last by move=> ?; exact: outer_measure_ge0.
rewrite [X in _ + X](_ : _ = 0) ?adde0//; last first.
  rewrite eseries_cond/= eseries_mkcond eseries0//.
  by move=> k _; case: ifPn => //; rewrite /F' leqNgt => /negbTE ->.
by apply: lee_sum => i _; rewrite /F' ltn_ord.
Qed.

Lemma outer_measureU2 A B : mu (A `|` B) <= mu A + mu B.
Proof.
have := outer_measure_subadditive (bigcup2 A B) 2.
by rewrite !big_ord_recl/= !big_ord0 setU0 adde0.
Qed.

End outer_measureU.

Lemma le_outer_measureIC (R : realFieldType) T
  (mu : {outer_measure set T -> \bar R}) (A X : set T) :
  mu X <= mu (X `&` A) + mu (X `&` ~` A).
Proof.
pose B : (set T) ^nat := bigcup2 (X `&` A) (X `&` ~` A).
have cvg_mu : (fun n => \sum_(i < n) mu (B i)) --> mu (B 0%N) + mu (B 1%N).
  rewrite -2!cvg_shiftS /=.
  rewrite [X in X --> _](_ : _ = (fun=> mu (B 0%N) + mu (B 1%N))); last first.
    rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _.
    by rewrite /B /bigcup2 /=.
  exact: cvg_cst.
have := outer_measure_sigma_subadditive mu B.
suff : \bigcup_n B n = X.
  move=> -> /le_trans; apply; under eq_fun do rewrite big_mkord.
  by rewrite (cvg_lim _ cvg_mu).
transitivity (\big[setU/set0]_(i < 2) B i).
  by rewrite (bigcup_splitn 2) // -bigcup_mkord setUidl// => t -[].
by rewrite 2!big_ord_recl big_ord0 setU0 /= -setIUr setUCr setIT.
Unshelve. all: by end_near. Qed.

Definition caratheodory_measurable (R : realType) (T : Type)
  (mu : set T -> \bar R) (A : set T) := forall X,
  mu X = mu (X `&` A) + mu (X `&` ~` A).

Local Notation "mu .-caratheodory" :=
   (caratheodory_measurable mu) : classical_set_scope.

Lemma le_caratheodory_measurable (R : realType) T
  (mu : {outer_measure set T -> \bar R}) (A : set T) :
  (forall X, mu (X `&` A) + mu (X `&` ~` A) <= mu X) ->
  mu.-caratheodory A.
Proof.
move=> suf X; apply/eqP; rewrite eq_le; apply/andP; split;
  [exact: le_outer_measureIC | exact: suf].
Qed.

Section caratheodory_theorem_sigma_algebra.
Variables (R : realType) (T : Type) (mu : {outer_measure set T -> \bar R}).

Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X :
  mu (X `&` \bigcup_k A k) <= \sum_(k <oo) mu (X `&` A k).
Proof.
apply: (le_trans _ (outer_measure_sigma_subadditive mu (fun n => X `&` A n))).
by apply/le_outer_measure; rewrite setI_bigcupr.
Qed.

Let M := mu.-caratheodory.

Lemma caratheodory_measurable_set0 : M set0.
Proof. by move=> X /=; rewrite setI0 outer_measure0 add0e setC0 setIT. Qed.

Lemma caratheodory_measurable_setC A : M A -> M (~` A).
Proof. by move=> MA X; rewrite setCK addeC -MA. Qed.

Lemma caratheodory_measurable_setU_le (X A B : set T) :
  mu.-caratheodory A -> mu.-caratheodory B ->
  mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <= mu X.
Proof.
move=> mA mB; pose Y := X `&` A `|` X `&` B `&` ~` A.
have /(lee_add2r (mu (X `&` ~` (A `|` B)))) :
    mu Y <= mu (X `&` A) + mu (X `&` B `&` ~` A).
  pose Z := bigcup2 (X `&` A) (X `&` B `&` ~` A).
  have -> : Y = \bigcup_k Z k.
    rewrite predeqE => t; split=> [[?|?]|[]]; [by exists O|by exists 1%N|].
    by move=> [_ ?|[_ ?|//]]; [left|right].
  rewrite (le_trans (outer_measure_sigma_subadditive mu Z))//.
  rewrite le_eqVlt; apply/orP; left; apply/eqP.
  apply/cvg_lim => //; rewrite -(cvg_shiftn 2)/=; apply: cvg_near_cst.
  apply: nearW => k; rewrite big_mkord addn2 2!big_ord_recl big1 ?adde0//.
  by move=> ? _; exact: outer_measure0.
have /le_trans : mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <=
    mu Y + mu (X `&` ~` (A `|` B)).
  rewrite setIUr (_ : X `&` A `|` X `&` B = Y) //.
  rewrite /Y -[in LHS](setIT B) -(setUCr A) 2!setIUr setUC -[in RHS]setIA.
  rewrite setUC setUA; congr (_ `|` _).
  by rewrite setUidPl setICA; apply: subIset; right.
suff -> : mu (X `&` A) + mu (X `&` B `&` ~` A) +
    mu (X `&` (~` (A `|` B))) = mu X by exact.
by rewrite setCU setIA -(setIA X) setICA (setIC B) -addeA -mB -mA.
Qed.

Lemma caratheodory_measurable_setU A B : M A -> M B -> M (A `|` B).
Proof.
move=> mA mB X; apply/eqP; rewrite eq_le.
by rewrite le_outer_measureIC andTb caratheodory_measurable_setU_le.
Qed.

Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) :
  (forall n, M (A n)) -> forall n, M (\big[setU/set0]_(i < n) A i).
Proof.
move=> MA n; elim/big_ind : _ => //; first exact: caratheodory_measurable_set0.
exact: caratheodory_measurable_setU.
Qed.

Lemma caratheodory_measurable_setI A B : M A -> M B -> M (A `&` B).
Proof.
move=> mA mB; rewrite -(setCK A) -(setCK B) -setCU.
by apply/caratheodory_measurable_setC/caratheodory_measurable_setU;
  exact/caratheodory_measurable_setC.
Qed.

Lemma caratheodory_measurable_setD A B : M A -> M B -> M (A `\` B).
Proof.
move=> mA mB; rewrite setDE; apply: caratheodory_measurable_setI => //.
exact: caratheodory_measurable_setC.
Qed.

Section additive_ext_lemmas.
Variable A B : set T.
Hypothesis (mA : M A) (mB : M B).

Let caratheodory_decomp X :
  mu X = mu (X `&` A `&` B) + mu (X `&` A `&` ~` B) +
         mu (X `&` ~` A `&` B) + mu (X `&` ~` A `&` ~` B).
Proof. by rewrite mA mB [X in _ + _ + X = _]mB addeA. Qed.

Let caratheorody_decompIU X : mu (X `&` (A `|` B)) =
  mu (X `&` A `&` B) + mu (X `&` ~` A `&` B) + mu (X `&` A `&` ~` B).
Proof.
rewrite caratheodory_decomp -!addeA; congr (mu _ + _).
  rewrite -!setIA; congr (_ `&` _).
  by rewrite setIC; apply/setIidPl; apply: subIset; left; exact: subsetUl.
rewrite addeA addeC [X in mu X + _](_ : _ = set0); last first.
  by rewrite -setIA -setCU -setIA setICr setI0.
rewrite outer_measure0 add0e addeC -!setIA; congr (mu (X `&` _) + mu (X `&` _)).
  by rewrite setIC; apply/setIidPl; apply: subIset; right; exact: subsetUr.
by rewrite setIC; apply/setIidPl; apply: subIset; left; exact: subsetUl.
Qed.

Lemma disjoint_caratheodoryIU X : [disjoint A & B] ->
  mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B).
Proof.
move=> /eqP AB; rewrite caratheodory_decomp -setIA AB setI0 outer_measure0.
rewrite add0e addeC -setIA -setCU -setIA setICr setI0 outer_measure0 add0e.
rewrite -!setIA; congr (mu (X `&` _ ) + mu (X `&` _)).
rewrite (setIC A) setIA setIC; apply/setIidPl.
- by rewrite setIUl setICr setU0 subsetI; move/disjoints_subset in AB; split.
- rewrite setIA setIC; apply/setIidPl; rewrite setIUl setICr set0U.
  by move: AB; rewrite setIC => /disjoints_subset => AB; rewrite subsetI; split.
Qed.
End additive_ext_lemmas.

Lemma caratheodory_additive (A : (set T) ^nat) : (forall n, M (A n)) ->
  trivIset setT A -> forall n X,
    mu (X `&` \big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (X `&` A i).
Proof.
move=> MA ta; elim=> [|n ih] X; first by rewrite !big_ord0 setI0 outer_measure0.
rewrite big_ord_recr /= disjoint_caratheodoryIU // ?ih ?big_ord_recr //.
- exact: caratheodory_measurable_bigsetU.
- by apply/eqP/(@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE.
Qed.

Lemma caratheodory_lime_le (A : (set T) ^nat) : (forall n, M (A n)) ->
  trivIset setT A -> forall X,
  \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` \bigcup_k A k) <= mu X.
Proof.
move=> MA tA X.
set A' := \bigcup_k A k; set B := fun n => \big[setU/set0]_(k < n) (A k).
suff : forall n, \sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X.
  move=> XA; rewrite (_ : lim _ = ereal_sup
      ((fun n => \sum_(k < n) mu (X `&` A k)) @` setT)); last first.
    under eq_fun do rewrite big_mkord.
    apply/cvg_lim => //; apply: ereal_nondecreasing_cvg.
    apply: (lee_sum_nneg_ord (fun n => mu (X `&` A n)) xpredT) => n _.
    exact: outer_measure_ge0.
  move XAx : (mu (X `&` ~` A')) => [x| |].
  - rewrite -lee_subr_addr //; apply: ub_ereal_sup => /= _ [n _] <-.
    by rewrite EFinN lee_subr_addr // -XAx XA.
  - suff : mu X = +oo by move=> ->; rewrite leey.
    by apply/eqP; rewrite -leye_eq -XAx le_outer_measure.
  - by rewrite addeNy leNye.
move=> n.
apply: (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))).
  apply/lee_add2l/le_outer_measure; apply: setIS; exact/subsetC/bigsetU_bigcup.
rewrite [in leRHS](caratheodory_measurable_bigsetU MA n) lee_add2r//.
by rewrite caratheodory_additive.
Qed.
#[deprecated(since="mathcomp-analysis 0.6.0",
      note="renamed `caratheodory_lime_le`")]
Notation caratheodory_lim_lee := caratheodory_lime_le (only parsing).

Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) :
  (forall n, M (A n)) -> trivIset setT A -> M (\bigcup_k (A k)).
Proof.
move=> MA tA; apply: le_caratheodory_measurable => X /=.
have /(lee_add2r (mu (X `&` ~` \bigcup_k A k))) := outer_measure_bigcup_lim A X.
by move/le_trans; apply; exact: caratheodory_lime_le.
Qed.

Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (forall n, M (A n)) ->
  M (\bigcup_k (A k)).
Proof.
move=> MA; rewrite -eq_bigcup_seqD_bigsetU.
apply/caratheodory_measurable_trivIset_bigcup; last first.
  by apply: trivIset_seqD => m n mn; exact/subsetPset/subset_bigsetU.
by case=> [|n /=]; [| apply/caratheodory_measurable_setD => //];
  exact/caratheodory_measurable_bigsetU.
Qed.

End caratheodory_theorem_sigma_algebra.

Definition caratheodory_type (R : realType) (T : Type)
  (mu : set T -> \bar R) := T.

Definition caratheodory_display R T : (set T -> \bar R) -> measure_display.
Proof. exact. Qed.

Section caratheodory_sigma_algebra.
Variables (R : realType) (T : pointedType) (mu : {outer_measure set T -> \bar R}).

HB.instance Definition _ := @isMeasurable.Build (caratheodory_display mu)
  (caratheodory_type mu) (Pointed.class T) mu.-caratheodory
    (caratheodory_measurable_set0 mu)
    (@caratheodory_measurable_setC _ _ mu)
    (@caratheodory_measurable_bigcup _ _ mu).

End caratheodory_sigma_algebra.

Notation "mu .-cara" := (caratheodory_display mu) : measure_display_scope.
Notation "mu .-cara.-measurable" :=
  (measurable : set (set (caratheodory_type mu))) : classical_set_scope.

Section caratheodory_measure.
Variables (R : realType) (T : pointedType).
Variable mu : {outer_measure set T -> \bar R}.
Let U := caratheodory_type mu.

Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
Proof. exact: outer_measure0. Qed.

Lemma caratheodory_measure_ge0 (A : set U) : 0 <= mu A.
Proof. exact: outer_measure_ge0. Qed.

Lemma caratheodory_measure_sigma_additive :
  semi_sigma_additive (mu : set U -> _).
Proof.
move=> A mA tA mbigcupA; set B := \bigcup_k A k.
suff : forall X, mu X = \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` B).
  move/(_ B); rewrite setICr outer_measure0 adde0.
  rewrite (_ : (fun n => _) = fun n => \sum_(k < n) mu (A k)); last first.
    rewrite funeqE => n; rewrite big_mkord; apply: eq_bigr => i _; congr (mu _).
    by rewrite setIC; apply/setIidPl; exact: bigcup_sup.
  move=> ->; have := fun n (_ : xpredT n) => outer_measure_ge0 mu (A n).
  move/(@is_cvg_nneseries _ _ _ 0) => /cvg_ex[l] hl.
  under [in X in _ --> X]eq_fun do rewrite -(big_mkord xpredT (mu \o A)).
  by move/cvg_lim : (hl) => ->.
move=> X.
have mB : mu.-cara.-measurable B := caratheodory_measurable_bigcup mA.
apply/eqP; rewrite eq_le (caratheodory_lime_le mA tA X) andbT.
have /(lee_add2r (mu (X `&` ~` B))) := outer_measure_bigcup_lim mu A X.
by rewrite -le_caratheodory_measurable // => ?; rewrite -mB.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _
  (mu : set (caratheodory_type mu) -> _)
  caratheodory_measure0 caratheodory_measure_ge0
  caratheodory_measure_sigma_additive.

Lemma measure_is_complete_caratheodory :
  measure_is_complete (mu : set (caratheodory_type mu) -> _).
Proof.
move=> B [A [mA muA0 BA]]; apply: le_caratheodory_measurable => X.
suff -> : mu (X `&` B) = 0.
  by rewrite add0e le_outer_measure //; apply: subIset; left.
have muB0 : mu B = 0.
  apply/eqP; rewrite eq_le outer_measure_ge0 andbT.
  by apply: (le_trans (le_outer_measure mu _ _ BA)); rewrite -muA0.
apply/eqP; rewrite eq_le outer_measure_ge0 andbT.
have : X `&` B `<=` B by apply: subIset; right.
by move/(le_outer_measure mu); rewrite muB0 => ->.
Qed.

End caratheodory_measure.

Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) e
    (P : pred nat) : (forall n, 0 <= A n) -> (0 <= e)%R ->
  \sum_(i <oo | P i) (A i + (e / (2 ^ i.+1)%:R)%:E) <=
  \sum_(i <oo | P i) A i + e%:E.
Proof.
move=> A0 /nonnegP[{}e].
rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) +
    \sum_(0 <= i < n) (e%:num / (2 ^ i.+1)%:R)%:E))) //.
  rewrite nneseriesD // limeD //.
  - rewrite lee_add2l //; apply: lee_lim => //.
    + exact: is_cvg_nneseries.
    + exact: is_cvg_nneseries.
    + by near=> n; exact: lee_sum_nneg_subset.
  - exact: is_cvg_nneseries.
  - exact: is_cvg_nneseries.
  - exact: adde_def_nneseries.
suff cvggeo : (fun n => \sum_(0 <= i < n) (e%:num / (2 ^ i.+1)%:R)%:E) -->
    e%:num%:E.
  rewrite limeD //.
  - by rewrite lee_add2l // (cvg_lim _ cvggeo).
  - exact: is_cvg_nneseries.
  - by apply: is_cvg_nneseries => ?; rewrite lee_fin divr_ge0.
  - by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_defl.
rewrite (_ : (fun n => _) = EFin \o
    (fun n => \sum_(0 <= i < n) (e%:num / (2 ^ (i + 1))%:R))%R); last first.
  rewrite funeqE => n /=; rewrite (@big_morph _ _ EFin 0 adde)//.
  by under [in RHS]eq_bigr do rewrite addn1.
apply: cvg_comp; last by apply cvg_refl.
have := cvg_geometric_series_half e%:num O.
by rewrite expr0 divr1; apply: cvg_trans.
Unshelve. all: by end_near. Qed.

Lemma epsilon_trick0 (R : realType) (eps : R) (P : pred nat) :
  (0 <= eps)%R -> \sum_(i <oo | P i) (eps / (2 ^ i.+1)%:R)%:E <= eps%:E.
Proof.
move=> epspos; have := epsilon_trick P (fun=> lexx 0) epspos.
(* TODO: breaks coq 8.15 and below *)
(* (under eq_eseriesr  do rewrite add0e) => /le_trans; apply. *)
rewrite (@eq_eseriesr _ (fun n => 0 + _) (fun n => (eps/(2^n.+1)%:R)%:E)).
  by move/le_trans; apply; rewrite eseries0 ?add0e; [exact: lexx | move=> ? ?].
by move=> ? ?; rewrite add0e.
Qed.

Section measurable_cover.
Context d (T : semiRingOfSetsType d).
Implicit Types (X : set T) (F : (set T)^nat).

Definition measurable_cover X := [set F : (set T)^nat |
  (forall i, measurable (F i)) /\ X `<=` \bigcup_k (F k)].

Lemma cover_measurable X F : measurable_cover X F -> forall k, measurable (F k).
Proof. by move=> + k; rewrite /measurable_cover => -[] /(_ k). Qed.

Lemma cover_subset X F : measurable_cover X F -> X `<=` \bigcup_k (F k).
Proof. by case. Qed.

End measurable_cover.

Lemma measurable_uncurry (T1 T2 : Type) d (T : semiRingOfSetsType d)
    (G : T1 -> T2 -> set T) (x : T1 * T2) :
  measurable (G x.1 x.2) <-> measurable (uncurry G x).
Proof. by case: x. Qed.

Section outer_measure_construction.
Context d (T : semiRingOfSetsType d) (R : realType).
Variable mu : set T -> \bar R.
Hypothesis (measure0 : mu set0 = 0) (measure_ge0 : forall X, mu X >= 0).
Hint Resolve measure_ge0 measure0 : core.

Definition mu_ext (X : set T) : \bar R :=
  ereal_inf [set \sum_(k <oo) mu (A k) | A in measurable_cover X].
Local Notation "mu^*" := mu_ext.

Lemma le_mu_ext : {homo mu^* : A B / A `<=` B >-> A <= B}.
Proof.
move=> A B AB; apply/le_ereal_inf => x [B' [mB' BB']].
by move=> <-{x}; exists B' => //; split => //; apply: subset_trans AB BB'.
Qed.

Lemma mu_ext_ge0 A : 0 <= mu^* A.
Proof.
apply: lb_ereal_inf => x [B [mB AB] <-{x}]; rewrite lime_ge //=.
  exact: is_cvg_nneseries.
by near=> n; rewrite sume_ge0.
Unshelve. all: by end_near. Qed.

Lemma mu_ext0 : mu^* set0 = 0.
Proof.
apply/eqP; rewrite eq_le; apply/andP; split; last exact/mu_ext_ge0.
rewrite /mu_ext; apply: ereal_inf_lb; exists (fun=> set0); first by split.
by apply: lim_near_cst => //; near=> n => /=; rewrite big1.
Unshelve. all: by end_near. Qed.

Lemma mu_ext_sigma_subadditive : sigma_subadditive mu^*.
Proof.
move=> A; have [[i ioo]|] := pselect (exists i, mu^* (A i) = +oo).
  rewrite (eseries_pinfty _ _ ioo) ?leey// => n _.
  by rewrite -ltNye (lt_le_trans _ (mu_ext_ge0 _)).
rewrite -forallNE => Aoo.
suff add2e (e : {posnum R}) :
    mu^* (\bigcup_n A n) <= \sum_(i <oo) mu^* (A i) + e%:num%:E.
  by apply/lee_addgt0Pr => _/posnumP[].
rewrite (le_trans _ (epsilon_trick _ _ _))//; last first.
  by move=> n; exact: mu_ext_ge0.
pose P n (B : (set T)^nat) := measurable_cover (A n) B /\
  \sum_(k <oo) mu (B k) <= mu^* (A n) + (e%:num / (2 ^ n.+1)%:R)%:E.
have [G PG] : {G : ((set T)^nat)^nat & forall n, P n (G n)}.
  apply: (@choice _ _ P) => n; rewrite /P /mu_ext.
  set S := (X in ereal_inf X); move infS : (ereal_inf S) => iS.
  case: iS infS => [r Sr|Soo|Soo].
  - have en1 : (0 < e%:num / (2 ^ n.+1)%:R)%R by [].
    have /(lb_ereal_inf_adherent en1) : ereal_inf S \is a fin_num by rewrite Sr.
    move=> [x [B [mB AnB muBx] xS]].
    by exists B; split => //; rewrite muBx -Sr; exact/ltW.
  - by have := Aoo n; rewrite /mu^* Soo.
  - suff : lbound S 0 by move/lb_ereal_inf; rewrite Soo.
    by move=> /= _ [B [mB AnB] <-]; exact: nneseries_ge0.
have muG_ge0 x : 0 <= (mu \o uncurry G) x by exact: measure_ge0.
apply: (@le_trans _ _ (\esum_(i in setT) (mu \o uncurry G) i)).
  rewrite /mu_ext; apply: ereal_inf_lb => /=.
  have /card_esym/ppcard_eqP[f] := card_nat2.
  exists (uncurry G \o f).
    split => [i|]; first exact/measurable_uncurry/(PG (f i).1).1.1.
    apply: (@subset_trans _  (\bigcup_n \bigcup_k G n k)) => [t [i _]|].
      by move=> /(cover_subset (PG i).1) -[j _ ?]; exists i => //; exists j.
    move=> t [i _ [j _ Bijt]]; exists (f^-1%FUN (i, j)) => //=.
    by rewrite invK ?inE.
  rewrite -(esum_pred_image (mu \o uncurry G) _ xpredT) ?[fun=> _]set_true//.
  by rewrite image_eq.
rewrite (_ : esum _ _ = \sum_(i <oo) \sum_(j <oo ) mu (G i j)); last first.
  pose J : nat -> set (nat * nat) := fun i => [set (i, j) | j in setT].
  rewrite (_ : setT = \bigcup_k J k); last first.
    by rewrite predeqE => -[a b]; split => // _; exists a => //; exists b.
  rewrite esum_bigcupT /=; last 2 first.
    - apply/trivIsetP => i j _ _ ij.
      rewrite predeqE => -[n m] /=; split => //= -[] [_] _ [<-{n} _].
      by move=> [m' _] [] /esym/eqP; rewrite (negbTE ij).
    - by move=> /= [n m]; apply: measure_ge0; exact: (cover_measurable (PG n).1).
  rewrite -(image_id [set: nat]) -fun_true esum_pred_image//; last first.
    by move=> n _; exact: esum_ge0.
  apply: eq_eseriesr => /= j _.
  rewrite -(esum_pred_image (mu \o uncurry G) (pair j) predT)//=; last first.
    by move=> ? ? _ _; exact: (@can_inj _ _ _ snd).
  by congr esum; rewrite predeqE => -[a b]; split; move=> [i _ <-]; exists i.
apply: lee_lim.
- apply: is_cvg_nneseries => n _.
  by apply: nneseries_ge0 => m _; exact: (muG_ge0 (n, m)).
- by apply: is_cvg_nneseries => n _; apply: adde_ge0 => //; exact: mu_ext_ge0.
- by near=> n; apply: lee_sum => i _; exact: (PG i).2.
Unshelve. all: by end_near. Qed.

End outer_measure_construction.
Declare Scope measure_scope.
Delimit Scope measure_scope with mu.
Notation "mu ^*" := (mu_ext mu) : measure_scope.
Local Open Scope measure_scope.

Section outer_measure_of_content.
Context d (R : realType) (T : semiRingOfSetsType d).
Variable mu : {content set T -> \bar R}.

HB.instance Definition _ := isOuterMeasure.Build
  R T _ (@mu_ext0 _ _ _ _ (measure0 mu) (measure_ge0 mu))
      (mu_ext_ge0 (measure_ge0 mu))
      (le_mu_ext mu)
      (mu_ext_sigma_subadditive (measure_ge0 mu)).

End outer_measure_of_content.

Section g_salgebra_measure_unique_trace.
Context d (R : realType) (T : measurableType d).
Variables (G : set (set T)) (D : set T) (mD : measurable D).
Let H := [set X | G X /\ X `<=` D] (* "trace" of G wrt D *).
Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H) (HD : H D).
Variables m1 m2 : {measure set T -> \bar R}.
Hypotheses (m1m2 : forall A, H A -> m1 A = m2 A) (m1oo : (m1 D < +oo)%E).

Lemma g_salgebra_measure_unique_trace :
  (forall X, (<<s D, H >>) X -> X `<=` D) -> forall X, <<s D, H >> X ->
  m1 X = m2 X.
Proof.
move=> sDHD; set E := [set A | [/\ measurable A, m1 A = m2 A & A `<=` D] ].
have HE : H `<=` E.
  by move=> X HX; rewrite /E /=; split; [exact: Hm|exact: m1m2|case: HX].
have setDE : setD_closed E.
  move=> A B BA [mA m1m2A AD] [mB m1m2B BD]; split; first exact: measurableD.
  - rewrite measureD//; last first.
      by rewrite (le_lt_trans _ m1oo)//; apply: le_measure => // /[!inE].
    rewrite setIidr//= m1m2A m1m2B measureD// ?setIidr//.
    by rewrite (le_lt_trans _ m1oo)//= -m1m2A; apply: le_measure => // /[!inE].
  - by rewrite setDE; apply: subIset; left.
have ndE : ndseq_closed E.
  move=> A ndA EA; split; have mA n : measurable (A n) by have [] := EA n.
  - exact: bigcupT_measurable.
  - transitivity (lim (m1 \o A)).
      apply/esym/cvg_lim=>//.
      exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable.
    transitivity (lim (m2 \o A)).
      by congr (lim _); rewrite funeqE => n; have [] := EA n.
    apply/cvg_lim => //.
    exact/(nondecreasing_cvg_mu mA _ ndA)/bigcupT_measurable.
  - by apply: bigcup_sub => n; have [] := EA n.
have sDHE : <<s D, H >> `<=` E.
  by apply: monotone_class_subset => //; split => //; [move=> A []|exact/HE].
by move=> X /sDHE[].
Qed.

End g_salgebra_measure_unique_trace.

Section g_salgebra_measure_unique.
Context d (R : realType) (T : measurableType d).
Variable G : set (set T).
Hypothesis Gm : G `<=` measurable.
Variable g : (set T)^nat.
Hypotheses Gg : forall i, G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T -> \bar R}.

Lemma g_salgebra_measure_unique_cover :
  (forall n A, <<s G >> A -> m1 (g n `&` A) = m2 (g n `&` A)) ->
  forall A, <<s G >> A -> m1 A = m2 A.
Proof.
pose GT := [the ringOfSetsType _ of salgebraType G].
move=> sGm1m2; pose g' k := \bigcup_(i < k) g i.
have sGm := smallest_sub (@sigma_algebra_measurable _ T) Gm.
have Gg' i : <<s G >> (g' i).
  apply: (@fin_bigcup_measurable _ GT) => //.
  by move=> n _; apply: sub_sigma_algebra.
have sG'm1m2 n A : <<s G >> A -> m1 (g' n `&` A) = m2 (g' n `&` A).
  move=> sGA; rewrite setI_bigcupl bigcup_mkord.
  elim: n => [|n IHn] in A sGA *; rewrite (big_ord0, big_ord_recr) ?measure0//=.
  have sGgA i : <<s G >> (g i `&` A).
    by apply: (@measurableI _ GT) => //; exact: sub_sigma_algebra.
  apply: eq_measureU; rewrite ?sGm1m2 ?IHn//; last first.
  - by rewrite -big_distrl -setIA big_distrl/= IHn// setICA setIid.
  - exact/sGm.
  - by apply: bigsetU_measurable => i _; apply/sGm.
have g'_cover : \bigcup_k (g' k) = setT.
  by rewrite -subTset -g_cover => x [k _ gx]; exists k.+1 => //; exists k => /=.
have nd_g' : nondecreasing_seq g'.
  move=> m n lemn; rewrite subsetEset => x [k km gx]; exists k => //=.
  exact: leq_trans lemn.
move=> A gA.
have -> : A = \bigcup_n (g' n `&` A) by rewrite -setI_bigcupl g'_cover setTI.
transitivity (lim (fun n => m1 (g' n `&` A))).
  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
  - by move=> n; apply: measurableI; exact/sGm.
  - by apply: bigcupT_measurable => k; apply: measurableI; exact/sGm.
  - by move=> ? ? ?; apply/subsetPset; apply: setSI; exact/subsetPset/nd_g'.
transitivity (lim (fun n => m2 (g' n `&` A))).
  by congr (lim _); rewrite funeqE => x; apply: sG'm1m2 => //; exact/sGm.
apply/cvg_lim => //; apply: nondecreasing_cvg_mu.
- by move=> k; apply: measurableI => //; exact/sGm.
- by apply: bigcupT_measurable => k; apply: measurableI; exact/sGm.
- by move=> a b ab; apply/subsetPset; apply: setSI; exact/subsetPset/nd_g'.
Qed.

Hypothesis setIG : setI_closed G.
Hypothesis m1m2 : forall A, G A -> m1 A = m2 A.
Hypothesis m1goo : forall k, (m1 (g k) < +oo)%E.

Lemma g_salgebra_measure_unique : forall E, <<s G >> E -> m1 E = m2 E.
Proof.
pose G_ n := [set X | G X /\ X `<=` g n]. (* "trace" *)
have G_E n : G_ n = [set g n `&` C | C in G].
  rewrite eqEsubset; split.
    by move=> X [GX Xgn] /=; exists X => //; rewrite setIidr.
  by rewrite /G_ => X [Y GY <-{X}]; split; [exact: setIG|apply: subIset; left].
have gIsGE n : [set g n `&` A | A in <<s G >>] =
               <<s g n, preimage_class (g n) id G >>.
  rewrite sigma_algebra_preimage_classE eqEsubset; split.
    by move=> _ /= [Y sGY <-]; exists Y => //; rewrite preimage_id setIC.
  by move=> _ [Y mY <-] /=; exists Y => //; rewrite preimage_id setIC.
have preimg_gGE n : preimage_class (g n) id G = G_ n.
  rewrite eqEsubset; split => [_ [Y GY <-]|].
    by rewrite preimage_id G_E /=; exists Y => //; rewrite setIC.
  by move=> X [GX Xgn]; exists X => //; rewrite preimage_id setIidr.
apply: g_salgebra_measure_unique_cover => //.
move=> n A sGA; apply: (@g_salgebra_measure_unique_trace _ _ _ G (g n)) => //.
- exact: Gm.
- by move=> ? [? _]; exact/Gm.
- by move=> ? ? [? ?] [? ?]; split; [exact: setIG|apply: subIset; tauto].
- by split.
- by move=> ? [? ?]; exact: m1m2.
- move=> X; rewrite -/(G_ n) -preimg_gGE -gIsGE.
  by case=> B sGB <-{X}; apply: subIset; left.
- by rewrite -/(G_ n) -preimg_gGE -gIsGE; exists A.
Qed.

End g_salgebra_measure_unique.

Section measure_unique.
Context d (R : realType) (T : measurableType d).
Variables  (G : set (set T)) (g : (set T)^nat).
Hypotheses (mG : measurable = <<s G >>) (setIG : setI_closed G).
Hypothesis Gg : forall i, G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T -> \bar R}.
Hypothesis m1m2 : forall A, G A -> m1 A = m2 A.
Hypothesis m1goo : forall k, (m1 (g k) < +oo)%E.

Lemma measure_unique A : measurable A -> m1 A = m2 A.
Proof.
move=> mA; apply: (@g_salgebra_measure_unique _ _ _ G); rewrite -?mG//.
by rewrite mG; exact: sub_sigma_algebra.
Qed.

End measure_unique.
Arguments measure_unique {d R T} G g.

Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d)
    (mu : {measure set T -> \bar R}) X :
  measurable X -> mu^* X = mu X.
Proof.
move=> mX; apply/eqP; rewrite eq_le; apply/andP; split.
  apply: ereal_inf_lb; exists (fun n => if n is 0%N then X else set0).
    by split=> [[]// _|t Xt]; exists 0%N.
  apply/cvg_lim => //; rewrite -cvg_shiftS.
  rewrite (_ : [sequence _]_n = cst (mu X)); first exact: cvg_cst.
  by rewrite funeqE => n /=; rewrite big_nat_recl//= big1 ?adde0.
apply/lb_ereal_inf => x [A [mA XA] <-{x}].
have XUA : X = \bigcup_n (X `&` A n).
  rewrite predeqE => t; split => [Xt|[i _ []//]].
  by have [i _ Ait] := XA _ Xt; exists i.
apply: (@le_trans _ _ (\sum_(i <oo) mu (X `&` A i))).
  by rewrite measure_sigma_sub_additive//= -?XUA => // i; apply: measurableI.
apply: lee_lim; [exact: is_cvg_nneseries|exact: is_cvg_nneseries|].
by apply: nearW => n; apply: lee_sum => i  _; exact: measureIr.
Qed.

Section Rmu_ext.
Import SetRing.

Lemma Rmu_ext d (R : realType) (T : semiRingOfSetsType d)
    (mu : {content set T -> \bar R}) :
  (measure mu)^* = mu^*.
Proof.
apply/funeqP => /= X; rewrite /mu_ext/=; apply/eqP; rewrite eq_le.
rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lb//; last first.
  exists F; first by split=> // i; apply: sub_gen_smallest.
  by rewrite (eq_eseriesr (fun _ _ => RmuE _ (Fm _))).
pose K := [set: nat] `*`` fun i => decomp (F i).
have /ppcard_eqP[f] : (K #= [set: nat])%card.
  apply: cardMR_eq_nat => // i; split; last by apply/set0P; rewrite decompN0.
  by apply: finite_set_countable => //; exact: decomp_finite_set.
pose g i := (f^-1%FUN i).2; exists g; first split.
- move=> k; have [/= _ /mem_set] : K (f^-1%FUN k) by apply: funS.
  exact: decomp_measurable.
- move=> i /XS [k _]; rewrite -[F k]cover_decomp => -[D /= DFk Di].
  by exists (f (k, D)) => //; rewrite /g invK// inE.
rewrite !nneseries_esum//= /measure ?set_true.
transitivity (\esum_(i in setT) \sum_(X0 \in decomp (F i)) mu X0); last first.
  by apply: eq_esum => /= k _; rewrite fsbig_finite//; exact: decomp_finite_set.
rewrite -(eq_esum (fun _ _ => esum_fset _ _))//; last first.
  by move=> ? _; exact: decomp_finite_set.
rewrite esum_esum//= (reindex_esum K setT f) => //=.
by apply: eq_esum => i Ki; rewrite /g funK ?inE.
Qed.

End Rmu_ext.

Lemma measurable_Rmu_extE d (R : realType) (T : semiRingOfSetsType d)
    (mu : {measure set T -> \bar R}) X :
  d.-ring.-measurable X -> mu^* X = SetRing.measure mu X.
Proof. by move=> Xm/=; rewrite -Rmu_ext/= measurable_mu_extE. Qed.

Section measure_extension.
Context d (T : semiRingOfSetsType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Let Rmu := SetRing.measure mu.
Notation rT := (SetRing.type T).

Lemma sub_caratheodory :
  (d.-measurable).-sigma.-measurable `<=` mu^*.-cara.-measurable.
Proof.
suff: <<s d.-ring.-measurable >> `<=` mu^*.-cara.-measurable.
   by apply: subset_trans; apply: sub_smallest2r => //; exact: sub_smallest.
apply: smallest_sub.
  split => //; [by move=> X mX; rewrite setTD; exact: measurableC |
                by move=> u_ mu_; exact: bigcupT_measurable].
move=> A mA; apply le_caratheodory_measurable => // X.
apply lb_ereal_inf => _ [B [mB XB] <-].
rewrite -(eq_eseriesr (fun _ _ => SetRing.RmuE _ (mB _))) => //.
have RmB i : measurable (B i : set rT) by exact: sub_gen_smallest.
set BA := eseries (fun n => Rmu (B n `&` A)).
set BNA := eseries (fun n => Rmu (B n `&` ~` A)).
apply: (@le_trans _ _ (lim BA + lim BNA)); [apply: lee_add|].
  - rewrite (_ : BA = eseries (fun n => mu_ext mu (B n `&` A))); last first.
      rewrite funeqE => n; apply: eq_bigr => k _.
      by rewrite /= measurable_Rmu_extE //; exact: measurableI.
    apply: (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `&` A)))).
      by apply: le_mu_ext; rewrite -setI_bigcupl; exact: setISS.
    exact: outer_measure_sigma_subadditive.
  - rewrite (_ : BNA = eseries (fun n => mu_ext mu (B n `\` A))); last first.
      rewrite funeqE => n; apply: eq_bigr => k _.
      by rewrite /= measurable_Rmu_extE //; exact: measurableD.
    apply: (@le_trans _ _ (mu_ext mu (\bigcup_k (B k `\` A)))).
      by apply: le_mu_ext; rewrite -setI_bigcupl; exact: setISS.
    exact: outer_measure_sigma_subadditive.
have ? : cvg BNA by exact: is_cvg_nneseries.
have ? : cvg BA by exact: is_cvg_nneseries.
have ? : cvg (eseries (Rmu \o B)) by exact: is_cvg_nneseries.
have [def|] := boolP (lim BA +? lim BNA); last first.
  rewrite /adde_def negb_and !negbK=> /orP[/andP[BAoo BNAoo]|/andP[BAoo BNAoo]].
  - suff -> : lim (eseries (Rmu \o B)) = +oo by rewrite leey.
    apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/lee_lim => //.
    near=> n; apply: lee_sum => m _; apply: le_measure; rewrite /mkset; by
      [rewrite inE; exact: measurableI | rewrite inE | apply: subIset; left].
  - suff -> : lim (eseries (Rmu \o B)) = +oo by rewrite leey.
    apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/lee_lim => //.
    by near=> n; apply: lee_sum => m _; rewrite -setDE; apply: le_measure;
       rewrite /mkset ?inE//; apply: measurableD.
rewrite -limeD // (_ : (fun _ => _) =
    eseries (fun k => Rmu (B k `&` A) + Rmu (B k `&` ~` A))); last first.
  by rewrite funeqE => n; rewrite -big_split /=; exact: eq_bigr.
apply/lee_lim => //.
  by apply/is_cvg_nneseries => // n _; exact: adde_ge0.
near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2.
- apply: le_measure; rewrite /mkset ?inE//; [|by rewrite -setIUr setUCr setIT].
  by apply: measurableU; [exact:measurableI|rewrite -setDE; exact:measurableD].
- exact: measurableI.
- by rewrite -setDE; exact: measurableD.
- by apply: measurableU; [exact:measurableI|rewrite -setDE; exact:measurableD].
- by rewrite setIACA setICr setI0.
Unshelve. all: by end_near. Qed.

Let I := [the measurableType _ of salgebraType (@measurable _ T)].

Definition measure_extension : set I -> \bar R := mu^*.

Local Lemma measure_extension0 : measure_extension set0 = 0.
Proof. exact: mu_ext0. Qed.

Local Lemma measure_extension_ge0 (A : set I) : 0 <= measure_extension A.
Proof. exact: mu_ext_ge0. Qed.

Local Lemma measure_extension_semi_sigma_additive :
  semi_sigma_additive measure_extension.
Proof.
move=> F mF tF mUF; rewrite /measure_extension.
apply: caratheodory_measure_sigma_additive => //; last exact: sub_caratheodory.
by move=> i; exact: (sub_caratheodory (mF i)).
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ measure_extension
  measure_extension0 measure_extension_ge0
  measure_extension_semi_sigma_additive.

Lemma measure_extension_sigma_finite : @sigma_finite _ T _ setT mu ->
  @sigma_finite _ _ _ setT measure_extension.
Proof.
move=> -[S setTS mS]; exists S => //; move=> i; split.
  by have := (mS i).1; exact: sub_sigma_algebra.
by rewrite /measure_extension /= measurable_mu_extE //;
  [exact: (mS i).2 | exact: (mS i).1].
Qed.

Lemma measure_extension_unique : sigma_finite [set: T] mu ->
  (forall mu' : {measure set I -> \bar R},
    (forall X, d.-measurable X -> mu X = mu' X) ->
    (forall X, (d.-measurable).-sigma.-measurable X ->
      measure_extension X = mu' X)).
Proof.
move=> [F TF /all_and2[Fm muF]] mu' mu'mu X mX.
apply: (@measure_unique _ _ [the measurableType _ of I] d.-measurable F) => //.
- by move=> A B Am Bm; apply: measurableI.
- by move=> A Am; rewrite /= /measure_extension measurable_mu_extE// mu'mu.
- by move=> k; rewrite /= /measure_extension measurable_mu_extE.
Qed.

End measure_extension.

Lemma caratheodory_measurable_mu_ext d (R : realType) (T : measurableType d)
    (mu : {measure set T -> \bar R}) A :
  d.-measurable A -> mu^*.-cara.-measurable A.
Proof.
by move=> Am; apply: sub_caratheodory => //; apply: sub_sigma_algebra.
Qed.

Definition preimage_classes d1 d2
    (T1 : measurableType d1) (T2 : measurableType d2) (T : Type)
    (f1 : T -> T1) (f2 : T -> T2)  :=
  <<s preimage_class setT f1 measurable `|`
      preimage_class setT f2 measurable >>.

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

Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) =
                              preimage_class setT g (preimage_classes f1 f2).
Proof.
rewrite {1}/preimage_classes -sigma_algebra_preimage_classE; congr (<<s _ >>).
rewrite predeqE => C; split.
- move=> [[A mA <-{C}]|[A mA <-{C}]].
  + by exists (f1 @^-1` A) => //; left; exists A => //; rewrite setTI.
  + by exists (f2 @^-1` A) => //; right; exists A => //; rewrite setTI.
- move=> [A [[B mB <-{A} <-{C}]|[B mB <-{A} <-{C}]]].
  + by left; rewrite !setTI; exists B => //; rewrite setTI.
  + by right; rewrite !setTI; exists B => //; rewrite setTI.
Qed.

End product_lemma.

Definition measure_prod_display :
  (measure_display * measure_display) -> measure_display.
Proof. exact. Qed.

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

Lemma prod_salgebra_set0 : preimage_classes f1 f2 (set0 : set (T1 * T2)).
Proof. exact: sigma_algebra0. Qed.

Lemma prod_salgebra_setC A : preimage_classes f1 f2 A ->
  preimage_classes f1 f2 (~` A).
Proof. exact: sigma_algebraC. Qed.

Lemma prod_salgebra_bigcup (F : _^nat) : (forall i, preimage_classes f1 f2 (F i)) ->
  preimage_classes f1 f2 (\bigcup_i (F i)).
Proof. exact: sigma_algebra_bigcup. Qed.

HB.instance Definition prod_salgebra_mixin :=
  @isMeasurable.Build (measure_prod_display (d1, d2))
    (T1 * T2)%type (Pointed.class _) (preimage_classes f1 f2)
    (prod_salgebra_set0) (prod_salgebra_setC) (prod_salgebra_bigcup).

End product_salgebra_instance.
Notation "p .-prod" := (measure_prod_display p) : measure_display_scope.
Notation "p .-prod.-measurable" :=
  ((p.-prod).-measurable : set (set (_ * _))) :
    classical_set_scope.

Lemma measurableM d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
    (A : set T1) (B : set T2) :
  measurable A -> measurable B -> measurable (A `*` B).
Proof.
move=> mA mB.
have -> : A `*` B = (A `*` setT) `&` (setT `*` B) :> set (T1 * T2).
  by rewrite -{1}(setIT A) -{1}(setTI B) setMI.
rewrite setMT setTM; apply: measurableI.
- by apply: sub_sigma_algebra; left; exists A => //; rewrite setTI.
- by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI.
Qed.

Section product_salgebra_measurableType.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
Let M1 := @measurable _ T1.
Let M2 := @measurable _ T2.
Let M1xM2 := [set A `*` B | A in M1 & B in M2].

Lemma measurable_prod_measurableType :
  (d1, d2).-prod.-measurable = <<s M1xM2 >>.
Proof.
rewrite eqEsubset; split.
  apply: smallest_sub; first exact: smallest_sigma_algebra.
  rewrite subUset; split.
  - have /subset_trans : preimage_class setT fst M1 `<=` M1xM2.
      by move=> _ [X MX <-]; exists X=> //; exists setT; rewrite /M2 // setIC//.
    by apply; exact: sub_sigma_algebra.
  - have /subset_trans : preimage_class setT snd M2 `<=` M1xM2.
      by move=> _ [Y MY <-]; exists setT; rewrite /M1 //; exists Y.
    by apply; exact: sub_sigma_algebra.
apply: smallest_sub; first exact: smallest_sigma_algebra.
by move=> _ [A MA] [B MB] <-; apply: measurableM => //; exact: sub_sigma_algebra.
Qed.

End product_salgebra_measurableType.

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

(* NB: useful? *)
Lemma measurable_prod_g_measurableTypeR :
  @measurable _ [the measurableType _ of T1 * salgebraType C2 : Type]
  = <<s [set A `*` B | A in measurable & B in C2] >>.
Proof.
rewrite measurable_prod_measurableType //; congr (<<s _ >>).
rewrite predeqE => X; split=> [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}].
  by exists A => //; exists B => //; exact: setTC2.
by exists A => //; exists B => //; exact: sub_sigma_algebra.
Qed.

End product_salgebra_g_measurableTypeR.

Section product_salgebra_g_measurableType.
Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)).
Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2).

Lemma measurable_prod_g_measurableType :
  @measurable _ [the measurableType _ of salgebraType C1 * salgebraType C2 : Type]
  = <<s [set A `*` B | A in C1 & B in C2] >>.
Proof.
rewrite measurable_prod_measurableType //; congr (<<s _ >>).
rewrite predeqE => X; split=> [[A mA] [B mB] <-{X}|[A C1A] [B C2B] <-{X}].
  by exists A; [exact: setTC1|exists B => //; exact: setTC2].
by exists A; [exact: sub_sigma_algebra|exists B => //; exact: sub_sigma_algebra].
Qed.

End product_salgebra_g_measurableType.

Section prod_measurable_fun.
Context d d1 d2 (T : measurableType d) (T1 : measurableType d1)
        (T2 : measurableType d2).

Lemma prod_measurable_funP (h : T -> T1 * T2) : measurable_fun setT h <->
  measurable_fun setT (fst \o h) /\ measurable_fun setT (snd \o h).
Proof.
apply: (@iff_trans _ (preimage_classes (fst \o h) (snd \o h) `<=` measurable)).
- rewrite preimage_classes_comp; split=> [mf A [C HC <-]|f12]; first exact: mf.
  by move=> _ A mA; apply: f12; exists A.
- split => [h12|[mf1 mf2]].
    split => _ A mA; apply: h12; apply: sub_sigma_algebra;
    by [left; exists A|right; exists A].
  apply: smallest_sub; first exact: sigma_algebra_measurable.
  by rewrite subUset; split=> [|] A [C mC <-]; [exact: mf1|exact: mf2].
Qed.

Lemma measurable_fun_prod (f : T -> T1) (g : T -> T2) :
  measurable_fun setT f -> measurable_fun setT g ->
  measurable_fun setT (fun x => (f x, g x)).
Proof. by move=> mf mg; exact/prod_measurable_funP. Qed.

End prod_measurable_fun.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_fun_prod`")]
Notation measurable_fun_pair := measurable_fun_prod (only parsing).

Section prod_measurable_proj.
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).

Lemma measurable_fst : measurable_fun [set: T1 * T2] fst.
Proof.
by have /prod_measurable_funP[] :=
  @measurable_id _ [the measurableType _ of (T1 * T2)%type] setT.
Qed.
#[local] Hint Resolve measurable_fst : core.

Lemma measurable_snd : measurable_fun [set: T1 * T2] snd.
Proof.
by have /prod_measurable_funP[] :=
  @measurable_id _ [the measurableType _ of (T1 * T2)%type] setT.
Qed.
#[local] Hint Resolve measurable_snd : core.

Lemma measurable_swap : measurable_fun [set: _] (@swap T1 T2).
Proof. exact: measurable_fun_prod. Qed.

End prod_measurable_proj.
Arguments measurable_fst {d1 d2 T1 T2}.
Arguments measurable_snd {d1 d2 T1 T2}.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_fst`")]
Notation measurable_fun_fst := measurable_fst (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_snd`")]
Notation measurable_fun_snd := measurable_snd (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_swap`")]
Notation measurable_fun_swap := measurable_swap (only parsing).
#[global] Hint Extern 0 (measurable_fun _ fst) =>
  solve [apply: measurable_fst] : core.
#[global] Hint Extern 0 (measurable_fun _ snd) =>
  solve [apply: measurable_snd] : core.

Lemma measurable_fun_if_pair d d' (X : measurableType d)
    (Y : measurableType d') (x y : X -> Y) :
  measurable_fun setT x -> measurable_fun setT y ->
  measurable_fun setT (fun tb => if tb.2 then x tb.1 else y tb.1).
Proof.
by move=> mx my; apply: measurable_fun_ifT => //=; exact: measurableT_comp.
Qed.

Section partial_measurable_fun.
Context d d1 d2 (T : measurableType d) (T1 : measurableType d1)
  (T2 : measurableType d2).
Variable f : T1 * T2 -> T.

Lemma measurable_pair1 (x : T1) : measurable_fun [set: T2] (pair x).
Proof.
have m1pairx : measurable_fun [set: T2] (fst \o pair x) by exact/measurable_cst.
have m2pairx : measurable_fun [set: T2] (snd \o pair x) by exact/measurable_id.
exact/(prod_measurable_funP _).
Qed.

Lemma measurable_pair2 (y : T2) : measurable_fun [set: T1] (pair^~ y).
Proof.
have m1pairy : measurable_fun [set: T1] (fst \o pair^~y) by exact/measurable_id.
have m2pairy : measurable_fun [set: T1] (snd \o pair^~y) by exact/measurable_cst.
exact/(prod_measurable_funP _).
Qed.

End partial_measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ (pair _)) =>
  solve [apply: measurable_pair1] : core.
#[global] Hint Extern 0 (measurable_fun _ (pair^~ _)) =>
  solve [apply: measurable_pair2] : core.

Section absolute_continuity.
Context d (T : measurableType d) (R : realType).
Implicit Types m : set T -> \bar R.

Definition measure_dominates m1 m2 :=
  forall A, measurable A -> m2 A = 0 -> m1 A = 0.

Local Notation "m1 `<< m2" := (measure_dominates m1 m2).

Lemma measure_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3.
Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed.

End absolute_continuity.
Notation "m1 `<< m2" := (measure_dominates m1 m2).

Section essential_supremum.
Context d {T : measurableType d} {R : realType}.
Variable mu : {measure set T -> \bar R}.
Implicit Types f : T -> R.

Definition ess_sup f :=
  ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]).

Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R ->
  0 <= ess_sup f.
Proof.
move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt.
apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//.
by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)).
Qed.

End essential_supremum.