Module mathcomp.analysis.measurable_realfun

From HB Require Import structures.
From mathcomp Require Import boot order finmap ssralg ssrnum ssrint.
From mathcomp Require Import interval interval_inference archimedean rat.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals ereal topology numfun tvs normedtype.
From mathcomp Require Import real_interval sequences esum measure realfun exp.
From mathcomp Require Import lebesgue_stieltjes_measure.

# Measurable Functions over $\mathbb{R}$ and $\overline{\mathbb{R}}$ This file further develops the theory of measurable functions (including Egorov's theorem). Main references: - Daniel Li, Intégration et applications, 2016 - Achim Klenke, Probability Theory 2nd edition, 2014 ``` completed_algebra_gen == generator of the completed Lebesgue sigma-algebra ps_infty == inductive definition of the powerset {0, {-oo}, {+oo}, {-oo,+oo}} emeasurable G == sigma-algebra over \bar R built out of the measurables G of a sigma-algebra over R ``` The module NGenCInfty provides a proof of equivalence between the sigma-algebra for natural numbers and the sigma-algebra generated by closed rays. The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs of equivalence between emeasurable and the sigma-algebras generated by open rays and closed rays. ``` mindic mD := \1_D where mD is a proof that D is measurable indic_mfun mD := mindic mD scale_mfun k f := k \o* f max_mfun f g := f \max g min_mfun f g := f \min g ```

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

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

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

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

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

Proof.

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

Lemma ( : set T) ( : 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 ( : realType) ( : set_system R).
Let : set_system R := G.-sigma.-measurable.

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

Lemma : emeasurable set0.

Proof.

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

Lemma ( : 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]; last by constructor.
  by rewrite predeqE => x; split => // -[->].
- rewrite setIUl setICr setU0 -setDE.
  have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; last by constructor.
  by rewrite predeqE => x; split => // -[->].
- by rewrite setICr; constructor.
Qed.

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

Proof.

move=> mF; pose P := fun => measurableR j.1 /\ ps_infty j.2 /\
                            F i = [set x%:E | in j.1] `|` j.2.
have [f fi] : { : nat -> (set R) * (set \bar R) & forall , P i (f i) }.
  by apply: choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x, y).
exists (\bigcup_ (f i).1).
  by apply: bigcupT_measurable => i; exact: (fi i).1.
exists (\bigcup_ (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 => [set x%:E | in (f i).1] `|` (f i).2)).
  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 : isMeasurable default_measure_display (\bar R) :=
  isMeasurable.Build _ _
    emeasurable0 emeasurableC bigcupT_emeasurable.

End salgebra_ereal.

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

Lemma : [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 : [set` Interval -oo%O (BSide b y%:E)] =
[set -oo%E] `|` EFin @` [set | 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 : range (@EFin R) `|` [set +oo] = [set~ -oo].

Proof.

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

Proof.

End puncture_ereal_itv.

Section salgebra_R_ssets.
Context { : realType}.

. (ereal_isMeasurable (R.-ocitv.-measurable)).

Import MeasurableR.

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

Proof.

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

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

Proof.

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

#[local] Hint Resolve emeasurable_set1 : core.

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

Proof.

move: y => [y| |].
- exists [set` Interval (BSide b y) +oo%O]; first by [].
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 ( : \bar R) :
measurable [set` Interval -oo%O (BSide b y)].

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite ball_itv -?RGenOpenSets.measurableE//. Qed.

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

Proof.

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

End salgebra_R_ssets.
#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: emeasurable_set1] : core.

Import MeasurableR.

Lemma ( : realType) ( : 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).
  apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]].
  - by case: ifPn => _; split => //; left; exists r.
  - by rewrite mem_set//; split => //; right; right.
  - by rewrite mem_set//; split => //; right; left.
  - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr.
  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
  - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []].
case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin.
by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU].
Qed.

#[global] Hint Extern 0 (measurable_fun _ fine) =>
solve [exact: fine_measurable] : core.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

rewrite [X in measurable X](_ : _ = \bigcup_ (D `&`
    ([set | - k%:R%:E <= f x] `&` [set | f x <= k%:R%:E]))); last first.
  apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA.
  exact/measurableI/emeasurable_fun_infty_c/emeasurable_fun_c_infty.
