Module mathcomp.analysis.lebesgue_measure

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

# Lebesgue Measure This file contains a formalization of the Lebesgue measure using the Measure Extension theorem from measure.v, further develops the theory of of measurable functions, and prove properties of the Lebesgue measure such as Vitali's covering lemma (infinite case), 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 ``` lebesgue_measure == the Lebesgue measure 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 elebesgue_measure == the Lebesgue measure extended to \bar R ``` The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs of equivalence between the sigma-algebra generated by list of intervals and the sigma-algebras generated by open rays, closed rays, and open intervals. The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs of equivalence between emeasurable and the sigma-algebras generated open rays and closed rays. ``` 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.

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 - 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 - 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 case: (i.2 : \bar _) => //= [r _]; rewrite leey.
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: lee_sub => /=.
  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 ler_oppl 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 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core.


Section hlength_extension.
Context {R : realType}.

Notation hlength := (@hlength R).

Lemma hlength_semi_additive : 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_sub_additive :
  sigma_sub_additive (hlength : set (ocitv_type R) -> _).
Proof.
move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
move=> [a _ <-]; rewrite 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 -lee_subl_addr//.
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 ltr_addl.
  apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=.
  move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=.
  by rewrite ltr_addl.
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 ler_add// subr_le0 leNgt.
Qed.

HB.instance Definition _ := Content_SubSigmaAdditive_isMeasure.Build _ _ _
  hlength hlength_sigma_sub_additive.

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 [the measure _ _ of 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
       salgebraType R.-ocitv.-measurable] -> \bar R :=
  [the measure _ _ of lebesgue_stieltjes_measure [the cumulative _ of idfun]].
HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
HB.instance Definition _ (R : realType) :=
  SigmaFiniteMeasure.on (@lebesgue_measure R).

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 _ _ (Pointed.class _)
    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.
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move=> [x| |] //= _; [left; exists x|right].
Qed.

Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo].
Proof.
rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //.
by move=> [x| |] //= _; [left; exists x|right].
Qed.

End puncture_ereal_itv.

Section salgebra_R_ssets.
Variable R : realType.

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

