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

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 "{ '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 := ∀ 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.

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

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


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


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


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 [set: 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.
Context d (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.
Context d (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.
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).

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 (T : measurableType d) (F : rat → set T) :
  (∀ i, measurable (F i)) → measurable (\bigcup_i F i).

Section discrete_measurable_unit.

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

Let discrete_measurable0 : discrete_measurable_unit set0.

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

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


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.

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

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


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.

Let discrete_measurable_natC X :
  discrete_measurable_nat X → discrete_measurable_nat (~` X).

Let discrete_measurable_natU (F : (set nat)^nat) :
  (∀ i, discrete_measurable_nat (F i)) →
  discrete_measurable_nat (\bigcup_i F i).


End discrete_measurable_nat.

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

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

Lemma measurableT_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 (f g : T1 → T2) :
  {in D, f =1 g} → measurable_fun D f → measurable_fun D g.

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

Lemma measurable_fun_bigcup (E : (set T1)^nat) (f : T1 → T2) :
  (∀ i, measurable (E i)) →
  measurable_fun (\bigcup_i E i) f ↔ (∀ i, measurable_fun (E i) f).

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.

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

Lemma measurable_funTS D (f : T1 → T2) :
  measurable_fun setT f → measurable_fun D f.

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

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

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

Lemma measurable_fun_bool D (f : T1 → bool) b :
  measurable (f @^-1` [set b]) → measurable_fun D f.

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.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")]
Notation measurable_fun_id := measurable_id.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_cst`")]
Notation measurable_fun_cst := measurable_cst.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_comp`")]
Notation measurable_fun_comp := measurable_comp.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurableT_comp`")]
Notation measurable_funT_comp := measurableT_comp.

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

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.
Context d (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).

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

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.

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?*))
  (T : semiRingOfSetsType d) (mu : set T → \bar R) :
  mu set0 = 0 → semi_sigma_additive mu → semi_additive mu.

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

Lemma sigma_additive_is_additive
  (R : realFieldType) d (T : measurableType d) (mu : set T → \bar R) :
  mu set0 = 0 → sigma_additive mu → additive 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).

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.

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

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

#[global]
Hint Resolve measureU measure_bigsetU : core.


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

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

End measure_signed.



Let semi_additive_mu : semi_additive mu.


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

Section measure_lemmas.
Context d (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.

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

Lemma measure_bigcup (D : set nat) F : (∀ 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).

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.

Let pushforward_ge0 A : 0 ≤ pushforward mf A.

Let pushforward_sigma_additive : semi_sigma_additive (pushforward mf).


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.

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.

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.

Lemma dirac0 (a : T) : \d_a set0 = 0 :> \bar R.

Lemma diracT (a : T) : \d_a setT = 1 :> \bar R.

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.

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

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.
Context d (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.
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.

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.

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

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.
Context d (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.

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


Let counting0 : counting set0 = 0.

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

Let counting_sigma_additive : semi_sigma_additive counting.


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.

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 < n) A i]].

Lemma covered_by_countable P :
    (∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
    (∀ (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 | ∃ 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 measurable_subring : (d.-measurable : set (set T)) `<=` d.-ring.-measurable.

Lemma ring_finite_set (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_finite_set 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 content.
Context {R : realFieldType} (mu : {content 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 _ := isContent.Build _ _ _ Rmu Rmu_ge0 Rmu_additive.

End content.

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 : {content 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 : {content set T → \bar R}) (A : set T) :
  (mu A ≤ 0)%E = (mu A == 0)%E.

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.

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.
Context d (R : realType) (T : ringOfSetsType d).
Variable mu : {content 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 : {content set T → \bar R}).
Import SetRing.

Lemma ring_sigma_sub_additive : sigma_sub_additive mu → sigma_sub_additive Rmu.

Lemma ring_semi_sigma_additive : sigma_sub_additive mu → semi_sigma_additive Rmu.

Lemma semiring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive mu.

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


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.

End more_premeasure_ring_lemmas.

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

Let ring_sigma_content : semi_sigma_additive Rmu.


End ring_sigma_content.

Definition fin_num_fun d (T : semiRingOfSetsType d) (R : numDomainType)
  (mu : set T → \bar R) := ∀ 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.

Lemma lty_fin_num_fun d (T : algebraOfSetsType d)
    (R : realFieldType) (mu : {measure set T → \bar R}) :
  mu setT < +oo → fin_num_fun mu.

Definition sfinite_measure d (T : measurableType d) (R : realType)
    (mu : set T → \bar R) :=
  exists2 s : {measure set T → \bar R}^nat,
    ∀ n, fin_num_fun (s n) &
    ∀ 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 &
      ∀ 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.

Lemma sfinite_measure_sigma_finite d (T : measurableType d)
    (R : realType) (mu : {measure set T → \bar R}) :
  sigma_finite setT mu → sfinite_measure 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.


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



Lemma sfinite : sfinite_measure mu.




Lemma sigma_finite_mzero d (T : measurableType d) (R : realType) :
  sigma_finite setT (@mzero d T R).


Lemma sfinite_mzero d (T : measurableType d) (R : realType) :
  sfinite_measure (@mzero d T R).




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.



Let sfinite : sfinite_measure k.


Let sigma_finite : sigma_finite setT k.


Let finite : fin_num_fun k.





Let sfinite : sfinite_measure k.



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.

Let s_ge0 n x : 0 ≤ s n x.

Let s_semi_sigma_additive n : semi_sigma_additive (s n).


Let s_fin n : fin_num_fun (s 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.

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.



Let restr_fin : fin_num_fun restr.


End measure_frestr.


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



Let finite : @Measure_isFinite d T R P.





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

End probability_lemmas.



Let subprobability : @Measure_isSubProbability d T R P.




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.

Let mnormalize_ge0 U : 0 ≤ mnormalize U.

Let mnormalize_sigma_additive : semi_sigma_additive mnormalize.


Let mnormalize1 : mnormalize [set: T] = 1.


End mnormalize.

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


End pdirac.

Lemma sigma_finite_counting (R : realType) :
  sigma_finite [set: nat] (@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.

Lemma measureIr : mu (A `&` B) ≤ mu B.

Lemma subset_measure0 : A `<=` B → mu B = 0 → mu A = 0.

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

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

Lemma measureU2 A B : measurable A → measurable B →
  mu (A `|` B) ≤ mu A + mu B.

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

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

Lemma null_set_setU A B : measurable A → measurable B →
  mu A = 0 → mu B = 0 → mu (A `|` B) = 0.

Lemma measureU0 A B : measurable A → measurable B → mu B = 0 →
  mu (A `|` B) = mu A.

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

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) :
  (∀ i, measurable (F i)) → measurable (\bigcup_n F n) →
  nondecreasing_seq F →
  mu \o F --> mu (\bigcup_n F n).

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 →
  (∀ i, measurable (F i)) → measurable (\bigcap_n F n) →
  nonincreasing_seq F → mu \o F --> mu (\bigcap_n F n).

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 :
    (∀ 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.
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 ∧ ∀ i, measurable (F i) ∧ mu (F i) < +oo.

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) :
  (∀ 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.
Context d (T : semiRingOfSetsType d) (R : realFieldType).

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


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

Lemma negligibleP A : measurable A → mu.-negligible A ↔ mu A = 0.

Lemma negligible_set0 : mu.-negligible set0.

Lemma measure_negligible (A : set T) :
  measurable A → mu.-negligible A → mu A = 0%E.

Lemma negligibleS A B : B `<=` A → mu.-negligible A → mu.-negligible B.

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

End negligible_ringOfSetsType.

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.

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.

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

#[global]
Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType)
  (mu : {measure set T → \bar R}) : Filter (almost_everywhere mu).

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

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 (∀ 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) :
  (∀ x, P x) → {ae mu, ∀ x, P x}.

Definition sigma_subadditive {T} {R : numFieldType}
  (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} _.

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

Lemma outer_measureU2 A B : mu (A `|` B) ≤ mu A + mu B.

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

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_lime_le (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.
#[deprecated(since="mathcomp-analysis 0.6.0",
      note="renamed `caratheodory_lime_le`")]
Notation caratheodory_lim_lee := caratheodory_lime_le.

Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) :
  (∀ 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.

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.

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.

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

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

Section outer_measure_construction.
Context d (T : semiRingOfSetsType d) (R : realType).
Variable mu : set T → \bar R.
Hypothesis (measure0 : mu set0 = 0) (measure_ge0 : ∀ 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].

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 mu_ext_sigma_subadditive : sigma_subadditive mu^*.

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


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] .
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.
Context d (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.
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 : ∀ 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 : {measure set T → \bar R}) X :
  measurable X → mu^* X = mu X.

Section Rmu_ext.
Import SetRing.

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

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.

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.

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

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





Lemma measure_extension_sigma_finite : @sigma_finite _ T _ setT mu →
  @sigma_finite _ _ _ setT measure_extension.

Lemma measure_extension_unique : sigma_finite [set: T] mu →
  (∀ mu' : {measure set I → \bar R},
    (∀ X, d.-measurable X → mu X = mu' X) →
    (∀ X, (d.-measurable).-sigma.-measurable X →
      measure_extension X = mu' X)).

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.

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

End product_lemma.

Definition measure_prod_display :
  (measure_display × measure_display) → measure_display.

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

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

End product_salgebra_measurableType.

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