rewrite predeqE => t; split => [/= [Dt ft]|].
  exists (Num.bound (fine (f t))) => //=.
  rewrite -(fineK ft) !lee_fin (fineK ft) lerNl.
  by rewrite !ltW// (ltrNbound, ltr_bound).
move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry.
Qed.

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

Proof.

rewrite (_ : [set | f x != y] = f @^-1` (setT `\ y)); last first.
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.

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

Lemma : 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 : [set | r%:E < s%:E] = `]r, +oo[%classic.

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
move=> [r|/(_ O Logic.I)|]// /(_ (Num.bound r) Logic.I) /=.
by rewrite in_itv/= lte_fin ltNge lerNl ltW// ltrNbound.
Qed.

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

Proof.

rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
move=> [r| |/(_ O Logic.I)] // /(_ (Num.bound r) Logic.I) /=.
by rewrite in_itv/= andbT lte_fin ltNge ltW// ltr_bound.
Qed.

End erealwithrays.

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

Local Open Scope ereal_scope.

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

Lemma : 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 : G.-sigma.-measurable [set +oo].

Proof.

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

Lemma : 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 .
Section erealgencinfty.
Variable : realType.
Implicit Types (x y z : \bar R) (r s : R).
Local Open Scope ereal_scope.

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

Lemma : 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 : 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 : 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 .
Section erealgeninftyo.
Variable : realType.

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

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

Proof.

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

End erealgeninftyo.
End ErealGenInftyO.

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

Proof.

by move/is_intervalP => ->; rewrite -?RGenOpenSets.measurableE//. Qed.

Section coutinuous_measurable.
Variable : realType.

Lemma ( : 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 ( : set R) ( : 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 ( : set R) : closed A -> measurable A.

Proof.

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

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

Proof.

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

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

Proof.

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

Corollary ( : set R) ( : 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 ( : R -> R) :
continuous f -> measurable_fun setT f.

Proof.

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

End coutinuous_measurable.

Lemma { : realType} ( : 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_itvoy; move/lower_semicontinuousP : scif; exact.
Qed.

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

Lemma : measurable_fun D -%R.

Proof.

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

Lemma : measurable_fun D (@normr _ R).

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End standard_measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ -%R) =>
  solve [exact: oppr_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ normr) =>
  solve [exact: normr_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ ( *%R _)) =>
  solve [exact: mulrl_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ (fun => x ^+ _)) =>
  solve [exact: exprn_measurable] : core.

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

Proof.

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

by move=> ?; rewrite -/(GRing.opp \o f); exact: measurableT_comp. Qed.

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

Proof.

move=> mf mg.
have ->: f \* g = (fun => 2%:R^-1 * (f x + g x) ^+ 2)
  \- (fun => 2%:R^-1 * (f x ^+ 2)) \- (fun => 2%:R^-1 * (g x ^+ 2)).
  rewrite funeqE => x /=; rewrite -2!mulrBr -addrA -opprD sqrrD.
  by rewrite -[_ + (_ ^+ 2)]addrA addrCA addrK [RHS]mulrC -mulr_natr mulfK.
apply: measurable_funB; first apply: measurable_funB.
- apply: measurableT_comp => //.
  by apply: measurable_funX; exact: measurable_funD.
- by apply: measurableT_comp => //; exact: measurable_funX.
by apply: measurableT_comp => //; exact: measurable_funX.
Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma :
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_fun D f -> measurable_fun D f^\+.

Proof.

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

Lemma : measurable_fun D f -> measurable_fun D f^\-.

Proof.

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

Lemma :
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 ( : (T -> R)^nat) :
  (forall , D t -> has_ubound (range (h ^~ t))) ->
  (forall , measurable_fun D (h m)) ->
  measurable_fun D (fun => sups (h ^~ x) n).

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma : measurable D <-> measurable_fun setT (\1_D : _ -> R).

Proof.

split=> [|m1]; first exact: measurable_indic.
have -> : D = (\1_D : _ -> R) @^-1` `]0, +oo[.
  apply/seteqP; split => t/=.
    by rewrite indicE => /mem_set ->; rewrite in_itv/= ltr01.
  by rewrite in_itv/= andbT indicE ltr0n; have [/set_mem|//] := boolP (t \in D).
by rewrite -[_ @^-1` _]setTI; exact: m1.
Qed.

