Library mathcomp.analysis.measure

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

Measure Theory
This files provides a formalization of the basics of measure theory. This includes the formalization of mathematical structures for measure theory and of measures, as well as standard theorems such as the Boole inequality, Caratheodory's theorem, the Hahn extension, etc.
Main references:
  • Daniel Li, Intégration et applications, 2016
  • Achim Klenke, Probability Theory 2nd edition, 2014
    setI_closed G == the set of sets G is closed under finite intersection setU_closed G == the set of sets G is closed under finite union setC_closed G == the set of sets G is closed under complement setD_closed G == the set of sets G is closed under difference ndseq_closed G == the set of sets G is closed under non-decreasing countable union trivIset_closed G == the set of sets G is closed under pairwise-disjoint countable union
    setring G == the set of sets G contains the empty set, is closed by union, and difference r G := smallest setring G sigma_algebra D G == the set of sets G forms a sigma algebra on D s D, G == sigma-algebra generated by G on D := smallest (sigma_algebra D) G s G := s setT, G monotone_class D G == G is a monotone class of subsets of D m D, G == monotone class generated by G on D m G := m setT, G dynkin G == G is a set of sets that form a Dynkin (or a lambda) system d G == Dynkin system generated by G, i.e., smallest dynkin G

Mathematical structures for measure theory:

semiRingOfSetsType == the type of semirings of sets; the carrier is a set of sets A such that "measurable A" holds; "measurable A" is printed as "d.-measurable A" where d is a "display parameter" whose purpose is to distinguish different measurable's within the same context ringOfSetsType == the type of rings of sets r G is equipped with a canonical structure of ring of sets G.-ring.-measurable A == A is measurable for the ring of sets r G algebraOfSetsType == the type of algebras of sets measurableType == the type of sigma-algebras s G is equipped with a canonical structure of measurableType G.-sigma.-measurable A == A is measurable for the sigma-algebra s G
discrete_measurable == the measurableType corresponding to [set: set nat] salgebraType G == the measurableType corresponding to s G
measurable_fun D f == the function f with domain D is measurable preimage_class D f G == class of the preimages by f of sets in G image_class D f G == class of the sets with a preimage by f in G

Measures:

