Module mathcomp.analysis.lebesgue_measure

From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat archimedean.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop reals ereal signed.
From mathcomp Require Import topology numfun normedtype function_spaces.
From HB Require Import structures.
From mathcomp Require Import sequences esum measure real_interval realfun exp.
From mathcomp Require Export lebesgue_stieltjes_measure.

# Lebesgue Measure This file further develops the theory of measurable functions (including Egorov's theorem), contains a formalization of the Lebesgue measure using the Measure Extension theorem from measure.v, and proves properties of the Lebesgue measure such as Vitali's theorem, i.e., given a Vitali cover $V$ of $A$, there exists a countable subcollection $D \subseteq V$ of pairwise disjoint closed balls such that $\lambda(A \setminus \bigcup_k D_k) = 0$. Main references: - Daniel Li, Intégration et applications, 2016 - Achim Klenke, Probability Theory 2nd edition, 2014 ``` completed_algebra_gen == generator of the completed Lebesgue sigma-algebra ps_infty == inductive definition of the powerset {0, {-oo}, {+oo}, {-oo,+oo}} emeasurable G == sigma-algebra over \bar R built out of the measurables G of a sigma-algebra over R ``` The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs of equivalence between the sigma-algebra generated by open-closed intervals and the sigma-algebras generated by open rays, closed rays, and open intervals. The module NGenCInfty provides a proof of equivalence between the sigma-algebra for natural numbers and the sigma-algebra generated by closed rays. The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs of equivalence between emeasurable and the sigma-algebras generated by open rays and closed rays. ``` lebesgue_measure == the Lebesgue measure completed_lebesgue_measure == the completed Lebesgue measure elebesgue_measure == the Lebesgue measure extended to \bar R ``` ``` vitali_cover A B V == V is a Vitali cover of A, here B is a collection of non-empty closed balls ```

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition completed_algebra_gen d {T : semiRingOfSetsType d} {R : realType}
(mu : set T -> \bar R) : set _ :=
[set A `|` N | A in d.-measurable & N in mu.-negligible].

Section ps_infty.
Context {T : Type}.
Local Open Scope ereal_scope.

Inductive ps_infty : set \bar T -> Prop :=
| ps_infty0 : ps_infty set0
| ps_ninfty : ps_infty [set -oo]
| ps_pinfty : ps_infty [set +oo]
| ps_inftys : ps_infty [set -oo; +oo].

Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo].

Proof.

split => [[]//|Aoo].
by have [] := subset_set2 Aoo; move=> ->; constructor.
Qed.

Lemma setCU_Efin (A : set T) (B : set \bar T) : ps_infty B ->
~` (EFin @` A) `&` ~` B = (EFin @` ~` A) `|` ([set -oo%E; +oo%E] `&` ~` B).

Proof.

move=> ps_inftyB.
have -> : ~` (EFin @` A) = EFin @` (~` A) `|` [set -oo; +oo]%E.
by rewrite EFin_setC setDKU // => x [|] -> -[].
rewrite setIUl; congr (_ `|` _); rewrite predeqE => -[x| |]; split; try by case.
by move=> [] x' Ax' [] <-{x}; split; [exists x'|case: ps_inftyB => // -[]].
Qed.

End ps_infty.

Section salgebra_ereal.
Variables (R : realType) (G : set (set R)).
Let measurableR : set (set R) := G.-sigma.-measurable.

Definition emeasurable : set (set \bar R) :=
[set EFin @` A `|` B | A in measurableR & B in ps_infty].

Lemma emeasurable0 : emeasurable set0.

Proof.

exists set0; first exact: measurable0.
by exists set0; rewrite ?setU0// ?image_set0//; constructor.
Qed.

Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X).

Proof.

move => -[A mA] [B PooB <-]; rewrite setCU setCU_Efin //.
exists (~` A); [exact: measurableC | exists ([set -oo%E; +oo%E] `&` ~` B) => //].
case: PooB.
- by rewrite setC0 setIT; constructor.
- rewrite setIUl setICr set0U -setDE.
  have [_ ->] := @setDidPl (\bar R) [set +oo%E] [set -oo%E]; first by constructor.
  by rewrite predeqE => x; split => // -[->].
- rewrite setIUl setICr setU0 -setDE.
  have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor.
  by rewrite predeqE => x; split => // -[->].
- by rewrite setICr; constructor.
Qed.

Lemma bigcupT_emeasurable (F : (set \bar R)^nat) :
(forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)).

Proof.

move=> mF; pose P := fun i j => measurableR j.1 /\ ps_infty j.2 /\
                            F i = [set x%:E | x in j.1] `|` j.2.
have [f fi] : {f : nat -> (set R) * (set \bar R) & forall i, P i (f i) }.
  by apply: choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x, y).
exists (\bigcup_i (f i).1).
  by apply: bigcupT_measurable => i; exact: (fi i).1.
exists (\bigcup_i (f i).2).
  apply/ps_inftyP => x [n _] fn2x.
  have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n.
  exact.
rewrite [RHS](@eq_bigcupr _ _ _ _
    (fun i => [set x%:E | x in (f i).1] `|` (f i).2)); last first.
  by move=> i; have [_ []] := fi i.
rewrite bigcupU; congr (_ `|` _).
rewrite predeqE => i /=; split=> [[r [n _ fn1r <-{i}]]|[n _ [r fn1r <-{i}]]];
by [exists n => //; exists r | exists r => //; exists n].
Qed.

Definition ereal_isMeasurable : isMeasurable default_measure_display (\bar R) :=
  isMeasurable.Build _ _
    emeasurable0 emeasurableC bigcupT_emeasurable.

End salgebra_ereal.

Section puncture_ereal_itv.
Variable R : realDomainType.
Implicit Types (y : R) (b : bool).
Local Open Scope ereal_scope.

Lemma punct_eitv_bndy b y : [set` Interval (BSide b y%:E) +oo%O] =
  EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo].

Proof.

rewrite predeqE => x; split; rewrite /= in_itv andbT.
- move: x => [x| |] yxb; [|by right|by case: b yxb].
  by left; exists x => //; rewrite in_itv /= andbT; case: b yxb.
- move=> [[r]|->].
  + by rewrite in_itv /= andbT => yxb <-; case: b yxb.
  + by case: b => /=; rewrite ?(ltry, leey).
Qed.

Lemma punct_eitv_Nybnd b y : [set` Interval -oo%O (BSide b y%:E)] =
[set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)].

Proof.

rewrite predeqE => x; split; rewrite /= in_itv.
- move: x => [x| |] yxb; [|by case: b yxb|by left].
  by right; exists x => //; rewrite in_itv /= andbT; case: b yxb.
- move=> [->|[r]].
  + by case: b => /=; rewrite ?(ltNyr, leNye).
  + by rewrite in_itv /= => yxb <-; case: b yxb.
Qed.

Lemma punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set~ -oo].

Proof.

Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo].

Proof.

End puncture_ereal_itv.

Section salgebra_R_ssets.
Variable R : realType.

Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
  (R.-ocitv.-measurable).-sigma.-measurable.

HB.instance Definition _ := Pointed.on R.
HB.instance Definition R_isMeasurable :
  isMeasurable default_measure_display R :=
  @isMeasurable.Build _ measurableTypeR measurableR
    measurable0 (@measurableC _ _) (@bigcupT_measurable _ _).

Lemma measurable_set1 (r : R) : measurable [set r].

Proof.

rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _.
by apply: sub_sigma_algebra; exact/is_ocitv.
Qed.

#[local] Hint Resolve measurable_set1 : core.

Lemma measurable_itv (i : interval R) : measurable [set` i].

Proof.

have moc (a b : R) : measurable `]a, b].
  by apply: sub_sigma_algebra; apply: is_ocitv.
have mopoo (x : R) : measurable `]x, +oo[.
  by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable.
have mnooc (x : R) : measurable `]-oo, x].
  by rewrite -setCitvr; exact/measurableC.
have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b.
  case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
have moo (a b : R) : measurable `]a, b[.
  by rewrite ooE; exact: measurableD.
have mcc (a b : R) : measurable `[a, b].
  case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
  by rewrite -setU1itv//; apply/measurableU.
have mco (a b : R) : measurable `[a, b[.
  case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
  by rewrite -setU1itv//; apply/measurableU.
have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
  by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
- by rewrite -setU1itv//; exact/measurableU.
- by rewrite oooE; exact/measurableD.
- by rewrite set_itv_infty_infty.
Qed.

#[local] Hint Resolve measurable_itv : core.

Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) :
measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
measurable_fun `[x, y[ f.

Proof.

have [xy|yx _] := ltP x y; last first.
  by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0.
move: b0 b1 => [|] [|] // mf.
- apply: measurable_funS mf => //; exact: subset_itv_co_cc.
- rewrite -setU1itv//= measurable_funU//; split => //.
  exact: measurable_fun_set1.
- rewrite -setU1itv//= measurable_funU//; split.
    exact: measurable_fun_set1.
  by apply: measurable_funS mf => //; exact: subset_itv_oo_oc.
Qed.

Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) :
measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
measurable_fun `]x, y] f.

Proof.

have [xy|yx _] := ltP x y; last first.
  by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0.
move: b0 b1 => [|] [|] // mf.
- rewrite -setUitv1//= measurable_funU//; split.
    by apply: measurable_funS mf => //; exact: subset_itv_oo_co.
  exact: measurable_fun_set1.
- by apply: measurable_funS mf => //; exact: subset_itv_oc_cc.
- rewrite -setUitv1//= measurable_funU//; split => //.
  exact: measurable_fun_set1.
Qed.

Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) :
measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
measurable_fun `[x, y] f.

Proof.

move=> mf.
have [xy|] := ltP x y; last first.
  rewrite le_eqVlt => /predU1P[->|ba].
    by rewrite set_itv1; exact: measurable_fun_set1.
  rewrite set_itv_ge//; first exact: measurable_fun_set0.
  by rewrite -leNgt bnd_simp.
rewrite -setUitv1//=; last by rewrite bnd_simp ltW.
  rewrite measurable_funU//; split => //.
  exact: measurable_fun_itv_co mf.
exact: measurable_fun_set1.
Qed.

HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)).

Lemma measurable_image_EFin (A : set R) :
measurableR A -> measurable (EFin @` A).

Proof.

by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0].
Qed.

Lemma emeasurable_set1 (x : \bar R) : measurable [set x].

Proof.

case: x => [r| |].
- by rewrite -image_set1; apply: measurable_image_EFin; apply: measurable_set1.
- exists set0 => //; [exists [set +oo%E]; [by constructor|]].
by rewrite image_set0 set0U.
- exists set0 => //; [exists [set -oo%E]; [by constructor|]].
by rewrite image_set0 set0U.
Qed.

#[local] Hint Resolve emeasurable_set1 : core.

Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).

Proof.

by rewrite itv_cyy. Qed.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")]
Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty (only parsing).

Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R).

Proof.

by rewrite itv_oyy. Qed.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")]
Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty (only parsing).

Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R).

Proof.

by rewrite itv_cNyy. Qed.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")]
Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty (only parsing).

Lemma __deprecated__itv_oninfty_pinfty :
`]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).

Proof.

by rewrite itv_oNyy. Qed.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")]
Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty (only parsing).

Let emeasurable_itv_bndy b (y : \bar R) :
measurable [set` Interval (BSide b y) +oo%O].

Proof.

move: y => [y| |].
- exists [set` Interval (BSide b y) +oo%O]; first exact: measurable_itv.
by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy].
- by case: b; rewrite ?itv_oyy ?itv_cyy.
- case: b; first by rewrite itv_cNyy.
by rewrite itv_oNyy; exact/measurableC.
Qed.

Let emeasurable_itv_Nybnd b (y : \bar R) :
measurable [set` Interval -oo%O (BSide b y)].

Proof.

by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bndy. Qed.