End measurable_fun_realType.

Section funrposneg_measurable.
Context {} { : measurableType d} { : realType}.

. ( aT >-> rT}) :=
  @isMeasurableFun.Build d _ _ _ f^\+
    (measurable_funrpos (@measurable_funPT _ _ _ _ f)).

. ( aT >-> rT}) :=
  @isMeasurableFun.Build d _ _ _ f^\-
    (measurable_funrneg (@measurable_funPT _ _ _ _ f)).

End funrposneg_measurable.

Section mono_measurable.
Context { : realType}.

Lemma ( : set R) ( : R -> R) : measurable D ->
  nondecreasing_fun f -> measurable_fun D f.

Proof.

move=> mD f_nd.
rewrite /measurable_fun.
apply: (@measurability).
rewrite -RGenOpenSets.measurableE.
by rewrite RGenCInfty.measurableE.
move => /= _ [_] [r] -> <-.
apply: measurableI => //; apply: is_interval_measurable => s t/=.
rewrite !in_itv/= !andbT => fs ft u /andP[su ut].
by rewrite in_itv/= andbT (le_trans fs)// f_nd.
Qed.

Lemma ( : set R) ( : R -> R) : measurable D ->
nonincreasing_fun f -> measurable_fun D f.

Proof.

move=> mD f_ni; rewrite -(opprK f); apply/measurable_funN.
by apply: nondecreasing_measurable => // s t st; rewrite lerN2 f_ni.
Qed.

End mono_measurable.

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

Proof.

rewrite -set_itvNyy (@itv_bndbnd_setU _ _ _ (BRight 0))//.
apply/measurable_funU => //; split.
- apply/measurable_restrictT => //=.
  rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE.
  by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW.
- apply: subspace_continuous_measurable_fun => //.
  rewrite continuous_open_subspace; first exact: interval_open.
  by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln.
Qed.

#[global] Hint Extern 0 (measurable_fun _ (@ln _)) =>
solve [apply: measurable_ln] : core.

Lemma ( : 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.

Section mfun_realType.
Context { : realType}.

..Build _ _ _ rT
  (@normr rT rT) (@normr_measurable rT setT).

.
  isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT).

End mfun_realType.

Notation :=
  (GRing.SubChoice_isSubComPzRing.Build _ _ U (subringClosedP _))
  (format "[ 'SubChoice_isSubComPzRing' 'of' U 'by' <: ]")
  : form_scope.

Section ring.
Context ( : measurableType d) ( : realType).

Lemma : subring_closed (@mfun _ _ aT rT).

Proof.

split=> [|f g|f g]; rewrite !inE/=.
- exact: measurable_cst.
- exact: measurable_funB.
- exact: measurable_funM.
Qed.

..isSubringClosed.Build _
(@mfun d lebesgue_display aT rT) mfun_subring_closed.

. of {mfun aT >-> rT} by <:].

Implicit Types (f g : {mfun aT >-> rT}).

Lemma : (0 : {mfun aT >-> rT}) =1 cst 0 :> (_ -> _)

Proof.

by []. Qed.

Lemma : (1 : {mfun aT >-> rT}) =1 cst 1 :> (_ -> _)

Proof.

by []. Qed.

Lemma : - f = \- f :> (_ -> _)

Proof.

by []. Qed.

Lemma : f + g = f \+ g :> (_ -> _)

Proof.

by []. Qed.

Lemma : f - g = f \- g :> (_ -> _)

Proof.

by []. Qed.

Lemma : f * g = f \* g :> (_ -> _)

Proof.

by []. Qed.

Lemma : (f *+ n) = (fun => f x *+ n) :> (_ -> _).

Proof.

by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed.

Lemma ( : {pred I}) ( : I -> {mfun aT >-> rT}) ( : aT) :
(\sum_( <- r | P i) f i) x = \sum_( <- r | P i) f i x.

Proof.

by elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma ( : {pred I}) ( : I -> {mfun aT >-> rT}) ( : aT) :
(\sum_( <- r | P i) f i) x = \sum_( <- r | P i) f i x.

Proof.

by elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma : f ^+ n = (fun => f x ^+ n) :> (_ -> _).

Proof.

by apply/funext=> x; elim: n => [|n IHn]//; rewrite !exprS mfunM/= IHn. Qed.