{additive_measure set T -> \bar R} == type of a function over sets of elements of type T where R is expected to be a numFieldType such that this function maps set0 to 0, is non-negative over measurable sets, and is semi-additive isAdditiveMeasure == corresponding mixin AdditiveMeasure == corresponding structure {measure set T -> \bar R} == type of a function over sets of elements of type T where R is expected to be a numFieldType such that this function maps set0 to 0, is non-negative over measurable sets and is semi-sigma-additive isMeasure0 == mixin that extends an additive measure to a measure with the proof that it is semi_sigma_additive isMeasure == factory corresponding to the type of measures Measure == structure corresponding to measures
pushforward f m == pushforward/image measure of m by f \d_a == Dirac measure msum mu n == the measure corresponding to the sum of the measures mu_0, ..., mu{n-1} @mzero T R == the zero measure measure_add m1 m2 == the measure corresponding to the sum of the measures m1 and m2 mscale r m == the measure of corresponding to fun A => r * m A where r has type {nonneg R} mseries mu n == the measure corresponding to the sum of the measures mu_n, mu{n+1}, ... mrestr mu mD == restriction of the measure mu to a set D; mD is a proof that D is measurable counting T R == counting measure
sigma_finite A f == the measure f is sigma-finite on A : set T with T : ringOfSetsType. mu.-negligible A == A is mu negligible {ae mu, forall x, P x} == P holds almost everywhere for the measure mu
{outer_measure set T -> \bar R} == type of an outer measure over sets of elements of type T where R is expected to be a numFieldType isOuterMeasure == corresponding mixin OuterMeasure == corresponding structure mu.-measurable A == A is Caratheodory measurable for the outer measure mu, i.e., forall B, mu A = mu (A `&` B) + mu (A `&` ~` B) measure_is_complete mu == the measure mu is complete

Caratheodory theorem (from an outer measure to a measure):

caratheodory_type mu := T, where mu : {outer_measure set T -> \bar R} it is a canonical mesurableType copy of T the restriction of the outer measure mu to the sigma algebra of Caratheodory measurable sets is a measure Remark: sets that are negligible for this measure are Caratheodory measurable

Caratheodory theorem (from a premeasure to an outer measure):

measurable_cover X == the set of sequences F such that
  • forall k, F k is measurable
  • X `<=` \bigcup_k (F k)
mu^* == extension of the measure mu over a semiring of sets; it is an outer measure, declared as; we have the notation [the outer_measure of mu^* ])

Hahn Extension:

Hahn_ext mu == extension of the additive measure 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

Set Implicit Arguments.
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 "{ 'additive_measure' fUV }"
  (at level 0, format "{ 'additive_measure' fUV }").
Reserved Notation "[ 'additive_measure' 'of' f 'as' g ]"
  (at level 0, format "[ 'additive_measure' 'of' f 'as' g ]").
Reserved Notation "[ 'additive_measure' 'of' f ]"
  (at level 0, format "[ 'additive_measure' 'of' f ]").
Reserved Notation "{ 'measure' fUV }"
  (at level 0, format "{ 'measure' fUV }").
Reserved Notation "[ 'measure' 'of' f 'as' g ]"
  (at level 0, format "[ 'measure' 'of' f 'as' g ]").
Reserved Notation "[ 'measure' 'of' f ]"
  (at level 0, format "[ 'measure' 'of' f ]").
Reserved Notation "{ 'outer_measure' fUV }"
  (at level 0, format "{ 'outer_measure' fUV }").
Reserved Notation "[ 'outer_measure' 'of' f 'as' g ]"
  (at level 0, format "[ 'outer_measure' 'of' f 'as' g ]").
Reserved Notation "[ 'outer_measure' 'of' f ]"
  (at level 0, format "[ 'outer_measure' 'of' f ]").
Reserved Notation "p .-prod" (at level 1, format "p .-prod").
Reserved Notation "p .-prod.-measurable"
 (at level 2, format "p .-prod.-measurable").

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

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

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

Definition fin_bigcap_closed :=
    ∀ I (D : set I) A_, finite_set D → (∀ i, D i → G (A_ i)) →
  G (\bigcap_(i in D) (A_ i)).

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

Definition fin_bigcup_closed :=
    ∀ I (D : set I) A_, finite_set D → (∀ i, D i → G (A_ i)) →
  G (\bigcup_(i in D) (A_ i)).

Definition semi_setD_closed := ∀ A B, G A → G B → ∃ D,
  [/\ finite_set D, D `<=` G, A `\` B = \bigcup_(X in D) X & trivIset D id].

Definition ndseq_closed :=
 ∀ F, nondecreasing_seq F → (∀ i, G (F i)) → G (\bigcup_i (F i)).

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

Definition fin_trivIset_closed :=
  ∀ I (D : set I) (F : I → set T), finite_set D → trivIset D F →
   (∀ 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, (∀ A, G A → G (D `\` A)) &
     (∀ A : (set T)^nat, (∀ n, G (A n)) → G (\bigcup_k A k))].

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

Definition monotone_class :=
  [/\ ∀ 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.

Lemma finN0_bigcap_closedP T (G : set (set T)) :
  setI_closed G ↔ finN0_bigcap_closed G.

Lemma sedDI_closedP T (G : set (set T)) :
  setDI_closed G ↔ (setI_closed G ∧ setD_closed G).

Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T)
    (F : I → set (set T)) (J : set I) :
  (∀ n, J n → sigma_algebra D (F n)) →
  sigma_algebra D (\bigcap_(i in J) F i).

Lemma sigma_algebraP T U (C : set (set T)) :
  (∀ X, C X → X `<=` U) →
  sigma_algebra U C ↔
  [/\ C U, setD_closed C, ndseq_closed C & setI_closed C].

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 >>.
Hint Resolve smallest_sigma_algebra : core.

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

Lemma sigma_algebra_id : sigma_algebra D G → <<s D, G >> = G.

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

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

Lemma sigma_algebraCD : ∀ A, <<s D, G >> A → <<s D, G >> (D `\` A).

Lemma sigma_algebra_bigcup (A : (set T)^nat) :
  (∀ i, <<s D, G >> (A i)) → <<s D, G >> (\bigcup_i (A i)).

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 >>.
Hint Resolve smallest_setring : core.

Lemma sub_setring2 M : M `<=` G → <<r M >> `<=` <<r G >>.

Lemma setring_id : setring G → <<r G >> = G.

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

Lemma setring0 : <<r G >> set0.

Lemma setringDI : setDI_closed <<r G>>.

Lemma setringU : setU_closed <<r G>>.

Lemma setring_fin_bigcup : fin_bigcup_closed <<r G>>.

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

Lemma monotone_class_g_salgebra T (G : set (set T)) (D : set T) :
  (∀ X, <<s D, G >> X → X `<=` D) → G D →
  monotone_class D (<<s D, G >>).

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 : (∀ X, <<s D, G >> X → X `<=` D) →
  (∀ E, monotone_class D E → G `<=` E → H `<=` E) →
  H = <<s D, G >>.

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 : (∀ X, (<<s D, G >>) X → X `<=` D) →
  <<s D, G >> `<=` H.

End monotone_class_subset.

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

Lemma dynkinT G : dynkin G → G setT.

Lemma dynkinC G : dynkin G → setC_closed G.

Lemma dynkinU G : dynkin G → (∀ F : (set T)^nat, trivIset setT F →
  (∀ n, G (F n)) → G (\bigcup_k F k)).

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.

Lemma dynkin_g_dynkin G : dynkin (<<d G >>).

Lemma sigma_algebra_dynkin G : sigma_algebra setT G → dynkin G.

Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G → setI_closed G →
  (∀ n, G (F n)) → ∀ n, G (\big[setI/setT]_(i < n) F i).

Lemma dynkin_setI_sigma_algebra G : dynkin G → setI_closed G →
  sigma_algebra setT G.

Lemma setI_closed_gdynkin_salgebra G : setI_closed G → <<d G >> = <<s G >>.

End dynkin_lemmas.


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

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


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

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


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

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


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

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


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

Lemma mI : setI_closed measurable.

Lemma mD : semi_setD_closed measurable.






Lemma mD : setDI_closed measurable.


Lemma measurableT : measurable (@setT T).





Obligation Tactic := idtac.

Lemma mU : setU_closed measurable.

Lemma mC : setC_closed measurable.




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

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

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

Lemma fin_bigcup_measurable I (D : set I) (F : I → set T) :
    finite_set D →
    (∀ i, D i → measurable (F i)) →
  measurable (\bigcup_(i in D) F i).

Lemma measurableD : setDI_closed (@measurable d T).

End ringofsets_lemmas.

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

Lemma measurableC A : measurable A → measurable (~` A).