Lemma emeasurable_itv (i : interval (\bar R)) :
measurable ([set` i]%classic : set \bar R).

Proof.

rewrite -[X in measurable X]setCK; apply: measurableC.
rewrite set_interval.setCitv /=; apply: measurableU => [|].
- by move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE.
- by move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE.
Qed.

Lemma measurable_image_fine (X : set \bar R) : measurable X ->
measurable [set fine x | x in X `\` [set -oo; +oo]%E].

Proof.

case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]].
- rewrite setU0 => <-{X}.
  rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
    by move=> [x [[x' Yx' <-{x}/= _ <-//]]].
  by move=> Yr; exists r%:E; split => [|[]//]; exists r.
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
    move=> [x [[[x' Yx' <- _ <-//]|]]].
    by move=> <-; rewrite not_orP => -[]/(_ erefl).
  by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
    move=> [x [[[x' Yx' <-{x} _ <-//]|]]].
    by move=> ->; rewrite not_orP => -[_]/(_ erefl).
  by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split.
    by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-].
  by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r.
Qed.

Lemma measurable_ball (x : R) e : measurable (ball x e).

Proof.

by rewrite ball_itv; exact: measurable_itv. Qed.

Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r).

Proof.

have [r0|r0] := leP r 0; first by rewrite closed_ball0.
rewrite closed_ball_itv//.
Qed.

End salgebra_R_ssets.
#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1|
apply: emeasurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_bnd_pinfty := emeasurable_itv (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing).

Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D ->
measurable_fun D fine.

Proof.

move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then
    D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first.
  apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]].
  - by case: ifPn => _; split => //; left; exists r.
  - by rewrite mem_set//; split => //; right; right.
  - by rewrite mem_set//; split => //; right; left.
  - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr.
  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin.
by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU].
Qed.

#[global] Hint Extern 0 (measurable_fun _ fine) =>
solve [exact: fine_measurable] : core.
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `fine_measurable` instead")]
Notation measurable_fine := fine_measurable (only parsing).

Section measurable_fun_measurable.
Local Open Scope ereal_scope.
Context d (T : sigmaRingType d) (R : realType).
Variables (D : set T) (f : T -> \bar R).
Hypotheses (mD : measurable D) (mf : measurable_fun D f).
Implicit Types y : \bar R.

Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]).

Proof.

by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed.

Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]).

Proof.

by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed.

Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]).

Proof.

by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed.

Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]).

Proof.

by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed.

Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]).

Proof.

rewrite [X in measurable X](_ : _ =
  \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))).
  apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA.
  by apply: measurableI; [exact: emeasurable_fun_c_infty|
                          exact: emeasurable_fun_infty_c].
rewrite predeqE => t; split => [/= [Dt ft]|].
  have [ft0|ft0] := leP 0%R (fine (f t)).
    exists `|ceil (fine (f t))|%N => //=; split => //; split.
      by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0.
    rewrite natr_absz ger0_norm; last first.
      by rewrite -ceil_ge0 (lt_le_trans _ ft0).
    by rewrite -(fineK ft) lee_fin ceil_ge.
  exists `|floor (fine (f t))|%N => //=; split => //; split.
    rewrite natr_absz ltr0_norm -?floor_lt0// EFinN.
    by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real.
  by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry.
Qed.

Lemma emeasurable_neq y : measurable (D `&` [set x | f x != y]).

Proof.

rewrite (_ : [set x | f x != y] = f @^-1` (setT `\ y)).
exact/mf/measurableD.
rewrite predeqE => t; split; last by rewrite /preimage /= => -[_ /eqP].
by rewrite /= => ft0; rewrite /preimage /=; split => //; exact/eqP.
Qed.

End measurable_fun_measurable.

Module RGenOInfty.
Section rgenoinfty.
Variable R : realType.
Implicit Types x y z : R.

Definition G := [set A | exists x, A = `]x, +oo[%classic].

Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; last by apply: sub_sigma_algebra; eexists; reflexivity.
rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k.
by apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma measurable_itv_bounded a b x : a != +oo%O ->
G.-sigma.-measurable [set` Interval a (BSide b x)].

Proof.

case: a => [a r _|[_|//]].
by rewrite set_itv_splitD; apply: measurableD => //;
exact: measurable_itv_bnd_infty.
by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty.
Qed.

Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

rewrite eqEsubset; split => A.
apply: smallest_sub; first exact: smallest_sigma_algebra.
by move=> I [x _ <-]; exact: measurable_itv_bounded.
apply: smallest_sub; first exact: smallest_sigma_algebra.
by move=> A' /= [x ->]; exact: measurable_itv.
Qed.

End rgenoinfty.
End RGenOInfty.

Module RGenInftyO.
Section rgeninftyo.
Variable R : realType.
Implicit Types x y z : R.

Definition G := [set A | exists x, A = `]-oo, x[%classic].

Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set` Interval -oo%O (BSide b x)].

Proof.

case: b; first by apply sub_sigma_algebra; eexists; reflexivity.
rewrite -setCitvr itv_o_inftyEbigcup; apply/measurableC/bigcupT_measurable => n.
rewrite -setCitvl; apply: measurableC.
by apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma measurable_itv_bounded a b x : a != -oo%O ->
G.-sigma.-measurable [set` Interval (BSide b x) a].

Proof.

case: a => [a r _|[//|_]].
by rewrite set_itv_splitD; apply/measurableD => //;
rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty.
by rewrite -setCitvl; apply: measurableC; apply: measurable_itv_bnd_infty.
Qed.

Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

rewrite eqEsubset; split => A.
apply: smallest_sub; first exact: smallest_sigma_algebra.
by move=> I [x _ <-]; apply: measurable_itv_bounded.
apply: smallest_sub; first exact: smallest_sigma_algebra.
by move=> A' /= [x ->]; apply: measurable_itv.
Qed.

End rgeninftyo.
End RGenInftyO.

Module RGenCInfty.
Section rgencinfty.
Variable R : realType.
Implicit Types x y z : R.

Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic].

Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty.
rewrite itv_o_inftyEbigcup; apply: bigcupT_measurable => k.
by apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma measurable_itv_bounded a b y : a != +oo%O ->
G.-sigma.-measurable [set` Interval a (BSide b y)].

Proof.

case: a => [a r _|[_|//]].
rewrite set_itv_splitD.
by apply: measurableD; apply: measurable_itv_bnd_infty.
by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty.
Qed.

Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

End rgencinfty.
End RGenCInfty.

Module RGenOpens.
Section rgenopens.
Variable R : realType.
Implicit Types x y z : R.

Definition G := [set A | exists x y, A = `]x, y[%classic].

Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic.

Proof.

by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed.

Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic.

Proof.

rewrite itv_bnd_inftyEbigcup; apply: bigcupT_measurable => i.
exact: measurable_itvoo.
Qed.

Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; last exact: measurable_itv_o_infty.
rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k.
exact: measurable_itv_o_infty.
Qed.

Lemma measurable_itv_infty_bnd b x :
G.-sigma.-measurable [set` Interval -oo%O (BSide b x)].

Proof.

by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty.
Qed.

Lemma measurable_itv_bounded a x b y :
G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)].

Proof.

move: a b => [] []; rewrite -[X in measurable X]setCK setCitv;
apply: measurableC; apply: measurableU; try solve[
exact: measurable_itv_infty_bnd|exact: measurable_itv_bnd_infty].
Qed.

Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

End rgenopens.
End RGenOpens.

Section erealwithrays.
Variable R : realType.
Implicit Types (x y z : \bar R) (r s : R).
Local Open Scope ereal_scope.

Lemma EFin_itv_bnd_infty b r : EFin @` [set` Interval (BSide b r) +oo%O] =
[set` Interval (BSide b r%:E) +oo%O] `\ +oo.

Proof.

rewrite eqEsubset; split => [x [s /itvP rs <-]|x []].
  split => //=; rewrite in_itv /=.
  by case: b in rs *; rewrite /= ?(lee_fin, lte_fin) rs.
move: x => [s|_ /(_ erefl)|] //=; rewrite in_itv /= andbT; last first.
  by case: b => /=; rewrite 1?(leNgt,ltNge) 1?(ltNyr, leNye).
by case: b => /=; rewrite 1?(lte_fin,lee_fin) => rs _;
  exists s => //; rewrite in_itv /= rs.
Qed.

Lemma EFin_itv r : [set s | r%:E < s%:E] = `]r, +oo[%classic.

Proof.

by rewrite predeqE => s; split => [|]; rewrite /= lte_fin in_itv/= andbT.
Qed.

Lemma preimage_EFin_setT : @EFin R @^-1` [set x | x \in `]-oo%E, +oo[] = setT.

Proof.

by rewrite set_itvE predeqE => r; split=> // _; rewrite /preimage /= ltNyr.
Qed.

Lemma eitv_bnd_infty b r : `[r%:E, +oo[%classic =
\bigcap_k [set` Interval (BSide b (r - k.+1%:R^-1)%:E) +oo%O] :> set _.

Proof.

rewrite predeqE => x; split=> [|].
- move: x => [s /=| _ n _|//].
  + rewrite in_itv /= andbT lee_fin => rs n _ /=; rewrite in_itv/= andbT.
    case: b => /=.
    * by rewrite lee_fin lerBlDl (le_trans rs)// lerDr.
    * by rewrite lte_fin ltrBlDl (le_lt_trans rs)// ltrDr.
  + by rewrite /= in_itv /= andbT; case: b => /=; rewrite lteey.
- move: x => [s| |/(_ 0%N Logic.I)] /=; rewrite ?in_itv/= ?leey//; last first.
    by case: b.
  move=> h; rewrite lee_fin leNgt andbT; apply/negP => /ltr_add_invr[k skr].
  have {h} := h k Logic.I; rewrite /= in_itv /= andbT; case: b => /=.
  + by rewrite lee_fin lerBlDr leNgt skr.
  + by rewrite lte_fin ltrBlDr ltNge (ltW skr).
Qed.

Lemma eitv_infty_bnd b r : `]-oo, r%:E]%classic =
\bigcap_k [set` Interval -oo%O (BSide b (r%:E + k.+1%:R^-1%:E))] :> set _.

Proof.

rewrite predeqE => x; split=> [|].
- move: x => [s /=|//|_ n _].
  + rewrite in_itv /= lee_fin => sr n _; rewrite /= in_itv /= -EFinD.
    case: b => /=.
    * by rewrite lte_fin (le_lt_trans sr)// ltrDl.
    * by rewrite lee_fin (le_trans sr)// lerDl.
  + by rewrite /= in_itv /= -EFinD; case: b => //=; rewrite lteNye.
- move: x => [s|/(_ 0%N Logic.I)|]/=; rewrite !in_itv/= ?leNye//; last first.
    by case: b.
  move=> h; rewrite lee_fin leNgt; apply/negP => /ltr_add_invr[k rks].
  have {h} := h k Logic.I; rewrite /= in_itv /= -EFinD; case: b => /=.
  + by rewrite lte_fin ltNge (ltW rks).
  + by rewrite lee_fin leNgt rks.
Qed.

Lemma eset1Ny :
[set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R).

Proof.

rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
move=> [r|/(_ O Logic.I)|]//.
move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge.
rewrite lee_fin; have [r0|r0] := leP 0%R r.
by rewrite (le_trans _ r0) // lerNl oppr0 ler0n.
rewrite lerNl -abszN natr_absz gtr0_norm; last first.
by rewrite ltrNr oppr0 -floor_lt0.
by rewrite mulrNz lerNl opprK ge_floor.
Qed.

Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).

Proof.

rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=.
rewrite andbT lte_fin ltNge.
have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0).
by rewrite natr_absz gtr0_norm// ?ceil_ge// -ceil_gt0.
Qed.

End erealwithrays.

Module ErealGenOInfty.
Section erealgenoinfty.
Variable R : realType.
Implicit Types (x y z : \bar R) (r s : R).

Local Open Scope ereal_scope.

Definition G := [set A : set \bar R | exists r, A = `]r%:E, +oo[%classic].

Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo].

Proof.

rewrite eset1Ny; apply: bigcap_measurable => // i _.
rewrite -setCitvr; apply: measurableC; rewrite (eitv_bnd_infty false).
apply: bigcap_measurable => // j _; apply: sub_sigma_algebra.
by exists (- (i%:R + j.+1%:R^-1))%R; rewrite opprD.
Qed.

Lemma measurable_set1y : G.-sigma.-measurable [set +oo].

Proof.

rewrite eset1y; apply: bigcapT_measurable => i.
by apply: sub_sigma_algebra; exists i%:R.
Qed.

Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable.

Proof.

apply/seteqP; split; last first.
  apply: smallest_sub.
    split; first exact: emeasurable0.
      by move=> *; rewrite setTD; exact: emeasurableC.
    by move=> *; exact: bigcupT_emeasurable.
  move=> _ [r ->]; rewrite /emeasurable /=.
  exists `]r, +oo[%classic.
    rewrite RGenOInfty.measurableE.
    exact: RGenOInfty.measurable_itv_bnd_infty.
  by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy].
move=> A [B mB [C mC]] <-; apply: measurableU; last first.
  case: mC; [by []|exact: measurable_set1Ny|exact: measurable_set1y|].
  - by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y].
rewrite RGenOInfty.measurableE in mB.
have smB := smallest_sub _ _ mB.
(* BUG: elim/smB : _. fails !! *)
apply: (smB (G.-sigma.-measurable \o (image^~ EFin))); last first.
  move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD.
    by apply: sub_sigma_algebra => /=; exists r.
  exact: measurable_set1y.
split=> /= [|D mD|F mF]; first by rewrite image_set0.
- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC.
  by apply: measurableU; [exact: measurable_set1Ny| exact: measurable_set1y].
- by rewrite EFin_bigcup; apply: bigcup_measurable => i _ ; exact: mF.
Qed.

End erealgenoinfty.
End ErealGenOInfty.

Module ErealGenCInfty.
Section erealgencinfty.
Variable R : realType.
Implicit Types (x y z : \bar R) (r s : R).
Local Open Scope ereal_scope.

Definition G := [set A : set \bar R | exists r, A = `[r%:E, +oo[%classic].

Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo].

Proof.

rewrite eset1Ny; apply: bigcapT_measurable=> i; rewrite -setCitvr.
by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%R.
Qed.

Lemma measurable_set1y : G.-sigma.-measurable [set +oo].

Proof.

rewrite eset1y; apply: bigcap_measurable => // i _.
rewrite -setCitvl; apply: measurableC; rewrite (eitv_infty_bnd true).
apply: bigcap_measurable => // j _; rewrite -setCitvr; apply: measurableC.
by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R.
Qed.

Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable.

Proof.

apply/seteqP; split; last first.
  apply: smallest_sub.
    split; first exact: emeasurable0.
      by move=> *; rewrite setTD; exact: emeasurableC.
    by move=> *; exact: bigcupT_emeasurable.
  move=> _ [r ->]/=; exists `[r, +oo[%classic.
    rewrite RGenOInfty.measurableE.
    exact: RGenOInfty.measurable_itv_bnd_infty.
  by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy].
move=> _ [A' mA' [C mC]] <-; apply: measurableU; last first.
  case: mC; [by []|exact: measurable_set1Ny| exact: measurable_set1y|].
  by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y].
rewrite RGenCInfty.measurableE in mA'.
have smA' := smallest_sub _ _ mA'.
(* BUG: elim/smA' : _. fails !! *)
apply: (smA' (G.-sigma.-measurable \o (image^~ EFin))); last first.
  move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD.
    by apply: sub_sigma_algebra => /=; exists r.
  exact: measurable_set1y.
split=> /= [|D mD|F mF]; first by rewrite image_set0.
- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC.
  by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y].
- by rewrite EFin_bigcup; apply: bigcup_measurable => i _; exact: mF.
Qed.

End erealgencinfty.
End ErealGenCInfty.

Module ErealGenInftyO.
Section erealgeninftyo.
Variable R : realType.

Definition G := [set A : set \bar R | exists r, A = `]-oo, r%:E[%classic].

Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable.

Proof.

rewrite ErealGenCInfty.measurableE eqEsubset; split => A.
  apply: smallest_sub; first exact: smallest_sigma_algebra.
  move=> _ [x ->]; rewrite -[X in _.-measurable X]setCK; apply: measurableC.
  by apply: sub_sigma_algebra; exists x; rewrite setCitvr.
apply: smallest_sub; first exact: smallest_sigma_algebra.
move=> x Gx; rewrite -(setCK x); apply: measurableC; apply: sub_sigma_algebra.
by case: Gx => y ->; exists y; rewrite setCitvl.
Qed.

End erealgeninftyo.
End ErealGenInftyO.

Lemma is_interval_measurable (R : realType) (I : set R) :
is_interval I -> measurable I.

Proof.

by move/is_intervalP => ->; exact: measurable_itv. Qed.

Section coutinuous_measurable.
Variable R : realType.

Lemma open_measurable (A : set R) : open A -> measurable A.

Proof.

move=>/open_bigcup_rat ->; rewrite bigcup_mkcond; apply: bigcupT_measurable_rat.
move=> q; case: ifPn => // qfab; apply: is_interval_measurable => //.
exact: is_interval_bigcup_ointsub.
Qed.

Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) :
measurable D -> open U -> measurable (D `&` U).

Proof.

move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD.
by apply: measurableI => //; exact: open_measurable.
Qed.

Lemma closed_measurable (A : set R) : closed A -> measurable A.

Proof.

by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed.

Lemma compact_measurable (A : set R) : compact A -> measurable A.

Proof.

by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable.
Qed.

Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) :
measurable D -> continuous f -> measurable_fun D f.

Proof.

move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)).
move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //.
exact/cf/interval_open.
Qed.

Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) :
open D -> {in D, continuous f} -> measurable_fun D f.

Proof.

move=> oD; rewrite -(continuous_open_subspace f oD).
by apply: subspace_continuous_measurable_fun; exact: open_measurable.
Qed.

Lemma continuous_measurable_fun (f : R -> R) :
continuous f -> measurable_fun setT f.

Proof.

by move=> cf; apply: open_continuous_measurable_fun => //; exact: openT.
Qed.

End coutinuous_measurable.

Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) :
lower_semicontinuous f -> measurable_fun setT f.

Proof.

move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)).
move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable.
by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact.
Qed.

Section standard_measurable_fun.
Variable R : realType.
Implicit Types D : set R.

Lemma oppr_measurable D : measurable_fun D -%R.

Proof.

apply: measurable_funTS => /=; apply: continuous_measurable_fun.
exact: opp_continuous.
Qed.

Lemma normr_measurable D : measurable_fun D (@normr _ R).

Proof.

move=> mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
move=> /= _ [_ [x ->] <-]; apply: measurableI => //.
have [x0|x0] := leP 0 x.
  rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic.
    by apply: measurableU; apply: measurable_itv.
  rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=.
  - have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm] => // xr;
      rewrite 2!in_itv/=.
    + by right; rewrite xr.
    + by left; rewrite ltrNr.
  - move=> rx /=.
    by rewrite ler0_norm 1?ltrNr// (le_trans (ltW rx))// lerNl oppr0.
  - by rewrite in_itv /= andbT => xr; rewrite (lt_le_trans _ (ler_norm _)).
rewrite [X in measurable X](_ : _ = setT)// predeqE => r.
by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0).
Qed.

Lemma mulrl_measurable D (k : R) : measurable_fun D ( *%R k).

Proof.

apply: measurable_funTS => /=.
by apply: continuous_measurable_fun; exact: mulrl_continuous.
Qed.

Lemma mulrr_measurable D (k : R) : measurable_fun D (fun x => x * k).

Proof.

apply: measurable_funTS => /=.
by apply: continuous_measurable_fun; exact: mulrr_continuous.
Qed.

Lemma exprn_measurable D n : measurable_fun D (fun x => x ^+ n).

Proof.

apply measurable_funTS => /=.
by apply continuous_measurable_fun; exact: exprn_continuous.
Qed.

End standard_measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ -%R) =>
  solve [exact: oppr_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ normr) =>
  solve [exact: normr_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ ( *%R _)) =>
  solve [exact: mulrl_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) =>
  solve [exact: exprn_measurable] : core.
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `exprn_measurable` instead")]
Notation measurable_exprn := exprn_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrl_measurable` instead")]
Notation measurable_mulrl := mulrl_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrr_measurable` instead")]
Notation measurable_mulrr := mulrr_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppr_measurable` instead")]
Notation measurable_oppr := oppr_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `normr_measurable` instead")]
Notation measurable_normr := normr_measurable (only parsing).

Section measurable_fun_realType.
Context d (T : measurableType d) (R : realType).
Implicit Types (D : set T) (f g : T -> R).

Lemma measurable_funD D f g :
  measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).

Proof.

move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty.
rewrite [X in measurable X](_ : _ = \bigcup_(q : rat)
  ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))).
  apply: bigcupT_measurable_rat => q; apply: measurableI.
  - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv.
  - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv.
rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]].
  rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h.
  exists r => //; rewrite setIACA setIid; split => //; split => /=.
    by rewrite h.
  by rewrite ltrBlDr addrC -ltrBlDr h.
by rewrite ltrBlDr=> afg; rewrite (lt_le_trans afg)// addrC lerD2r ltW.
Qed.

Lemma measurable_funB D f g : measurable_fun D f ->
measurable_fun D g -> measurable_fun D (f \- g).

Proof.

by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. Qed.

Lemma measurable_funM D f g :
measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g).

Proof.

move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2)
  \- (fun x => 2%:R^-1 * (f x ^+ 2)) \- (fun x => 2%:R^-1 * (g x ^+ 2))).
  apply: measurable_funB; first apply: measurable_funB.
  - apply: measurableT_comp => //.
    by apply: measurableT_comp (exprn_measurable _) _; exact: measurable_funD.
  - apply: measurableT_comp => //.
    exact: measurableT_comp (exprn_measurable _) _.
  - apply: measurableT_comp => //.
    exact: measurableT_comp (exprn_measurable _) _.
rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA.
rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK.
by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE.
Qed.

Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x < g x).

Proof.

move=> mf mg mD; apply: (measurable_fun_bool true) => //.
under eq_fun do rewrite -subr_gt0.
by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB.
Qed.

Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x <= g x).

Proof.

move=> mf mg mD; apply: (measurable_fun_bool true) => //.
under eq_fun do rewrite -subr_ge0.
by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB.
Qed.

Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x == g x).

Proof.

move=> mf mg.
rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))).
by apply: measurable_and; exact: measurable_fun_ler.
by under eq_fun do rewrite eq_le.
Qed.

Lemma measurable_maxr D f g :
measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g).

Proof.

by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //;
[exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf].
Qed.

Lemma measurable_minr D f g :
measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g).

Proof.

by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //;
[exact: measurable_fun_ltr|exact: measurable_funS mf|exact: measurable_funS mg].
Qed.

Lemma measurable_fun_sups D (h : (T -> R)^nat) n :
  (forall t, D t -> has_ubound (range (h ^~ t))) ->
  (forall m, measurable_fun D (h m)) ->
  measurable_fun D (fun x => sups (h ^~ x) n).

Proof.

move=> f_ub mf mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
move=> _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr.
by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv.
Qed.

