Library mathcomp.analysis.lebesgue_measure

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
Require Import boolp reals ereal classical_sets signed topology numfun.
Require Import mathcomp_extra functions normedtype.
From HB Require Import structures.
Require Import sequences esum measure fsbigop cardinality set_interval.
Require Import realfun.

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv").
Reserved Notation "R .-ocitv.-measurable"
 (at level 2, format "R .-ocitv.-measurable").

Section hlength.
Local Open Scope ereal_scope.
Variable R : realType.
Implicit Types i j : interval R.

Definition hlength (A : set R) : \bar R := let i := Rhull A in i.2 - 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 - 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_hlengthE 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 pinfty_hlength i : hlength [set` i] = +oo →
  (∃ s r, i = Interval -oo%O (BSide s r) ∨ i = Interval (BSide s r) +oo%O)
  ∨ i = `]-oo, +oo[.

Lemma hlength_ge0 i : 0 ≤ hlength [set` i].
Local Hint Extern 0 (0%:E ≤ hlength _) ⇒ solve[apply: hlength_ge0] : core.

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

End hlength.
Arguments hlength {R}.
#[global] Hint Extern 0 (0%:E ≤ hlength _) ⇒ solve[apply: hlength_ge0] : core.

Section itv_semiRingOfSets.
Variable R : realType.
Implicit Types (I J K : set R).
Definition ocitv_type : Type := R.

Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R × R]].

Lemma is_ocitv a b : ocitv `]a, b]%classic.
Hint Extern 0 (ocitv _) ⇒ solve [apply: is_ocitv] : core.

Lemma ocitv0 : ocitv set0.
Hint Resolve ocitv0 : core.

Lemma ocitvP X : ocitv X ↔ X = set0 ∨ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic.

Lemma ocitvD : semi_setD_closed ocitv.

Lemma ocitvI : setI_closed ocitv.

Definition ocitv_display : Type → measure_display.


Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type))) :
  classical_set_scope.

Lemma hlength_ge0' (I : set ocitv_type) : (0 ≤ hlength I)%E.

Lemma hlength_semi_additive : semi_additive (hlength : set ocitv_type → _).


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

Lemma hlength_sigma_sub_additive :
  sigma_sub_additive (hlength : set ocitv_type → _).

Lemma hlength_sigma_finite : sigma_finite [set: ocitv_type] hlength.

Let gitvs := [the semiRingOfSetsType _ of salgebraType ocitv].

Definition lebesgue_measure := Hahn_ext
  [the additive_measure _ _ of hlength : set ocitv_type → _].

Let lebesgue_measure0 : lebesgue_measure set0 = 0%E.

Let lebesgue_measure_ge0 : ∀ x, (0 ≤ lebesgue_measure x)%E.

Let lebesgue_measure_semi_sigma_additive : semi_sigma_additive lebesgue_measure.


End itv_semiRingOfSets.
Arguments lebesgue_measure {R}.

Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
  classical_set_scope.

Section lebesgue_measure.
Variable R : realType.
Let gitvs := [the measurableType _ of salgebraType (@ocitv R)].

Lemma lebesgue_measure_unique (mu : {measure set gitvs → \bar R}) :
  (∀ X, ocitv X → hlength X = mu X) →
  ∀ X, measurable X → lebesgue_measure X = mu X.

End lebesgue_measure.

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) :
  (∀ i, emeasurable (F i)) → emeasurable (\bigcup_i (F i)).

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

End salgebra_ereal.

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

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

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

Lemma set1_bigcap_oc (R : realType) (r : R) :
   [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.

Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
  [set` Interval (BSide b r) (BLeft s)] =
  \bigcup_n [set` Interval (BSide b r) (BRight (s - n.+1%:R^-1))].

Lemma itv_open_bnd_bigcup (R : realType) b (r s : R) :
  [set` Interval (BRight s) (BSide b r)] =
  \bigcup_n [set` Interval (BLeft (s + n.+1%:R^-1)) (BSide b r)].

Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) :
  [set` Interval (BSide b x) +oo%O] =
  \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))].

Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
  [set` Interval -oo%O (BSide b x)] =
  \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)].

Section salgebra_R_ssets.
Variable R : realType.

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

Lemma measurable_set1 (r : R) : measurable [set r].
#[local] Hint Resolve measurable_set1 : core.

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

Lemma measurable_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 itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).

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

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

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

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

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

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


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

Section lebesgue_measure_itv.
Variable R : realType.

Let lebesgue_measure_itvoc (a b : R) :
  (lebesgue_measure (`]a, b] : set R) = hlength `]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) = hlength `]a, b[)%classic.

Let lebesgue_measure_itvcc (a b : R) :
  (lebesgue_measure (`[a, b] : set R) = hlength `[a, b])%classic.

Let lebesgue_measure_itvco (a b : R) :
  (lebesgue_measure (`[a, b[ : set R) = hlength `[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) =
  hlength [set` Interval (BSide x a) (BSide y b)].

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