Lemma bigsetI_measurable I r (P : pred I) (F : I → set T) :
  (∀ i, P i → measurable (F i)) →
  measurable (\big[setI/setT]_(i <- r | P i) F i).

Lemma fin_bigcap_measurable I (D : set I) (F : I → set T) :
    finite_set D →
    (∀ i, D i → measurable (F i)) →
  measurable (\bigcap_(i in D) F i).

End algebraofsets_lemmas.

Section measurable_lemmas.
Variables (d : measure_display) (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).

Lemma bigcup_measurable F P :
  (∀ k, P k → measurable (F k)) → measurable (\bigcup_(i in P) F i).

Lemma bigcap_measurable F P :
  (∀ k, P k → measurable (F k)) → measurable (\bigcap_(i in P) F i).

Lemma bigcapT_measurable F : (∀ i, measurable (F i)) →
  measurable (\bigcap_i (F i)).

End measurable_lemmas.

Lemma bigcupT_measurable_rat (d : measure_display) (T : measurableType d)
    (F : rat → set T) :
  (∀ i, measurable (F i)) → measurable (\bigcup_i F i).

Section discrete_measurable.
Variable T : pointedType.

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

Let discrete_measurable0 : discrete_measurable set0.

Let discrete_measurableC X :
  discrete_measurable X → discrete_measurable (~` X).

Let discrete_measurableU (F : (set nat)^nat) :
  (∀ i, discrete_measurable (F i)) →
  discrete_measurable (\bigcup_i F i).


End discrete_measurable.

Definition sigma_display {T} : set (set T) → measure_display.

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

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

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.

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

Section measurable_fun.
Variables (d1 d2 d3 : measure_display).
Variables (T1 : measurableType d1).
Variables (T2 : measurableType d2).
Variables (T3 : measurableType d3).

Lemma measurable_fun_id (D : set T1) : measurable_fun D id.

Lemma measurable_fun_comp (f : T2 → T3) E (g : T1 → T2) :
  measurable_fun setT f → measurable_fun E g → measurable_fun E (f \o g).

Lemma eq_measurable_fun (D : set T1) (f g : T1 → T2) :
  {in D, f =1 g} → measurable_fun D f → measurable_fun D g.

Lemma measurable_fun_cst (D : set T1) (r : T2) :
  measurable_fun D (cst r : T1 → _).

Lemma measurable_funU (D E : set T1) (f : T1 → T2) :
  measurable D → measurable E →
  measurable_fun (D `|` E) f ↔ measurable_fun D f ∧ measurable_fun E f.

Lemma measurable_funS (E D : set T1) (f : T1 → T2) :
     measurable E → D `<=` E → measurable_fun E f →
  measurable_fun D f.

Lemma measurable_fun_ext (D : set T1) (f g : T1 → T2) :
  {in D, f =1 g} → measurable_fun D f → measurable_fun D g.

Lemma measurable_restrict D E (f : T1 → T2) :
  measurable D → measurable E → D `<=` E →
  measurable_fun D f ↔ measurable_fun E (f \_ D).

End measurable_fun.
Arguments measurable_fun_ext {d1 d2 T1 T2 D} f {g}.

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.

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

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

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

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.

End measurability.

Local Open Scope ereal_scope.

Section additivity.
Variables (d : measure_display) (R : numFieldType)
          (T : semiRingOfSetsType d) (mu : set T → \bar R).

Definition semi_additive2 := ∀ A B, measurable A → measurable B →
  measurable (A `|` B) →
  A `&` B = set0 → mu (A `|` B) = mu A + mu B.

Definition semi_additive := ∀ F n,
 (∀ 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 :=
  ∀ F, (∀ 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 := ∀ A B, measurable A → measurable B →
  A `&` B = set0 → mu (A `|` B) = mu A + mu B.

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

Definition sigma_additive :=
  ∀ F, (∀ 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 := ∀ (A : set T) (F : nat → set T) n,
 (∀ 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 := ∀ (A : set T) (F : nat → set T),
 (∀ n, measurable (F n)) → measurable A →
  A `<=` \bigcup_n F n →
  mu A ≤ \sum_(n <oo) mu (F n).

Definition sigma_finite (A : set T) (mu : set T → \bar R) :=
  exists2 F : (set T)^nat, A = \bigcup_(i : nat) F i &
      ∀ i, measurable (F i) ∧ mu (F i) < +oo.

Lemma semi_additiveW : mu set0 = 0 → semi_additive → semi_additive2.

End additivity.

Section ring_additivity.
Variables (d : measure_display) (R : numFieldType)
          (T : ringOfSetsType d) (mu : set T → \bar R).

Lemma semi_additiveE : semi_additive mu = additive mu.

Lemma semi_additive2E : semi_additive2 mu = additive2 mu.

Lemma additive2P : mu set0 = 0 → semi_additive mu ↔ additive2 mu.

End ring_additivity.

Lemma semi_sigma_additive_is_additive d
  (R : realFieldType (*TODO: numFieldType if possible?*))
  (X : semiRingOfSetsType d) (mu : set X → \bar R) :
  mu set0 = 0 → semi_sigma_additive mu → semi_additive mu.

Lemma semi_sigma_additiveE
  (R : numFieldType) d (X : measurableType d) (mu : set X → \bar R) :
  semi_sigma_additive mu = sigma_additive mu.

Lemma sigma_additive_is_additive
  (R : realFieldType) d (X : measurableType d) (mu : set X → \bar R) :
  mu set0 = 0 → sigma_additive mu → additive mu.



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

Arguments measure_ge0 {d R T} _.

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

Variable mu : {additive_measure set T → \bar R}.

Lemma additive_measure_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).

Canonical additive_measure_snum S :=
  Signed.mk (additive_measure_snum_subproof S).

End additive_measure_signed.

Section additive_measure_on_semiring_of_sets.
Variables (d : measure_display) (R : numFieldType) (T : semiRingOfSetsType d)
  (mu : {additive_measure set T → \bar R}).

Lemma measure0 : mu set0 = 0.

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) :
  (∀ (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).

Lemma measure_semi_additive_ord_I (F : nat → set T) (n : nat) :
  (∀ 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).

Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
    finite_set D →
    trivIset D F →
    (∀ 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).

Lemma measure_semi_additive2 : semi_additive2 mu.
Hint Resolve measure_semi_additive2 : core.

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

#[global] Hint Extern 0
  (is_true (0 ≤ (_ : {additive_measure set _ → \bar _}) _)%E) ⇒
  solve [apply: measure_ge0] : core.

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

Section additive_measure_on_ring_of_sets.
Variables (d : measure_display) (R : realFieldType)(T : ringOfSetsType d)
  (mu : {additive_measure set T → \bar R}).

Lemma measureU : additive2 mu.

Lemma measure_bigsetU : additive mu.

Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
    finite_set D →
    trivIset D F →
    (∀ i, D i → measurable (F i)) →
  mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).

Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n → set T) :
  (∀ 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.

Lemma measure_bigsetU_ord n (P : {pred 'I_n}) (F : 'I_n → set T) :
  (∀ 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.

Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I → set T) :
  (∀ 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.

End additive_measure_on_ring_of_sets.

#[global]
Hint Resolve measureU measure_bigsetU : core.


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

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

Section measure_signed.
Variables (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).

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

End measure_signed.



Let semi_additive_mu : semi_additive mu.


Lemma eq_measure (d : measure_display) (T : measurableType d) (R : realType)
  (m1 m2 : {measure set T → \bar R}) :
  (m1 = m2 :> (set T → \bar R)) → m1 = m2.

Section measure_lemmas.
Variables (d : measure_display) (R : realFieldType) (T : semiRingOfSetsType d).

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

Lemma measure_semi_bigcup A : (∀ i : nat, measurable (A i)) →
    trivIset setT A → measurable (\bigcup_n A n) →
  mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).

End measure_lemmas.

Section measure_lemmas.
Variables (d : measure_display) (R : realFieldType) (T : measurableType d).
Variable mu : {measure set T → \bar R}.

Lemma measure_sigma_additive : sigma_additive mu.

Lemma measure_bigcup A : (∀ i : nat, measurable (A i)) →
  trivIset setT A →
  mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).

End measure_lemmas.
Arguments measure_bigcup {d R T} mu A.

#[global] Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: measure0] : core.
#[global] Hint Extern 0 (sigma_additive _) ⇒
  solve [apply: measure_sigma_additive] : core.
#[global] Hint Extern 0 (is_true (0 ≤ _)) ⇒ solve [apply: measure_ge0] : core.

Section pushforward_measure.
Local Open Scope ereal_scope.
Variables (d d' : measure_display).
Variables (T1 : measurableType d) (T2 : measurableType d') (f : T1 → T2).
Hypothesis mf : measurable_fun setT f.
Variables (R : realFieldType) (m : {measure set T1 → \bar R}).

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

Let pushforward0 : pushforward set0 = 0.

Let pushforward_ge0 A : 0 ≤ pushforward A.

Let pushforward_sigma_additive : semi_sigma_additive pushforward.


End pushforward_measure.

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

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

Let dirac0 : dirac set0 = 0.

Let dirac_ge0 B : 0 ≤ dirac B.

Let dirac_sigma_additive : semi_sigma_additive dirac.


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

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

Lemma diracE d (T : measurableType d) (R : realFieldType) a (A : set T) :
  \d_a A = (a \in A)%:R%:E :> \bar R.

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

Lemma finite_card_dirac (A : set T) : finite_set A →
  \esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.

Lemma infinite_card_dirac (A : set T) : infinite_set A →
  \esum_(i in A) \d_ i A = +oo :> \bar R.

End dirac_lemmas.

Section measure_sum.
Local Open Scope ereal_scope.
Variables (d : measure_display) (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.

Let msum_ge0 B : 0 ≤ msum B.

Let msum_sigma_additive : semi_sigma_additive msum.


End measure_sum.
Arguments msum {d T R}.

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

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

Let mzero0 : mzero set0 = 0.

Let mzero_ge0 B : 0 ≤ mzero B.

Let mzero_sigma_additive : semi_sigma_additive mzero.


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.

Section measure_add.
Local Open Scope ereal_scope.
Variables (d : measure_display) (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.

End measure_add.

Section measure_scale.
Local Open Scope ereal_scope.
Variables (d : measure_display) (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.

Let mscale_ge0 B : 0 ≤ mscale B.

Let mscale_sigma_additive : semi_sigma_additive mscale.


End measure_scale.
Arguments mscale {d T R}.

Section measure_series.
Local Open Scope ereal_scope.
Variables (d : measure_display) (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.

Let mseries_ge0 B : 0 ≤ mseries B.

Let mseries_sigma_additive : semi_sigma_additive mseries.


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.
Variables (d : measure_display) (T : measurableType d) (R : realFieldType).
Variables (mu : {measure set T → \bar R}) (D : set T) (mD : measurable D).


Let restr0 : restr set0 = 0%E.

Let restr_ge0 (A : set _) : (0 ≤ restr A)%E.

Let restr_sigma_additive : semi_sigma_additive restr.


End measure_restr.

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

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

Let counting0 : counting set0 = 0.

Let counting_ge0 (A : set _) : 0 ≤ counting A.

Let counting_sigma_additive : semi_sigma_additive counting.


End measure_count.

Lemma sigma_finite_counting (R : realType) :
  sigma_finite [set: nat] (counting R).

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

Section covering.
Context {T : Type}.
Implicit Type (C : ∀ I, set (set I)).
Implicit Type (P : ∀ I, set I → set (I → set T)).

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

Lemma covered_bySr C P P' : (∀ I D A, P I D A → P' I D A) →
  covered_by C P `<=` covered_by C P'.

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

Lemma covered_by_finite P :
    (∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
    (∀ (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 | ∃ n A, [/\ P nat `I_n A & X = \bigcup_(i in `I_n) A i]].

Lemma covered_by_countable P :
    (∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
    (∀ (I : pointedType) (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 | ∃ A, [/\ P nat [set: nat] A & X = \bigcup_i A i]].

End covering.

Module SetRing.
Definition type (T : Type) := T.
Definition display : measure_display → measure_display.

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



Lemma ring_measurableE : d.-ring.-measurable = measurable_fin_trivIset.

Lemma ring_fsets (A : set rT) : measurable A → ∃ B : set (set T),
  [/\ finite_set B,
      (∀ X, B X → X !=set0),
      trivIset B id,
      (∀ X : set T, X \in B → measurable X) &
      A = \bigcup_(X in B) X].

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_fsets mA)) else
  [set A].

Lemma decomp_finite_set (A : set rT) : finite_set (decomp A).

Lemma decomp_triv (A : set rT) : trivIset (decomp A) id.
Hint Resolve decomp_triv : core.

Lemma all_decomp_neq0 (A : set rT) :
  A !=set0 → (∀ X, decomp A X → X !=set0).

Lemma decomp_neq0 (A : set rT) X : A !=set0 → X \in decomp A → X !=set0.

Lemma decomp_measurable (A : set rT) (X : set T) :
  measurable A → X \in decomp A → measurable X.

Lemma cover_decomp (A : set rT) : \bigcup_(X in decomp A) X = A.

Lemma decomp_sub (A : set rT) (X : set T) : X \in decomp A → X `<=` A.

Lemma decomp_set0 : decomp set0 = [set set0].

Lemma decompN0 (A : set rT) : decomp A != set0.

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

Section additive_measure.
Context {R : realFieldType} (mu : {additive_measure set T → \bar R}).
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 → (∀ i, i \in D → measurable (F i)) →
  Rmu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i).

Lemma RmuE (A : set T) : measurable A → Rmu A = mu A.

Let Rmu0 : Rmu set0 = 0.

Lemma Rmu_ge0 A : Rmu A ≥ 0.

Lemma Rmu_additive : semi_additive Rmu.

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

End additive_measure.

End SetRing.
Module Exports.
Canonical ring_eqType.
Canonical ring_choiceType.
Canonical ring_ptType.
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 : {additive_measure set T → \bar R}) :
  {in measurable &, {homo mu : A B / A `<=` B >-> (A ≤ B)%E}}.

Lemma measure_le0 d (T : semiRingOfSetsType d) (R : realFieldType)
  (mu : {additive_measure set T → \bar R}) (A : set T) :
  (mu A ≤ 0)%E = (mu A == 0)%E.

Section more_content_semiring_lemmas.
Variables (d : measure_display) (R : realFieldType) (T : semiRingOfSetsType d).
Variable mu : {additive_measure set T → \bar R}.

Lemma content_sub_additive : sub_additive mu.

Lemma content_sub_fsum (I : choiceType) D (A : set T) (A_ : I → set T) :
  finite_set D →
  (∀ i, D i → measurable (A_ i)) →
  measurable A →
  A `<=` \bigcup_(i in D) A_ i → mu A ≤ \sum_(i \in D) mu (A_ i).

(* (* 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 := \bigsetU/set0_(i < n) A i. 
 set C := \bigsetU/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 -Bbigcup_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.
Variables (d : measure_display) (R : realType) (T : ringOfSetsType d).
Variable mu : {additive_measure set T → \bar R}.

Lemma content_ring_sup_sigma_additive (A : nat → set T) :
  (∀ i, measurable (A i)) → measurable (\bigcup_i A i) →
  trivIset [set: nat] A → \sum_(i <oo) mu (A i) ≤ mu (\bigcup_i A i).

Lemma content_ring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive mu.

End content_ring_lemmas.

Section ring_sigma_sub_additive_content.
Context d (R : realType) (T : semiRingOfSetsType d)
        (mu : {additive_measure set T → \bar R}).
Import SetRing.

Lemma ring_sigma_sub_additive : sigma_sub_additive mu → sigma_sub_additive Rmu.

Lemma ring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive Rmu.

End ring_sigma_sub_additive_content.

Section more_premeasure_ring_lemmas.
Variables (d : measure_display) (R : realType) (T : semiRingOfSetsType d).
Variable mu : {measure set T → \bar R}.
Import SetRing.

Lemma measure_sigma_sub_additive : sigma_sub_additive mu.

End more_premeasure_ring_lemmas.

Section ring_sigma_additive_measure.
Context d (R : realType) (T : semiRingOfSetsType d)
        (mu : {measure set T → \bar R}).
Import SetRing.

Let ring_sigma_additive_measure : semi_sigma_additive Rmu.


End ring_sigma_additive_measure.

Lemma measureIl d (R : realFieldType) (T : semiRingOfSetsType d)
    (mu : {additive_measure set T → \bar R}) (A B : set T) :
  measurable A → measurable B → (mu (A `&` B) ≤ mu A)%E.

Lemma measureIr d (R : realFieldType) (T : semiRingOfSetsType d)
    (mu : {additive_measure set T → \bar R}) (A B : set T) :
  measurable A → measurable B → (mu (A `&` B) ≤ mu B)%E.

Lemma subset_measure0 d (T : semiRingOfSetsType d) (R : realType)
  (mu : {additive_measure set T → \bar R}) (A B : set T) :
  measurable A → measurable B → A `<=` B →
  mu B = 0%E → mu A = 0%E.

Section measureD.
Variables (d : measure_display) (R : realFieldType) (T : ringOfSetsType d).
Variable mu : {measure set T → \bar R}.

Lemma measureDI A B : measurable A → measurable B →
  mu A = mu (A `\` B) + mu (A `&` B).

Lemma measureD A B : measurable A → measurable B →
  mu A < +oo → mu (A `\` B) = mu A - mu (A `&` B).

End measureD.

Lemma measureUfinr d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
   (mu : {measure set T → \bar R}):
    measurable A → measurable B → (mu B < +oo)%E →
  mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.

Lemma measureUfinl d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
   (mu : {measure set T → \bar R}):
    measurable A → measurable B → (mu A < +oo)%E →
  mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.

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

Lemma null_set_setU d (R : realFieldType) (T : ringOfSetsType d)
  (mu : {measure set T → \bar R}) (A B : set T) :
  measurable A → measurable B → mu A = 0%E → mu B = 0%E → mu (A `|` B) = 0%E.

Lemma cvg_mu_inc d (R : realFieldType) (T : ringOfSetsType d)
  (mu : {measure set T → \bar R}) (F : (set T) ^nat) :
  (∀ i, measurable (F i)) → measurable (\bigcup_n F n) →
  nondecreasing_seq F →
  mu \o F --> mu (\bigcup_n F n).

Section boole_inequality.
Variables (d : measure_display) (R : realFieldType) (T : ringOfSetsType d).
Variables (mu : {additive_measure set T → \bar R}).

Theorem Boole_inequality (A : (set T) ^nat) n :
    (∀ i, `I_n i → measurable (A i)) →
  mu (\big[setU/set0]_(i < n) A i) ≤ \sum_(i < n) mu (A i).

End boole_inequality.
Notation le_mu_bigsetU := Boole_inequality.

Section sigma_finite_lemma.
Variables (d : measure_display) (R : realFieldType)
  (T : ringOfSetsType d) (A : set T)
  (mu : {additive_measure set T → \bar R}).

Lemma sigma_finiteP : sigma_finite A mu →
  exists2 F, A = \bigcup_i F i &
    nondecreasing_seq F ∧ ∀ i, measurable (F i) ∧ mu (F i) < +oo.

End sigma_finite_lemma.

Section generalized_boole_inequality.
Variables (d : measure_display) (R : realType) (T : ringOfSetsType d).
Variable (mu : {measure set T → \bar R}).

Theorem generalized_Boole_inequality (A : (set T) ^nat) :
  (∀ i, measurable (A i)) → measurable (\bigcup_n A n) →
  mu (\bigcup_n A n) ≤ \sum_(i <oo) mu (A i).

End generalized_boole_inequality.
Notation le_mu_bigcup := generalized_Boole_inequality.

Section negligible.
Variables (d : measure_display) (R : realFieldType) (T : ringOfSetsType d).

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


Lemma negligibleP (mu : {additive_measure set _ → \bar _}) A :
  measurable A → mu.-negligible A ↔ mu A = 0.

Lemma negligible_set0 (mu : {additive_measure set _ → \bar _}) : mu.-negligible set0.

Lemma measure_negligible (mu : {additive_measure set T → \bar R}) (A : set T) :
  measurable A → mu.-negligible A → mu A = 0%E.

Definition almost_everywhere (mu : set T → \bar R) (P : T → Prop)
     & (phantom Prop (∀ x, P x)) :=
   mu.-negligible (~` [set x | P x]).

Lemma aeW (mu : {measure set _ → \bar _}) (P : T → Prop) :
  (∀ x, P x) → {ae mu, ∀ x, P x}.

End negligible.

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

Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) : type_scope.

Definition sigma_subadditive (R : numFieldType) (T : Type)
  (mu : set T → \bar R) := ∀ (F : (set T) ^nat),
  mu (\bigcup_n (F n)) ≤ \sum_(i <oo) mu (F i).


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

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

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

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

Lemma le_outer_measureIC (R : realFieldType) T
  (mu : {outer_measure set T → \bar R}) (A X : set T) :
  mu X ≤ mu (X `&` A) + mu (X `&` ~` A).

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


Lemma le_caratheodory_measurable (R : realType) T
  (mu : {outer_measure set T → \bar R}) (A : set T) :
  (∀ X, mu (X `&` A) + mu (X `&` ~` A) ≤ mu X) →
  mu.-caratheodory A.

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

Let M := mu.-caratheodory.

Lemma caratheodory_measurable_set0 : M set0.

Lemma caratheodory_measurable_setC A : M A → M (~` A).

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.

Lemma caratheodory_measurable_setU A B : M A → M B → M (A `|` B).

Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) : (∀ n, M (A n)) →
  ∀ n, M (\big[setU/set0]_(i < n) A i).

Lemma caratheodory_measurable_setI A B : M A → M B → M (A `&` B).

Lemma caratheodory_measurable_setD A B : M A → M B → M (A `\` B).

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

Let caratheorody_decompIU X : mu (X `&` (A `|` B)) =
  mu (X `&` A `&` B) + mu (X `&` ~` A `&` B) + mu (X `&` A `&` ~` B).

Lemma disjoint_caratheodoryIU X : [disjoint A & B] →
  mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B).
End additive_ext_lemmas.

Lemma caratheodory_additive (A : (set T) ^nat) : (∀ n, M (A n)) →
  trivIset setT A → ∀ n X,
    mu (X `&` \big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (X `&` A i).

Lemma caratheodory_lim_lee (A : (set T) ^nat) : (∀ n, M (A n)) →
  trivIset setT A → ∀ X,
  \sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` \bigcup_k A k) ≤ mu X.

Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) :
  (∀ n, M (A n)) → trivIset setT A → M (\bigcup_k (A k)).

Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (∀ n, M (A n)) →
  M (\bigcup_k (A k)).

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.

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