HB.instance Definition R_isMeasurable :
  isMeasurable default_measure_display R :=
  @isMeasurable.Build _ measurableTypeR (Pointed.class R) 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.

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.

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 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 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 _ _ _ [the measure _ _ of (@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 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 measurable_fine (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: measurable_fine] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")]
Notation measurable_fun_fine := measurable_fine (only parsing).

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 (lim (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 ler_sub// ler_pinv ?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; first by rewrite invr1 subrr set_itvoc0.
  rewrite wlength_itv/= lte_fin ifT; last first.
    by rewrite ler_lt_sub// 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 _ [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 ltr_subl_addr ltr_addl 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 ltr_subl_addr ltr_addl.
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.
by move: x y => [|] [|]; [exact: lebesgue_measure_itvco |
  exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo |
  exact: lebesgue_measure_itvoc].
Qed.

Let limnatR : lim (fun k => (k%:R)%:E : \bar R) = +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 (lim (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 ler_add// 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 ltr_addl 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 (lim (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 ler_sub// 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 ltr_subl_addr ltr_addl 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 - 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.

End lebesgue_measure_itv.

Section measurable_ball.
Variable R : realType.

Lemma measurable_ball (x : R) e : measurable (ball x e).
Proof.
by rewrite ball_itv; exact: measurable_itv. Qed.

Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R ->
  lebesgue_measure (ball x r) = (r *+ 2)%:E.
Proof.
rewrite le_eqVlt => /orP[/eqP <-|r0].
  by rewrite (ball0 _ _).2// measure0 mul0rn.
rewrite ball_itv lebesgue_measure_itv/= lte_fin ltr_subl_addr -addrA ltr_addl.
by rewrite addr_gt0 // -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n.
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.
by rewrite closed_ball_itv.
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.
rewrite closed_ball_itv// lebesgue_measure_itv/= lte_fin -ltr_subl_addl addrAC.
rewrite subrr add0r gtr_opp// ?mulr_gt0// -EFinD; congr (_%:E).
by rewrite opprB addrAC addrCA subrr addr0 -mulr2n.
Qed.

End measurable_ball.

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 measurable_fun_measurable.
Local Open Scope ereal_scope.
Context d (T : measurableType 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)// ler_oppl oppr0.
    by rewrite natr_absz ger0_norm ?ceil_ge0// -(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 floor_le.
  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.
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 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.
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 [y ->]]; apply: measurable_itv.
Qed.

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 ler_subl_addl (le_trans rs)// ler_addr.
    * by rewrite lte_fin ltr_subl_addl (le_lt_trans rs)// ltr_addr.
  + 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 ler_subl_addr leNgt skr.
  + by rewrite lte_fin ltr_subl_addr 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)// ltr_addl.
    * by rewrite lee_fin (le_trans sr)// ler_addl.
  + 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) // ler_oppl oppr0 ler0n.
rewrite ler_oppl -abszN natr_absz gtr0_norm; last first.
  by rewrite ltr_oppr oppr0 floor_lt0.
by rewrite mulrNz ler_oppl opprK floor_le.
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.

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

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

Lemma stracexx G D : G D -> strace G D D.
Proof.
by rewrite /strace /=; exists D => //; rewrite setIid. Qed.

Lemma sigma_algebra_strace G D :
  sigma_algebra setT G -> sigma_algebra D (strace G D).
Proof.
move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I.
- move=> S [A mA ADS]; have mCA := GC _ mA.
  have : strace G D (D `&` ~` A).
    by rewrite setIC; exists (setT `\` A) => //; rewrite setTD.
  rewrite -setDE => trDA.
  have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0.
  by rewrite DADS in trDA.
- move=> S mS; have /choice[M GM] : forall n, exists A, G A /\ S n = A `&` D.
    by move=> n; have [A mA ADSn] := mS n; exists A.
  exists (\bigcup_i (M i)); first by apply GU => i; exact: (GM i).1.
  by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2.
Qed.

End trace.

Lemma strace_measurable d (T : measurableType d) (A : set T) : measurable A ->
  strace measurable A `<=` measurable.
Proof.
by move=> mA=> _ [C mC <-]; apply: measurableI. Qed.


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 measurable_oppr D : measurable_fun D (-%R).
Proof.
apply: measurable_funTS => /=; apply: continuous_measurable_fun.
exact: (@opp_continuous R [the normedModType R of R^o]).
Qed.

Lemma measurable_normr 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 ltr_oppr.
  - move=> rx /=.
    by rewrite ler0_norm 1?ltr_oppr// (le_trans (ltW rx))// ler_oppl 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 measurable_mulrl D (k : R) : measurable_fun D ( *%R k).
Proof.
apply: measurable_funTS => /=.
by apply: continuous_measurable_fun; exact: mulrl_continuous.
Qed.

Lemma measurable_mulrr D (k : R) : measurable_fun D (fun x => x * k).
Proof.
apply: measurable_funTS => /=.
by apply: continuous_measurable_fun; exact: mulrr_continuous.
Qed.

Lemma measurable_exprn 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: measurable_oppr] : core.
#[global] Hint Extern 0 (measurable_fun _ normr) =>
  solve [exact: measurable_normr] : core.
#[global] Hint Extern 0 (measurable_fun _ ( *%R _)) =>
  solve [exact: measurable_mulrl] : core.
#[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) =>
  solve [exact: measurable_exprn] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")]
Notation measurable_fun_sqr := measurable_exprn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")]
Notation measurable_fun_opp := measurable_oppr (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")]
Notation measurable_funN := measurable_oppr (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_normr` instead")]
Notation measurable_fun_normr := measurable_normr (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")]
Notation measurable_fun_exprn := measurable_exprn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mulrl` instead")]
Notation measurable_funrM := measurable_mulrl (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 -ltr_subl_addr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h.
  exists r => //; rewrite setIACA setIid; split => //; split => /=.
    by rewrite h.
  by rewrite ltr_subl_addr addrC -ltr_subl_addr h.
by rewrite ltr_subl_addr=> afg; rewrite (lt_le_trans afg)// addrC ler_add2r 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 (measurable_exprn _) _; exact: measurable_funD.
  - apply: measurableT_comp => //.
    exact: measurableT_comp (measurable_exprn _) _.
  - apply: measurableT_comp => //.
    exact: measurableT_comp (measurable_exprn _) _.
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 Y mY; have [| | |] := set_bool Y => /eqP ->.
- under eq_fun do rewrite -subr_gt0.
  rewrite preimage_true -preimage_itv_o_infty.
  by apply: (measurable_funB mg mf) => //; exact: measurable_itv.
- under eq_fun do rewrite ltNge -subr_ge0.
  rewrite preimage_false set_predC setCK -preimage_itv_c_infty.
  by apply: (measurable_funB mf mg) => //; exact: measurable_itv.
- by rewrite preimage_set0 setI0.
- by rewrite preimage_setT setIT.
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; first exact: Rhausdorff.
  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_ub; [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 --> 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).
  exact: Rhausdorff.
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.
- apply/bounded_fun_has_ubound/(@cvg_seq_bounded _ [normedModType R of R^o]).
  by apply/cvg_ex; eexists; exact: f_f.
- apply/bounded_fun_has_lbound/(@cvg_seq_bounded _ [normedModType R of R^o]).
  by apply/cvg_ex; eexists; exact: f_f.
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_restrict _ _ _ _ _ setT) => //.
  rewrite (_ : _ \_ _ = cst (0:R))//; 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 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])//.
  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).

Section standard_emeasurable_fun.
Variable R : realType.

Lemma measurable_EFin (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 measurable_abse (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).
  rewrite -[X in measurable X]setTI.
  by apply: measurable_normr => //; exact: measurable_itv.
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 measurable_oppe (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 lee_oppr.
Qed.

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

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

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 => //=.
+ apply: (measurable_fun_bool true).
  rewrite /preimage/= -[X in measurable X]setTI.
  exact/emeasurable_fin_num.
+ exact/EFin_measurable_fun/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_measurable => ? ?; 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_maxr => -[Dx /orP[|]];
      tauto.
  by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_maxr;
    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 --> 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 lebesgue_regularity.
Context {R : realType}.
Let mu := [the measure _ _ of @lebesgue_measure R].

Local Open Scope ereal_scope.

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 muDpos 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_spaddr.
  rewrite measureU/=.
  - rewrite !lebesgue_measure_itv/= !lte_fin alb ltr_spaddr//=.
    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_spaddr.
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_le_add//.
  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 --> 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 ler_oppl 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) // ?lte_add //.
  - 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 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 lee_add//; [apply: ereal_sup_ub => /=; 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]] :=
  sigmaT_finite_lebesgue_stieltjes_measure [the @cumulative R of idfun]
  (*TODO: sigma_finiteT mu should be enough but does not seem to work with older
    versions of MathComp/Coq (Coq <= 8.15?) *).
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_ub; exists V => //=; split => //.
  exact: (subset_trans VFND (@subIsetr _ _ _)).
rewrite -(@lee_add2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//.
rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI.
rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first.
  by rewrite measureIr//; apply: measurableI.
by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI.
Qed.

End lebesgue_regularity.

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_fun A g ->
  measurable A -> mu A < +oo -> (forall x, A x -> f_ ^~ x --> g x) ->
  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
    {uniform A `\` B, f_ --> g}].
Proof.
move=> mf mg mA finA fptwsg epspos; pose h q (z : T) : R := `|f_ q z - g z|%R.
have mfunh q : measurable_fun A (h q).
  by apply: measurableT_comp; [exact: measurable_normr |exact: measurable_funB].
pose E k n := \bigcup_(i in [set j : nat | (n <= j)%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 => //; apply: 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 /= Bool.andb_true_r.
  exact: mfunh.
have nEcvg x k : exists n, A x -> (~` (E k n)) x.
  case : (pselect (A x)); last by move => ?; exists point.
  move=> Ax; 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 done.
  rewrite setC_bigcap; case : (pselect (A z)) => [Az | nAz].
    by have [N /(_ Az) ?] := nEcvg z k; exists N.
  by exists O; rewrite // /E setC_bigcup => n ? [].
have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E.
  move=> k; pose ek :R := eps/2 / (2 ^ k.+1)%:R; have : mu \o E k --> (0%R)%:E.
    rewrite -(measure0 mu) -(Ek0 k); apply: nonincreasing_cvg_mu => //.
    - apply: (le_lt_trans _ finA); apply: le_measure; rewrite ?inE //.
      by move=> ? [? _ []].
    - by apply: bigcap_measurable => ?.
  case/fine_cvg/(_ (interior (ball (0:R) ek))%R).
    apply: open_nbhs_nbhs; split; first exact: open_interior.
    by apply: nbhsx_ballx; 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 apply:(le_lt_trans _ finA); apply le_measure; rewrite ?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)%R%:E); first last.
    by rewrite lte_fin ltr_pdivr_mulr // ltr_pmulr // Rint_ltr_addr1 // ?Rint1.
  apply: le_trans.
    apply: (measure_sigma_sub_additive _ (fun k => mE k (badn k)) _ _) => //.
    exact: bigcup_measurable.
  apply: le_trans; first last.
    by apply: (@epsilon_trick0 R _ xpredT); rewrite divr_ge0 //; exact: ltW.
  by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))).
apply/uniform_restrict_cvg => /= U /=; rewrite ?uniform_nbhsT.
case/nbhs_ex => del /filterS; apply.
have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del.
exists (badn N) => // r badNr x.
rewrite /patch; case xAB: (x \in A `\` _) => //; apply: (lt_trans _ Ndel).
move/set_mem: xAB; rewrite setDE; case => Ax; rewrite setC_bigcup => /(_ N I).
rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP [] //.
by move/negP; rewrite real_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 --> g x)} ->
  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
    {uniform A `\` B, (fun n => (f_ n : T -> R)) --> 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_ --> g}].
  apply: pointwise_almost_uniform => //.
  - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
  - by apply : (measurable_funS mA _ (mg)) => ? [].
  - by apply: measurableI => //; exact: measurableC.
  - apply: (le_lt_trans _ Afin); apply: le_measure; rewrite ?inE //.
    by apply: measurableI => //; exact: measurableC.
  - 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.

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_minr// 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))// le_minl lexx orbT.
    - by rewrite (lt_le_trans ie)// le_minl 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_norm_add _ _))//.
  rewrite addrC ltr_le_add// -(subrK (cpoint (B n)) y) -(addrA (y - _)%R).
  rewrite (le_trans (ler_norm_add _ _))// (_ : 2 = 1 + 1)%R// ler_add//.
    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 ler_addr.
  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 ?ceil_ge0// -ltr_pdivr_mulr//.
  by rewrite -ltr_subl_addr (lt_le_trans _ (ceil_ge _))// ltr_subl_addr ltr_addl.
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 /=.
  move/(@cvgrPdist_lt _ [pseudoMetricNormedZmodType R of R^o]).
  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)// lee_addr//; 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 _
        [normedModType R of R^o] _ _ closedK Kz).
      have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R.
        by rewrite lt_minr (divr_gt0 d0)//= andbT divr_gt0// subr_gt0.
      exists (PosNum rz0) => /=.
        by rewrite lt_minl ltr_pdivr_mulr// ltr_pmulr ?subr_gt0// ltr1n.
      apply: dzK => //=.
      rewrite sub0r normrN gtr0_norm// lt_minl (ltr_pdivr_mulr d d)//.
      by rewrite ltr_pmulr// 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_norm_add _ _))//.
      rewrite (@le_lt_trans _ _ (d%:num / 2 + `|cpoint (B i)|)%R)//.
        rewrite ler_add2r// 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 ler_add2l//; exact: ler_norm_add.
      rewrite (@le_lt_trans _ _ (d%:num + `|z|)%R)//.
        rewrite [in leRHS](splitr d%:num) -!addrA ler_add2l// ler_add2r//.
        by rewrite (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW.
      by move: dzr; rewrite -ltr_subr_addr.
    apply: subsetI_eq0 zdK0 => // y Biy.
    rewrite (@closed_ballE _ [normedModType R of R^o])//= /closed_ball_/=.
    rewrite -(@subrK _ (cpoint (B i)) z) -(addrA (z - _)%R).
    rewrite (le_trans (ler_norm_add _ _))// [in leRHS](splitr d%:num) ler_add//.
      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_sub_additive_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 (lim _); apply/funext => x.
    by under [RHS]eq_bigr do rewrite (fun_if mu) measure0.
  apply: measure_sigma_sub_additive => //.
  + 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_pdivl_mull 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.
Generated by a fork of coq2html