Lemma measurable_fun_infs D (h : (T -> R)^nat) n :
  (forall t, D t -> has_lbound (range (h ^~ t))) ->
  (forall n, measurable_fun D (h n)) ->
  measurable_fun D (fun x => infs (h ^~ x) n).

Proof.

move=> lb_f mf mD; apply: (measurability (RGenInftyO.measurableE R)) =>//.
move=> _ [_ [x ->] <-]; rewrite infs_preimage // setI_bigcupr.
by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv.
Qed.

Lemma measurable_fun_limn_sup D (h : (T -> R)^nat) :
  (forall t, D t -> has_ubound (range (h ^~ t))) ->
  (forall t, D t -> has_lbound (range (h ^~ t))) ->
  (forall n, measurable_fun D (h n)) ->
  measurable_fun D (fun x => limn_sup (h ^~ x)).

Proof.

move=> f_ub f_lb mf.
have : {in D, (fun x => inf [set sups (h ^~ x) n | n in [set n | 0 <= n]%N])
              =1 (fun x => limn_sup (h^~ x))}.
  move=> t; rewrite inE => Dt; apply/esym/cvg_lim => //.
  rewrite [X in _ --> X](_ : _ = inf (range (sups (h^~t)))).
    by apply: cvg_sups_inf; [exact: f_ub|exact: f_lb].
  by congr (inf [set _ | _ in _]); rewrite predeqE.
move/eq_measurable_fun; apply; apply: measurable_fun_infs => //.
  move=> t Dt; have [M hM] := f_lb _ Dt; exists M => _ [m /= nm <-].
  rewrite (@le_trans _ _ (h m t)) //; first by apply hM => /=; exists m.
  by apply: sup_ubound; [exact/has_ubound_sdrop/f_ub|exists m => /=].
by move=> k; exact: measurable_fun_sups.
Qed.

Lemma measurable_fun_cvg D (h : (T -> R)^nat) f :
(forall m, measurable_fun D (h m)) -> (forall x, D x -> h ^~ x @ \oo --> f x) ->
measurable_fun D f.

Proof.

move=> mf_ f_f; have fE x : D x -> f x = limn_sup (h ^~ x).
move=> Dx; have /cvg_lim <-// := @cvg_sups _ (h ^~ x) (f x) (f_f _ Dx).
apply: (@eq_measurable_fun _ _ _ _ D (fun x => limn_sup (h ^~ x))).
by move=> x; rewrite inE => Dx; rewrite -fE.
apply: (@measurable_fun_limn_sup _ h) => // t Dt.
- by apply/bounded_fun_has_ubound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f.
- by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f.
Qed.

Lemma measurable_fun_indic D (U : set T) : measurable U ->
measurable_fun D (\1_U : _ -> R).

Proof.

move=> mU mD /= Y mY.
have [Y0|Y0] := pselect (Y 0%R); have [Y1|Y1] := pselect (Y 1%R).
- rewrite [X in measurable X](_ : _ = D)//.
  by apply/seteqP; split => //= r Dr /=; rewrite indicE; case: (_ \in _).
- rewrite [X in measurable (_ `&` X)](_ : _ = ~` U)//.
    by apply: measurableI => //; exact: measurableC.
  apply/seteqP; split => [//= r /= + Ur|r Ur]; rewrite /= indicE.
    by rewrite mem_set.
  by rewrite memNset.
- rewrite [X in measurable (_ `&` X)](_ : _ = U); first exact: measurableI.
  apply/seteqP; split => [//= r /=|r Ur]; rewrite /= indicE.
    by have [//|Ur] := pselect (U r); rewrite memNset.
  by rewrite mem_set.
- rewrite [X in measurable X](_ : _ = set0)//.
  by apply/seteqP; split => // r /= -[_]; rewrite indicE; case: (_ \in _).
Qed.

End measurable_fun_realType.
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")]
Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing).

Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R).

Proof.

rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first.
  by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=;
    rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP].
apply/measurable_funU => //; split.
- apply/measurable_restrictT => //=.
  rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE.
  by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW.
- have : {in `]0, +oo[%classic, continuous (@ln R)}.
    by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln.
  rewrite -continuous_open_subspace; last exact: interval_open.
  by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv.
Qed.

#[global] Hint Extern 0 (measurable_fun _ (@ln _)) =>
solve [apply: measurable_ln] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_ln` instead")]
Notation measurable_fun_ln := measurable_ln (only parsing).

Lemma measurable_expR (R : realType) : measurable_fun [set: R] expR.

Proof.

by apply: continuous_measurable_fun; exact: continuous_expR. Qed.

#[global] Hint Extern 0 (measurable_fun _ expR) =>
solve [apply: measurable_expR] : core.

Lemma natmul_measurable {R : realType} D n :
measurable_fun D (fun x : R => x *+ n).

Proof.

under eq_fun do rewrite -mulr_natr.
by do 2 apply: measurable_funM => //.
Qed.

Lemma measurable_funX d (T : measurableType d) {R : realType} D (f : T -> R) n :
measurable_fun D f -> measurable_fun D (fun x => f x ^+ n).

Proof.

move=> mf.
exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
Qed.

Lemma measurable_powR (R : realType) p :
measurable_fun [set: R] (@powR R ^~ p).

Proof.

apply: measurable_fun_if => //.
- apply: (measurable_fun_bool true).
  rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//.
  by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx.
- rewrite setTI; apply: measurableT_comp => //.
  rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp.
  by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP.
Qed.

#[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) =>
solve [apply: measurable_powR] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_powR` instead")]
Notation measurable_fun_power_pos := measurable_powR (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `measurable_powR` instead")]
Notation measurable_power_pos := measurable_powR (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")]
Notation measurable_fun_max := measurable_maxr (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")]
Notation measurable_fun_pow := measurable_funX (only parsing).

Module NGenCInfty.
Section ngencinfty.
Implicit Types x y z : nat.

Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic].

Lemma measurable_itv_bnd_infty b x :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty.
rewrite [X in measurable X](_ : _ =
    \bigcup_(k in [set k | k >= x]%N) `[k.+1, +oo[%classic); last first.
  apply/seteqP; split => [z /=|/= z [t/= xt]].
    rewrite in_itv/= andbT => xz; exists z.-1 => /=.
      by rewrite -ltnS//=; case: z xz.
    by case: z xz => //= z xz; rewrite in_itv/= lexx andbT.
  by rewrite !in_itv/= !andbT; apply: lt_le_trans; rewrite ltEnat/= ltnS.
rewrite bigcup_mkcond; apply: bigcupT_measurable => k.
by case: ifPn => //= _; apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma measurable_itv_bounded a b y : a != +oo%O ->
G.-sigma.-measurable [set` Interval a (BSide b y)].

Proof.

case: a => [a r _|[_|//]].
by rewrite set_itv_splitD; apply: measurableD; apply: measurable_itv_bnd_infty.
by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty.
Qed.

Lemma measurableE : @measurable _ nat = G.-sigma.-measurable.

Proof.

rewrite eqEsubset; split => [A mA|A]; last exact: smallest_sub.
rewrite (_ : A = \bigcup_(i in A) `[i, i.+1[%classic).
by apply: bigcup_measurable => k Ak; exact: measurable_itv_bounded.
apply/seteqP; split => [x Ax|x [k Ak]].
by exists x => //=; rewrite in_itv/= lexx/= ltEnat /= ltnS.
by rewrite /= in_itv/= leEnat ltEnat /= ltnS -eqn_leq => /eqP <-.
Qed.

End ngencinfty.
End NGenCInfty.

Section measurable_fun_nat.
Context d (T : measurableType d).
Implicit Types (D : set T) (f g : T -> nat).

Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x + g x)%N.

Proof.

move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty.
rewrite [X in measurable X](_ : _ = \bigcup_q
  ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))).
  apply: bigcupT_measurable => q; apply: measurableI.
  - by rewrite -preimage_itv_c_infty; exact: mf.
  - by rewrite -preimage_itv_c_infty; exact: mg.
rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[?]].
- move=> afxgx; exists (a - g x)%N => //=; split; split => //.
    by rewrite leEnat leq_subLR// addnC -leEnat.
  have [gxa|gxa] := leqP (g x) a; first by rewrite subKn.
  by move/ltnW : (gxa); rewrite -subn_eq0 => /eqP ->; rewrite subn0 ltW.
- rewrite leEnat leq_subLR => arg; split => //.
  by rewrite (leq_trans arg)// leq_add2r.
Qed.

Lemma measurable_fun_maxn D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => maxn (f x) (g x)).

Proof.

move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ =
  ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))).
  apply: measurableU.
  - by rewrite -preimage_itv_c_infty; exact: mf.
  - by rewrite -preimage_itv_c_infty; exact: mg.
rewrite predeqE => x; split => [[Dx /=]|].
- by rewrite in_itv/= andbT; have [fg agx|gf afx] := leqP (f x) (g x); tauto.
- move=> [[Dx /= afx]|[Dx /= agx]].
  + rewrite in_itv/= andbT; split => //.
    by rewrite (le_trans afx)// leEnat leq_maxl.
  + rewrite in_itv/= andbT; split => //.
    by rewrite (le_trans agx)// leEnat leq_maxr.
Qed.

Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N ->
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x - g x)%N.

Proof.

move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty.
rewrite [X in measurable X](_ : _ = \bigcup_q
  ((D `&` [set x | maxn a q <= f x]%O) `&`
   (D `&` [set x | g x <= (q - a)%N]%O))).
  apply: bigcupT_measurable => q; apply: measurableI.
  - by rewrite -preimage_itv_c_infty; exact: mf.
  - by rewrite -preimage_itv_infty_c; exact: mg.
rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[_]].
- move=> afxgx; exists (g x + a)%N => //; split; split => //=.
    rewrite leEnat; have /maxn_idPr -> := leq_addl (g x) a.
    by rewrite -leq_subRL.
  by rewrite leEnat addnK.
- rewrite leEnat => gxra; split => //; rewrite -(leq_add2r (g x)) subnK//.
  have [afx|afx] := leqP a (f x).
    rewrite -(@leq_sub2rE a)// addnC addnK (leq_trans gxra)// leq_sub2r//.
    by rewrite (leq_trans _ rfx)//; exact: leq_maxr.
  move: gxra; rewrite -(leq_add2l a) subnKC//; last first.
    by have := leq_ltn_trans rfx afx; rewrite ltnNge leq_maxl.
  by move=> /leq_trans; apply; rewrite (leq_trans _ rfx)//; exact: leq_maxr.
Qed.

Lemma measurable_fun_subn D f g : measurable_fun D f ->
measurable_fun D g -> measurable_fun D (fun x => f x - g x)%N.

Proof.

move=> mf mg.
rewrite [X in measurable_fun _ X](_ : _ = fun x => (maxn (f x) (g x) - g x)%N).
apply: measurable_fun_subn' => //; last exact: measurable_fun_maxn.
by move=> t; rewrite leq_maxr.
apply/funext => x; have [//|gf] := leqP (g x) (f x).
by apply/eqP; rewrite subnn subn_eq0// ltnW.
Qed.

Lemma measurable_fun_ltn D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x < g x)%N.

Proof.

move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
- have -> : (fun x => f x < g x)%O = (fun x => 0%N < (g x - f x)%N)%O.
    apply/funext => n; apply/idP/idP.
      by rewrite !ltEnat /ltn/= => fg; rewrite subn_gt0.
    by rewrite !ltEnat /ltn/= => fg; rewrite -subn_gt0.
  by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_fun_subn.
- under eq_fun do rewrite ltnNge.
  rewrite preimage_false set_predC setCK.
  rewrite [X in _ `&` X](_ : _ = \bigcup_(i in range f)
      ([set y | g y <= i]%O `&` [set t | i <= f t]%O)).
    rewrite setI_bigcupr; apply: bigcup_measurable => k fk.
    rewrite setIIr; apply: measurableI => //.
    + by rewrite -preimage_itv_infty_c; exact: mg.
    + by rewrite -preimage_itv_c_infty; exact: mf.
  apply/funext => n/=.
  suff : (g n <= f n)%N <->
      (\bigcup_(i in range f) ([set y | g y <= i]%O `&` [set t | i <= f t]%O)) n.
    by move/propext.
  split=> [gfn|[k [t _ <- []]] /=].
    by exists (f n) => //; split => /=.
  by move=> /leq_trans; apply.
- by rewrite preimage_set0 setI0.
- by rewrite preimage_setT setIT.
Qed.

Lemma measurable_fun_leq D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x <= g x)%N.

Proof.

move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
- rewrite preimage_true [X in _ `&` X](_ : _ =
      \bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)).
    rewrite setI_bigcupr; apply: bigcup_measurable => k fk.
    rewrite setIIr; apply: measurableI => //.
    + by rewrite -preimage_itv_infty_c; exact: mf.
    + by rewrite -preimage_itv_c_infty; exact: mg.
  apply/funext => n/=.
  suff : (f n <= g n)%N <->
    (\bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)) n.
    by move/propext.
  split=> [gfn|[k [t _ <- []]] /=].
    by exists (g n) => //; split => /=.
  by move=> /leq_trans; apply.
- under eq_fun do rewrite leqNgt.
  by rewrite preimage_false set_predC setCK; exact: measurable_fun_ltn.
- by rewrite preimage_set0 setI0.
- by rewrite preimage_setT setIT.
Qed.

Lemma measurable_fun_eqn D f g : measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => f x == g x).

Proof.

move=> mf mg.
rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))%N).
by apply: measurable_and; exact: measurable_fun_leq.
by under eq_fun do rewrite eq_le.
Qed.

End measurable_fun_nat.

Section standard_emeasurable_fun.
Variable R : realType.

Lemma EFin_measurable (D : set R) : measurable_fun D EFin.

Proof.

move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
move=> /= _ [_ [x ->]] <-; apply: measurableI => //.
by rewrite preimage_itv_o_infty EFin_itv; exact: measurable_itv.
Qed.

Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse.

Proof.

move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
move=> /= _ [_ [x ->] <-].
rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr.
apply: measurableU; last first.
  by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU.
apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic).
  by rewrite -[X in measurable X]setTI; exact: normr_measurable.
exists set0; first by constructor.
rewrite setU0 predeqE => -[y| |]; split => /= => -[r];
  rewrite ?/= /= ?in_itv /= ?andbT => xr//.
  + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry.
  + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry.
Qed.

Lemma oppe_measurable (D : set (\bar R)) :
measurable_fun D (-%E : \bar R -> \bar R).

Proof.

move=> mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //.
move=> _ [_ [x ->] <-]; rewrite (_ : _ @^-1` _ = `]-oo, (- x)%:E]%classic).
by apply: measurableI => //; exact: emeasurable_itv.
by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv leeNr.
Qed.

End standard_emeasurable_fun.
#[global] Hint Extern 0 (measurable_fun _ abse) =>
  solve [exact: abse_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ EFin) =>
  solve [exact: EFin_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ -%E) =>
  solve [exact: oppe_measurable] : core.
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppe_measurable` instead")]
Notation measurable_oppe := oppe_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `abse_measurable` instead")]
Notation measurable_abse := abse_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `EFin_measurable` instead")]
Notation measurable_EFin := EFin_measurable (only parsing).
#[deprecated(since="mathcomp-analysis 1.4.0", note="use `natmul_measurable` instead")]
Notation measurable_natmul := natmul_measurable (only parsing).

Lemma measurable_EFinP d (T : measurableType d) (R : realType) (D : set T)
    (g : T -> R) :
  measurable_fun D (EFin \o g) <-> measurable_fun D g.

Proof.

split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp.
rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)).
by apply: mf => //; exists A => //; exists set0; [constructor|rewrite setU0].
congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]].
by move=> ? ?; exact: preimage_image.
Qed.

#[deprecated(since="mathcomp-analysis 1.6.0", note="use `measurable_EFinP` instead")]
Notation EFin_measurable_fun := measurable_EFinP (only parsing).

Lemma measurable_fun_dirac
d {T : measurableType d} {R : realType} D (U : set T) :
measurable U -> measurable_fun D (fun x => \d_x U : \bar R).

Proof.

by move=> /measurable_fun_indic/measurable_EFinP. Qed.

Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) :
measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f).

Proof.

move=> mf;rewrite (_ : er_map _ =
fun x => if x \is a fin_num then (f (fine x))%:E else x); last first.
by apply: funext=> -[].
apply: measurable_fun_ifT => //=.
+ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num.
+ exact/measurable_EFinP/measurableT_comp.
Qed.

#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")]
Notation measurable_fun_er_map := measurable_er_map (only parsing).

Section emeasurable_fun.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Implicit Types (D : set T).

Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) :
(forall n, measurable_fun D (f n)) ->
forall n, measurable_fun D (fun x => einfs (f ^~ x) n).

Proof.

move=> mf n mD.
apply: (measurability (ErealGenCInfty.measurableE R)) => //.
move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=.
by apply: bigcap_measurableType => ? ?; exact/mf/emeasurable_itv.
Qed.

Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) :
(forall n, measurable_fun D (f n)) ->
forall n, measurable_fun D (fun x => esups (f ^~ x) n).

Proof.

move=> mf n mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
move=> _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr.
by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv.
Qed.

Lemma measurable_maxe D (f g : T -> \bar R) :
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => maxe (f x) (g x)).

Proof.