End caratheodory_sigma_algebra.

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

Definition measure_is_complete d (R : realType) (T : measurableType d)
    (mu : set T → \bar R) :=
  ∀ X, mu.-negligible X → measurable X.

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

Lemma caratheodory_measure0 : mu (set0 : set U) = 0.

Lemma caratheodory_measure_ge0 (A : set U) : 0 ≤ mu A.

Lemma caratheodory_measure_sigma_additive :
  semi_sigma_additive (mu : set U → _).


Lemma measure_is_complete_caratheodory :
  measure_is_complete (mu : set (caratheodory_type mu) → _).

End caratheodory_measure.

Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) e
    (P : pred nat) : (∀ 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.

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

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

Lemma cover_measurable X F : measurable_cover X F → ∀ k, measurable (F k).

Lemma cover_subset X F : measurable_cover X F → X `<=` \bigcup_k (F k).

End measurable_cover.

Section measure_extension.
Variables (R : realType) (d : measure_display) (T : semiRingOfSetsType d).
Variable mu : set T → \bar R.
Hypothesis measure0 : mu set0 = 0.
Hypothesis measure_ge0 : ∀ X, mu X ≥ 0.
Hint Resolve measure_ge0 measure0 : core.

Definition mu_ext (X : set T) : \bar R :=
  ereal_inf [set \sum_(i <oo) mu (A i) | A in measurable_cover X].

Lemma le_mu_ext : {homo mu^* : A B / A `<=` B >-> A ≤ B}.

Lemma mu_ext_ge0 A : 0 ≤ mu^* A.

Lemma mu_ext0 : mu^* set0 = 0.

Lemma measurable_uncurry (G : ((set T)^nat)^nat) (x : nat × nat) :
  measurable (G x.1 x.2) → measurable (uncurry G x).

Lemma mu_ext_sigma_subadditive : sigma_subadditive mu^*.

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

Section measure_extension.
Variables (d : measure_display) (R : realType) (T : semiRingOfSetsType d).
Variable mu : {additive_measure set T → \bar R}.


End measure_extension.

Section g_salgebra_measure_unique_trace.
Variables (d : measure_display) (R : realType) (T : measurableType d).
Variables (G : set (set T)) (D : set T) (mD : measurable D).
Let H := [set X | G X ∧ X `<=` D] .
Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H) (HD : H D).
Variables m1 m2 : {measure set T → \bar R}.
Hypotheses (m1m2 : ∀ A, H A → m1 A = m2 A) (m1oo : (m1 D < +oo)%E).

