Top

Module mathcomp.analysis.measurable_realfun

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


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

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

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

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

Proof.

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

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

Proof.

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

End ps_infty.

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

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

Lemma emeasurable0 : emeasurable set0.

Proof.

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

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

Proof.

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

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

Proof.

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

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

End salgebra_ereal.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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 := g_sigma_algebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
  (R.-ocitv.-measurable).-sigma.-measurable.

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

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

Proof.

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

#[local] Hint Resolve measurable_set1 : core.

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

Proof.

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

#[local] Hint Resolve measurable_itv : core.

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

Proof.

have [ab|ab] := leP a (BLeft b).
- move: a => [a0 a|[|//]] in ab *;
    move=> mf; rewrite -setUitv1//; apply/measurable_funU => //;
    by split => //; exact: measurable_fun_set1.
- move: a => [[|] a|[|]//] in ab *; rewrite bnd_simp in ab.
  + move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//.
    exact: measurable_fun_set0.
  + move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//.
    exact: measurable_fun_set0.
Qed.

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

Proof.

have [ab|ab] := leP (BRight a) b.
- move: b => [[|] b|[//|]] in ab *;
    move=> mf; rewrite -setU1itv//; apply/measurable_funU => //;
    by split => //; exact: measurable_fun_set1.
- move: b => [[|] b|[|//]] in ab *; rewrite bnd_simp in ab.
  + move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//.
    exact: measurable_fun_set0.
  + move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//.
    exact: measurable_fun_set0.
  + by move=> _; rewrite set_itv_ge//=; exact: measurable_fun_set0.
Qed.

#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")]
Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) :
  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
  measurable_fun `[x, y[ f.

Proof.

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

#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_bndo_bndc` instead")]
Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) :
  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
  measurable_fun `]x, y] f.

Proof.

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

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

Proof.

move: b0 b1 => [|] [|]//.
- exact: measurable_fun_itv_bndo_bndc.
- move=> mf.
  have : measurable_fun `[x, y[ f by exact: measurable_fun_itv_obnd_cbnd.
  exact: measurable_fun_itv_bndo_bndc.
- exact: measurable_fun_itv_obnd_cbnd.
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.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite ball_itv; exact: measurable_itv. Qed.

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

Proof.

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

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

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

Proof.

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

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

by rewrite -preimage_itvNyc; 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.
  exact/measurableI/emeasurable_fun_infty_c/emeasurable_fun_c_infty.
rewrite predeqE => t; split => [/= [Dt ft]|].
  exists `|ceil `|fine (f t)| |%N => //=; split=> //; split.
    rewrite -[leRHS](fineK ft) lee_fin lerNl pmulrn abszE ceil_ge_int ger0_norm.
      by rewrite ceil_le// -normrN ler_norm.
    by rewrite -(ceil0 R) ceil_le.
  rewrite -[leLHS](fineK ft) lee_fin pmulrn abszE ceil_ge_int ger0_norm.
    by rewrite ceil_le// ler_norm.
  by rewrite -(ceil0 R) ceil_le.
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 lerBlDl (le_trans rs)// lerDr.
    * by rewrite lte_fin ltrBlDl (le_lt_trans rs)// ltrDr.
  + by rewrite /= in_itv /= andbT; case: b => /=; rewrite lteey.
- move: x => [s| |/(_ 0%N Logic.I)] /=; rewrite ?in_itv/= ?leey//; last first.
    by case: b.
  move=> h; rewrite lee_fin leNgt andbT; apply/negP => /ltr_add_invr[k skr].
  have {h} := h k Logic.I; rewrite /= in_itv /= andbT; case: b => /=.
  + by rewrite lee_fin lerBlDr leNgt skr.
  + by rewrite lte_fin ltrBlDr ltNge (ltW skr).
Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

End erealwithrays.

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

Local Open Scope ereal_scope.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End erealgenoinfty.
End ErealGenOInfty.

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End erealgencinfty.
End ErealGenCInfty.

Module ErealGenInftyO.
Section erealgeninftyo.
Variable R : realType.

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

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

Proof.

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

End erealgeninftyo.
End ErealGenInftyO.


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

Proof.

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

Section coutinuous_measurable.
Variable R : realType.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End coutinuous_measurable.

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

Proof.

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

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

Lemma oppr_measurable D : measurable_fun D -%R.

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

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

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

Proof.

move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy.
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_itvoy; apply: mf => //; exact: measurable_itv.
  - by rewrite -preimage_itvoy; apply: mg => //; exact: measurable_itv.
rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]].
  rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h.
  exists r => //; rewrite setIACA setIid; split => //; split => /=.
    by rewrite h.
  by rewrite ltrBlDr addrC -ltrBlDr h.
by rewrite ltrBlDr=> afg; rewrite (lt_le_trans afg)// addrC lerD2r ltW.
Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

Lemma measurable_indicP D : 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.
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")]
Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing).

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

Proof.

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

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

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

Proof.

by apply: continuous_measurable_fun; exact: continuous_expR. Qed.

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

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

Proof.

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

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

Proof.

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

#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")]
Notation measurable_fun_pow := measurable_funX (only parsing).

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

Proof.

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

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

Lemma measurable_powRr {R : realType} b : 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.

#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")]
Notation measurable_fun_max := measurable_maxr (only parsing).

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End ngencinfty.
End NGenCInfty.

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

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

Proof.

move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
rewrite [X in measurable X](_ : _ = \bigcup_q
  ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))).
  apply: bigcupT_measurable => q; apply: measurableI.
  - by rewrite -preimage_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_maxn D f g : measurable_fun D f -> measurable_fun D g ->
  measurable_fun D (fun x => maxn (f x) (g x)).

Proof.

move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ =
  ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))).
  apply: measurableU.
  - by rewrite -preimage_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 measurable_fun_subn' D f g : (forall t, g t <= f t)%N ->
  measurable_fun D f -> measurable_fun D g ->
  measurable_fun D (fun x => f x - g x)%N.

Proof.

move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
rewrite [X in measurable X](_ : _ = \bigcup_q
  ((D `&` [set x | maxn a q <= f x]%O) `&`
   (D `&` [set x | g x <= (q - a)%N]%O))).
  apply: bigcupT_measurable => q; apply: measurableI.
  - by rewrite -preimage_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//; last first.
    by have := leq_ltn_trans rfx afx; rewrite ltnNge leq_maxl.
  by move=> /leq_trans; apply; rewrite (leq_trans _ rfx)//; exact: leq_maxr.
Qed.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

End measurable_fun_nat.

Section standard_emeasurable_fun.
Variable R : realType.

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

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

Proof.

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

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

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

Proof.

by move=> /measurable_indic/measurable_EFinP. Qed.

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

Proof.

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

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

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

Proof.

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

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

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

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

Let l := (@wlength R idfun).

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

Proof.

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

End open_itv_cover.

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

Local Open Scope ereal_scope.

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

Proof.

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

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

Proof.

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

End egorov.