..copy (f \+ g) (f + g).
..copy (\- f) (- f).
..copy (f \- g) (f - g).
..copy (f \* g) (f * g).

Definition ( : set aT) & measurable D : aT -> rT := \1_D.

Lemma ( : set aT) ( : measurable D) :
mindic mD = (fun => (x \in D)%:R).

Proof.

by rewrite /mindic funeqE => t; rewrite indicE. Qed.

..Build _ _ aT rT (mindic mD)
(@measurable_indic _ aT rT setT D mD).

Definition ( : set aT) ( : measurable D) : {mfun aT >-> rT} :=
mindic mD.

..copy (k \o* f) (f * cst k).
Definition : {mfun aT >-> rT} := k \o* f.

Let : @isMeasurableFun d _ aT rT (f \max g).

Proof.

by split; apply: measurable_maxr. Qed.

. f g.

Definition : {mfun aT >-> _} := f \max g.

Let : @isMeasurableFun d _ aT rT (f \min g).

Proof.

by split; apply: measurable_minr. Qed.

. f g.

Definition : {mfun aT >-> _} := f \min g.

End ring.
Arguments indic_mfun {d aT rT} _.
#[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) =>
(exact: measurable_indic ) : core.

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

Proof.

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

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

Proof.

apply: measurable_fun_ifT => //.
- apply: (measurable_fun_bool true).
rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//.
by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx.
- by apply: measurableT_comp => //; exact: measurable_funM.
Qed.

#[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) =>
solve [apply: measurable_powR] : core.

Lemma { : realType} : measurable_fun [set: R] (@powR R b).

Proof.

rewrite /powR; apply: measurable_fun_if => //.
- rewrite preimage_true setTI/=.
  case: (b == 0); rewrite ?set_true ?set_false.
  + by apply: measurableT_comp => //; exact: measurable_fun_eqr.
  + exact: measurable_fun_set0.
- rewrite preimage_false setTI; apply: measurableT_comp => //.
  exact: mulrr_measurable.
Qed.

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End ngencinfty.
End NGenCInfty.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End measurable_fun_nat.

Section standard_emeasurable_fun.
Variable : realType.

Lemma ( : set R) : measurable_fun D EFin.

Proof.

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

Lemma ( : 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.
  rewrite RGenOpenSets.measurableE.
  exact: normr_measurable.
exists set0; first by constructor.
rewrite setU0 predeqE => -[y| |]; split => /= => -[r];
  rewrite ?/= /= ?in_itv /= ?andbT => xr//.
  + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry.
  + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry.
Qed.

Lemma ( : 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 rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv leeNr.
by apply: measurableI => //; exact: emeasurable_itv.
Qed.

End standard_emeasurable_fun.
#[global] Hint Extern 0 (measurable_fun _ abse) =>
  solve [exact: abse_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ EFin) =>
  solve [exact: EFin_measurable] : core.
#[global] Hint Extern 0 (measurable_fun _ -%E) =>
  solve [exact: oppe_measurable] : core.

Lemma ( : measurableType d) ( : realType) ( : set T)
    ( : 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)); last first.
  apply: mf => //; exists A => //.
    by rewrite RGenOpenSets.measurableE//.
  by exists set0; [constructor|rewrite setU0].
congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]].
by move=> ? ?; exact: preimage_image.
Qed.

Section measurable_fun_itvW.
Context { : realType}.

Lemma ( : R) ( : itv_bound R) ( : R -> \bar R) :
measurable_fun [set` Interval (BRight a) b] f <->
measurable_fun [set` Interval (BLeft a) b] f.

Proof.

have [ab|ba] := leP (BRight a) b; last first.
by rewrite !set_itv_ge// -leNgt ?(ltW ba)// -ltBRight_leBLeft.
rewrite -setU_1itvob// measurable_funU// (propT (measurable_fun_set1 _)).
by split => // -[].
Qed.

Lemma ( : R) ( : itv_bound R) ( : R -> R) :
measurable_fun [set` Interval (BRight a) b] f <->
measurable_fun [set` Interval (BLeft a) b] f.

Proof.

by split => /measurable_EFinP/emeasurable_fun_itvob_itvcbP/measurable_EFinP.
Qed.