Lemma g_salgebra_measure_unique_trace :
  (∀ X, (<<s D, H >>) X → X `<=` D) → ∀ X, <<s D, H >> X →
  m1 X = m2 X.

End g_salgebra_measure_unique_trace.

Section g_salgebra_measure_unique.
Variables (d : measure_display) (R : realType) (T : measurableType d).
Variable (G : set (set T)).
Hypothesis (Gm : G `<=` measurable).
Variable g : (set T)^nat.
Hypotheses (Gg : ∀ 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 :
  (∀ n A, <<s G >> A → m1 (g n `&` A) = m2 (g n `&` A)) →
  ∀ A, <<s G >> A → m1 A = m2 A.

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

Lemma g_salgebra_measure_unique : ∀ E, <<s G >> E → m1 E = m2 E.

End g_salgebra_measure_unique.

Section measure_unique.
Variables (d : measure_display) (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 : ∀ i, G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T → \bar R}.
Hypothesis m1m2 : ∀ A, G A → m1 A = m2 A.
Hypothesis m1goo : ∀ k, (m1 (g k) < +oo)%E.

Lemma measure_unique A : measurable A → m1 A = m2 A.

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

Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d)
    (mu : {additive_measure set T → \bar R}) X :
  sigma_sub_additive mu →
  measurable X → mu^* X = mu X.

