Top

Module mathcomp.analysis.lebesgue_measure

From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import reals ereal signed topology numfun normedtype function_spaces.
From HB Require Import structures.
Require Import sequences esum measure real_interval realfun exp.
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 numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


Section hlength_extension.
Context {R : realType}.

Notation hlength := (@hlength R).

Lemma hlength_semi_additive : measure.semi_additive hlength.

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

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

Lemma hlength_sigma_sub_additive :
  sigma_sub_additive (hlength : set (ocitv_type R) -> _).

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

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

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

Let sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.

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

End hlength_extension.

End LebesgueMeasure.

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

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

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

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

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

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.

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

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

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

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

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

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

End puncture_ereal_itv.

Section salgebra_R_ssets.
Variable R : realType.

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

HB.instance Definition _ := 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].
#[local] Hint Resolve measurable_set1 : core.

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

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

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

Lemma emeasurable_set1 (x : \bar R) : measurable [set x].
#[local] Hint Resolve emeasurable_set1 : core.

Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")]
Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty (only parsing).

Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")]
Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty (only parsing).

Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")]
Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty (only parsing).

Lemma __deprecated__itv_oninfty_pinfty :
  `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")]
Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty (only parsing).

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

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

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

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

Lemma elebesgue_measure0 : elebesgue_measure set0 = 0%E.

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

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

Lemma semi_sigma_additive_elebesgue_measure :
  semi_sigma_additive elebesgue_measure.

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

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

Lemma measurable_fine (R : realType) (D : set (\bar R)) : measurable D ->
  measurable_fun D fine.
#[global] Hint Extern 0 (measurable_fun _ fine) =>
  solve [exact: measurable_fine] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")]
Notation measurable_fun_fine := measurable_fine (only parsing).

Section lebesgue_measure_itv.
Variable R : realType.

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

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

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

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

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

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

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

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

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

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

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

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

End lebesgue_measure_itv.

Section measurable_ball.
Variable R : realType.

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

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

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

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

End measurable_ball.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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.

End erealgeninftyo.
End ErealGenInftyO.

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

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

Lemma stracexx G D : G D -> strace G D D.

Lemma sigma_algebra_strace G D :
  sigma_algebra setT G -> sigma_algebra D (strace G D).

End trace.

Lemma strace_measurable d (T : measurableType d) (A : set T) : measurable A ->
  strace measurable A `<=` measurable.


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

Section coutinuous_measurable.
Variable R : realType.

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

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

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

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

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

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

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

End coutinuous_measurable.

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

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

Lemma measurable_oppr D : measurable_fun D (-%R).

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

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

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

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

End standard_measurable_fun.
#[global] Hint Extern 0 (measurable_fun _ (-%R)) =>
  solve [exact: measurable_oppr] : core.
#[global] Hint Extern 0 (measurable_fun _ normr) =>
  solve [exact: measurable_normr] : core.
#[global] Hint Extern 0 (measurable_fun _ ( *%R _)) =>
  solve [exact: measurable_mulrl] : core.
#[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) =>
  solve [exact: measurable_exprn] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")]
Notation measurable_fun_sqr := measurable_exprn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")]
Notation measurable_fun_opp := measurable_oppr (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")]
Notation measurable_funN := measurable_oppr (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_normr` instead")]
Notation measurable_fun_normr := measurable_normr (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")]
Notation measurable_fun_exprn := measurable_exprn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mulrl` instead")]
Notation measurable_funrM := measurable_mulrl (only parsing).

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

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

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

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

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

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

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

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

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

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

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.

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).
#[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.
#[global] Hint Extern 0 (measurable_fun _ expR) =>
  solve [apply: measurable_expR] : core.

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

Section standard_emeasurable_fun.
Variable R : realType.

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

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

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

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

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

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

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

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

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

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

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

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

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.
End emeasurable_fun.
Arguments emeasurable_fun_cvg {d T R D} f_.

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

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

Local Open Scope ereal_scope.

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

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

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

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

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

End lebesgue_regularity.

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

Local Open Scope ereal_scope.

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

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

End egorov.

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

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

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

End vitali_theorem.