Lemma ( : itv_bound R) ( : R) ( : R -> \bar R) :
measurable_fun [set` Interval a (BLeft b)] f <->
measurable_fun [set` Interval a (BRight b)] f.

Proof.

have [ab|ba] := leP a (BLeft b); last first.
by rewrite !set_itv_ge// -leNgt// ltW.
rewrite -setU_itvob1// measurable_funU// (propT (measurable_fun_set1 _)).
by split => // -[].
Qed.

Lemma ( : itv_bound R) ( : R) ( : R -> R) :
measurable_fun [set` Interval a (BLeft b)] f <->
measurable_fun [set` Interval a (BRight b)] f.

Proof.

by split => /measurable_EFinP/emeasurable_fun_itvbo_itvbcP/measurable_EFinP.
Qed.

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

Proof.

move: b0 b1 => [|] [|]//.
- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
- by move/measurable_fun_itvob_itvcbP.
- move=> mf.
have : measurable_fun `[x, y] f by exact/measurable_fun_itvob_itvcbP.
by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
Qed.

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

Proof.

move: b0 b1 => [|] [|]//.
- move=> mf.
have : measurable_fun `[x, y] f by exact/measurable_fun_itvbo_itvbcP.
by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
- by move/measurable_fun_itvbo_itvbcP.
Qed.

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

Proof.

move: b0 b1 => [|] [|]//.
- by move/emeasurable_fun_itvbo_itvbcP.
- move=> mf.
have : measurable_fun `[x, y[ f by exact/emeasurable_fun_itvob_itvcbP.
by move/emeasurable_fun_itvbo_itvbcP.
- by move/emeasurable_fun_itvob_itvcbP.
Qed.

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

Proof.

by move=> /measurable_EFinP/emeasurable_fun_itvbb_itvcc/measurable_EFinP.
Qed.

End measurable_fun_itvW.
#[deprecated(since="mathcomp-analysis 1.17.0", use=emeasurable_fun_itvob_itvcbP)]
Notation := emeasurable_fun_itvob_itvcbP (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=measurable_fun_itvob_itvcbP)]
Notation := measurable_fun_itvob_itvcbP (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=emeasurable_fun_itvbo_itvbcP)]
Notation := emeasurable_fun_itvbo_itvbcP (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=measurable_fun_itvbo_itvbcP)]
Notation := measurable_fun_itvbo_itvbcP (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=measurable_fun_itvbb_itvco)]
Notation := measurable_fun_itvbb_itvco (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=measurable_fun_itvbb_itvoc)]
Notation := measurable_fun_itvbb_itvoc (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=emeasurable_fun_itvbb_itvcc)]
Notation := emeasurable_fun_itvbb_itvcc (only parsing).
#[deprecated(since="mathcomp-analysis 1.17.0", use=measurable_fun_itvbb_itvcc)]
Notation := measurable_fun_itvbb_itvcc (only parsing).

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

Proof.

by move=> /measurable_indic/measurable_EFinP. Qed.

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

Proof.

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

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

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

Proof.

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

Lemma ( : (T -> \bar R)^nat) :
(forall , measurable_fun D (f n)) ->
forall , measurable_fun D (fun => 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 ( : T -> \bar R) :
measurable_fun D f -> measurable_fun D g ->
measurable_fun D (fun => 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[)).
  rewrite predeqE => t /=; split.
    by rewrite !/= /= !in_itv /= !andbT le_max => -[Dx /orP[|]];
      tauto.
  by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_max;
    move=> [Dx ->]//; rewrite orbT.
by apply: measurableU; [exact/mf/emeasurable_itv| exact/mg/emeasurable_itv].
Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

move=> mf mD; rewrite (_ : (fun _ => _) =
    (fun => ereal_inf [set esups (f^~ x) n | in [set | n >= 0]%N])); last first.
  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)))); last first.
  exact: cvg_esups_inf.
by congr (ereal_inf [set _ | _ in _]); rewrite predeqE.
Qed.

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

Proof.

move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x).
  rewrite limn_esup_lim.
  by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx).
apply: (eq_measurable_fun (fun => 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_.

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

Let := (@wlength R idfun).

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

Proof.

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

End open_itv_cover.

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

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

Proof.

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

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

Proof.

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

End egorov.

Files

Module mathcomp.analysis.measurable_realfun