Lemma lebesgue_measure_itv (i : interval R) :
  lebesgue_measure ([set` i] : set R) = hlength [set` i].

End lebesgue_measure_itv.

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

Section measurable_fun_measurable.
Local Open Scope ereal_scope.
Variables (d : measure_display) (T : measurableType d).
Variables (R : realType) (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 | ∃ 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 :
  (R.-ocitv.-measurable).-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 | ∃ 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 : (R.-ocitv.-measurable).-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 | ∃ 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 : (R.-ocitv.-measurable).-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 | ∃ x y, A = `]x, y[%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 : (R.-ocitv.-measurable).-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_c_infty r : `[r%:E, +oo[%classic =
  \bigcap_k `](r - k.+1%:R^-1)%:E, +oo[%classic :> set _.

Lemma eitv_infty_c r : `]-oo, r%:E]%classic =
  \bigcap_k `]-oo, (r%:E + k.+1%:R^-1%:E)]%classic :> set _.

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

Lemma eset1_pinfty :
  [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 | ∃ x, A = `]x, +oo[%classic].

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

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

Lemma measurableE : emeasurable (R.-ocitv.-measurable) = 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 | ∃ x, A = `[x, +oo[%classic].

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

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

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

End erealgencinfty.
End ErealGenCInfty.

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 (U : set R) : open U → measurable U.

Lemma continuous_measurable_fun (f : R → R) : continuous f →
  measurable_fun setT f.

End coutinuous_measurable.

Section standard_measurable_fun.

Lemma measurable_fun_normr (R : realType) (D : set R) :
  measurable_fun D (@normr _ R).

End standard_measurable_fun.

Section measurable_fun_realType.
Variables (d : measure_display) (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_funrM D f (k : R) : measurable_fun D f →
  measurable_fun D (fun x ⇒ k × f x).

Lemma measurable_funN D f : measurable_fun D f → measurable_fun D (-%R \o f).

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

Lemma measurable_fun_exprn D n f :
  measurable_fun D f → measurable_fun D (fun x ⇒ f x ^+ n).

Lemma measurable_fun_sqr D f :
  measurable_fun D f → measurable_fun D (fun x ⇒ f x ^+ 2).

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

Lemma measurable_fun_max D f g :
  measurable_fun D f → measurable_fun D g → measurable_fun D (f \max g).

Lemma measurable_fun_sups D (h : (T → R)^nat) n :
  (∀ t, D t → has_ubound (range (h ^~ t))) →
  (∀ 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 :
  (∀ t, D t → has_lbound (range (h ^~ t))) →
  (∀ n, measurable_fun D (h n)) →
  measurable_fun D (fun x ⇒ infs (h ^~ x) n).

Lemma measurable_fun_lim_sup D (h : (T → R)^nat) :
  (∀ t, D t → has_ubound (range (h ^~ t))) →
  (∀ t, D t → has_lbound (range (h ^~ t))) →
  (∀ n, measurable_fun D (h n)) →
  measurable_fun D (fun x ⇒ lim_sup (h ^~ x)).

Lemma measurable_fun_cvg D (h : (T → R)^nat) f :
  (∀ m, measurable_fun D (h m)) → (∀ x, D x → h ^~ x --> f x) →
  measurable_fun D f.

End measurable_fun_realType.

Section standard_emeasurable_fun.
Variable R : realType.

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

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

Lemma emeasurable_fun_minus (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_fun_abse] : core.
#[global] Hint Extern 0 (measurable_fun _ EFin) ⇒
  solve [exact: measurable_fun_EFin] : core.

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.

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

Lemma measurable_fun_einfs D (f : (T → \bar R)^nat) :
  (∀ n, measurable_fun D (f n)) →
  ∀ n, measurable_fun D (fun x ⇒ einfs (f ^~ x) n).

Lemma measurable_fun_esups D (f : (T → \bar R)^nat) :
  (∀ n, measurable_fun D (f n)) →
  ∀ n, measurable_fun D (fun x ⇒ esups (f ^~ x) n).

Lemma emeasurable_fun_max 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 emeasurable_funN D (f : T → \bar R) :
  measurable_fun D f → measurable_fun D (\- f).

Lemma emeasurable_fun_funepos D (f : T → \bar R) :
  measurable_fun D f → measurable_fun D f^\+.

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

Lemma emeasurable_fun_min 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_elim_sup D (f : (T → \bar R)^nat) :
  (∀ n, measurable_fun D (f n)) →
  measurable_fun D (fun x ⇒ elim_sup (f ^~ x)).

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

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