move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //.
move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ =
    (D `&` f @^-1` `[x%:E, +oo[) `|` (D `&` g @^-1` `[x%:E, +oo[)); last first.
  rewrite predeqE => t /=; split.
    by rewrite !/= /= !in_itv /= !andbT le_max => -[Dx /orP[|]];
      tauto.
  by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_max;
    move=> [Dx ->]//; rewrite orbT.
by apply: measurableU; [exact/mf/emeasurable_itv| exact/mg/emeasurable_itv].
Qed.

Lemma measurable_funepos D (f : T -> \bar R) :
measurable_fun D f -> measurable_fun D f^\+.

Proof.

by move=> mf; exact: measurable_maxe. Qed.

Lemma measurable_funeneg D (f : T -> \bar R) :
measurable_fun D f -> measurable_fun D f^\-.

Proof.

by move=> mf; apply: measurable_maxe => //; exact: measurableT_comp. Qed.

Lemma measurable_mine D (f g : T -> \bar R) :
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun x => mine (f x) (g x)).

Proof.

move=> mf mg; rewrite (_ : (fun _ => _) = (fun x => - maxe (- f x) (- g x))).
apply: measurableT_comp => //.
by apply: measurable_maxe; exact: measurableT_comp.
by rewrite funeqE => x; rewrite oppe_max !oppeK.
Qed.

Lemma measurable_fun_limn_esup D (f : (T -> \bar R)^nat) :
(forall n, measurable_fun D (f n)) ->
measurable_fun D (fun x => limn_esup (f ^~ x)).

Proof.

move=> mf mD; rewrite (_ : (fun _ => _) =
    (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])).
  by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups.
rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //.
rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))).
  exact: cvg_esups_inf.
by congr (ereal_inf [set _ | _ in _]); rewrite predeqE.
Qed.

Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) :
(forall m, measurable_fun D (f_ m)) ->
(forall x, D x -> f_ ^~ x @ \oo --> f x) -> measurable_fun D f.

Proof.

move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x).
  rewrite limn_esup_lim.
  by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx).
apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //.
  by move=> x; rewrite inE => Dx; rewrite fE.
exact: measurable_fun_limn_esup.
Qed.

End emeasurable_fun.
Arguments emeasurable_fun_cvg {d T R D} f_.

#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurableT_comp` instead")]
Notation emeasurable_funN := measurableT_comp (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")]
Notation emeasurable_fun_max := measurable_maxe (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mine` instead")]
Notation emeasurable_fun_min := measurable_mine (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")]
Notation emeasurable_fun_funepos := measurable_funepos (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funeneg` instead")]
Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")]
Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing).

Section open_itv_cover.
Context {R : realType}.
Implicit Types (A : set R).
Local Open Scope ereal_scope.

Let l := (@wlength R idfun).

Lemma outer_measure_open_itv_cover A : (l^* A)%mu =
ereal_inf [set \sum_(k <oo) l (F k) | F in open_itv_cover A].

Proof.

apply/eqP; rewrite eq_le; apply/andP; split.
- apply: le_ereal_inf => _ /= [F [Fitv AF <-]].
  exists (fun i => `](sval (cid (Fitv i))).1, (sval (cid (Fitv i))).2]%classic).
  + split=> [i|].
    * have [?|?] := ltP (sval (cid (Fitv i))).1 (sval (cid (Fitv i))).2.
      - by apply/ocitvP; right; exists (sval (cid (Fitv i))).
      - by apply/ocitvP; left; rewrite set_itv_ge// -leNgt.
    * apply: (subset_trans AF) => r /= [n _ Fnr]; exists n => //=.
      have := Fitv n; move: Fnr; case: cid => -[x y]/= ->/= + _.
      exact: subset_itv_oo_oc.
  + apply: eq_eseriesr => k _; rewrite /l wlength_itv/=.
    case: (Fitv k) => /= -[a b]/= Fkab.
    by case: cid => /= -[x1 x2] ->; rewrite wlength_itv.
- have [/lb_ereal_inf_adherent lA|] :=
      boolP ((l^* A)%mu \is a fin_num); last first.
    rewrite ge0_fin_numE ?outer_measure_ge0// -leNgt leye_eq => /eqP ->.
    exact: leey.
  apply/lee_addgt0Pr => /= e e0.
  have : (0 < e / 2)%R by rewrite divr_gt0.
  move=> /lA[_ [/= F [mF AF]] <-]; rewrite -/((l^* A)%mu) => lFe.
  have Fcover n : exists2 B, F n `<=` B &
      is_open_itv B /\ l B <= l (F n) + (e / 2 ^+ n.+2)%:E.
    have [[a b] _ /= abFn] := mF n.
    exists `]a, b + e / 2^+n.+2[%classic.
      rewrite -abFn => x/= /[!in_itv] /andP[->/=] /le_lt_trans; apply.
      by rewrite ltrDl divr_gt0.
    split; first by exists (a, b + e / 2^+n.+2).
    have [ab|ba] := ltP a b.
      rewrite /l -abFn !wlength_itv//= !lte_fin ifT.
        by rewrite ab -!EFinD lee_fin addrAC.
      by rewrite ltr_wpDr// divr_ge0// ltW.
    rewrite -abFn [in leRHS]set_itv_ge ?bnd_simp -?leNgt// /l wlength0 add0r.
    rewrite wlength_itv//=; case: ifPn => [abe|_]; last first.
      by rewrite lee_fin divr_ge0// ltW.
    by rewrite -EFinD addrAC lee_fin -[leRHS]add0r lerD2r subr_le0.
  pose G := fun n => sval (cid2 (Fcover n)).
  have FG n : F n `<=` G n by rewrite /G; case: cid2.
  have Gitv n : is_open_itv (G n) by rewrite /G; case: cid2 => ? ? [].
  have lGFe n : l (G n) <= l (F n) + (e / 2 ^+ n.+2)%:E.
    by rewrite /G; case: cid2 => ? ? [].
  have AG : A `<=` \bigcup_k G k.
    by apply: (subset_trans AF) => [/= r [n _ /FG Gnr]]; exists n.
  apply: (@le_trans _ _ (\sum_(0 <= k <oo) (l (F k) + (e / 2 ^+ k.+2)%:E))).
    apply: (@le_trans _ _ (\sum_(0 <= k <oo) l (G k))).
      by apply: ereal_inf_lbound => /=; exists G.
    exact: lee_nneseries.
  rewrite nneseriesD//; last first.
    by move=> i _; rewrite lee_fin// divr_ge0// ltW.
  rewrite [in leRHS](splitr e) EFinD addeA leeD//; first exact/ltW.
  have := @cvg_geometric_eseries_half R e 1; rewrite expr1.
  rewrite [X in eseries X](_ : _ = (fun k => (e / (2 ^+ (k.+2))%:R)%:E)); last first.
    by apply/funext => n; rewrite addn2 natrX.
  move/cvg_lim => <-//; apply: lee_nneseries => //.
  - by move=> n _; rewrite lee_fin divr_ge0// ltW.
  - by move=> n _; rewrite lee_fin -natrX.
Qed.

End open_itv_cover.

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

Local Open Scope ereal_scope.

Lemma pointwise_almost_uniform
    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
  (forall n, measurable_fun A (f n)) ->
  measurable A -> mu A < +oo -> (forall x, A x -> f ^~ x @ \oo --> g x) ->
  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
    {uniform A `\` B, f @ \oo --> g}].

Proof.

move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R.
have mfunh q : measurable_fun A (h q).
  apply: measurableT_comp => //; apply: measurable_funB => //.
  exact: measurable_fun_cvg.
pose E k n := \bigcup_(i >= n) (A `&` [set x | h i x >= k.+1%:R^-1]%R).
have Einc k : nonincreasing_seq (E k).
  move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?].
  by exists i => //; exact: mi.
have mE k n : measurable (E k n).
  apply: bigcup_measurable => q /= ?.
  have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[.
    by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT.
  exact: mfunh.
have nEcvg x k : exists n, A x -> (~` E k n) x.
  have [Ax|?] := pselect (A x); last by exists point.
  have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)).
    by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx].
  move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni.
  apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC.
  by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
have Ek0 k : \bigcap_n (E k n) = set0.
  rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by [].
  rewrite setC_bigcap; have [Az | nAz] := pselect (A z).
    by have [N /(_ Az) ?] := nEcvg z k; exists N.
  by exists 0%N => //; rewrite setC_bigcup => n _ [].
have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E.
  pose ek : R := eps / 2 / (2 ^ k.+1)%:R.
  have : mu \o E k @ \oo --> mu set0.
    rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //.
    - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
    - exact: bigcap_measurable.
  rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))).
    apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)).
    by rewrite !divr_gt0.
  move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN.
  rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//.
  by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k E k (badn k)); split.
- exact: bigcup_measurable.
- apply: (@le_lt_trans _ _ (eps / 2)%:E); first last.
    by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1.
  apply: le_trans.
    apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //.
    exact: bigcup_measurable.
  apply: le_trans; first last.
    by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// ltW.
  by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))).
apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT.
case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU.
have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del.
exists (badn N) => // r badNr x.
rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel).
move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I).
rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//.
by move/negP; rewrite ltNge // distrC.
Qed.

Lemma ae_pointwise_almost_uniform
    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
  (forall n, measurable_fun A (f n)) -> measurable_fun A g ->
  measurable A -> mu A < +oo ->
  {ae mu, (forall x, A x -> f ^~ x @ \oo --> g x)} ->
  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
    {uniform A `\` B, f @ \oo --> g}].

Proof.

move=> mf mg mA Afin [C [mC C0 nC] epspos].
have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
    {uniform (A `\` C) `\` B, f @ \oo --> g}].
  apply: pointwise_almost_uniform => //.
  - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
  - by apply: measurableI => //; exact: measurableC.
  - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD.
  - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact.
exists (B `|` C); split.
- exact: measurableU.
- by apply: (le_lt_trans _ Beps); rewrite measureU0.
- by rewrite setUC -setDDl.
Qed.

End egorov.

Module LebesgueMeasure.
Section hlength.
Context {R : realType}.
Local Open Scope ereal_scope.
Implicit Types i j : interval R.

Definition hlength (A : set (ocitv_type R)) : \bar R :=
let i := Rhull A in (i.2 : \bar R) - i.1.

Lemma hlength0 : hlength (set0 : set R) = 0.

Proof.

by rewrite /hlength Rhull0 /= subee. Qed.

Lemma hlength_singleton (r : R) : hlength `[r, r] = 0.

Proof.

rewrite /hlength /= asboolT// sup_itvcc//= asboolT//.
by rewrite asboolT inf_itvcc//= ?subee// inE.
Qed.

Lemma hlength_setT : hlength setT = +oo%E :> \bar R.

Proof.

by rewrite /hlength RhullT. Qed.

Lemma hlength_itv i :
hlength [set` i] = if i.2 > i.1 then (i.2 : \bar R) - i.1 else 0.

Proof.

case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK.
rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first.
  rewrite (_ : [set` i] = set0) ?hlength0//.
  by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12).
case: i => -[ba a|[|]] [bb b|[|]] //=.
- rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try
    by rewrite set_itvE hlength0.
  by rewrite hlength_singleton.
- by move=> _; rewrite set_itvE hlength0.
- by move=> _; rewrite set_itvE hlength0.
Qed.

Lemma hlength_finite_fin_num i : neitv i -> hlength [set` i] < +oo ->
((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num).

Proof.

move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx.
by move=> _; rewrite hlength_itv /= ltry.
by move=> _; rewrite hlength_itv /= ltNyr.
by move=> _; rewrite hlength_itv.
Qed.

Lemma finite_hlength_itv i : neitv i -> hlength [set` i] < +oo ->
hlength [set` i] = (fine i.2)%:E - (fine i.1)%:E.

Proof.

move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo.
rewrite !fineK// hlength_itv; case: ifPn => //.
rewrite -leNgt le_eqVlt => /predU1P[->|]; first by rewrite subee.
by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->.
Qed.

Lemma hlength_infty_bnd b r :
hlength [set` Interval -oo%O (BSide b r)] = +oo :> \bar R.

Proof.

by rewrite hlength_itv /= ltNyr. Qed.

Lemma hlength_bnd_infty b r :
hlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R.

Proof.

by rewrite hlength_itv /= ltry. Qed.

Lemma infinite_hlength_itv i : hlength [set` i] = +oo ->
(exists s r, i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O)
\/ i = `]-oo, +oo[.

Proof.

rewrite hlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|].
- by case: ifPn.
- by left; exists ba, a; right.
- by left; exists bb, b; left.
- by right.
Qed.

Lemma hlength_itv_ge0 i : 0 <= hlength [set` i].

Proof.

rewrite hlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |].
- by rewrite suber_ge0//; exact: ltW.
- by rewrite ltNge leey.
- by move=> i2gtNy; rewrite addey//; case: (i.2 : \bar R) i2gtNy.
Qed.

Lemma hlength_Rhull (A : set R) : hlength [set` Rhull A] = hlength A.

Proof.

by rewrite /hlength Rhull_involutive. Qed.

Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j].

Proof.

set I := [set` i]; set J := [set` j].
have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_itv_ge0.
have [J0|/set0P J0] := eqVneq J set0.
  by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->.
move=> /subset_itvP ij; apply: leeB => /=.
  have [ui|ui] := asboolP (has_ubound I).
    have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
    by rewrite lee_fin le_sup // => r Ir; exists r; split => //; apply: ij.
  have [uj /=|//] := asboolP (has_ubound J).
  by move: ui; have := subset_has_ubound ij uj.
have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
have [li /=|li] := asboolP (has_lbound I); last first.
  by move: li; have := subset_has_lbound ij lj.
rewrite lee_fin lerNl opprK le_sup// ?has_inf_supN//; last exact/nonemptyN.
move=> r [r' Ir' <-{r}]; exists (- r')%R.
by split => //; exists r' => //; apply: ij.
Qed.

Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}.

Proof.

move=> a b /le_Rhull /le_hlength_itv.
by rewrite (hlength_Rhull a) (hlength_Rhull b).
Qed.

Lemma hlength_ge0 I : (0 <= hlength I)%E.

Proof.

by rewrite -hlength0 le_hlength. Qed.

End hlength.
#[local] Hint Extern 0 (is_true (0%R <= hlength _)) =>
solve[apply: hlength_ge0] : core.

Section hlength_extension.
Context {R : realType}.

Notation hlength := (@hlength R).

Lemma hlength_semi_additive : measure.semi_additive hlength.

Proof.

move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->.
rewrite hlength_itv ?lte_fin/= -EFinB.
case: ifPn => a12; last first.
  pose I i := `](b i).1, (b i).2]%classic.
  rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0.
  by under eq_bigr => i _ do rewrite I0//= hlength0; rewrite big1.
set A := `]a1, a2]%classic.
rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//.
move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *.
rewrite ltnS => cP /esym AE.
have : A a2 by rewrite /A /= in_itv/= lexx andbT.
rewrite AE/= => -[i /= Pi] a2bi.
case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi.
have {}a2bi : a2 = (b i).2.
  apply/eqP; rewrite eq_le (itvP a2bi)/=.
  suff: A (b i).2 by move=> /itvP->.
  by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT.
rewrite {a2}a2bi in a12 A AE *.
rewrite (bigD1 i)//= hlength_itv ?lte_fin/= bi !EFinD -addeA.
congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//.
rewrite ?EFinN oppeK addeC; apply/eqP.
case: (eqVneq a1 (b i).1) => a1bi.
  rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j.
  move=> /andP[Pj Nji]; rewrite hlength_itv ?lte_fin/=; case: ifPn => bj//.
  exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv.
  pose m := ((b j).1 + (b j).2) / 2%:R.
  have mbj : `](b j).1, (b j).2]%classic m.
     by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW.
  rewrite -subset0 => /(_ m); apply; split=> //.
  by suff: A m by []; rewrite AE; exists j => //.
have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2.
  move=> Pj bj; suff /itvP-> : A (b j).2 by [].
  by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=.
have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1.
  move=> Pj bj; case: ltP=> // bj1a.
  suff : A a1 by rewrite /A/= in_itv/= ltxx.
  by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2.
have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2.
  move=> Pj bj; suff /itvP-> : A (b j).2 by [].
  by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=.
apply/IHp.
- by rewrite lt_neqAle a1bi/= a1b.
- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P).
  rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first.
    by move=> j; rewrite !inE andbC; case: eqVneq => // ->.
  rewrite ?card1 ?ltnS// subset_leq_card//.
  by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC.
apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi].
  case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge.
  apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt.
  have /trivIsetP/(_ j i I I Nji) := Itriv.
  rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2.
  by rewrite !in_itv/= bj !lexx bi1j2 bbi2.
have: A x.
  rewrite /A/= in_itv/= (itvP xabi)/= ltW//.
  by rewrite (le_lt_trans _ bi) ?(itvP xabi).
rewrite AE => -[j /= Pj xbj].
exists j => //=.
apply/andP; split=> //; apply: contraTneq xbj => ->.
by rewrite in_itv/= le_gtF// (itvP xabi).
Qed.

HB.instance Definition _ := isContent.Build _ _ R
hlength hlength_ge0 hlength_semi_additive.

Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core.

Lemma hlength_sigma_subadditive :
measurable_subset_sigma_subadditive (hlength : set (ocitv_type R) -> _).

Proof.

move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-].
rewrite /subset_sigma_subadditive hlength_itv ?lte_fin/= -EFinB => lebig.
case: ifPn => a12; last by rewrite nneseries_esum// esum_ge0.
apply/lee_addgt0Pr => _ /posnumP[e].
rewrite [e%:num]splitr [in leRHS]EFinD addeA -leeBlDr//.
apply: le_trans (epsilon_trick _ _ _) => //=.
have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R.
  by rewrite divr_gt0// ltr0n// expn_gt0.
have eVn_ge0 n := ltW (eVn_gt0 n).
pose Aoo i : set (ocitv_type R) :=
  `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic.