Section Rmu_ext.
Import SetRing.

Lemma Rmu_ext d (R : realType) (T : semiRingOfSetsType d)
    (mu : {additive_measure set T → \bar R}) :
  (measure mu)^* = mu^*.

End Rmu_ext.

Lemma measurable_Rmu_extE d (R : realType) (T : semiRingOfSetsType d)
    (mu : {additive_measure set T → \bar R}) X :
  sigma_sub_additive mu →
  d.-ring.-measurable X → mu^* X = SetRing.measure mu X.

Section Hahn_extension.
Variables (d : measure_display) (R : realType) (T : semiRingOfSetsType d).
Variable mu : {additive_measure set T → \bar R}.
Hypothesis mu_sub : sigma_sub_additive mu.
Let Rmu := SetRing.measure mu.
Notation rT := (SetRing.type T).

Lemma sub_caratheodory :
  (d.-measurable).-sigma.-measurable `<=` mu^*.-cara.-measurable.

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

Definition Hahn_ext : set I → \bar R := mu^*.





Lemma Hahn_ext_sigma_finite : @sigma_finite _ _ T setT mu →
  @sigma_finite _ _ _ setT Hahn_ext.

Lemma Hahn_ext_unique : @sigma_finite _ _ T setT mu →
  (∀ mu' : {measure set I → \bar R},
    (∀ X, d.-measurable X → mu X = mu' X) →
    (∀ X, (d.-measurable).-sigma.-measurable X → Hahn_ext X = mu' X)).
End Hahn_extension.

Lemma caratheodory_measurable_mu_ext d (R : realType) (T : measurableType d)
    (mu : {measure set T → \bar R}) A :
  d.-measurable A → mu^*.-cara.-measurable A.

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.
Variables (d1 d2 : measure_display) (T1 : measurableType d1).
Variables (T2 : measurableType d2) (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).

End product_lemma.

Definition measure_prod_display :
  (measure_display × measure_display) → measure_display.

Section product_salgebra_instance.
Variables (d1 d2 : measure_display).
Variables (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)).

Lemma prod_salgebra_setC A : preimage_classes f1 f2 A →
  preimage_classes f1 f2 (~` A).

Lemma prod_salgebra_bigcup (F : _^nat) : (∀ i, preimage_classes f1 f2 (F i)) →
  preimage_classes f1 f2 (\bigcup_i (F i)).


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

Section product_salgebra_measurableType.
Variables (d1 d2 : measure_display).
Variables (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 >>.

End product_salgebra_measurableType.

Section product_salgebra_g_measurableTypeR.
Variables (d1 : measure_display) (T1 : measurableType d1).
Variables (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] >>.

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

End product_salgebra_g_measurableType.

Section prod_measurable_fun.
Variables (d d1 d2 : measure_display).
Variables (T : measurableType d) (T1 : measurableType d1).
Variables (T2 : measurableType d2) (f : T → T1 × T2).

Lemma prod_measurable_funP : measurable_fun setT f ↔
  measurable_fun setT (fst \o f) ∧ measurable_fun setT (snd \o f).

End prod_measurable_fun.

Section partial_measurable_fun.
Variables (d d1 d2 : measure_display).
Variables (T : measurableType d) (T1 : measurableType d1).
Variables (T2 : measurableType d2) (f : T1 × T2 → T).

Lemma measurable_fun_prod1 x :
  measurable_fun setT f → measurable_fun setT (fun y ⇒ f (x, y)).

Lemma measurable_fun_prod2 y :
  measurable_fun setT f → measurable_fun setT (fun x ⇒ f (x, y)).

End partial_measurable_fun.