pose Aoc i : set (ocitv_type R) :=
  `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R]%classic.
have: `[a.1 + e%:num / 2, a.2] `<=` \bigcup_i Aoo i.
  apply: (@subset_trans _ `]a.1, a.2]).
    move=> x; rewrite /= !in_itv /= => /andP[+ -> //].
    by move=> /lt_le_trans-> //; rewrite ltrDl.
  apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=.
  move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=.
  by rewrite ltrDl.
have := @segment_compact _ (a.1 + e%:num / 2) a.2; rewrite compact_cover.
move=> /[apply]-[i _|X _ Xc]; first exact: interval_open.
have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i.
  move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix.
  by exists i => //; apply: subset_itv_oo_oc Aooix.
have /[apply] := @content_sub_fsum _ _ _
  [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X].
move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans.
  rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD.
  by case: ltP => //; rewrite lee_fin subr_le0.
rewrite nneseries_esum//; last by move=> *; rewrite adde_ge0//= ?lee_fin.
rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=.
rewrite fsbig_finite//= set_fsetK//.
rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=.
do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW.
  by rewrite addrAC.
by rewrite addrAC lee_fin lerD// subr_le0 leNgt.
Qed.

HB.instance Definition _ := Content_SigmaSubAdditive_isMeasure.Build _ _ _
hlength hlength_sigma_subadditive.

Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _).

Proof.

exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT.
by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry.
Qed.

Definition lebesgue_measure := measure_extension hlength.
HB.instance Definition _ := Measure.on lebesgue_measure.

Let sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.

Proof.

exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.

HB.instance Definition _ := @isSigmaFinite.Build _ _ _
  lebesgue_measure sigmaT_finite_lebesgue_measure.

End hlength_extension.

End LebesgueMeasure.

Definition lebesgue_measure {R : realType} :
  set [the measurableType _.-sigma of
       g_sigma_algebraType R.-ocitv.-measurable] -> \bar R :=
  [the measure _ _ of lebesgue_stieltjes_measure idfun].
HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
HB.instance Definition _ (R : realType) :=
  SigmaFiniteMeasure.on (@lebesgue_measure R).

Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R :=
  [the measure _ _ of completed_lebesgue_stieltjes_measure idfun].
HB.instance Definition _ (R : realType) :=
  Measure.on (@completed_lebesgue_measure R).
HB.instance Definition _ (R : realType) :=
  SigmaFiniteMeasure.on (@completed_lebesgue_measure R).

Lemma completed_lebesgue_measure_is_complete {R : realType} :
  measure_is_complete (@completed_lebesgue_measure R).

Proof.

exact: measure_is_complete_caratheodory. Qed.

Section completed_algebra_caratheodory.
Context {R : realType}.
Local Open Scope ereal_scope.

Notation hlength := (@wlength R idfun).
Notation mu := (@lebesgue_measure R).
Notation completed_mu := (@completed_lebesgue_measure R).

Let cara_sub_calgebra : hlength^*%mu.-cara.-measurable `<=`
(completed_algebra_gen mu).-sigma.-measurable.

Proof.

move=> E; wlog : E / completed_mu E < +oo.
  move=> /= wlg.
  have /sigma_finiteP[/= F [UFI ndF mF]] :=
    measure_extension_sigma_finite (@wlength_sigma_finite R idfun).
  move=> mE.
  rewrite -(setIT E)/= UFI setI_bigcupr; apply: bigcupT_measurable => i.
  apply: wlg.
  - rewrite (le_lt_trans _ (mF i).2)//= le_measure// inE/=.
    + by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1.
    + by apply: sub_caratheodory; exact: (mF i).1.
  - by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1.
move=> mEoo /= mE.
have inv0 n : (0 < n.+1%:R^-1 :> R)%R by rewrite invr_gt0.
set S := [set \sum_(0 <= k <oo) hlength (A k) | A in measurable_cover E].
have coverE s : (0 < s)%R ->
   exists2 A, @measurable_cover _ (ocitv_type R) E A &
   \sum_(0 <= k <oo) hlength (A k) < completed_mu E + s%:E.
  move=> s0; have : mu E \is a fin_num by rewrite ge0_fin_numE.
  by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [A EA] <-] ?; exists A.
pose A n := projT1 (cid2 (coverE _ (inv0 n))).
have mA k : @measurable_cover _ (ocitv_type R) E (A k).
  by rewrite /A; case: cid2.
have mA_E n :
    \sum_(0 <= k <oo) hlength (A n k) < completed_mu E + n.+1%:R^-1%:E.
  by rewrite /A; case: cid2.
pose F_ n := \bigcup_m (A n m).
have EF_n n : E `<=` F_ n.
  have [/= _] := mA n.
  by move=> /subset_trans; apply; apply: subset_bigcup => i _.
have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E.
  apply: (le_lt_trans _ (mA_E m)).
  apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (A m))).
  apply: lee_nneseries => // n _.
  by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m.
pose F := \bigcap_n (F_ n).
have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F.
  apply: bigcapT_measurable => k; apply: bigcupT_measurable => i.
  by apply: sub_sigma_algebra; have [/(_ i)] := mA k.
have EF : E `<=` F by exact: sub_bigcap.
have muEF : completed_mu E = mu F.
  apply/eqP; rewrite eq_le le_outer_measure//=.
  apply/lee_addgt0Pr => /= _/posnumP[e]; near \oo => n.
  apply: (@le_trans _ _ (mu (F_ n))).
    by apply: le_outer_measure; exact: bigcap_inf.
  rewrite (le_trans (ltW (mF_ n)))// leeD// lee_fin ltW//.
  by near: n; apply: near_infty_natSinv_lt.
have coverEF s : (0 < s)%R ->
     exists2 A, @measurable_cover _ (ocitv_type R) (F `\` E) A &
     \sum_(0 <= k <oo) hlength (A k) < completed_mu (F `\` E) + s%:E.
  move=> s0.
  have : mu (F `\` E) \is a fin_num.
    rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu F))//; last by rewrite -muEF.
    by apply: le_outer_measure; exact: subDsetl.
  by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [B FEB] <-] ?; exists B.
pose B n := projT1 (cid2 (coverEF _ (inv0 n))).
have mB k : @measurable_cover _ (ocitv_type R) (F `\` E) (B k).
  by rewrite /B; case: cid2.
have mB_FE n :
    \sum_(0 <= k <oo) hlength (B n k) < completed_mu (F `\` E) + n.+1%:R^-1%:E.
  by rewrite /B; case: cid2.
pose G_ n := \bigcup_m (B n m).
have FEG_n n : F `\` E `<=` G_ n.
  have [/= _] := mB n.
  by move=> /subset_trans; apply; apply: subset_bigcup => i _.
have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E.
  apply: (le_lt_trans _ (mB_FE m)).
  apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (B m))).
  apply: lee_nneseries => // n _.
  by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m.
pose G := \bigcap_n (G_ n).
have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G.
  apply: bigcapT_measurable => k; apply: bigcupT_measurable => i.
  by apply: sub_sigma_algebra; have [/(_ i)] := mB k.
have FEG : F `\` E `<=` G by exact: sub_bigcap.
have muG : mu G = 0.
  transitivity (completed_mu (F `\` E)).
    apply/eqP; rewrite eq_le; apply/andP; split; last exact: le_outer_measure.
    apply/lee_addgt0Pr => _/posnumP[e].
    near \oo => n.
    apply: (@le_trans _ _ (mu (G_ n))).
      by apply: le_outer_measure; exact: bigcap_inf.
    rewrite (le_trans (ltW (mG_ n)))// leeD// lee_fin ltW//.
    by near: n; apply: near_infty_natSinv_lt.
  rewrite measureD//=.
  + by rewrite setIidr// muEF subee// ge0_fin_numE//; move: mEoo; rewrite muEF.
  + exact: sub_caratheodory.
  + by move: mEoo; rewrite muEF.
apply: sub_sigma_algebra; exists (F `\` G); first exact: measurableD.
exists (E `&` G).
  by apply: (@negligibleS _ _ _ mu G _ (@subIsetr _ E G)); exists G; split.
apply/seteqP; split=> [/= x [[Fx Gx]|[]//]|x Ex].
- by rewrite -(notK (E x)) => Ex; apply: Gx; exact: FEG.
- have [|FGx] := pselect ((F `\` G) x); first by left.
  right; split => //.
  move/not_andP : FGx => [|].
    by have := EF _ Ex.
  by rewrite notK.
Unshelve. all: by end_near. Qed.

Lemma g_sigma_completed_algebra_genE :
(completed_algebra_gen mu).-sigma.-measurable = completed_algebra_gen mu.

Proof.

apply/seteqP; split; last first.
  move=> _ [/= A /= mA [N neglN]] <-.
  by apply: sub_sigma_algebra; exists A => //; exists N.
apply: smallest_sub => //=; split => /=.
- by exists set0 => //; exists set0; [exact: negligible_set0|rewrite setU0].
- move=> G [/= A mA [N negN ANG]]; case: negN => /= F [mF F0 NF].
  have GANA : ~` G = ~` A `\` (N `&` ~` A).
    by rewrite -ANG setCU setDE setCI setCK setIUr setICl setU0.
  pose AA := ~` A `\` (F `&` ~` A).
  pose NN := (F `&` ~` A) `\` (N `&` ~` A).
  have GAANN : ~` G = AA `|` NN.
    rewrite (_ : ~` G = ~` A `\` (N `&` ~` A))//.
    by apply: setDU; [exact: setSI|exact: subIsetr].
  exists AA.
    apply: measurableI => //=; first exact: measurableC.
    by apply: measurableC; apply: measurableI => //; exact: measurableC.
  by exists NN; [exists F; split => // x [] []|rewrite setDE setTI].
- move=> F mF/=.
  pose A n := projT1 (cid2 (mF n)).
  pose N n := projT1 (cid2 (projT2 (cid2 (mF n))).2).
  exists (\bigcup_k A k).
    by apply: bigcupT_measurable => i; rewrite /A; case: cid2.
  exists (\bigcup_k N k).
    apply: negligible_bigcup => /= k.
    by rewrite /N; case: (cid2 (mF k)) => //= *; case: cid2.
  rewrite -bigcupU; apply: eq_bigcup => // i _.
  by rewrite /A /N; case: (cid2 (mF i)) => //= *; case: cid2.
Qed.

Lemma negligible_sub_caratheodory :
completed_mu.-negligible `<=` hlength^*%mu.-cara.-measurable.

Proof.

move=> N /= [/= A] [mA A0 NA].
apply: le_caratheodory_measurable => /= X.
apply: (@le_trans _ _ (hlength^*%mu N + hlength^*%mu (X `&` ~` N))).
by rewrite leeD2r// le_outer_measure//; exact: subIsetr.
have -> : hlength^*%mu N = 0.
by apply/eqP; rewrite eq_le outer_measure_ge0//= andbT -A0 le_outer_measure.
by rewrite add0e// le_outer_measure//; exact: subIsetl.
Qed.

Let calgebra_sub_cara : (completed_algebra_gen mu).-sigma.-measurable `<=`
hlength^*%mu.-cara.-measurable.

Proof.

rewrite g_sigma_completed_algebra_genE => A -[/= X mX] [N negN] <-{A}.
apply: measurableU => //; first exact: sub_caratheodory.
apply: negligible_sub_caratheodory; case: negN => /= B [mB B0 NB].
by exists B; split => //=; exact: sub_caratheodory.
Qed.

Lemma completed_caratheodory_measurable :
(completed_algebra_gen mu).-sigma.-measurable =
hlength^*%mu.-cara.-measurable.

Proof.

by apply/seteqP; split; [exact: calgebra_sub_cara | exact: cara_sub_calgebra].
Qed.

End completed_algebra_caratheodory.

Section elebesgue_measure.
Variable R : realType.

Definition elebesgue_measure : set \bar R -> \bar R :=
fun S => lebesgue_measure (fine @` (S `\` [set -oo; +oo]%E)).

Lemma elebesgue_measure0 : elebesgue_measure set0 = 0%E.

Proof.

by rewrite /elebesgue_measure set0D image_set0 measure0. Qed.

Lemma elebesgue_measure_ge0 X : (0 <= elebesgue_measure X)%E.

Proof.

exact/measure_ge0. Qed.

Lemma semi_sigma_additive_elebesgue_measure :
semi_sigma_additive elebesgue_measure.

Proof.

move=> /= F mF tF mUF; rewrite /elebesgue_measure.
rewrite [X in lebesgue_measure X](_ : _ =
    \bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first.
  rewrite predeqE => r; split.
    by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x.
  by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n.
apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R)
  (fun n => fine @` (F n `\` [set -oo; +oo]%E))).
- move=> n; have := mF n.
  move=> [X mX [X' mX']] XX'Fn.
  apply: measurable_image_fine.
  rewrite -XX'Fn.
  apply: measurableU; first exact: measurable_image_EFin.
  by case: mX' => //; exact: measurableU.
- move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]].
  move: tF => /(_ i j Logic.I Logic.I); apply.
  suff ab : a = b by exists a; split => //; rewrite ab.
  move: a b {Fia Fjb} aoo boo ax bx.
  move=> [a| |] [b| |] /=.
  + by move=> _ _ -> ->.
  + by move=> _; rewrite not_orP => -[_]/(_ erefl).
  + by move=> _; rewrite not_orP => -[]/(_ erefl).
  + by rewrite not_orP => -[_]/(_ erefl).
  + by rewrite not_orP => -[_]/(_ erefl).
  + by rewrite not_orP => -[_]/(_ erefl).
  + by rewrite not_orP => -[]/(_ erefl).
  + by rewrite not_orP => -[]/(_ erefl).
  + by rewrite not_orP => -[]/(_ erefl).
- move: mUF.
  rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}.
  - rewrite setU0 => h.
    rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
      move=> -[n _ [x [Fnx xoo <-{r}]]].
      have : (\bigcup_n F n) x by exists n.
      by rewrite -h => -[x' Xx' <-].
    have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r.
    by exists n => //; exists r%:E => //; split => //; case.
  - move=> h.
    rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
      move=> -[n _ [x [Fnx xoo <-]]].
      have : (\bigcup_n F n) x by exists n.
      by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[].
    have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r.
    by exists n => //; exists r%:E => //; split => //; case.
  - (* NB: almost the same as the previous one, factorize?*)
    move=> h.
    rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
      move=> -[n _ [x [Fnx xoo <-]]].
      have : (\bigcup_n F n) x by exists n.
      by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[].
    have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r.
    by exists n => //; exists r%:E => //; split => //; case.
  - move=> h.
    rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr].
      move=> -[n _ [x [Fnx xoo <-]]].
      have : (\bigcup_n F n) x by exists n.
      by rewrite -h => -[[x' Xx' <-//]|].
    have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r.
    by exists n => //; exists r%:E => //; split => //; case.
Qed.

HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure
  elebesgue_measure0 elebesgue_measure_ge0
  semi_sigma_additive_elebesgue_measure.

End elebesgue_measure.

Section lebesgue_measure_itv.
Variable R : realType.

Let lebesgue_measure_itvoc (a b : R) :
  (lebesgue_measure (`]a, b] : set R) =
  wlength [the cumulative _ of idfun] `]a, b])%classic.

Proof.

rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=.
by rewrite measurable_mu_extE//; exact: is_ocitv.
Qed.

Let lebesgue_measure_itvoo_subr1 (a : R) :
lebesgue_measure (`]a - 1, a[%classic : set R) = 1%E.

Proof.

rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o
    (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))).
  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
  - by move=> ?; exact: measurable_itv.
  - by apply: bigcup_measurable => k _; exact: measurable_itv.
  - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=].
    by move/le_trans; apply; rewrite lerB// ler_pV2 ?ler_nat//;
      rewrite inE ltr0n andbT unitfE.
rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first.
  apply/funext => n /=; rewrite lebesgue_measure_itvoc.
  have [->|n0] := eqVneq n 0%N.
    by rewrite invr1 subrr set_itvoc0 wlength0.
  rewrite wlength_itv/= lte_fin ifT; last first.
    by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n.
  by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e.
apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW.
apply/(@cvgrPdist_lt _ [the pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e].
near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//.
by near: n; exact: near_infty_natSinv_lt.
Unshelve. all: by end_near. Qed.

Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0%E.

Proof.

suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) =
        lebesgue_measure (`]a - 1, a[%classic%R : set R) +
        lebesgue_measure [set a])%E.
  rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP.
  rewrite wlength_itv lte_fin ltrBlDr ltrDl ltr01.
  rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e.
  by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP.
rewrite -setUitv1// ?bnd_simp; last by rewrite ltrBlDr ltrDl.
rewrite measureU //; apply/seteqP; split => // x []/=.
by rewrite in_itv/= => + xa; rewrite xa ltxx andbF.
Qed.

Let lebesgue_measure_itvoo (a b : R) :
(lebesgue_measure (`]a, b[ : set R) =
wlength [the cumulative _ of idfun] `]a, b[)%classic.

Proof.

have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
have := lebesgue_measure_itvoc a b.
rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//.
- by have /= -> := lebesgue_measure_set1 b; rewrite adde0.
- by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF.
Qed.

Let lebesgue_measure_itvcc (a b : R) :
(lebesgue_measure (`[a, b] : set R) =
wlength [the cumulative _ of idfun] `[a, b])%classic.

Proof.

have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
have := lebesgue_measure_itvoc a b.
rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
- by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
Qed.

Let lebesgue_measure_itvco (a b : R) :
(lebesgue_measure (`[a, b[ : set R) =
wlength [the cumulative _ of idfun] `[a, b[)%classic.

Proof.

have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
have := lebesgue_measure_itvoo a b.
rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
- by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
Qed.

Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) :
lebesgue_measure ([set` Interval (BSide x a) (BSide y b)] : set R) =
wlength [the cumulative _ of idfun] [set` Interval (BSide x a) (BSide y b)].

Proof.

Let limnatR : lim (((k%:R)%:E : \bar R) @[k --> \oo]) = +oo%E.

Proof.

by apply/cvg_lim => //; apply/cvgenyP. Qed.

Let lebesgue_measure_itv_bnd_infty x (a : R) :
lebesgue_measure ([set` Interval (BSide x a) +oo%O] : set R) = +oo%E.

Proof.

rewrite itv_bnd_infty_bigcup; transitivity (limn (lebesgue_measure \o
    (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))).
  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
  + by move=> k; exact: measurable_itv.
  + by apply: bigcup_measurable => k _; exact: measurable_itv.
  + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=].
    by move=> /le_trans; apply; rewrite lerD// ler_nat.
rewrite (_ : _ \o _ = (fun k => k%:R%:E))//.
apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/=.
rewrite lte_fin; have [->|n0] := eqVneq n 0%N; first by rewrite addr0 ltxx.
by rewrite ltrDl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e.
Qed.

Let lebesgue_measure_itv_infty_bnd y (b : R) :
lebesgue_measure ([set` Interval -oo%O (BSide y b)] : set R) = +oo%E.

Proof.

rewrite itv_infty_bnd_bigcup; transitivity (limn (lebesgue_measure \o
    (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))).
  apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.
  + by move=> k; exact: measurable_itv.
  + by apply: bigcup_measurable => k _; exact: measurable_itv.
  + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->].
    by rewrite andbT; apply: le_trans; rewrite lerB// ler_nat.
rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//.
apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/= lte_fin.
have [->|n0] := eqVneq n 0%N; first by rewrite subr0 ltxx.
rewrite ltrBlDr ltrDl ltr0n lt0n n0 EFinN EFinB fin_num_oppeB// addeA.
by rewrite subee// add0e.
Qed.

Let lebesgue_measure_itv_infty_infty :
lebesgue_measure ([set` Interval -oo%O +oo%O] : set R) = +oo%E.

Proof.

rewrite set_itv_infty_infty -(setUv (`]-oo, 0[)) setCitv.
rewrite [X in _ `|` (X `|` _) ]set_itvE set0U measureU//; last first.
apply/seteqP; split => //= x [] /= /[swap].
by rewrite !in_itv/= andbT ltNge => ->//.
rewrite [X in (X + _)%E]lebesgue_measure_itv_infty_bnd.
by rewrite [X in (_ + X)%E]lebesgue_measure_itv_bnd_infty.
Qed.

Lemma lebesgue_measure_itv (i : interval R) :
lebesgue_measure ([set` i] : set R) =
(if i.1 < i.2 then (i.2 : \bar R) - i.1 else 0)%E.

Proof.

move: i => [[x a|[|]]] [y b|[|]].
by rewrite lebesgue_measure_itv_bnd wlength_itv.
- by rewrite set_itvE ?measure0.
- by rewrite lebesgue_measure_itv_bnd_infty/= ltry.
- by rewrite lebesgue_measure_itv_infty_bnd/= ltNyr.
- by rewrite set_itvE ?measure0.
- by rewrite lebesgue_measure_itv_infty_infty.
- by rewrite set_itvE ?measure0.
- by rewrite set_itvE ?measure0.
- by rewrite set_itvE ?measure0.
Qed.

Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R ->
lebesgue_measure (ball x r) = (r *+ 2)%:E.

Proof.

rewrite le_eqVlt => /predU1P[ <-|r0].
by rewrite (ball0 _ _).2// measure0 mul0rn.
rewrite ball_itv lebesgue_measure_itv/= lte_fin ltrBlDr -addrA ltrDl.
by rewrite addr_gt0 // -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n.
Qed.

Lemma lebesgue_measure_closed_ball (x r : R) : 0 <= r ->
lebesgue_measure (closed_ball x r) = (r *+ 2)%:E.

Proof.

rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0// measure0.
rewrite closed_ball_itv// lebesgue_measure_itv/= lte_fin -ltrBlDl addrAC.
rewrite subrr add0r gtrN// ?mulr_gt0// -EFinD; congr (_%:E).
by rewrite opprB addrAC addrCA subrr addr0 -mulr2n.
Qed.

End lebesgue_measure_itv.

Lemma lebesgue_measure_rat (R : realType) :
lebesgue_measure (range ratr : set R) = 0%E.

Proof.

have /pcard_eqP/bijPex[f bijf] := card_rat; set f1 := 'pinv_(fun=> 0) setT f.
rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first.
  apply/seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n).
  exists (f q) => //=; rewrite /f1 pinvKV// ?in_setE// => x y _ _.
  by apply: bij_inj; rewrite -setTT_bijective.
rewrite measure_bigcup//; last first.
  apply/trivIsetP => i j _ _ ij; apply/seteqP; split => //= _ [/= ->].
  move=> /fmorph_inj.
  have /set_bij_inj /[apply] := bijpinv_bij (fun=> 0) bijf.
  by rewrite in_setE => /(_ Logic.I Logic.I); exact/eqP.
by rewrite eseries0// => n _ _; exact: lebesgue_measure_set1.
Qed.

Section negligible_outer_measure.
Context {R : realType}.
Implicit Types (A : set R).
Local Open Scope ereal_scope.

Let l := (@wlength R idfun).
Let mu := (@lebesgue_measure R).

Lemma outer_measure_open_le A (e : R) : (0 < e)%R ->
exists U, [/\ open U, A `<=` U & mu U <= (l^* A)%mu + e%:E].

Proof.

have [|Aoo e0] := leP +oo (l^* A)%mu.
  rewrite leye_eq => /eqP Aoo e0.
  by exists [set: R]; split => //; [exact: openT|rewrite Aoo leey].
have [F AF Fe] : exists2 I_, open_itv_cover A I_ &
    \sum_(0 <= k <oo) l (I_ k) <= (l^* A)%mu + e%:E.
  have : (l^* A)%mu\is a fin_num by rewrite ge0_fin_numE// outer_measure_ge0.
  rewrite outer_measure_open_itv_cover.
  move=> /lb_ereal_inf_adherent-/(_ _ e0)[_/= [F]] AF <- Fe.
  by exists F => //; exact/ltW.
exists (\bigcup_i F i); split.
- apply: bigcup_open => // i _.
  by case: AF => /(_ i)[ab -> _]; exact: interval_open.
- by case: AF.
- rewrite (le_trans _ Fe)//.
  apply: (le_trans (outer_measure_sigma_subadditive mu F)).
  apply: lee_nneseries => // i _.
  case: AF => /(_ i)[[a b] -> _]/=.
  by rewrite /l wlength_itv/= -(@lebesgue_measure_itv R `]a, b[).
Qed.

Lemma outer_measure_open A : (l^* A)%mu =
ereal_inf [set (l^* U)%mu | U in [set U | open U /\ A `<=` U]].

Proof.

apply/eqP; rewrite eq_le; apply/andP; split.
by apply: lb_ereal_inf => /= _ /= [U [oU AU] <-]; exact: le_outer_measure.
apply/lee_addgt0Pr => /= e e0; apply: ereal_inf_le.
have [U [oU AU UAe]] := @outer_measure_open_le A _ e0.
by exists (mu U) => //=; exists U.
Qed.

Lemma outer_measure_Gdelta A :
  exists G : (set R)^nat, [/\ (forall i, open (G i)),
    A `<=` \bigcap_i G i &
    mu (\bigcap_i G i) = (l^* A)%mu].

Proof.

have inv0 k : (0 < k.+1%:R^-1 :> R)%R by rewrite invr_gt0.
pose F k := projT1 (cid (outer_measure_open_le A (inv0 k))).
have oF k : open (F k) by rewrite /F; case: cid => x /= [].
have AF k : A `<=` F k by rewrite /F; case: cid => x /= [].
have mF k : mu (F k) <= (l^* A)%mu + k.+1%:R^-1%:E.
  by rewrite /F; case: cid => x /= [].
pose G := \bigcap_k (F k).
exists F; split => //; first exact: sub_bigcap.
apply/eqP; rewrite eq_le; apply/andP; split.
  apply/lee_addgt0Pr => /= _/posnumP[e].
  near \oo => k.
  apply: (@le_trans _ _ ((l^* A)%mu + k.+1%:R^-1%:E)).
    by rewrite (le_trans _ (mF k))// le_outer_measure//; exact: bigcap_inf.
  rewrite leeD2l// lee_fin; apply: ltW.
  by near: k; exact: near_infty_natSinv_lt.
rewrite [leRHS](_ : _ = l^* (\bigcap_i F i))%mu// le_outer_measure//.
exact: sub_bigcap.
Unshelve. all: by end_near. Qed.

Lemma negligible_outer_measure (N : set R) : mu.-negligible N <-> (l^* N)%mu = 0.

Proof.

split=> [[/= A [mA mA0 NA]]|N0].
- by apply/eqP; rewrite eq_le outer_measure_ge0 andbT -mA0 le_outer_measure.
- have := @outer_measure_Gdelta N; rewrite N0 => -[F [oF NF mF0]].
exists (\bigcap_i F i); split => //=.
by apply: bigcapT_measurable => i; exact: open_measurable.
Qed.

End negligible_outer_measure.

Section lebesgue_regularity.
Local Open Scope ereal_scope.
Context {R : realType}.
Let mu := [the measure _ _ of @lebesgue_measure R].

Lemma lebesgue_regularity_outer (D : set R) (eps : R) :
measurable D -> mu D < +oo -> (0 < eps)%R ->
exists U : set R, [/\ open U , D `<=` U & mu (U `\` D) < eps%:E].

Proof.

move=> mD muDoo epspos.
have /ereal_inf_lt[z [/= M' covDM sMz zDe]] : mu D < mu D + (eps / 2)%:E.
  by rewrite lte_spaddre ?lte_fin ?divr_gt0// ge0_fin_numE.
pose e2 n := (eps / 2) / (2 ^ n.+1)%:R.
have e2pos n : (0 < e2 n)%R by rewrite ?divr_gt0.
pose M n := if pselect (M' n = set0) then set0 else
            (`] inf (M' n), sup (M' n) + e2 n [%classic)%R.
have muM n : mu (M n) <= mu (M' n) + (e2 n)%:E.
  rewrite /M; case: pselect => /= [->|].
    by rewrite measure0 add0e lee_fin ltW.
  have /ocitvP[-> //| [[a b /= alb -> ab0]]] : ocitv (M' n).
    by case: covDM => /(_ n).
  rewrite inf_itv// sup_itv//.
  have -> : (`]a, (b + e2 n)%R[ = `]a, b] `|` `]b, (b + e2 n)%R[ )%classic.
    apply: funext=> r /=; rewrite (@itv_splitU _ _ (BRight b)).
      by rewrite propeqE; split=> /orP.
    by rewrite !bnd_simp (ltW alb)/= ltr_pwDr.
  rewrite measureU/=.
  - rewrite !lebesgue_measure_itv/= !lte_fin alb ltr_pwDr//=.
    by rewrite -(EFinD (b + e2 n)) (addrC b) addrK.
  - by apply: sub_sigma_algebra; exact: is_ocitv.
  - by apply: open_measurable; exact: interval_open.
  - rewrite eqEsubset; split => // r []/andP [_ +] /andP[+ _] /=.
    by rewrite !bnd_simp => /le_lt_trans /[apply]; rewrite ltxx.
pose U := \bigcup_n M n.
exists U; have DU : D `<=` U.
  case: (covDM) => _ /subset_trans; apply; apply: subset_bigcup.
  rewrite /M => n _ x; case: pselect => [/= -> //|].
  have /ocitvP [-> //| [[/= a b alb -> mn]]] : ocitv (M' n).
    by case: covDM => /(_ n).
  rewrite /= !in_itv/= => /andP[ax xb]; rewrite ?inf_itv ?sup_itv//.
  by rewrite ax/= (le_lt_trans xb)// ltr_pwDr.
have mM n : measurable (M n).
  rewrite /M; case: pselect; first by move=> /= _; exact: measurable0.
  by move=> /= _; apply: open_measurable; apply: interval_open.
have muU : mu U < mu D + eps%:E.
  apply: (@le_lt_trans _ _ (\sum_(n <oo) mu (M n))).
    exact: outer_measure_sigma_subadditive.
  apply: (@le_lt_trans _ _ (\sum_(n <oo) (mu (M' n) + (e2 n)%:E))).
    by rewrite lee_nneseries.
  apply: le_lt_trans.
    by apply: epsilon_trick => //; rewrite divr_ge0// ltW.
  rewrite {2}[eps]splitr EFinD addeA lte_leD//.
  rewrite (le_lt_trans _ zDe)// -sMz lee_nneseries// => i _.
  rewrite /= -wlength_Rhull wlength_itv !er_map_idfun.
  rewrite -lebesgue_measure_itv le_measure//= ?inE.
  - by case: covDM => /(_ i) + _; exact: sub_sigma_algebra.
  - exact: measurable_itv.
  - exact: sub_Rhull.
split => //.
  apply: bigcup_open => n _.
  by rewrite /M; case: pselect => /= _; [exact: open0|exact: interval_open].
rewrite measureD//=.
- by rewrite setIidr// lte_subel_addl// ge0_fin_numE// (lt_le_trans muU)// leey.
- by apply: bigcup_measurable => k _; exact: mM.
- by rewrite (lt_le_trans muU)// leey.
Qed.

Lemma lebesgue_nearly_bounded (D : set R) (eps : R) :
measurable D -> mu D < +oo -> (0 < eps)%R ->
exists ab : R * R, mu (D `\` [set` `[ab.1,ab.2]]) < eps%:E.

Proof.

move=> mD Dfin epspos; pose Dn n := D `&` [set` `[-(n%:R), n%:R]]%R.
have mDn n : measurable (Dn n) by exact: measurableI.
have : mu \o Dn @ \oo --> mu (\bigcup_n Dn n).
  apply: nondecreasing_cvg_mu => //.
  - by apply: bigcup_measurable => // ? _; exact: mDn.
  - move=> n m nm; apply/subsetPset; apply: setIS => z /=; rewrite !in_itv/=.
    move=> /andP[nz zn]; rewrite (le_trans _ nz)/= ?(le_trans zn) ?ler_nat//.
    by rewrite lerNl opprK ler_nat.
rewrite -setI_bigcupr; rewrite bigcup_itvT setIT.
have finDn n : mu (Dn n) \is a fin_num.
  rewrite ge0_fin_numE// (le_lt_trans _ Dfin)//.
  by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl].
have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs.
rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[].
  exact/nbhs_interior/nbhsx_ballx.
move=> n _ /(_ _ (leqnn n))/interior_subset muDN.
exists (-n%:R, n%:R)%R; rewrite measureD//=.
move: muDN; rewrite /ball/= /ereal_ball/= -fineB//=; last exact: finDn.
rewrite -lte_fin; apply: le_lt_trans.
have finDDn : mu D - mu (Dn n) \is a fin_num
  by rewrite ?fin_numB ?finD /= ?(finDn n).
rewrite -fine_abse // gee0_abs ?sube_ge0 ?finD ?(finDn _) //.
  by rewrite -[_ - _]fineK // lte_fin fine.
by rewrite le_measure// ?inE//; [exact: measurableI |exact: subIsetl].
Qed.

Lemma lebesgue_regularity_inner (D : set R) (eps : R) :
measurable D -> mu D < +oo -> (0 < eps)%R ->
exists V : set R, [/\ compact V , V `<=` D & mu (D `\` V) < eps%:E].

Proof.

move=> mD finD epspos.
wlog : eps epspos D mD finD / exists ab : R * R, D `<=` `[ab.1, ab.2]%classic.
  move=> WL; have [] := @lebesgue_nearly_bounded _ (eps / 2)%R mD finD.
    by rewrite divr_gt0.
  case=> a b /= muDabe; have [] := WL (eps / 2) _ (D `&` `[a,b]).
  - by rewrite divr_gt0.
  - exact: measurableI.
  - by rewrite (le_lt_trans _ finD)// le_measure// inE//; exact: measurableI.
  - by exists (a, b).
  move=> V [/= cptV VDab Dabeps2]; exists (V `&` `[a, b]); split.
  - apply: (subclosed_compact _ cptV) => //; apply: closedI.
      by apply: compact_closed => //; exact: Rhausdorff.
    exact: interval_closed.
  - by move=> ? [/VDab []].
  rewrite setDIr (setU_id2r ((D `&` `[a, b]) `\` V)); last first.
    move=> z ; rewrite setDE setCI setCK => -[?|?];
    by apply/propext; split => [[]|[[]]].
  have mV : measurable V.
    by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff.
  rewrite [eps]splitr EFinD (measureU mu) // ?lteD //.
  - by apply: measurableD => //; exact: measurableI.
  - exact: measurableD.
  - by rewrite eqEsubset; split => z // [[[_ + _] [_]]].
case=> -[a b] /= Dab; pose D' := `[a,b] `\` D.
have mD' : measurable D' by exact: measurableD.
have [] := lebesgue_regularity_outer mD' _ epspos.
  rewrite (@le_lt_trans _ _ (mu `[a,b]%classic))//.
    by rewrite le_measure ?inE//; exact: subIsetl.
  by rewrite /= lebesgue_measure_itv/= -EFinD -(fun_if EFin) ltry.
move=> U [oU /subsetC + mDeps]; rewrite setCI setCK => nCD'.
exists (`[a, b] `&` ~` U); split.
- apply: (subclosed_compact _ (@segment_compact _ a b)) => //.
  by apply: closedI; [exact: interval_closed | exact: open_closedC].
- by move=> z [abz] /nCD'[].
- rewrite setDE setCI setIUr setCK.
  rewrite [_ `&` ~` _ ](iffRL (disjoints_subset _ _)) ?setCK // set0U.
  move: mDeps; rewrite /D' ?setDE setCI setIUr setCK [U `&` D]setIC.
  move => /(le_lt_trans _); apply; apply: le_measure; last by move => ?; right.
    by rewrite inE; apply: measurableI => //; exact: open_measurable.
  rewrite inE; apply: measurableU.
    by apply: measurableI; [exact: open_measurable|exact: measurableC].
  by apply: measurableI => //; exact: open_measurable.
Qed.

Let lebesgue_regularity_innerE_bounded (A : set R) : measurable A ->
mu A < +oo ->
mu A = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` A]].

Proof.

move=> mA muA; apply/eqP; rewrite eq_le; apply/andP; split; last first.
by apply: ub_ereal_sup => /= x [B /= [cB BA <-{x}]]; exact: le_outer_measure.
apply/lee_addgt0Pr => e e0.
have [B [cB BA /= ABe]] := lebesgue_regularity_inner mA muA e0.
rewrite -{1}(setDKU BA) (@le_trans _ _ (mu B + mu (A `\` B)))//.
by rewrite setUC outer_measureU2.
by rewrite leeD//; [apply: ereal_sup_ubound => /=; exists B|exact/ltW].
Qed.

Lemma lebesgue_regularity_inner_sup (D : set R) : measurable D ->
mu D = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` D]].

Proof.

move=> mD; have [?|] := ltP (mu D) +oo.
  exact: lebesgue_regularity_innerE_bounded.
have /sigma_finiteP [F [RFU Fsub ffin]] :=
  sigma_finiteT (lebesgue_stieltjes_measure (@idfun R)).
rewrite leye_eq => /eqP /[dup] + ->.
have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI.
move=> FDp; apply/esym/eq_infty => M.
have : (fun n => mu (F n `&` D)) @ \oo --> +oo.
  rewrite -FDp; apply: nondecreasing_cvg_mu.
  - by move=> i; apply: measurableI => //; exact: (ffin i).1.
  - by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1).
  - by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub.
move/cvgey_ge => /(_ (M + 1)%R) [N _ /(_ _ (lexx N))].
have [mFN FNoo] := ffin N.
have [] := @lebesgue_regularity_inner (F N `&` D) _ _ _ ltr01.
- exact: measurableI.
- by rewrite (le_lt_trans _ (ffin N).2)//= measureIl.
move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD.
rewrite (@le_trans _ _ (mu V))//; last first.
  apply: ereal_sup_ubound; exists V => //=; split => //.
  exact: (subset_trans VFND (@subIsetr _ _ _)).
rewrite -(@leeD2rE _ 1)// -EFinD (le_trans M1FD)//.
rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI.
by rewrite addeC leeD//; [rewrite measureIr//; exact: measurableI|exact/ltW].
Qed.

End lebesgue_regularity.

Definition vitali_cover {R : realType} (E : set R) I
    (B : I -> set R) (D : set I) :=
  (forall i, is_ball (B i)) /\
  forall x, E x -> forall e : R, 0 < e -> exists i,
    [/\ D i, B i x & (radius (B i))%:num < e].

Section vitali_theorem.
Context {R : realType} (A : set R) (B : nat -> set R).
Hypothesis B0 : forall i, (0 < (radius (B i))%:num)%R.
Notation mu := (@lebesgue_measure R).
Local Open Scope ereal_scope.

Lemma vitali_theorem (V : set nat) : vitali_cover A B V ->
  exists D, [/\ countable D, D `<=` V, trivIset D (closure \o B) &
    mu (A `\` \bigcup_(k in D) closure (B k)) = 0].

Proof.

move=> ABV.
wlog VB1 : V ABV / forall i, V i -> ((radius (B i))%:num <= 1)%R.
  move=> wlg.
  pose V' := V `\` [set i | (radius (B i))%:num > 1]%R.
  have : vitali_cover A B V'.
    split; [exact: ABV.1|move=> x Ax e e0].
    have : (0 < minr e 1)%R by rewrite lt_min// e0/=.
    move=> /(ABV.2 x Ax)[i [Vi ix ie]].
    exists i; split => //.
    - split => //=; rewrite ltNge; apply/negP/negPn.
      by rewrite (le_trans (ltW ie))// ge_min lexx orbT.
    - by rewrite (lt_le_trans ie)// ge_min lexx.
  move/wlg.
  have V'B1 i : V' i -> ((radius (B i))%:num <= 1)%R.
    by move=> [Vi /=]; rewrite ltNge => /negP/negPn.
  move=> /(_ V'B1)[D [cD DV' tD h]].
  by exists D; split => //; apply: (subset_trans DV') => ? [].
have [D [cD DV tDB Dintersect]] := vitali_lemma_infinite ABV.1 B0 VB1.
exists D; split => //.
pose Z r := (A `\` \bigcup_(k in D) closure (B k)) `&` ball (0%R:R) r.
suff: forall r : {posnum R}, mu (Z r%:num) = 0.
  move=> Zr; have {}Zr n : mu (Z n%:R) = 0.
    move: n => [|n]; first by rewrite /Z (ball0 _ _).2// setI0.
    by rewrite (Zr (PosNum (ltr0Sn _ n))).
  set F := fun n => Z n%:R.
  have : mu (\bigcup_n F n) <= \sum_(i <oo) mu (F i).
    exact: outer_measure_sigma_subadditive.
  rewrite eseries0; last by move=> n _; rewrite /F Zr.
  by rewrite /F -setI_bigcupr bigcup_ballT setIT measure_le0 => /eqP.
move=> r.
pose E := [set i | D i /\ closure (B i) `&` ball (0%R:R) r%:num !=set0].
pose F := vitali_collection_partition B E 1.
have E_partition : E = \bigcup_n (F n).
  by rewrite -cover_vitali_collection_partition// => i [] /DV /VB1.
have EBr2 n : E n -> closure (B n) `<=` (ball (0:R) (r%:num + 2))%R.
  move=> [Dn] [x] => -[Bnx rx] y /= Bny.
  move: rx; rewrite /ball /= !sub0r !normrN => rx.
  rewrite -(subrK x y) (le_lt_trans (ler_normD _ _))//.
  rewrite addrC ltr_leD// -(subrK (cpoint (B n)) y) -(addrA (y - _)%R).
  rewrite (le_trans (ler_normD _ _))// (_ : 2 = 1 + 1)%R// lerD//.
    rewrite distrC; have := is_ball_closureP (ABV.1 n) Bny.
    by move=> /le_trans; apply; rewrite VB1//; exact: DV.
  have := is_ball_closureP (ABV.1 n) Bnx.
  by move=> /le_trans; apply; rewrite VB1//; exact: DV.
have measurable_closure (C : set R) : is_ball C -> measurable (closure C).
  by move=> ballC; rewrite is_ball_closure//; exact: measurable_closed_ball.
move: ABV => [is_ballB ABV].
have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
              mu (ball (0:R) (r%:num + 2))%R.
  rewrite -(set_mem_set E) -nneseries_esum// -measure_bigcup//; last 2 first.
    by move=> *; exact: measurable_closure.
    by apply: sub_trivIset tDB => ? [].
  apply/le_measure; rewrite ?inE; [|exact: measurable_ball|exact: bigcup_sub].
  by apply: bigcup_measurable => *; exact: measurable_closure.
have finite_set_F i : finite_set (F i).
  apply: contrapT.
  pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
  move/(infinite_set_fset M) => [/= C] CsubFi McardC.
  have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
            mu (\bigcup_(j in [set` C]) closure (B j)).
    rewrite (measure_bigcup _ [set` C])//; last 2 first.
      by move=> ? _; exact: measurable_closure.
      by apply: sub_trivIset tDB; by apply: (subset_trans CsubFi) => x [[]].
    rewrite /= nneseries_esum//= set_mem_set// esum_fset// fsbig_finite//=.
    rewrite set_fsetK.
    apply: (@le_trans _ _ (\sum_(i0 <- C) (1 / (2 ^ i.+1)%:R)%:E)).
      under eq_bigr do rewrite -(mul1r (_ / _)) EFinM.
      rewrite -ge0_sume_distrl// EFinM lee_wpmul2r// sumEFin lee_fin.
      by rewrite -(natr_sum _ _ _ (cst 1%N)) ler_nat -card_fset_sum1.
    rewrite big_seq [in leRHS]big_seq; apply: lee_sum => // j.
    move=> /CsubFi[_ /andP[+ _]].
    rewrite -lte_fin => /ltW/le_trans; apply.
    rewrite (is_ball_closure (is_ballB _))// lebesgue_measure_closed_ball//.
    by rewrite lee_fin mulr2n lerDr.
  have CFi : mu (\bigcup_(j in [set` C]) closure (B j)) <=
             mu (\bigcup_(j in F i) closure (B j)).
    apply: le_measure => //; rewrite ?inE.
    - rewrite bigcup_fset; apply: bigsetU_measurable => *.
      exact: measurable_closure.
    - by apply: bigcup_measurable => *; exact: measurable_closure.
    - apply: bigcup_sub => j Cj.
      exact/(@bigcup_sup _ _ _ _ (closure \o B))/CsubFi.
  have Fir2 : mu (\bigcup_(j in F i) closure (B j)) <=
              mu (ball (0:R) (r%:num + 2))%R.
    rewrite (le_trans _ EBr2)// -(set_mem_set E) -nneseries_esum //.
    rewrite E_partition -measure_bigcup//=; last 2 first.
      by move=> ? _; exact: measurable_closure.
      apply: trivIset_bigcup => //.
        by move=> n; apply: sub_trivIset tDB => ? [[]].
      by move=> n m i0 j nm [[Di0 _] _] [[Dj _] _]; exact: tDB.
    apply: le_measure; rewrite ?inE.
    - by apply: bigcup_measurable => *; exact: measurable_closure.
    - by apply: bigcup_measurable => *; exact: measurable_closure.
    - by move=> /= x [n Fni Bnx]; exists n => //; exists i.
  have {CFi Fir2} := le_trans MC (le_trans CFi Fir2).
  apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin.
  rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm; last first.
    by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)).
  by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl.
have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo.
  by rewrite lebesgue_measure_ball// ltry.
have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =
          mu (\bigcup_(i in E) closure (B i)).
  rewrite E_partition bigcup_bigcup; apply/esym.
  transitivity (\sum_(n <oo) mu (\bigcup_(i in F n) closure (B i))).
    apply: measure_semi_bigcup => //.
    - by move=> i; apply: bigcup_measurable => *; exact: measurable_closure.
    - apply: trivIsetT_bigcup => //.
        apply/trivIsetP => i j _ _ ij.
        by apply: disjoint_vitali_collection_partition => // k -[] /DV /VB1.
      by rewrite -E_partition; apply: sub_trivIset tDB => x [].
    - rewrite -bigcup_bigcup; apply: bigcup_measurable => k _.
      exact: measurable_closure.
  apply: (@eq_eseriesr _ (fun n => mu (\bigcup_(i in F n) closure (B i)))).
  move=> i _; rewrite bigcup_mkcond measure_semi_bigcup//; last 3 first.
    by move=> j; case: ifPn => // _; exact: measurable_closure.
    by apply/(trivIset_mkcond _ _).1; apply: sub_trivIset tDB => x [[]].
    rewrite -bigcup_mkcond; apply: bigcup_measurable => k _.
    exact: measurable_closure.
  rewrite esum_mkcond//= nneseries_esum// -fun_true//=.
  by under eq_esum do rewrite (fun_if mu) (measure0 [the measure _ _ of mu]).
apply/eqP; rewrite -measure_le0.
apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e.
have [N F5e] : exists N, \sum_(N <= n <oo) \esum_(i in F n) mu (closure (B i)) <
    5%:R^-1%:E * e%:num%:E.
  pose f n := \bigcup_(i in F n) closure (B i).
  have foo : \sum_(k <oo) (mu \o f) k < +oo.
    rewrite /f /= [ltLHS](_ : _ =
      \sum_(n <oo) \esum_(i in F n) mu (closure (B i))); last first.
    apply: (@eq_eseriesr _
        (fun k => mu (\bigcup_(i in F k) closure (B i)))) => i _.
      rewrite measure_bigcup//=.
      - by rewrite nneseries_esum// set_mem_set.
      - by move=> j D'ij; exact: measurable_closure.
      - by apply: sub_trivIset tDB => // x [[]].
    rewrite FE (@le_lt_trans _ _ (mu (ball (0 : R) (r%:num + 2))%R))//.
    rewrite (le_trans _ EBr2)// measure_bigcup//=.
    + by rewrite nneseries_esum// set_mem_set.
    + by move=> i _; exact: measurable_closure.
    + by apply: sub_trivIset tDB => // x [].
  have : \sum_(N <= k <oo) (mu \o f) k @[N --> \oo] --> 0.
    exact: nneseries_tail_cvg.
  rewrite /f /= => /fine_fcvg /= /cvgrPdist_lt /=.
  have : (0 < 5%:R^-1 * e%:num)%R by rewrite mulr_gt0// invr_gt0// ltr0n.
  move=> /[swap] /[apply].
  rewrite near_map => -[N _]/(_ _ (leqnn N)) h; exists N; move: h.
  rewrite sub0r normrN ger0_norm//; last by rewrite fine_ge0// nneseries_ge0.
  rewrite -lte_fin; apply: le_lt_trans.
  set X : \bar R := (X in fine X).
  have Xoo : X < +oo.
    apply: le_lt_trans foo.
    by rewrite (nneseries_split _ N)// leeDr//; exact: sume_ge0.
  rewrite fineK ?ge0_fin_numE//; last exact: nneseries_ge0.
  apply: lee_nneseries => //; first by move=> i _; exact: esum_ge0.
  move=> n Nn; rewrite measure_bigcup//=.
  - by rewrite nneseries_esum// set_mem_set.
  - by move=> i _; exact: measurable_closure.
  - by apply: sub_trivIset tDB => x [[]].
pose K := \bigcup_(i in `I_N) \bigcup_(j in F i) closure (B j).
have closedK : closed K.
  apply: closed_bigcup => //= i iN; apply: closed_bigcup => //.
  by move=> j Fij; exact: closed_closure.
have ZNF5 : Z r%:num `<=`
    \bigcup_(i in ~` `I_N) \bigcup_(j in F i) closure (5%:R *` B j).
  move=> z Zz.
  have Kz : ~ K z.
    rewrite /K => -[n /= nN [m] [[Dm _] _] Bmz].
    by case: Zz => -[_ + _]; apply; exists m.
  have [i [Vi Biz Bir BiK0]] : exists i, [/\ V i, (closure (B i)) z,
      closure (B i) `<=` ball (0%R:R) r%:num & closure (B i) `&` K = set0].
    case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz.
    have [d dzr zdK0] : exists2 d : {posnum R},
        (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0.
      have [d/= d0 dzK] := closed_disjoint_closed_ball closedK Kz.
      have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R.
        by rewrite lt_min (divr_gt0 d0)//= andbT divr_gt0// subr_gt0.
      exists (PosNum rz0) => /=.
        by rewrite gt_min ltr_pdivrMr// ltr_pMr ?subr_gt0// ltr1n.
      apply: dzK => //=.
      rewrite sub0r normrN gtr0_norm// gt_min (ltr_pdivrMr d d)//.
      by rewrite ltr_pMr// ltr1n orbT.
    have N0_gt0 : (0 < d%:num / 2)%R by rewrite divr_gt0.
    have [i [Vi Biz BiN0]] := ABV _ Az _ N0_gt0.
    exists i; split => //.
      exact: subset_closure.
      move=> y Biy; rewrite /ball/= sub0r normrN -(@subrK _ (cpoint (B i)) y).
      rewrite (le_lt_trans (ler_normD _ _))//.
      rewrite (@le_lt_trans _ _ (d%:num / 2 + `|cpoint (B i)|)%R)//.
        rewrite lerD2r// distrC.
        by rewrite (le_trans (is_ball_closureP (is_ballB i) Biy))// ltW.
      rewrite -(@subrK _ z (cpoint (B i))).
      rewrite (@le_lt_trans _ _ (d%:num / 2 + `|cpoint (B i) - z| + `|z|)%R)//.
        by rewrite -[leRHS]addrA lerD2l//; exact: ler_normD.
      rewrite (@le_lt_trans _ _ (d%:num + `|z|)%R)//.
        rewrite [in leRHS](splitr d%:num) -!addrA lerD2l// lerD2r//.
        by rewrite (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW.
      by move: dzr; rewrite -ltrBrDr.
    apply: subsetI_eq0 zdK0 => // y Biy.
    rewrite closed_ballE//= /closed_ball_/=.
    rewrite -(@subrK _ (cpoint (B i)) z) -(addrA (z - _)%R).
    rewrite (le_trans (ler_normD _ _))// [in leRHS](splitr d%:num) lerD//.
      by rewrite distrC (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW.
    by rewrite (le_trans (is_ball_closureP (is_ballB i) Biy))// ltW.
  have [j [Ej Bij0 Bij5]] : exists j, [/\ E j,
      closure (B i) `&` closure (B j) !=set0 &
      closure (B i) `<=` closure (5%:R *` B j)].
    have [j [Dj Bij0 Bij2 Bij5]] := Dintersect _ Vi.
    exists j; split => //; split => //.
    by move: Bij0; rewrite setIC; exact: subsetI_neq0.
  have BjK : ~ (closure (B j) `<=` K).
    move=> BjK; move/eqP : BiK0.
    by apply/negP/set0P; move: Bij0; exact: subsetI_neq0.
  have [k NK Fkj] : (\bigcup_(i in ~` `I_N) F i) j.
    move: Ej; rewrite E_partition => -[k _ Fkj].
    by exists k => //= kN; apply: BjK => x Bjx; exists k => //; exists j.
  by exists k => //; exists j => //; exact: Bij5.
have {}ZNF5 : mu (Z r%:num) <=
    \sum_(N <= m <oo) \esum_(i in F m) mu (closure (5%:R *` B i)).
  apply: (@le_trans _ _ (mu (\bigcup_(i in ~` `I_N)
      \bigcup_(j in F i) closure (5%:R *` B j)))).
    exact: le_outer_measure.
  apply: (@le_trans _ _ (\sum_(N <= i <oo) mu
                           (\bigcup_(j in F i) closure (5%:R *` B j)))).
    apply: measure_sigma_subadditive_tail => //.
      move=> n; apply: bigcup_measurable => k _.
      by apply: measurable_closure; exact: is_scale_ball.
    apply: bigcup_measurable => k _; apply: bigcup_measurable => k' _.
    by apply: measurable_closure; exact: is_scale_ball.
  apply: lee_nneseries => // n _.
  rewrite -[in leRHS](set_mem_set (F n)) -nneseries_esum// bigcup_mkcond.
  rewrite eseries_mkcond [leRHS](_ : _ = \sum_(i <oo) mu
      (if i \in F n then closure (5%:R *` B i) else set0)); last first.
    congr (limn _); apply/funext => x.
    by under [RHS]eq_bigr do rewrite (fun_if mu) measure0.
  apply: measure_sigma_subadditive => //.
  + move=> m; case: ifPn => // _.
    by apply: measurable_closure; exact: is_scale_ball.
  + apply: bigcup_measurable => k _; case: ifPn => // _.
    by apply: measurable_closure; exact: is_scale_ball.
apply/(le_trans ZNF5).
move/ltW: F5e; rewrite [in X in X -> _](@lee_pdivlMl R 5%:R) ?ltr0n//.
rewrite -nneseriesZl//; last by move=> *; exact: esum_ge0.
apply: le_trans; apply: lee_nneseries => //; first by move=> *; exact: esum_ge0.
move=> n _.
rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesZl//.
apply: lee_nneseries => // m mFn.
rewrite (ballE (is_ballB m))// closure_ball lebesgue_measure_closed_ball//.
rewrite scale_ballE// closure_ball lebesgue_measure_closed_ball//.
by rewrite -EFinM mulrnAr.
Qed.

End vitali_theorem.

Section vitali_theorem_corollary.
Context {R : realType} (A : set R) (B : nat -> set R).

Lemma vitali_coverS (F : set nat) (O : set R) : open O -> A `<=` O ->
vitali_cover A B F -> vitali_cover A B (F `&` [set k | B k `<=` O]).

Proof.

move=> oO AO [Bball ABF]; split => // x Ax r r0.
have [d xdO] : exists d : {posnum R}, ball x d%:num `<=` O.
  have [/= d d0 dxO] := open_subball oO (AO _ Ax).
  have d20 : (0 < d / 2)%R by rewrite divr_gt0.
  exists (PosNum d20) => z xdz.
  apply: (dxO (PosNum d20)%:num) => //=.
  by rewrite sub0r normrN gtr0_norm// gtr_pMr// invf_lt1// ltr1n.
pose rd2 : R := minr r (d%:num / 2)%R.
have rd2_gt0 : (0 < rd2)%R by rewrite lt_min r0//= divr_gt0.
have [k [Vk Bkr Bkd]] := ABF _ Ax _ rd2_gt0.
exists k => //; split => //; last by rewrite (lt_le_trans Bkd)// ge_min// lexx.
split => //=.
apply: subset_trans xdO => /= z Bkz.
rewrite /ball/= -(addrKA (- cpoint (B k))).
rewrite (le_lt_trans (ler_normB _ _))//= -(addrC z).
rewrite (splitr d%:num) ltrD//.
  rewrite distrC (lt_le_trans (is_ballP _ _))//.
  by rewrite (le_trans (ltW Bkd))// ge_min lexx orbT.
rewrite distrC (lt_le_trans (is_ballP _ _))//.
by rewrite (le_trans (ltW Bkd))// ge_min lexx orbT.
Qed.

Let vitali_cover_mclosure (F : set nat) k :
vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (closure (B k)).

Proof.

case => + _ => /(_ k)/ballE ->.
by rewrite closure_ball; exact: measurable_closed_ball.
Qed.

Let vitali_cover_measurable (F : set nat) k :
vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (B k).

Proof.

by case => + _ => /(_ k)/ballE ->; exact: measurable_ball. Qed.

Let vitali_cover_ballE (F : set nat) n :
vitali_cover A B F -> B n = ball (cpoint (B n)) (radius (B n))%:num.

Proof.

by case => + _ => /(_ n)/ballE. Qed.

Hypothesis B0 : forall i, (0 < (radius (B i))%:num)%R.
Notation mu := (@lebesgue_measure R).
Local Open Scope ereal_scope.

Let bigB (G : set nat) c := G `&` [set k | (radius (B k))%:num >= c]%R.

Let bigBS (G : set nat) r : bigB G r `<=` G.

Proof.

by move=> i []. Qed.

Let bigB0 (G : set nat) : bigB G 0%R = G.

Proof.

by apply/seteqP; split => [//|x Gx]; split => //=. Qed.

Lemma vitali_theorem_corollary (F : set nat) :
  mu A < +oo%E -> vitali_cover A B F ->
  forall e, (e > 0)%R -> exists G' : {fset nat}, [/\ [set` G'] `<=` F,
    trivIset [set` G'] (closure \o B) &
    ((wlength idfun)^* (A `\` \big[setU/set0]_(k <- G') closure (B k)))%mu
    < e%:E].

Proof.

move=> muAfin ABF e e0.
have [O [oO AO OAoo]] :
    exists O : set R, [/\ open O, A `<=` O & mu O < mu A + 1 < +oo].
  have /(outer_measure_open_le A) : (0 < 1 / 2 :> R)%R by rewrite divr_gt0.
  move=> [O [oA AO OAe]]; exists O; split => //.
  rewrite lte_add_pinfty ?ltry// andbT.
  rewrite (le_lt_trans OAe)// lteD2lE ?ge0_fin_numE ?outer_measure_ge0//.
  by rewrite lte_fin ltr_pdivrMr// mul1r ltr1n.
pose F' := F `&` [set k | B k `<=` O].
have ABF' : vitali_cover A B F' by exact: vitali_coverS.
have [G [cG GV' tB mAG0]] := vitali_theorem B0 ABF'.
have muGSfin C : C `<=` G -> mu (\bigcup_(k in C) closure (B k)) \is a fin_num.
  move=> CG; rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu O))//; last first.
    by move: OAoo => /andP[OA]; exact: lt_trans.
  rewrite (@le_trans _ _ (mu (\bigcup_(k in G) B k)))//; last first.
    by rewrite le_outer_measure//; apply: bigcup_sub => i /GV'[].
  rewrite bigcup_mkcond [in leRHS]bigcup_mkcond measure_bigcup//=; last 2 first.
    by move=> i _; case: ifPn => // iG; exact: vitali_cover_mclosure ABF.
    by apply/(trivIset_mkcond _ _).1; apply: sub_trivIset tB.
  rewrite measure_bigcup//=; last 2 first.
    by move=> i _; case: ifPn => // _; exact: vitali_cover_measurable ABF.
    apply/(trivIset_mkcond _ _).1/trivIsetP => /= i j Gi Gj ij.
    move/trivIsetP : tB => /(_ _ _ Gi Gj ij).
    by apply: subsetI_eq0; exact: subset_closure.
  apply: lee_nneseries => // n _.
  case: ifPn => [/set_mem nC|]; last by rewrite measure0.
  rewrite (vitali_cover_ballE _ ABF) ifT; last exact/mem_set/CG.
  by rewrite closure_ball lebesgue_measure_closed_ball// lebesgue_measure_ball.
have muGfin : mu (\bigcup_(k in G) closure (B k)) \is a fin_num.
  by rewrite -(bigB0 G) muGSfin.
have [c Hc] : exists c : {posnum R},
    mu (\bigcup_(k in bigB G c%:num) closure (B k)) >
    mu (\bigcup_(k in G) closure (B k)) - e%:E.
  have : \sum_(N <= k <oo | k \in G) mu (closure (B k)) @[N --> \oo] --> 0%E.
    have : \sum_(0 <= i <oo | i \in G) mu (closure (B i)) < +oo.
      rewrite -measure_bigcup -?ge0_fin_numE//=.
      by move=> i _; exact: vitali_cover_mclosure ABF.
    by move/(@nneseries_tail_cvg _ _ (mem G)); exact.
  move/fine_cvgP => [_] /cvgrPdist_lt /(_ _ e0)[n _ /=] nGe.
  have [c nc] : exists c : {posnum R}, forall k,
      (c%:num > (radius (B k))%:num)%R -> (k >= n)%N.
    pose x := (\big[minr/(radius (B 0))%:num]_(i < n.+1) (radius (B i))%:num)%R.
    have x_gt0 : (0 < x)%R by exact: lt_bigmin.
    exists (PosNum x_gt0) => k /=; apply: contraPleq => kn.
    apply/negP; rewrite -leNgt; apply/bigmin_leP => /=; right.
    by exists (widen_ord (@leqnSn _) (Ordinal kn)).
  exists c.
  suff: mu (\bigcup_(k in G `\` bigB G c%:num) closure (B k)) < e%:E.
    rewrite EFinN lteBlDl// -lteBlDr//; last exact: muGSfin.
    apply: le_lt_trans.
    pose setDbigB := (\bigcup_(k in G) closure (B k)) `\`
                     (\bigcup_(k in bigB G c%:num) closure (B k)).
    have ? : setDbigB `<=` \bigcup_(k in G `\` bigB G c%:num) closure (B k).
      move=> /= x [[k Gk Bkx]].
      rewrite -[X in X -> _]/((~` _) x) setC_bigcup => abs.
      by exists k => //; split=> // /abs.
    apply: (@le_trans _ _ (mu setDbigB)); last first.
      rewrite le_measure ?inE//.
        by apply: measurableD;
          apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
      by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
    rewrite measureD//=; last 3 first.
      by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
      by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
      by rewrite -ge0_fin_numE.
    rewrite leeB// le_measure ?inE//.
      by apply: measurableI;
        apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
    by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
  apply: (@le_lt_trans _ _ (normr (0 -
     fine (\sum_(n <= k <oo | k \in G) mu (closure (B k)))))%:E); last first.
    by rewrite lte_fin; apply: nGe => /=.
  rewrite sub0r normrN ger0_norm/=; last by rewrite fine_ge0// nneseries_ge0.
  rewrite fineK//; last first.
    move: muGfin; rewrite measure_bigcup//=; last first.
      by move=> i _; exact: vitali_cover_mclosure ABF.
    do 2 (rewrite ge0_fin_numE//; last exact: nneseries_ge0).
    apply: le_lt_trans.
    by rewrite [leRHS](nneseries_split_cond 0%N n)// add0n leeDr// sume_ge0.
  rewrite measure_bigcup//=; last 2 first.
    by move=> i _; exact: vitali_cover_mclosure ABF.
    by apply: sub_trivIset tB; exact: subDsetl.
  rewrite [in leRHS]eseries_cond.
  suff: forall i, i \in G `\` bigB G c%:num -> (n <= i)%N.
    move=> GG'n; apply: subset_lee_nneseries => //= m mGG'.
    by rewrite GG'n// andbT; case/set_mem: mGG' => /mem_set ->.
  move=> i iGG'; rewrite nc//.
  by move/set_mem: iGG' => [Gi] /not_andP[//|/negP]; rewrite -ltNge.
have {}Hc : mu (\bigcup_(k in G) closure (B k) `\`
                \bigcup_(k in bigB G c%:num) closure (B k)) < e%:E.
  rewrite measureD//=; first last.
  - by rewrite -ge0_fin_numE.
  - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
  - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
  rewrite setIidr; last exact: bigcup_subset.
  by rewrite lteBlDr-?lteBlDl//; exact: muGSfin.
have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num).
  pose M := `|ceil (fine (mu O) / r%:num)|.+1.
  apply: contrapT => /infinite_set_fset /= /(_ M)[G0 G0G'r] MG0.
  have : mu O < mu (\bigcup_(k in bigB G r%:num) closure (B k)).
    apply: (@lt_le_trans _ _ (mu (\bigcup_(k in [set` G0]) closure (B k)))).
      rewrite bigcup_fset measure_fbigsetU//=; last 2 first.
        by move=> k _; exact: vitali_cover_mclosure ABF.
        by apply: sub_trivIset tB => x /G0G'r[].
      apply: (@lt_le_trans _ _ (\sum_(i <- G0) r%:num%:E)%R).
        rewrite sumEFin big_const_seq iter_addr addr0 -mulr_natr.
        apply: (@lt_le_trans _ _ (r%:num * M%:R)%:E); last first.
          by rewrite lee_fin ler_wpM2l// ler_nat count_predT.
        rewrite EFinM -lte_pdivrMl// muleC -(@fineK _ (mu O)); last first.
          by rewrite ge0_fin_numE//; case/andP: OAoo => ?; exact: lt_trans.
        rewrite -EFinM /M lte_fin (le_lt_trans (ceil_ge _))//.
        rewrite -natr1 natr_absz ger0_norm ?ltrDl//.
        by rewrite -ceil_ge0// (@lt_le_trans _ _ 0%R)// divr_ge0// fine_ge0.
      rewrite big_seq [in leRHS]big_seq.
      apply: lee_sum => //= i /G0G'r [iG rBi].
      rewrite -[leRHS]fineK//; last first.
        rewrite (vitali_cover_ballE _ ABF).
        by rewrite closure_ball lebesgue_measure_closed_ball.
      rewrite (vitali_cover_ballE _ ABF) closure_ball.
      by rewrite lebesgue_measure_closed_ball// fineK// lee_fin mulr2n ler_wpDl.
    rewrite le_measure? inE//; last exact: bigcup_subset.
    - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
    - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
  apply/negP; rewrite -leNgt.
  apply: (@le_trans _ _ (mu (\bigcup_(k in bigB G r%:num) B k))).
    rewrite measure_bigcup//; last 2 first.
      by move=> k _; exact: vitali_cover_mclosure ABF.
      exact: sub_trivIset tB.
    rewrite /= measure_bigcup//; last 2 first.
      by move=> k _; exact: vitali_cover_measurable ABF.
      apply/trivIsetP => /= i j [Gi ri] [Gj rj] ij.
      move/trivIsetP : tB => /(_ _ _ Gi Gj ij).
      by apply: subsetI_eq0 => //=; exact: subset_closure.
    rewrite /= lee_nneseries// => n _.
    rewrite (vitali_cover_ballE _ ABF)// closure_ball.
    by rewrite lebesgue_measure_closed_ball// lebesgue_measure_ball.
  rewrite le_measure? inE//.
  + by apply: bigcup_measurable => k _; exact: vitali_cover_measurable ABF.
  + exact: open_measurable.
  + by apply: bigcup_sub => i [/GV'[? ?] cBi].
exists (fset_set (bigB G c%:num)); split.
- by move=> /= k; rewrite in_fset_set// inE /bigB /= => -[] /GV'[].
- by apply: sub_trivIset tB => k/=; rewrite in_fset_set// inE /bigB /= => -[].
- pose UG : set R := \bigcup_(k in G) closure (B k).
  rewrite bigsetU_fset_set//.
  apply: (@le_lt_trans _ _ ((wlength idfun)^*%mu (A `\`UG) +
       mu (UG `\` \bigcup_(k in bigB G c%:num) closure (B k)))); last first.
    by rewrite -[(wlength idfun)^*%mu]/mu mAG0 add0e.
  apply: (@le_trans _ _ ((wlength idfun)^*%mu
      (A `&` (UG `\` \bigcup_(k in bigB G c%:num) closure (B k))) +
      (wlength idfun)^*%mu (A `\` UG))); last first.
    by rewrite addeC leeD2l// le_outer_measure.
  apply: (le_trans _ (outer_measureU2 _ _ _)) => //=; apply: le_outer_measure.
  rewrite !(setDE A) -setIUr; apply: setIS.
  by rewrite setDE setUIl setUv setTI -setCI; exact: subsetC.
Qed.

End vitali_theorem_corollary.

Files

Module mathcomp.analysis.lebesgue_measure