From f71831742c9207cd7d3026e214b0242832ea3302 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Sun, 8 Sep 2024 23:12:24 +0900 Subject: [PATCH] fixes #1313 and moves Egorov (#1314) * fixes #1313 --- theories/lebesgue_integral.v | 27 +- theories/lebesgue_measure.v | 3590 +++++++++++++++++----------------- theories/normedtype.v | 2 +- theories/topology.v | 12 +- 4 files changed, 1821 insertions(+), 1810 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 74e0de193..d2e152fb3 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6051,21 +6051,16 @@ Let norm1 D f := \int[mu]_(y in D) `|(f y)%:E|. Lemma maximal_inequality f c : locally_integrable setT f -> (0 < c)%R -> - mu [set x | HL f x > c%:E] <= (3%:R / c)%:E * norm1 setT f. + mu [set x | HL f x > c%:E] <= (3 / c)%:E * norm1 setT f. Proof. move=> /= locf c0. -have r_proof x : HL f x > c%:E -> {r | (0 < r)%R & - \int[mu]_(y in ball x r) `|(f y)%:E| > c%:E * mu (ball x r)}. - move=> /ereal_sup_gt/cid2[y /= /cid2[r]]. - rewrite in_itv/= andbT => rg0 <-{y} Hc; exists r => //. - rewrite -(@fineK _ (mu (ball x r))) ?ge0_fin_numE//; last first. - by rewrite lebesgue_measure_ball ?ltry// ltW. - rewrite -lte_pdivlMr// 1?muleC// fine_gt0//. - by rewrite lebesgue_measure_ball 1?ltW// ltry lte_fin mulrn_wgt0. rewrite lebesgue_regularity_inner_sup//; last first. rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. exact: measurable_HL_maximal. apply: ub_ereal_sup => /= x /= [K [cK Kcmf <-{x}]]. +have r_proof x : HL f x > c%:E -> {r | (0 < r)%R & iavg f (ball x r) > c%:E}. + move=> /ereal_sup_gt/cid2[y /= /cid2[r]]. + by rewrite in_itv/= andbT => rg0 <-{y} Hc; exists r. pose r_ x := if pselect (HL f x > c%:E) is left H then s2val (r_proof _ H) else 1%R. have r_pos (x : R) : (0 < r_ x)%R. @@ -6073,7 +6068,13 @@ have r_pos (x : R) : (0 < r_ x)%R. have cMfx_int x : c%:E < HL f x -> \int[mu]_(y in ball x (r_ x)) `|(f y)|%:E > c%:E * mu (ball x (r_ x)). move=> cMfx; rewrite /r_; case: pselect => //= => {}cMfx. - by case: (r_proof _ cMfx). + case: (r_proof _ cMfx) => /= r r0. + have ? : 0%R < (fine (mu (ball x r)))%:E. + rewrite lte_fin fine_gt0// (lebesgue_measure_ball _ (ltW r0))// ltry. + by rewrite lte_fin mulrn_wgt0. + rewrite /iavg -(@lte_pmul2r _ (fine (mu (ball x r)))%:E)//. + rewrite muleAC -[in X in _ < X]EFinM mulVf ?gt_eqF// mul1e fineK//. + by rewrite ge0_fin_numE// (lebesgue_measure_ball _ (ltW r0)) ltry. set B := fun r => ball r (r_ r). have {}Kcmf : K `<=` cover [set i | HL f i > c%:E] (fun i => ball i (r_ i)). by move=> r /Kcmf /= cMfr; exists r => //; exact: ballxx. @@ -6086,10 +6087,10 @@ have KDB : K `<=` cover [set` D] B. have is_ballB i : is_ball (B i) by exact: is_ball_ball. have Bset0 i : B i !=set0 by exists i; exact: ballxx. have [E [uE ED tEB DE]] := @vitali_lemma_finite_cover _ _ B is_ballB Bset0 D. -rewrite (@le_trans _ _ (3%:R%:E * \sum_(i <- E) mu (B i)))//. +rewrite (@le_trans _ _ (3%:E * \sum_(i <- E) mu (B i)))//. have {}DE := subset_trans KDB DE. - apply: (le_trans (@content_subadditive _ _ _ [the measure _ _ of mu] - K (fun i => 3%:R *` B (nth 0%R E i)) (size E) _ _ _)) => //. + apply: (le_trans (@content_subadditive _ _ _ mu K + (fun i => 3 *` B (nth 0%R E i)) (size E) _ _ _)) => //. - by move=> k ?; rewrite scale_ballE//; exact: measurable_ball. - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. - apply: (subset_trans DE); rewrite /cover bigcup_seq. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 182f4f37a..eafcde9f9 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -11,28 +11,24 @@ Require Export lebesgue_stieltjes_measure. (**md**************************************************************************) (* # Lebesgue Measure *) (* *) -(* This file contains a formalization of the Lebesgue measure using the *) -(* Measure Extension theorem from measure.v, further develops the theory of *) -(* of measurable functions, and prove properties of the Lebesgue measure *) -(* such as Vitali's covering lemma (infinite case), i.e., given a Vitali *) -(* cover $V$ of $A$, there exists a countable subcollection $D \subseteq V$ *) -(* of pairwise disjoint closed balls such that *) -(* $\lambda(A \setminus \bigcup_k D_k) = 0$. *) +(* This file further develops the theory of measurable functions (including *) +(* Egorov's theorem), contains a formalization of the Lebesgue measure using *) +(* the Measure Extension theorem from measure.v, and proves properties of the *) +(* Lebesgue measure such as Vitali's theorem, i.e., given a Vitali cover $V$ *) +(* of $A$, there exists a countable subcollection $D \subseteq V$ of pairwise *) +(* disjoint closed balls such that $\lambda(A \setminus \bigcup_k D_k) = 0$. *) (* *) (* Main references: *) (* - Daniel Li, Intégration et applications, 2016 *) (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) (* ``` *) -(* lebesgue_measure == the Lebesgue measure *) -(* completed_lebesgue_measure == the completed Lebesgue measure *) (* completed_algebra_gen == generator of the completed Lebesgue *) (* sigma-algebra *) (* ps_infty == inductive definition of the powerset *) (* {0, {-oo}, {+oo}, {-oo,+oo}} *) (* emeasurable G == sigma-algebra over \bar R built out of the *) (* measurables G of a sigma-algebra over R *) -(* elebesgue_measure == the Lebesgue measure extended to \bar R *) (* ``` *) (* *) (* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) @@ -45,6 +41,12 @@ Require Export lebesgue_stieltjes_measure. (* rays and closed rays. *) (* *) (* ``` *) +(* lebesgue_measure == the Lebesgue measure *) +(* completed_lebesgue_measure == the completed Lebesgue measure *) +(* elebesgue_measure == the Lebesgue measure extended to \bar R *) +(* ``` *) +(* *) +(* ``` *) (* vitali_cover A B V == V is a Vitali cover of A, here B is a *) (* collection of non-empty closed balls *) (* ``` *) @@ -60,2062 +62,2166 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -(* This module contains a direct construction of the Lebesgue measure that is - kept here for archival purpose. The Lebesgue measure is actually defined as - an instance of the Lebesgue-Stieltjes measure. *) -Module LebesgueMeasure. -Section hlength. -Context {R : realType}. +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. -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. +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 hlength0 : hlength (set0 : set R) = 0. -Proof. by rewrite /hlength Rhull0 /= subee. Qed. +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 hlength_singleton (r : R) : hlength `[r, r] = 0. +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. -rewrite /hlength /= asboolT// sup_itvcc//= asboolT//. -by rewrite asboolT inf_itvcc//= ?subee// inE. +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. -Lemma hlength_setT : hlength setT = +oo%E :> \bar R. -Proof. by rewrite /hlength RhullT. Qed. +End ps_infty. -Lemma hlength_itv i : - hlength [set` i] = if i.2 > i.1 then (i.2 : \bar R) - i.1 else 0. +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. -case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK. -rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first. - rewrite (_ : [set` i] = set0) ?hlength0//. - by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12). -case: i => -[ba a|[|]] [bb b|[|]] //=. -- rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try - by rewrite set_itvE hlength0. - by rewrite hlength_singleton. -- by move=> _; rewrite set_itvE hlength0. -- by move=> _; rewrite set_itvE hlength0. +exists set0; first exact: measurable0. +by exists set0; rewrite ?setU0// ?image_set0//; constructor. Qed. -Lemma hlength_finite_fin_num i : neitv i -> hlength [set` i] < +oo -> - ((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num). +Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X). Proof. -move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx. -by move=> _; rewrite hlength_itv /= ltry. -by move=> _; rewrite hlength_itv /= ltNyr. -by move=> _; rewrite hlength_itv. +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 finite_hlength_itv i : neitv i -> hlength [set` i] < +oo -> - hlength [set` i] = (fine i.2)%:E - (fine i.1)%:E. +Lemma bigcupT_emeasurable (F : (set \bar R)^nat) : + (forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)). Proof. -move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo. -rewrite !fineK// hlength_itv; case: ifPn => //. -rewrite -leNgt le_eqVlt => /predU1P[->|]; first by rewrite subee. -by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->. +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. -Lemma hlength_infty_bnd b r : - hlength [set` Interval -oo%O (BSide b r)] = +oo :> \bar R. -Proof. by rewrite hlength_itv /= ltNyr. Qed. +Definition ereal_isMeasurable : isMeasurable default_measure_display (\bar R) := + isMeasurable.Build _ _ + emeasurable0 emeasurableC bigcupT_emeasurable. -Lemma hlength_bnd_infty b r : - hlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R. -Proof. by rewrite hlength_itv /= ltry. Qed. +End salgebra_ereal. -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[. +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 hlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|]. -- by case: ifPn. -- by left; exists ba, a; right. -- by left; exists bb, b; left. -- by right. +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 hlength_itv_ge0 i : 0 <= hlength [set` i]. +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 hlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |]. -- by rewrite suber_ge0//; exact: ltW. -- by rewrite ltNge leey. -- by move=> i2gtNy; rewrite addey//; case: (i.2 : \bar R) i2gtNy. +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 hlength_Rhull (A : set R) : hlength [set` Rhull A] = hlength A. -Proof. by rewrite /hlength Rhull_involutive. Qed. - -Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j]. +Lemma punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set~ -oo]. Proof. -set I := [set` i]; set J := [set` j]. -have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_itv_ge0. -have [J0|/set0P J0] := eqVneq J set0. - by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->. -move=> /subset_itvP ij; apply: leeB => /=. - have [ui|ui] := asboolP (has_ubound I). - have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey. - by rewrite lee_fin le_sup // => r Ir; exists r; split => //; apply: ij. - have [uj /=|//] := asboolP (has_ubound J). - by move: ui; have := subset_has_ubound ij uj. -have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye. -have [li /=|li] := asboolP (has_lbound I); last first. - by move: li; have := subset_has_lbound ij lj. -rewrite lee_fin lerNl opprK le_sup// ?has_inf_supN//; last exact/nonemptyN. -move=> r [r' Ir' <-{r}]; exists (- r')%R. -by split => //; exists r' => //; apply: ij. +rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. +by move=> [x| |] //= _; [left; exists x|right]. Qed. -Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}. +Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo]. Proof. -move=> a b /le_Rhull /le_hlength_itv. -by rewrite (hlength_Rhull a) (hlength_Rhull b). +rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. +by move=> [x| |] //= _; [left; exists x|right]. Qed. -Lemma hlength_ge0 I : (0 <= hlength I)%E. -Proof. by rewrite -hlength0 le_hlength. Qed. +End puncture_ereal_itv. -End hlength. -#[local] Hint Extern 0 (is_true (0%R <= hlength _)) => - solve[apply: hlength_ge0] : core. +Section salgebra_R_ssets. +Variable R : realType. -(* Unused *) -(* Lemma hlength_semi_additive2 : semi_additive2 hlength. *) -(* Proof. *) -(* move=> I J /ocitvP[|[a a12]] ->; first by rewrite set0U hlength0 add0e. *) -(* move=> /ocitvP[|[b b12]] ->; first by rewrite setU0 hlength0 adde0. *) -(* rewrite -subset0 => + ab0 => /ocitvP[|[x x12] abx]. *) -(* by rewrite setU_eq0 => -[-> ->]; rewrite setU0 hlength0 adde0. *) -(* rewrite abx !hlength_itv//= ?lte_fin a12 b12 x12/= -!EFinB -EFinD. *) -(* wlog ab1 : a a12 b b12 ab0 abx / a.1 <= b.1 => [hwlog|]. *) -(* have /orP[ab1|ba1] := le_total a.1 b.1; first by apply: hwlog. *) -(* by rewrite [in RHS]addrC; apply: hwlog => //; rewrite (setIC, setUC). *) -(* have := ab0; rewrite subset0 -set_itv_meet/=. *) -(* rewrite /Order.join /Order.meet/= ?(andbF, orbF)/= ?(meetEtotal, joinEtotal). *) -(* rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _. *) -(* move=> /eqP/neitvP/=; rewrite bnd_simp/= /d/c (max_idPr _)// => /negP. *) -(* rewrite -leNgt le_minl orbC lt_geF//= => {c} {d} a2b1. *) -(* have ab i j : i \in `]a.1, a.2] -> j \in `]b.1, b.2] -> i <= j. *) -(* by move=> ia jb; rewrite (le_le_trans _ _ a2b1) ?(itvP ia) ?(itvP jb). *) -(* have /(congr1 sup) := abx; rewrite sup_setU// ?sup_itv_bounded// => bx. *) -(* have /(congr1 inf) := abx; rewrite inf_setU// ?inf_itv_bounded// => ax. *) -(* rewrite -{}ax -{x}bx in abx x12 *. *) -(* case: ltgtP a2b1 => // a2b1 _; last first. *) -(* by rewrite a2b1 [in RHS]addrC subrKA. *) -(* exfalso; pose c := (a.2 + b.1) / 2%:R. *) -(* have /predeqP/(_ c)[_ /(_ _)/Box[]] := abx. *) -(* apply: subset_itv_oo_oc; have := mid_in_itvoo a2b1. *) -(* by apply/subitvP; rewrite subitvE ?bnd_simp/= ?ltW. *) -(* apply/not_orP; rewrite /= !in_itv/=. *) -(* by rewrite lt_geF ?midf_lt//= andbF le_gtF ?midf_le//= ltW. *) -(* Qed. *) +Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). +Definition measurableR : set (set R) := + (R.-ocitv.-measurable).-sigma.-measurable. -Section hlength_extension. -Context {R : realType}. +HB.instance Definition _ := Pointed.on R. +HB.instance Definition R_isMeasurable : + isMeasurable default_measure_display R := + @isMeasurable.Build _ measurableTypeR measurableR + measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +(*HB.instance (Real.sort R) R_isMeasurable.*) -Notation hlength := (@hlength R). +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 hlength_semi_additive : measure.semi_additive hlength. +Lemma measurable_itv (i : interval R) : measurable [set` i]. Proof. -move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->. -move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->. -rewrite hlength_itv ?lte_fin/= -EFinB. -case: ifPn => a12; last first. - pose I i := `](b i).1, (b i).2]%classic. - rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0. - by under eq_bigr => i _ do rewrite I0//= hlength0; rewrite big1. -set A := `]a1, a2]%classic. -rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//. -move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *. -rewrite ltnS => cP /esym AE. -have : A a2 by rewrite /A /= in_itv/= lexx andbT. -rewrite AE/= => -[i /= Pi] a2bi. -case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi. -have {}a2bi : a2 = (b i).2. - apply/eqP; rewrite eq_le (itvP a2bi)/=. - suff: A (b i).2 by move=> /itvP->. - by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT. -rewrite {a2}a2bi in a12 A AE *. -rewrite (bigD1 i)//= hlength_itv ?lte_fin/= bi !EFinD -addeA. -congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//. -rewrite ?EFinN oppeK addeC; apply/eqP. -case: (eqVneq a1 (b i).1) => a1bi. - rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j. - move=> /andP[Pj Nji]; rewrite hlength_itv ?lte_fin/=; case: ifPn => bj//. - exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv. - pose m := ((b j).1 + (b j).2) / 2%:R. - have mbj : `](b j).1, (b j).2]%classic m. - by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW. - rewrite -subset0 => /(_ m); apply; split=> //. - by suff: A m by []; rewrite AE; exists j => //. -have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2. - move=> Pj bj; suff /itvP-> : A (b j).2 by []. - by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=. -have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1. - move=> Pj bj; case: ltP=> // bj1a. - suff : A a1 by rewrite /A/= in_itv/= ltxx. - by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2. -have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2. - move=> Pj bj; suff /itvP-> : A (b j).2 by []. - by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=. -apply/IHp. -- by rewrite lt_neqAle a1bi/= a1b. -- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P). - rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first. - by move=> j; rewrite !inE andbC; case: eqVneq => // ->. - rewrite ?card1 ?ltnS// subset_leq_card//. - by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC. -apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi]. - case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge. - apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt. - have /trivIsetP/(_ j i I I Nji) := Itriv. - rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2. - by rewrite !in_itv/= bj !lexx bi1j2 bbi2. -have: A x. - rewrite /A/= in_itv/= (itvP xabi)/= ltW//. - by rewrite (le_lt_trans _ bi) ?(itvP xabi). -rewrite AE => -[j /= Pj xbj]. -exists j => //=. -apply/andP; split=> //; apply: contraTneq xbj => ->. -by rewrite in_itv/= le_gtF// (itvP xabi). +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. -HB.instance Definition _ := isContent.Build _ _ R - hlength hlength_ge0 hlength_semi_additive. - -Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core. +HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). +(* NB: Until we dropped support for Coq 8.12, we were using +HB.instance (\bar (Real.sort R)) + (ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))). +This was producing a warning but the alternative was failing with Coq 8.12 with + the following message (according to the CI): + # [redundant-canonical-projection,typechecker] + # forall (T : measurableType) (f : T -> R), measurable_fun setT f + # : Prop + # File "./theories/lebesgue_measure.v", line 4508, characters 0-88: + # Error: Anomaly "Uncaught exception Failure("sep_last")." + # Please report at http://coq.inria.fr/bugs/. +*) -Lemma hlength_sigma_subadditive : - measurable_subset_sigma_subadditive (hlength : set (ocitv_type R) -> _). +Lemma measurable_image_EFin (A : set R) : + measurableR A -> measurable (EFin @` A). Proof. -move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-]. -rewrite /subset_sigma_subadditive hlength_itv ?lte_fin/= -EFinB => lebig. -case: ifPn => a12; last by rewrite nneseries_esum// esum_ge0. -apply/lee_addgt0Pr => _ /posnumP[e]. -rewrite [e%:num]splitr [in leRHS]EFinD addeA -leeBlDr//. -apply: le_trans (epsilon_trick _ _ _) => //=. -have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R. - by rewrite divr_gt0// ltr0n// expn_gt0. -have eVn_ge0 n := ltW (eVn_gt0 n). -pose Aoo i : set (ocitv_type R) := - `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic. -pose Aoc i : set (ocitv_type R) := - `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R]%classic. -have: `[a.1 + e%:num / 2, a.2] `<=` \bigcup_i Aoo i. - apply: (@subset_trans _ `]a.1, a.2]). - move=> x; rewrite /= !in_itv /= => /andP[+ -> //]. - by move=> /lt_le_trans-> //; rewrite ltrDl. - apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=. - move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=. - by rewrite ltrDl. -have := @segment_compact _ (a.1 + e%:num / 2) a.2; rewrite compact_cover. -move=> /[apply]-[i _|X _ Xc]; first exact: interval_open. -have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i. - move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix. - by exists i => //; apply: subset_itv_oo_oc Aooix. -have /[apply] := @content_sub_fsum _ _ _ - [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X]. -move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans. - rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD. - by case: ltP => //; rewrite lee_fin subr_le0. -rewrite nneseries_esum//; last by move=> *; rewrite adde_ge0//= ?lee_fin. -rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=. -rewrite fsbig_finite//= set_fsetK//. -rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=. -do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW. - by rewrite addrAC. -by rewrite addrAC lee_fin lerD// subr_le0 leNgt. +by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0]. Qed. -HB.instance Definition _ := Content_SigmaSubAdditive_isMeasure.Build _ _ _ - hlength hlength_sigma_subadditive. - -Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _). +Lemma emeasurable_set1 (x : \bar R) : measurable [set x]. Proof. -exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT. -by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry. +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. -Definition lebesgue_measure := measure_extension hlength. -HB.instance Definition _ := Measure.on lebesgue_measure. +Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R). +Proof. by rewrite itv_cyy. Qed. +#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")] +Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty (only parsing). -Let sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure. -Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed. +Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R). +Proof. by rewrite itv_oyy. Qed. +#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")] +Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty (only parsing). -HB.instance Definition _ := @isSigmaFinite.Build _ _ _ - lebesgue_measure sigmaT_finite_lebesgue_measure. +Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R). +Proof. by rewrite itv_cNyy. Qed. +#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")] +Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty (only parsing). -End hlength_extension. +Lemma __deprecated__itv_oninfty_pinfty : + `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R). +Proof. by rewrite itv_oNyy. Qed. +#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")] +Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty (only parsing). -End LebesgueMeasure. +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. -Definition lebesgue_measure {R : realType} : - set [the measurableType _.-sigma of - g_sigma_algebraType R.-ocitv.-measurable] -> \bar R := - [the measure _ _ of lebesgue_stieltjes_measure idfun]. -HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). -HB.instance Definition _ (R : realType) := - SigmaFiniteMeasure.on (@lebesgue_measure R). +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. -Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R := - [the measure _ _ of completed_lebesgue_stieltjes_measure idfun]. -HB.instance Definition _ (R : realType) := - Measure.on (@completed_lebesgue_measure R). -HB.instance Definition _ (R : realType) := - SigmaFiniteMeasure.on (@completed_lebesgue_measure R). +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 completed_lebesgue_measure_is_complete {R : realType} : - measure_is_complete (@completed_lebesgue_measure R). -Proof. exact: measure_is_complete_caratheodory. 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. -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]. +Lemma measurable_ball (x : R) e : measurable (ball x e). +Proof. by rewrite ball_itv; exact: measurable_itv. Qed. -(* the completed sigma-algebra is the same as the caratheodory sigma-algebra *) -Section completed_algebra_caratheodory. -Context {R : realType}. -Local Open Scope ereal_scope. +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. -Notation hlength := (@wlength R idfun). -Notation mu := (@lebesgue_measure R). -Notation completed_mu := (@completed_lebesgue_measure R). +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). -Let cara_sub_calgebra : hlength^*%mu.-cara.-measurable `<=` - (completed_algebra_gen mu).-sigma.-measurable. +Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D -> + measurable_fun D fine. Proof. -move=> E; wlog : E / completed_mu E < +oo. - move=> /= wlg. - have /sigma_finiteP[/= F [UFI ndF mF]] := - measure_extension_sigma_finite (@wlength_sigma_finite R idfun). - move=> mE. - rewrite -(setIT E)/= UFI setI_bigcupr; apply: bigcupT_measurable => i. - apply: wlg. - - rewrite (le_lt_trans _ (mF i).2)//= le_measure// inE/=. - + by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1. - + by apply: sub_caratheodory; exact: (mF i).1. - - by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1. -move=> mEoo /= mE. -have inv0 n : (0 < n.+1%:R^-1 :> R)%R by rewrite invr_gt0. -set S := [set \sum_(0 <= k - exists2 A, @measurable_cover _ (ocitv_type R) E A & - \sum_(0 <= k s0; have : mu E \is a fin_num by rewrite ge0_fin_numE. - by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [A EA] <-] ?; exists A. -pose A n := projT1 (cid2 (coverE _ (inv0 n))). -have mA k : @measurable_cover _ (ocitv_type R) E (A k). - by rewrite /A; case: cid2. -have mA_E n : - \sum_(0 <= k /subset_trans; apply; apply: subset_bigcup => i _. -have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E. - apply: (le_lt_trans _ (mA_E m)). - apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (A m))). - apply: lee_nneseries => // n _. - by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m. -pose F := \bigcap_n (F_ n). -have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F. - apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. - by apply: sub_sigma_algebra; have [/(_ i)] := mA k. -have EF : E `<=` F by exact: sub_bigcap. -have muEF : completed_mu E = mu F. - apply/eqP; rewrite eq_le le_outer_measure//=. - apply/lee_addgt0Pr => /= _/posnumP[e]; near \oo => n. - apply: (@le_trans _ _ (mu (F_ n))). - by apply: le_outer_measure; exact: bigcap_inf. - rewrite (le_trans (ltW (mF_ n)))// leeD// lee_fin ltW//. - by near: n; apply: near_infty_natSinv_lt. -have coverEF s : (0 < s)%R -> - exists2 A, @measurable_cover _ (ocitv_type R) (F `\` E) A & - \sum_(0 <= k s0. - have : mu (F `\` E) \is a fin_num. - rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu F))//; last by rewrite -muEF. - by apply: le_outer_measure; exact: subDsetl. - by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [B FEB] <-] ?; exists B. -pose B n := projT1 (cid2 (coverEF _ (inv0 n))). -have mB k : @measurable_cover _ (ocitv_type R) (F `\` E) (B k). - by rewrite /B; case: cid2. -have mB_FE n : - \sum_(0 <= k /subset_trans; apply; apply: subset_bigcup => i _. -have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E. - apply: (le_lt_trans _ (mB_FE m)). - apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (B m))). - apply: lee_nneseries => // n _. - by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m. -pose G := \bigcap_n (G_ n). -have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G. - apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. - by apply: sub_sigma_algebra; have [/(_ i)] := mB k. -have FEG : F `\` E `<=` G by exact: sub_bigcap. -have muG : mu G = 0. - transitivity (completed_mu (F `\` E)). - apply/eqP; rewrite eq_le; apply/andP; split; last exact: le_outer_measure. - apply/lee_addgt0Pr => _/posnumP[e]. - near \oo => n. - apply: (@le_trans _ _ (mu (G_ n))). - by apply: le_outer_measure; exact: bigcap_inf. - rewrite (le_trans (ltW (mG_ n)))// leeD// lee_fin ltW//. - by near: n; apply: near_infty_natSinv_lt. - rewrite measureD//=. - + by rewrite setIidr// muEF subee// ge0_fin_numE//; move: mEoo; rewrite muEF. - + exact: sub_caratheodory. - + by move: mEoo; rewrite muEF. -apply: sub_sigma_algebra; exists (F `\` G); first exact: measurableD. -exists (E `&` G). - by apply: (@negligibleS _ _ _ mu G _ (@subIsetr _ E G)); exists G; split. -apply/seteqP; split=> [/= x [[Fx Gx]|[]//]|x Ex]. -- by rewrite -(notK (E x)) => Ex; apply: Gx; exact: FEG. -- have [|FGx] := pselect ((F `\` G) x); first by left. - right; split => //. - move/not_andP : FGx => [|]. - by have := EF _ Ex. - by rewrite notK. -Unshelve. all: by end_near. Qed. - -Lemma g_sigma_completed_algebra_genE : - (completed_algebra_gen mu).-sigma.-measurable = completed_algebra_gen mu. -Proof. -apply/seteqP; split; last first. - move=> _ [/= A /= mA [N neglN]] <-. - by apply: sub_sigma_algebra; exists A => //; exists N. -apply: smallest_sub => //=; split => /=. -- by exists set0 => //; exists set0; [exact: negligible_set0|rewrite setU0]. -- move=> G [/= A mA [N negN ANG]]; case: negN => /= F [mF F0 NF]. - have GANA : ~` G = ~` A `\` (N `&` ~` A). - by rewrite -ANG setCU setDE setCI setCK setIUr setICl setU0. - pose AA := ~` A `\` (F `&` ~` A). - pose NN := (F `&` ~` A) `\` (N `&` ~` A). - have GAANN : ~` G = AA `|` NN. - rewrite (_ : ~` G = ~` A `\` (N `&` ~` A))//. - by apply: setDU; [exact: setSI|exact: subIsetr]. - exists AA. - apply: measurableI => //=; first exact: measurableC. - by apply: measurableC; apply: measurableI => //; exact: measurableC. - by exists NN; [exists F; split => // x [] []|rewrite setDE setTI]. -- move=> F mF/=. - pose A n := projT1 (cid2 (mF n)). - pose N n := projT1 (cid2 (projT2 (cid2 (mF n))).2). - exists (\bigcup_k A k). - by apply: bigcupT_measurable => i; rewrite /A; case: cid2. - exists (\bigcup_k N k). - apply: negligible_bigcup => /= k. - by rewrite /N; case: (cid2 (mF k)) => //= *; case: cid2. - rewrite -bigcupU; apply: eq_bigcup => // i _. - by rewrite /A /N; case: (cid2 (mF i)) => //= *; case: cid2. -Qed. - -Lemma negligible_sub_caratheodory : - completed_mu.-negligible `<=` hlength^*%mu.-cara.-measurable. -Proof. -move=> N /= [/= A] [mA A0 NA]. -apply: le_caratheodory_measurable => /= X. -apply: (@le_trans _ _ (hlength^*%mu N + hlength^*%mu (X `&` ~` N))). - by rewrite leeD2r// le_outer_measure//; exact: subIsetr. -have -> : hlength^*%mu N = 0. - by apply/eqP; rewrite eq_le outer_measure_ge0//= andbT -A0 le_outer_measure. -by rewrite add0e// le_outer_measure//; exact: subIsetl. +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). -Let calgebra_sub_cara : (completed_algebra_gen mu).-sigma.-measurable `<=` - hlength^*%mu.-cara.-measurable. -Proof. -rewrite g_sigma_completed_algebra_genE => A -[/= X mX] [N negN] <-{A}. -apply: measurableU => //; first exact: sub_caratheodory. -apply: negligible_sub_caratheodory; case: negN => /= B [mB B0 NB]. -by exists B; split => //=; exact: sub_caratheodory. -Qed. +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 completed_caratheodory_measurable : - (completed_algebra_gen mu).-sigma.-measurable = - hlength^*%mu.-cara.-measurable. -Proof. -by apply/seteqP; split; [exact: calgebra_sub_cara | exact: cara_sub_calgebra]. -Qed. +Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]). +Proof. by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed. -End completed_algebra_caratheodory. +Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]). +Proof. by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed. -Section ps_infty. -Context {T : Type}. -Local Open Scope ereal_scope. +Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]). +Proof. by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed. -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 emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]). +Proof. by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed. -Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo]. +Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]). Proof. -split => [[]//|Aoo]. -by have [] := subset_set2 Aoo; move=> ->; constructor. +rewrite [X in measurable X](_ : _ = + \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))). + apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA. + by apply: measurableI; [exact: emeasurable_fun_c_infty| + exact: emeasurable_fun_infty_c]. +rewrite predeqE => t; split => [/= [Dt ft]|]. + have [ft0|ft0] := leP 0%R (fine (f t)). + exists `|ceil (fine (f t))|%N => //=; split => //; split. + by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. + rewrite natr_absz ger0_norm; last first. + by rewrite -ceil_ge0 (lt_le_trans _ ft0). + by rewrite -(fineK ft) lee_fin ceil_ge. + exists `|floor (fine (f t))|%N => //=; split => //; split. + rewrite natr_absz ltr0_norm -?floor_lt0// EFinN. + by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real. + by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). +move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. +by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. Qed. -Lemma setCU_Efin (A : set T) (B : set \bar T) : ps_infty B -> - ~` (EFin @` A) `&` ~` B = (EFin @` ~` A) `|` ([set -oo%E; +oo%E] `&` ~` B). +Lemma emeasurable_neq y : measurable (D `&` [set x | f x != y]). 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 => // -[]]. +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 ps_infty. +End measurable_fun_measurable. -Section salgebra_ereal. -Variables (R : realType) (G : set (set R)). -Let measurableR : set (set R) := G.-sigma.-measurable. +Module RGenOInfty. +Section rgenoinfty. +Variable R : realType. +Implicit Types x y z : R. -Definition emeasurable : set (set \bar R) := - [set EFin @` A `|` B | A in measurableR & B in ps_infty]. +Definition G := [set A | exists x, A = `]x, +oo[%classic]. -Lemma emeasurable0 : emeasurable set0. +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. Proof. -exists set0; first exact: measurable0. -by exists set0; rewrite ?setU0// ?image_set0//; constructor. +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 emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X). +Lemma measurable_itv_bounded a b x : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b 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. +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 bigcupT_emeasurable (F : (set \bar R)^nat) : - (forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)). +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. 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]. +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. -Definition ereal_isMeasurable : isMeasurable default_measure_display (\bar R) := - isMeasurable.Build _ _ - emeasurable0 emeasurableC bigcupT_emeasurable. - -End salgebra_ereal. +End rgenoinfty. +End RGenOInfty. -Section puncture_ereal_itv. -Variable R : realDomainType. -Implicit Types (y : R) (b : bool). -Local Open Scope ereal_scope. +Module RGenInftyO. +Section rgeninftyo. +Variable R : realType. +Implicit Types x y z : R. -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. +Definition G := [set A | exists x, A = `]-oo, x[%classic]. -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 measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. 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. +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 punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set~ -oo]. +Lemma measurable_itv_bounded a b x : a != -oo%O -> + G.-sigma.-measurable [set` Interval (BSide b x) a]. Proof. -rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. -by move=> [x| |] //= _; [left; exists x|right]. +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 punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo]. +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. Proof. -rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. -by move=> [x| |] //= _; [left; exists x|right]. +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 puncture_ereal_itv. +End rgeninftyo. +End RGenInftyO. -Section salgebra_R_ssets. +Module RGenCInfty. +Section rgencinfty. Variable R : realType. +Implicit Types x y z : R. -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 _ _). -(*HB.instance (Real.sort R) R_isMeasurable.*) +Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic]. -Lemma measurable_set1 (r : R) : measurable [set r]. +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. Proof. -rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. -by apply: sub_sigma_algebra; exact/is_ocitv. +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. -#[local] Hint Resolve measurable_set1 : core. -Lemma measurable_itv (i : interval R) : measurable [set` i]. +Lemma measurable_itv_bounded a b y : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b y)]. 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. +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. -HB.instance Definition _ := - (ereal_isMeasurable (R.-ocitv.-measurable)). -(* NB: Until we dropped support for Coq 8.12, we were using -HB.instance (\bar (Real.sort R)) - (ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))). -This was producing a warning but the alternative was failing with Coq 8.12 with - the following message (according to the CI): - # [redundant-canonical-projection,typechecker] - # forall (T : measurableType) (f : T -> R), measurable_fun setT f - # : Prop - # File "./theories/lebesgue_measure.v", line 4508, characters 0-88: - # Error: Anomaly "Uncaught exception Failure("sep_last")." - # Please report at http://coq.inria.fr/bugs/. -*) - -Lemma measurable_image_EFin (A : set R) : measurableR A -> measurable (EFin @` A). +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. Proof. -by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0]. +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. -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. +End rgencinfty. +End RGenCInfty. -Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R). -Proof. by rewrite itv_cyy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")] -Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty (only parsing). +Module RGenOpens. +Section rgenopens. +Variable R : realType. +Implicit Types x y z : R. -Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R). -Proof. by rewrite itv_oyy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")] -Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty (only parsing). +Definition G := [set A | exists x y, A = `]x, y[%classic]. -Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R). -Proof. by rewrite itv_cNyy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")] -Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty (only parsing). +Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic. +Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. -Lemma __deprecated__itv_oninfty_pinfty : - `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R). -Proof. by rewrite itv_oNyy. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")] -Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty (only parsing). +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. -Let emeasurable_itv_bndy b (y : \bar R) : - measurable [set` Interval (BSide b y) +oo%O]. +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +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. +case: b; last exact: measurable_itv_o_infty. +rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k. +exact: measurable_itv_o_infty. 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 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 emeasurable_itv (i : interval (\bar R)) : - measurable ([set` i]%classic : set \bar R). +Lemma measurable_itv_bounded a x b y : + G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)]. 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. +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. -Definition elebesgue_measure : set \bar R -> \bar R := - fun S => lebesgue_measure (fine @` (S `\` [set -oo; +oo]%E)). +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. -Lemma elebesgue_measure0 : elebesgue_measure set0 = 0%E. -Proof. by rewrite /elebesgue_measure set0D image_set0 measure0. Qed. +End rgenopens. +End RGenOpens. -Lemma measurable_image_fine (X : set \bar R) : measurable X -> - measurable [set fine x | x in X `\` [set -oo; +oo]%E]. -Proof. -case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. -- rewrite setU0 => <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. - by move=> Yr; exists r%:E; split => [|[]//]; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <- _ <-//]|]]]. - by move=> <-; rewrite not_orP => -[]/(_ erefl). - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. - by move=> ->; rewrite not_orP => -[_]/(_ erefl). - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -Qed. - -Lemma elebesgue_measure_ge0 X : (0 <= elebesgue_measure X)%E. -Proof. exact/measure_ge0. Qed. - -Lemma semi_sigma_additive_elebesgue_measure : - semi_sigma_additive elebesgue_measure. -Proof. -move=> /= F mF tF mUF; rewrite /elebesgue_measure. -rewrite [X in lebesgue_measure X](_ : _ = - \bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first. - rewrite predeqE => r; split. - by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x. - by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n. -apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) - (fun n => fine @` (F n `\` [set -oo; +oo]%E))). -- move=> n; have := mF n. - move=> [X mX [X' mX']] XX'Fn. - apply: measurable_image_fine. - rewrite -XX'Fn. - apply: measurableU; first exact: measurable_image_EFin. - by case: mX' => //; exact: measurableU. -- move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. - move: tF => /(_ i j Logic.I Logic.I); apply. - suff ab : a = b by exists a; split => //; rewrite ab. - move: a b {Fia Fjb} aoo boo ax bx. - move=> [a| |] [b| |] /=. - + by move=> _ _ -> ->. - + by move=> _; rewrite not_orP => -[_]/(_ erefl). - + by move=> _; rewrite not_orP => -[]/(_ erefl). - + by rewrite not_orP => -[_]/(_ erefl). - + by rewrite not_orP => -[_]/(_ erefl). - + by rewrite not_orP => -[_]/(_ erefl). - + by rewrite not_orP => -[]/(_ erefl). - + by rewrite not_orP => -[]/(_ erefl). - + by rewrite not_orP => -[]/(_ erefl). -- move: mUF. - rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. - - rewrite setU0 => h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-{r}]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[x' Xx' <-]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r. - by exists n => //; exists r%:E => //; split => //; case. - - move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. - by exists n => //; exists r%:E => //; split => //; case. - - (* NB: almost the same as the previous one, factorize?*) - move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. - by exists n => //; exists r%:E => //; split => //; case. - - move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[[x' Xx' <-//]|]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. - by exists n => //; exists r%:E => //; split => //; case. -Qed. - -HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure - elebesgue_measure0 elebesgue_measure_ge0 - semi_sigma_additive_elebesgue_measure. - -End salgebra_R_ssets. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| - apply: emeasurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. -#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_bnd_pinfty := emeasurable_itv (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing). - -Lemma 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 lebesgue_measure_itv. +Section erealwithrays. Variable R : realType. +Implicit Types (x y z : \bar R) (r s : R). +Local Open Scope ereal_scope. -Let lebesgue_measure_itvoc (a b : R) : - (lebesgue_measure (`]a, b] : set R) = - wlength [the cumulative _ of idfun] `]a, b])%classic. +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 /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=. -by rewrite measurable_mu_extE//; exact: is_ocitv. +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. -Let lebesgue_measure_itvoo_subr1 (a : R) : - lebesgue_measure (`]a - 1, a[%classic : set R) = 1%E. +Lemma EFin_itv r : [set s | r%:E < s%:E] = `]r, +oo[%classic. Proof. -rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o - (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. - - by move=> ?; exact: measurable_itv. - - by apply: bigcup_measurable => k _; exact: measurable_itv. - - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. - by move/le_trans; apply; rewrite lerB// ler_pV2 ?ler_nat//; - rewrite inE ltr0n andbT unitfE. -rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first. - apply/funext => n /=; rewrite lebesgue_measure_itvoc. - have [->|n0] := eqVneq n 0%N. - by rewrite invr1 subrr set_itvoc0 wlength0. - rewrite wlength_itv/= lte_fin ifT; last first. - by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n. - by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e. -apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW. -apply/(@cvgrPdist_lt _ [the pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e]. -near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//. -by near: n; exact: near_infty_natSinv_lt. -Unshelve. all: by end_near. Qed. +by rewrite predeqE => s; split => [|]; rewrite /= lte_fin in_itv/= andbT. +Qed. -Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0%E. +Lemma preimage_EFin_setT : @EFin R @^-1` [set x | x \in `]-oo%E, +oo[] = setT. Proof. -suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) = - lebesgue_measure (`]a - 1, a[%classic%R : set R) + - lebesgue_measure [set a])%E. - rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP. - rewrite wlength_itv lte_fin ltrBlDr ltrDl ltr01. - rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e. - by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP. -rewrite -setUitv1// ?bnd_simp; last by rewrite ltrBlDr ltrDl. -rewrite measureU //; apply/seteqP; split => // x []/=. -by rewrite in_itv/= => + xa; rewrite xa ltxx andbF. +by rewrite set_itvE predeqE => r; split=> // _; rewrite /preimage /= ltNyr. Qed. -Let lebesgue_measure_itvoo (a b : R) : - (lebesgue_measure (`]a, b[ : set R) = - wlength [the cumulative _ of idfun] `]a, b[)%classic. +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. -have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. -have := lebesgue_measure_itvoc a b. -rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//. -- by have /= -> := lebesgue_measure_set1 b; rewrite adde0. -- by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF. +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. -Let lebesgue_measure_itvcc (a b : R) : - (lebesgue_measure (`[a, b] : set R) = - wlength [the cumulative _ of idfun] `[a, b])%classic. +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. -have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt. -have := lebesgue_measure_itvoc a b. -rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//. -- by have /= -> := lebesgue_measure_set1 a; rewrite add0e. -- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. +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. -Let lebesgue_measure_itvco (a b : R) : - (lebesgue_measure (`[a, b[ : set R) = - wlength [the cumulative _ of idfun] `[a, b[)%classic. +Lemma eset1Ny : + [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R). Proof. -have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. -have := lebesgue_measure_itvoo a b. -rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//. -- by have /= -> := lebesgue_measure_set1 a; rewrite add0e. -- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. +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. -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)]. +Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). Proof. -by move: x y => [|] [|]; [exact: lebesgue_measure_itvco | - exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo | - exact: lebesgue_measure_itvoc]. +rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. +move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. +rewrite andbT lte_fin ltNge. +have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). +by rewrite natr_absz gtr0_norm// ?ceil_ge// -ceil_gt0. Qed. -Let limnatR : lim (((k%:R)%:E : \bar R) @[k --> \oo]) = +oo%E. -Proof. by apply/cvg_lim => //; apply/cvgenyP. Qed. +End erealwithrays. -Let lebesgue_measure_itv_bnd_infty x (a : R) : - lebesgue_measure ([set` Interval (BSide x a) +oo%O] : set R) = +oo%E. -Proof. -rewrite itv_bnd_infty_bigcup; transitivity (limn (lebesgue_measure \o - (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. - + by move=> k; exact: measurable_itv. - + by apply: bigcup_measurable => k _; exact: measurable_itv. - + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=]. - by move=> /le_trans; apply; rewrite lerD// ler_nat. -rewrite (_ : _ \o _ = (fun k => k%:R%:E))//. -apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/=. -rewrite lte_fin; have [->|n0] := eqVneq n 0%N; first by rewrite addr0 ltxx. -by rewrite ltrDl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e. -Qed. +Module ErealGenOInfty. +Section erealgenoinfty. +Variable R : realType. +Implicit Types (x y z : \bar R) (r s : R). -Let lebesgue_measure_itv_infty_bnd y (b : R) : - lebesgue_measure ([set` Interval -oo%O (BSide y b)] : set R) = +oo%E. +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 itv_infty_bnd_bigcup; transitivity (limn (lebesgue_measure \o - (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))). - apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. - + by move=> k; exact: measurable_itv. - + by apply: bigcup_measurable => k _; exact: measurable_itv. - + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->]. - by rewrite andbT; apply: le_trans; rewrite lerB// ler_nat. -rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//. -apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/= lte_fin. -have [->|n0] := eqVneq n 0%N; first by rewrite subr0 ltxx. -rewrite ltrBlDr ltrDl ltr0n lt0n n0 EFinN EFinB fin_num_oppeB// addeA. -by rewrite subee// add0e. +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. -Let lebesgue_measure_itv_infty_infty : - lebesgue_measure ([set` Interval -oo%O +oo%O] : set R) = +oo%E. +Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. Proof. -rewrite set_itv_infty_infty -(setUv (`]-oo, 0[)) setCitv. -rewrite [X in _ `|` (X `|` _) ]set_itvE set0U measureU//; last first. - apply/seteqP; split => //= x [] /= /[swap]. - by rewrite !in_itv/= andbT ltNge => ->//. -rewrite [X in (X + _)%E]lebesgue_measure_itv_infty_bnd. -by rewrite [X in (_ + X)%E]lebesgue_measure_itv_bnd_infty. +rewrite eset1y; apply: bigcapT_measurable => i. +by apply: sub_sigma_algebra; exists i%:R. Qed. -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. +Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. Proof. -move: i => [[x a|[|]]] [y b|[|]]. - by rewrite lebesgue_measure_itv_bnd wlength_itv. -- by rewrite set_itvE ?measure0. -- by rewrite lebesgue_measure_itv_bnd_infty/= ltry. -- by rewrite lebesgue_measure_itv_infty_bnd/= ltNyr. -- by rewrite set_itvE ?measure0. -- by rewrite lebesgue_measure_itv_infty_infty. -- by rewrite set_itvE ?measure0. -- by rewrite set_itvE ?measure0. -- by rewrite set_itvE ?measure0. +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 lebesgue_measure_itv. +End erealgenoinfty. +End ErealGenOInfty. -Section measurable_ball. +Module ErealGenCInfty. +Section erealgencinfty. Variable R : realType. +Implicit Types (x y z : \bar R) (r s : R). +Local Open Scope ereal_scope. -Lemma measurable_ball (x : R) e : measurable (ball x e). -Proof. by rewrite ball_itv; exact: measurable_itv. Qed. +Definition G := [set A : set \bar R | exists r, A = `[r%:E, +oo[%classic]. -Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R -> - lebesgue_measure (ball x r) = (r *+ 2)%:E. +Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. Proof. -rewrite le_eqVlt => /predU1P[ <-|r0]. - by rewrite (ball0 _ _).2// measure0 mul0rn. -rewrite ball_itv lebesgue_measure_itv/= lte_fin ltrBlDr -addrA ltrDl. -by rewrite addr_gt0 // -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n. +rewrite eset1Ny; apply: bigcapT_measurable=> i; rewrite -setCitvr. +by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%R. Qed. -Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). +Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. Proof. -have [r0|r0] := leP r 0; first by rewrite closed_ball0. -by rewrite closed_ball_itv. +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 lebesgue_measure_closed_ball (x r : R) : 0 <= r -> - lebesgue_measure (closed_ball x r) = (r *+ 2)%:E. +Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. Proof. -rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0// measure0. -rewrite closed_ball_itv// lebesgue_measure_itv/= lte_fin -ltrBlDl addrAC. -rewrite subrr add0r gtrN// ?mulr_gt0// -EFinD; congr (_%:E). -by rewrite opprB addrAC addrCA subrr addr0 -mulr2n. +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 measurable_ball. +End erealgencinfty. +End ErealGenCInfty. -Lemma lebesgue_measure_rat (R : realType) : - lebesgue_measure (range ratr : set R) = 0%E. +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. -have /pcard_eqP/bijPex[f bijf] := card_rat; set f1 := 'pinv_(fun=> 0) setT f. -rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first. - apply/seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n). - exists (f q) => //=; rewrite /f1 pinvKV// ?in_setE// => x y _ _. - by apply: bij_inj; rewrite -setTT_bijective. -rewrite measure_bigcup//; last first. - apply/trivIsetP => i j _ _ ij; apply/seteqP; split => //= _ [/= ->]. - move=> /fmorph_inj. - have /set_bij_inj /[apply] := bijpinv_bij (fun=> 0) bijf. - by rewrite in_setE => /(_ Logic.I Logic.I); exact/eqP. -by rewrite eseries0// => n _ _; exact: lebesgue_measure_set1. +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. -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_itv_c_infty; exact/mf/emeasurable_itv. Qed. +End erealgeninftyo. +End ErealGenInftyO. -Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]). -Proof. by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed. +(* more properties of measurable functions *) -Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]). -Proof. by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed. +Lemma is_interval_measurable (R : realType) (I : set R) : + is_interval I -> measurable I. +Proof. by move/is_intervalP => ->; exact: measurable_itv. Qed. -Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]). -Proof. by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed. +Section coutinuous_measurable. +Variable R : realType. -Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]). +Lemma open_measurable (A : set R) : open A -> measurable A. Proof. -rewrite [X in measurable X](_ : _ = - \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))). - apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA. - by apply: measurableI; [exact: emeasurable_fun_c_infty| - exact: emeasurable_fun_infty_c]. -rewrite predeqE => t; split => [/= [Dt ft]|]. - have [ft0|ft0] := leP 0%R (fine (f t)). - exists `|ceil (fine (f t))|%N => //=; split => //; split. - by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. - rewrite natr_absz ger0_norm; last first. - by rewrite -ceil_ge0 (lt_le_trans _ ft0). - by rewrite -(fineK ft) lee_fin ceil_ge. - exists `|floor (fine (f t))|%N => //=; split => //; split. - rewrite natr_absz ltr0_norm -?floor_lt0// EFinN. - by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real. - by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). -move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. -by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. +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 emeasurable_neq y : measurable (D `&` [set x | f x != y]). +Lemma open_measurable_subspace (D : set R) (U : set (subspace D)) : + measurable D -> open U -> measurable (D `&` U). 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. +move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. +by apply: measurableI => //; exact: open_measurable. 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 closed_measurable (A : set R) : closed A -> measurable A. +Proof. by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed. -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Lemma compact_measurable (A : set R) : compact A -> measurable A. 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. +by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable. Qed. -Lemma measurable_itv_bounded a b x : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b x)]. +Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : + measurable D -> continuous f -> measurable_fun D f. 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. +move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)). +move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //. +exact/cf/interval_open. 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)]. +Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) : + open D -> {in D, continuous f} -> measurable_fun D f. 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. +move=> oD; rewrite -(continuous_open_subspace f oD). +by apply: subspace_continuous_measurable_fun; exact: open_measurable. Qed. -Lemma measurable_itv_bounded a b x : a != -oo%O -> - G.-sigma.-measurable [set` Interval (BSide b x) a]. +Lemma continuous_measurable_fun (f : R -> R) : + continuous f -> measurable_fun setT f. 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. +by move=> cf; apply: open_continuous_measurable_fun => //; exact: openT. Qed. -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +End coutinuous_measurable. + +Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : + lower_semicontinuous f -> measurable_fun setT f. 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. +move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)). +move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. +by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact. Qed. -End rgeninftyo. -End RGenInftyO. - -Module RGenCInfty. -Section rgencinfty. +Section standard_measurable_fun. Variable R : realType. -Implicit Types x y z : R. - -Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic]. +Implicit Types D : set R. -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Lemma oppr_measurable D : measurable_fun D -%R. 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. +apply: measurable_funTS => /=; apply: continuous_measurable_fun. +exact: opp_continuous. Qed. -Lemma measurable_itv_bounded a b y : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b y)]. +Lemma normr_measurable D : measurable_fun D (@normr _ R). 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. +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 measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Lemma mulrl_measurable D (k : R) : measurable_fun D ( *%R k). 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. +apply: measurable_funTS => /=. +by apply: continuous_measurable_fun; exact: mulrl_continuous. Qed. -End rgencinfty. -End RGenCInfty. +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. -Module RGenOpens. -Section rgenopens. -Variable R : realType. -Implicit Types x y z : R. +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. -Definition G := [set A | exists x y, A = `]x, y[%classic]. +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). -Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic. -Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. +Section measurable_fun_realType. +Context d (T : measurableType d) (R : realType). +Implicit Types (D : set T) (f g : T -> R). -Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic. +Lemma measurable_funD D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). Proof. -rewrite itv_bnd_inftyEbigcup; apply: bigcupT_measurable => i. -exact: measurable_itvoo. +move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //. +move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty. +rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) + ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))). + apply: bigcupT_measurable_rat => q; apply: measurableI. + - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv. + - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv. +rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. + rewrite -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_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +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. -case: b; last exact: measurable_itv_o_infty. -rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k. -exact: measurable_itv_o_infty. +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_itv_infty_bnd b x : - G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. +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. -by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_gt0. +by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB. Qed. -Lemma measurable_itv_bounded a x b y : - G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)]. +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: 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]. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_ge0. +by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB. Qed. -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Lemma measurable_maxr D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g). 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. +by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; + [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. 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. +Lemma measurable_minr D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). 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. +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 EFin_itv r : [set s | r%:E < s%:E] = `]r, +oo[%classic. +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. -by rewrite predeqE => s; split => [|]; rewrite /= lte_fin in_itv/= andbT. +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 preimage_EFin_setT : @EFin R @^-1` [set x | x \in `]-oo%E, +oo[] = setT. +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. -by rewrite set_itvE predeqE => r; split=> // _; rewrite /preimage /= ltNyr. +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 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 _. +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. -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. +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 eset1Ny : - [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R). +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. -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. +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 eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). +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 eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. -move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. -rewrite andbT lte_fin ltNge. -have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). -by rewrite natr_absz gtr0_norm// ?ceil_ge// -ceil_gt0. +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). -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_expR (R : realType) : measurable_fun [set: R] expR. +Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. +#[global] Hint Extern 0 (measurable_fun _ expR) => + solve [apply: measurable_expR] : core. -Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. +Lemma natmul_measurable {R : realType} D n : + measurable_fun D (fun x : R => x *+ n). 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. +under eq_fun do rewrite -mulr_natr. +by do 2 apply: measurable_funM => //. Qed. -Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. +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. -rewrite eset1y; apply: bigcapT_measurable => i. -by apply: sub_sigma_algebra; exists i%:R. +move=> mf. +exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). Qed. -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma measurable_powR (R : realType) p : + measurable_fun [set: R] (@powR R ^~ p). 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. +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. +#[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). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] +Notation measurable_fun_pow := measurable_funX (only parsing). -End erealgenoinfty. -End ErealGenOInfty. - -Module ErealGenCInfty. -Section erealgencinfty. +Section standard_emeasurable_fun. 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 EFin_measurable (D : set R) : measurable_fun D EFin. Proof. -rewrite eset1Ny; apply: bigcapT_measurable=> i; rewrite -setCitvr. -by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%R. +move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. +move=> /= _ [_ [x ->]] <-; apply: measurableI => //. +by rewrite preimage_itv_o_infty EFin_itv; exact: measurable_itv. Qed. -Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. +Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. 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. +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 measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Lemma oppe_measurable (D : set (\bar R)) : + measurable_fun D (-%E : \bar R -> \bar R). 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. +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 erealgencinfty. -End ErealGenCInfty. - -Module ErealGenInftyO. -Section erealgeninftyo. -Variable R : realType. - -Definition G := [set A : set \bar R | exists r, A = `]-oo, r%:E[%classic]. +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 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. - -(* more properties of measurable functions *) - -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). +(* NB: real-valued function *) +(* TODO: rename to measurable_EFin after notation measurable_EFin is removed? *) +Lemma EFin_measurable_fun d (T : measurableType d) (R : realType) (D : set T) + (g : T -> R) : + measurable_fun D (EFin \o g) <-> measurable_fun D g. Proof. -move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. -by apply: measurableI => //; exact: open_measurable. +split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp. +rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)). + by apply: mf => //; exists A => //; exists set0; [constructor|rewrite setU0]. +congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. +by move=> ? ?; exact: preimage_image. Qed. -Lemma 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. +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. -by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable. +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/EFin_measurable_fun/measurableT_comp. Qed. +#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] +Notation measurable_fun_er_map := measurable_er_map (only parsing). -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. +Section emeasurable_fun. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). +Implicit Types (D : set T). -Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) : - open D -> {in D, continuous f} -> measurable_fun D f. +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=> oD; rewrite -(continuous_open_subspace f oD). -by apply: subspace_continuous_measurable_fun; exact: open_measurable. +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 continuous_measurable_fun (f : R -> R) : - continuous f -> measurable_fun setT f. +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. -by move=> cf; apply: open_continuous_measurable_fun => //; exact: openT. +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. -End coutinuous_measurable. - -Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : - lower_semicontinuous f -> measurable_fun setT f. +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=> scif; apply: (measurability (ErealGenOInfty.measurableE R)). -move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. -by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact. +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. -Section standard_measurable_fun. -Variable R : realType. -Implicit Types D : set R. +Lemma measurable_funepos D (f : T -> \bar R) : + measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; exact: measurable_maxe. Qed. -Lemma oppr_measurable D : measurable_fun D -%R. -Proof. -apply: measurable_funTS => /=; apply: continuous_measurable_fun. -exact: opp_continuous. -Qed. +Lemma measurable_funeneg D (f : T -> \bar R) : + measurable_fun D f -> measurable_fun D f^\-. +Proof. by move=> mf; apply: measurable_maxe => //; exact: measurableT_comp. Qed. -Lemma normr_measurable D : measurable_fun D (@normr _ R). +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=> 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). +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 mulrl_measurable D (k : R) : measurable_fun D ( *%R k). +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. -apply: measurable_funTS => /=. -by apply: continuous_measurable_fun; exact: mulrl_continuous. +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 mulrr_measurable D (k : R) : measurable_fun D (fun x => x * k). +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. -apply: measurable_funTS => /=. -by apply: continuous_measurable_fun; exact: mulrr_continuous. +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_. -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. +#[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). -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 open_itv_cover. +Context {R : realType}. +Implicit Types (A : set R). +Local Open Scope ereal_scope. -Section measurable_fun_realType. -Context d (T : measurableType d) (R : realType). -Implicit Types (D : set T) (f g : T -> R). +Definition is_open_itv A := exists ab, A = `]ab.1, ab.2[%classic. -Lemma measurable_funD D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). -Proof. -move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //. -move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty. -rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) - ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))). - apply: bigcupT_measurable_rat => q; apply: measurableI. - - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv. - - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv. -rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. - rewrite -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. +Definition open_itv_cover A := [set F : (set R)^nat | + (forall i, is_open_itv (F i)) /\ A `<=` \bigcup_k (F k)]. -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. +Let l := (@wlength R idfun). -Lemma measurable_funM D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g). +Lemma outer_measure_open_itv_cover A : (l^* A)%mu = + ereal_inf [set \sum_(k 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_itv_o_infty; exact: measurable_funB. +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 /=; 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. -Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x <= g x). +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. + +(*TODO : this generalizes to any metric space with a borel measure*) +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 mg mD; apply: (measurable_fun_bool true) => //. -under eq_fun do rewrite -subr_ge0. -by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB. +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 measurable_maxr D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max 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}]. Proof. -by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; - [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. +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. -Lemma measurable_minr D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). +End egorov. + +(* This module contains a direct construction of the Lebesgue measure that is + kept here for archival purpose. The Lebesgue measure is actually defined as + an instance of the Lebesgue-Stieltjes measure. *) +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. +Proof. by rewrite /hlength Rhull0 /= subee. Qed. + +Lemma hlength_singleton (r : R) : hlength `[r, r] = 0. Proof. -by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; - [exact: measurable_fun_ltr|exact: measurable_funS mf|exact: measurable_funS mg]. +rewrite /hlength /= asboolT// sup_itvcc//= asboolT//. +by rewrite asboolT inf_itvcc//= ?subee// inE. 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). +Lemma hlength_setT : hlength setT = +oo%E :> \bar R. +Proof. by rewrite /hlength RhullT. Qed. + +Lemma hlength_itv i : + hlength [set` i] = if i.2 > i.1 then (i.2 : \bar R) - i.1 else 0. 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. +case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK. +rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first. + rewrite (_ : [set` i] = set0) ?hlength0//. + by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12). +case: i => -[ba a|[|]] [bb b|[|]] //=. +- rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try + by rewrite set_itvE hlength0. + by rewrite hlength_singleton. +- by move=> _; rewrite set_itvE hlength0. +- by move=> _; rewrite set_itvE hlength0. Qed. -Lemma 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 hlength_finite_fin_num i : neitv i -> hlength [set` i] < +oo -> + ((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num). Proof. -move=> 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. +move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx. +by move=> _; rewrite hlength_itv /= ltry. +by move=> _; rewrite hlength_itv /= ltNyr. +by move=> _; rewrite hlength_itv. Qed. -Lemma 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 finite_hlength_itv i : neitv i -> hlength [set` i] < +oo -> + hlength [set` i] = (fine i.2)%:E - (fine i.1)%:E. 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. +move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo. +rewrite !fineK// hlength_itv; case: ifPn => //. +rewrite -leNgt le_eqVlt => /predU1P[->|]; first by rewrite subee. +by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->. Qed. -Lemma 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. +Lemma hlength_infty_bnd b r : + hlength [set` Interval -oo%O (BSide b r)] = +oo :> \bar R. +Proof. by rewrite hlength_itv /= ltNyr. Qed. + +Lemma hlength_bnd_infty b r : + hlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R. +Proof. by rewrite hlength_itv /= ltry. Qed. + +Lemma infinite_hlength_itv i : hlength [set` i] = +oo -> + (exists s r, i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O) + \/ i = `]-oo, +oo[. Proof. -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. +rewrite hlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|]. +- by case: ifPn. +- by left; exists ba, a; right. +- by left; exists bb, b; left. +- by right. +Qed. + +Lemma hlength_itv_ge0 i : 0 <= hlength [set` i]. +Proof. +rewrite hlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |]. +- by rewrite suber_ge0//; exact: ltW. +- by rewrite ltNge leey. +- by move=> i2gtNy; rewrite addey//; case: (i.2 : \bar R) i2gtNy. +Qed. + +Lemma hlength_Rhull (A : set R) : hlength [set` Rhull A] = hlength A. +Proof. by rewrite /hlength Rhull_involutive. Qed. + +Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j]. +Proof. +set I := [set` i]; set J := [set` j]. +have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_itv_ge0. +have [J0|/set0P J0] := eqVneq J set0. + by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->. +move=> /subset_itvP ij; apply: leeB => /=. + have [ui|ui] := asboolP (has_ubound I). + have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey. + by rewrite lee_fin le_sup // => r Ir; exists r; split => //; apply: ij. + have [uj /=|//] := asboolP (has_ubound J). + by move: ui; have := subset_has_ubound ij uj. +have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye. +have [li /=|li] := asboolP (has_lbound I); last first. + by move: li; have := subset_has_lbound ij lj. +rewrite lee_fin lerNl opprK le_sup// ?has_inf_supN//; last exact/nonemptyN. +move=> r [r' Ir' <-{r}]; exists (- r')%R. +by split => //; exists r' => //; apply: ij. +Qed. + +Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}. +Proof. +move=> a b /le_Rhull /le_hlength_itv. +by rewrite (hlength_Rhull a) (hlength_Rhull b). +Qed. + +Lemma hlength_ge0 I : (0 <= hlength I)%E. +Proof. by rewrite -hlength0 le_hlength. Qed. + +End hlength. +#[local] Hint Extern 0 (is_true (0%R <= hlength _)) => + solve[apply: hlength_ge0] : core. + +(* Unused *) +(* Lemma hlength_semi_additive2 : semi_additive2 hlength. *) +(* Proof. *) +(* move=> I J /ocitvP[|[a a12]] ->; first by rewrite set0U hlength0 add0e. *) +(* move=> /ocitvP[|[b b12]] ->; first by rewrite setU0 hlength0 adde0. *) +(* rewrite -subset0 => + ab0 => /ocitvP[|[x x12] abx]. *) +(* by rewrite setU_eq0 => -[-> ->]; rewrite setU0 hlength0 adde0. *) +(* rewrite abx !hlength_itv//= ?lte_fin a12 b12 x12/= -!EFinB -EFinD. *) +(* wlog ab1 : a a12 b b12 ab0 abx / a.1 <= b.1 => [hwlog|]. *) +(* have /orP[ab1|ba1] := le_total a.1 b.1; first by apply: hwlog. *) +(* by rewrite [in RHS]addrC; apply: hwlog => //; rewrite (setIC, setUC). *) +(* have := ab0; rewrite subset0 -set_itv_meet/=. *) +(* rewrite /Order.join /Order.meet/= ?(andbF, orbF)/= ?(meetEtotal, joinEtotal). *) +(* rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _. *) +(* move=> /eqP/neitvP/=; rewrite bnd_simp/= /d/c (max_idPr _)// => /negP. *) +(* rewrite -leNgt le_minl orbC lt_geF//= => {c} {d} a2b1. *) +(* have ab i j : i \in `]a.1, a.2] -> j \in `]b.1, b.2] -> i <= j. *) +(* by move=> ia jb; rewrite (le_le_trans _ _ a2b1) ?(itvP ia) ?(itvP jb). *) +(* have /(congr1 sup) := abx; rewrite sup_setU// ?sup_itv_bounded// => bx. *) +(* have /(congr1 inf) := abx; rewrite inf_setU// ?inf_itv_bounded// => ax. *) +(* rewrite -{}ax -{x}bx in abx x12 *. *) +(* case: ltgtP a2b1 => // a2b1 _; last first. *) +(* by rewrite a2b1 [in RHS]addrC subrKA. *) +(* exfalso; pose c := (a.2 + b.1) / 2%:R. *) +(* have /predeqP/(_ c)[_ /(_ _)/Box[]] := abx. *) +(* apply: subset_itv_oo_oc; have := mid_in_itvoo a2b1. *) +(* by apply/subitvP; rewrite subitvE ?bnd_simp/= ?ltW. *) +(* apply/not_orP; rewrite /= !in_itv/=. *) +(* by rewrite lt_geF ?midf_lt//= andbF le_gtF ?midf_le//= ltW. *) +(* Qed. *) + +Section hlength_extension. +Context {R : realType}. + +Notation hlength := (@hlength R). + +Lemma hlength_semi_additive : measure.semi_additive hlength. +Proof. +move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->. +move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->. +rewrite hlength_itv ?lte_fin/= -EFinB. +case: ifPn => a12; last first. + pose I i := `](b i).1, (b i).2]%classic. + rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0. + by under eq_bigr => i _ do rewrite I0//= hlength0; rewrite big1. +set A := `]a1, a2]%classic. +rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//. +move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *. +rewrite ltnS => cP /esym AE. +have : A a2 by rewrite /A /= in_itv/= lexx andbT. +rewrite AE/= => -[i /= Pi] a2bi. +case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi. +have {}a2bi : a2 = (b i).2. + apply/eqP; rewrite eq_le (itvP a2bi)/=. + suff: A (b i).2 by move=> /itvP->. + by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT. +rewrite {a2}a2bi in a12 A AE *. +rewrite (bigD1 i)//= hlength_itv ?lte_fin/= bi !EFinD -addeA. +congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//. +rewrite ?EFinN oppeK addeC; apply/eqP. +case: (eqVneq a1 (b i).1) => a1bi. + rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j. + move=> /andP[Pj Nji]; rewrite hlength_itv ?lte_fin/=; case: ifPn => bj//. + exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv. + pose m := ((b j).1 + (b j).2) / 2%:R. + have mbj : `](b j).1, (b j).2]%classic m. + by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW. + rewrite -subset0 => /(_ m); apply; split=> //. + by suff: A m by []; rewrite AE; exists j => //. +have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2. + move=> Pj bj; suff /itvP-> : A (b j).2 by []. + by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=. +have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1. + move=> Pj bj; case: ltP=> // bj1a. + suff : A a1 by rewrite /A/= in_itv/= ltxx. + by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2. +have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2. + move=> Pj bj; suff /itvP-> : A (b j).2 by []. + by rewrite AE; exists j => //=; rewrite ?in_itv/= bj//=. +apply/IHp. +- by rewrite lt_neqAle a1bi/= a1b. +- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P). + rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first. + by move=> j; rewrite !inE andbC; case: eqVneq => // ->. + rewrite ?card1 ?ltnS// subset_leq_card//. + by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC. +apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi]. + case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge. + apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt. + have /trivIsetP/(_ j i I I Nji) := Itriv. + rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2. + by rewrite !in_itv/= bj !lexx bi1j2 bbi2. +have: A x. + rewrite /A/= in_itv/= (itvP xabi)/= ltW//. + by rewrite (le_lt_trans _ bi) ?(itvP xabi). +rewrite AE => -[j /= Pj xbj]. +exists j => //=. +apply/andP; split=> //; apply: contraTneq xbj => ->. +by rewrite in_itv/= le_gtF// (itvP xabi). +Qed. + +HB.instance Definition _ := isContent.Build _ _ R + hlength hlength_ge0 hlength_semi_additive. + +Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core. + +Lemma hlength_sigma_subadditive : + measurable_subset_sigma_subadditive (hlength : set (ocitv_type R) -> _). +Proof. +move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-]. +rewrite /subset_sigma_subadditive hlength_itv ?lte_fin/= -EFinB => lebig. +case: ifPn => a12; last by rewrite nneseries_esum// esum_ge0. +apply/lee_addgt0Pr => _ /posnumP[e]. +rewrite [e%:num]splitr [in leRHS]EFinD addeA -leeBlDr//. +apply: le_trans (epsilon_trick _ _ _) => //=. +have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R. + by rewrite divr_gt0// ltr0n// expn_gt0. +have eVn_ge0 n := ltW (eVn_gt0 n). +pose Aoo i : set (ocitv_type R) := + `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic. +pose Aoc i : set (ocitv_type R) := + `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R]%classic. +have: `[a.1 + e%:num / 2, a.2] `<=` \bigcup_i Aoo i. + apply: (@subset_trans _ `]a.1, a.2]). + move=> x; rewrite /= !in_itv /= => /andP[+ -> //]. + by move=> /lt_le_trans-> //; rewrite ltrDl. + apply: (subset_trans lebig); apply: subset_bigcup => i _; rewrite AE /Aoo/=. + move=> x /=; rewrite !in_itv /= => /andP[-> /le_lt_trans->]//=. + by rewrite ltrDl. +have := @segment_compact _ (a.1 + e%:num / 2) a.2; rewrite compact_cover. +move=> /[apply]-[i _|X _ Xc]; first exact: interval_open. +have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i. + move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix. + by exists i => //; apply: subset_itv_oo_oc Aooix. +have /[apply] := @content_sub_fsum _ _ _ + [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X]. +move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans. + rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD. + by case: ltP => //; rewrite lee_fin subr_le0. +rewrite nneseries_esum//; last by move=> *; rewrite adde_ge0//= ?lee_fin. +rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite// ?set_fsetK//=. +rewrite fsbig_finite//= set_fsetK//. +rewrite lee_sum // => i _; rewrite ?AE// !hlength_itv/= ?lte_fin -?EFinD/=. +do !case: ifPn => //= ?; do ?by rewrite ?adde_ge0 ?lee_fin// ?subr_ge0// ?ltW. + by rewrite addrAC. +by rewrite addrAC lee_fin lerD// subr_le0 leNgt. +Qed. + +HB.instance Definition _ := Content_SigmaSubAdditive_isMeasure.Build _ _ _ + hlength hlength_sigma_subadditive. + +Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _). +Proof. +exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT. +by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry. +Qed. + +Definition lebesgue_measure := measure_extension hlength. +HB.instance Definition _ := Measure.on lebesgue_measure. + +Let sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure. +Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed. + +HB.instance Definition _ := @isSigmaFinite.Build _ _ _ + lebesgue_measure sigmaT_finite_lebesgue_measure. + +End hlength_extension. + +End LebesgueMeasure. + +Definition lebesgue_measure {R : realType} : + set [the measurableType _.-sigma of + g_sigma_algebraType R.-ocitv.-measurable] -> \bar R := + [the measure _ _ of lebesgue_stieltjes_measure idfun]. +HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). +HB.instance Definition _ (R : realType) := + SigmaFiniteMeasure.on (@lebesgue_measure R). + +Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R := + [the measure _ _ of completed_lebesgue_stieltjes_measure idfun]. +HB.instance Definition _ (R : realType) := + Measure.on (@completed_lebesgue_measure R). +HB.instance Definition _ (R : realType) := + SigmaFiniteMeasure.on (@completed_lebesgue_measure R). + +Lemma completed_lebesgue_measure_is_complete {R : realType} : + measure_is_complete (@completed_lebesgue_measure R). +Proof. exact: measure_is_complete_caratheodory. Qed. + +(* the completed sigma-algebra is the same as the caratheodory sigma-algebra *) +Section completed_algebra_caratheodory. +Context {R : realType}. +Local Open Scope ereal_scope. + +Notation hlength := (@wlength R idfun). +Notation mu := (@lebesgue_measure R). +Notation completed_mu := (@completed_lebesgue_measure R). + +Let cara_sub_calgebra : hlength^*%mu.-cara.-measurable `<=` + (completed_algebra_gen mu).-sigma.-measurable. +Proof. +move=> E; wlog : E / completed_mu E < +oo. + move=> /= wlg. + have /sigma_finiteP[/= F [UFI ndF mF]] := + measure_extension_sigma_finite (@wlength_sigma_finite R idfun). + move=> mE. + rewrite -(setIT E)/= UFI setI_bigcupr; apply: bigcupT_measurable => i. + apply: wlg. + - rewrite (le_lt_trans _ (mF i).2)//= le_measure// inE/=. + + by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1. + + by apply: sub_caratheodory; exact: (mF i).1. + - by apply: measurableI => //; apply: sub_caratheodory; exact: (mF i).1. +move=> mEoo /= mE. +have inv0 n : (0 < n.+1%:R^-1 :> R)%R by rewrite invr_gt0. +set S := [set \sum_(0 <= k + exists2 A, @measurable_cover _ (ocitv_type R) E A & + \sum_(0 <= k s0; have : mu E \is a fin_num by rewrite ge0_fin_numE. + by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [A EA] <-] ?; exists A. +pose A n := projT1 (cid2 (coverE _ (inv0 n))). +have mA k : @measurable_cover _ (ocitv_type R) E (A k). + by rewrite /A; case: cid2. +have mA_E n : + \sum_(0 <= k /subset_trans; apply; apply: subset_bigcup => i _. +have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E. + apply: (le_lt_trans _ (mA_E m)). + apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (A m))). + apply: lee_nneseries => // n _. + by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m. +pose F := \bigcap_n (F_ n). +have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F. + apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. + by apply: sub_sigma_algebra; have [/(_ i)] := mA k. +have EF : E `<=` F by exact: sub_bigcap. +have muEF : completed_mu E = mu F. + apply/eqP; rewrite eq_le le_outer_measure//=. + apply/lee_addgt0Pr => /= _/posnumP[e]; near \oo => n. + apply: (@le_trans _ _ (mu (F_ n))). + by apply: le_outer_measure; exact: bigcap_inf. + rewrite (le_trans (ltW (mF_ n)))// leeD// lee_fin ltW//. + by near: n; apply: near_infty_natSinv_lt. +have coverEF s : (0 < s)%R -> + exists2 A, @measurable_cover _ (ocitv_type R) (F `\` E) A & + \sum_(0 <= k s0. + have : mu (F `\` E) \is a fin_num. + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu F))//; last by rewrite -muEF. + by apply: le_outer_measure; exact: subDsetl. + by move/lb_ereal_inf_adherent => /(_ _ s0)[_/= [B FEB] <-] ?; exists B. +pose B n := projT1 (cid2 (coverEF _ (inv0 n))). +have mB k : @measurable_cover _ (ocitv_type R) (F `\` E) (B k). + by rewrite /B; case: cid2. +have mB_FE n : + \sum_(0 <= k /subset_trans; apply; apply: subset_bigcup => i _. +have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E. + apply: (le_lt_trans _ (mB_FE m)). + apply: (le_trans (outer_measure_sigma_subadditive hlength^*%mu (B m))). + apply: lee_nneseries => // n _. + by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m. +pose G := \bigcap_n (G_ n). +have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G. + apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. + by apply: sub_sigma_algebra; have [/(_ i)] := mB k. +have FEG : F `\` E `<=` G by exact: sub_bigcap. +have muG : mu G = 0. + transitivity (completed_mu (F `\` E)). + apply/eqP; rewrite eq_le; apply/andP; split; last exact: le_outer_measure. + apply/lee_addgt0Pr => _/posnumP[e]. + near \oo => n. + apply: (@le_trans _ _ (mu (G_ n))). + by apply: le_outer_measure; exact: bigcap_inf. + rewrite (le_trans (ltW (mG_ n)))// leeD// lee_fin ltW//. + by near: n; apply: near_infty_natSinv_lt. + rewrite measureD//=. + + by rewrite setIidr// muEF subee// ge0_fin_numE//; move: mEoo; rewrite muEF. + + exact: sub_caratheodory. + + by move: mEoo; rewrite muEF. +apply: sub_sigma_algebra; exists (F `\` G); first exact: measurableD. +exists (E `&` G). + by apply: (@negligibleS _ _ _ mu G _ (@subIsetr _ E G)); exists G; split. +apply/seteqP; split=> [/= x [[Fx Gx]|[]//]|x Ex]. +- by rewrite -(notK (E x)) => Ex; apply: Gx; exact: FEG. +- have [|FGx] := pselect ((F `\` G) x); first by left. + right; split => //. + move/not_andP : FGx => [|]. + by have := EF _ Ex. + by rewrite notK. +Unshelve. all: by end_near. Qed. + +Lemma g_sigma_completed_algebra_genE : + (completed_algebra_gen mu).-sigma.-measurable = completed_algebra_gen mu. +Proof. +apply/seteqP; split; last first. + move=> _ [/= A /= mA [N neglN]] <-. + by apply: sub_sigma_algebra; exists A => //; exists N. +apply: smallest_sub => //=; split => /=. +- by exists set0 => //; exists set0; [exact: negligible_set0|rewrite setU0]. +- move=> G [/= A mA [N negN ANG]]; case: negN => /= F [mF F0 NF]. + have GANA : ~` G = ~` A `\` (N `&` ~` A). + by rewrite -ANG setCU setDE setCI setCK setIUr setICl setU0. + pose AA := ~` A `\` (F `&` ~` A). + pose NN := (F `&` ~` A) `\` (N `&` ~` A). + have GAANN : ~` G = AA `|` NN. + rewrite (_ : ~` G = ~` A `\` (N `&` ~` A))//. + by apply: setDU; [exact: setSI|exact: subIsetr]. + exists AA. + apply: measurableI => //=; first exact: measurableC. + by apply: measurableC; apply: measurableI => //; exact: measurableC. + by exists NN; [exists F; split => // x [] []|rewrite setDE setTI]. +- move=> F mF/=. + pose A n := projT1 (cid2 (mF n)). + pose N n := projT1 (cid2 (projT2 (cid2 (mF n))).2). + exists (\bigcup_k A k). + by apply: bigcupT_measurable => i; rewrite /A; case: cid2. + exists (\bigcup_k N k). + apply: negligible_bigcup => /= k. + by rewrite /N; case: (cid2 (mF k)) => //= *; case: cid2. + rewrite -bigcupU; apply: eq_bigcup => // i _. + by rewrite /A /N; case: (cid2 (mF i)) => //= *; case: cid2. +Qed. + +Lemma negligible_sub_caratheodory : + completed_mu.-negligible `<=` hlength^*%mu.-cara.-measurable. +Proof. +move=> N /= [/= A] [mA A0 NA]. +apply: le_caratheodory_measurable => /= X. +apply: (@le_trans _ _ (hlength^*%mu N + hlength^*%mu (X `&` ~` N))). + by rewrite leeD2r// le_outer_measure//; exact: subIsetr. +have -> : hlength^*%mu N = 0. + by apply/eqP; rewrite eq_le outer_measure_ge0//= andbT -A0 le_outer_measure. +by rewrite add0e// le_outer_measure//; exact: subIsetl. +Qed. + +Let calgebra_sub_cara : (completed_algebra_gen mu).-sigma.-measurable `<=` + hlength^*%mu.-cara.-measurable. +Proof. +rewrite g_sigma_completed_algebra_genE => A -[/= X mX] [N negN] <-{A}. +apply: measurableU => //; first exact: sub_caratheodory. +apply: negligible_sub_caratheodory; case: negN => /= B [mB B0 NB]. +by exists B; split => //=; exact: sub_caratheodory. +Qed. + +Lemma completed_caratheodory_measurable : + (completed_algebra_gen mu).-sigma.-measurable = + hlength^*%mu.-cara.-measurable. +Proof. +by apply/seteqP; split; [exact: calgebra_sub_cara | exact: cara_sub_calgebra]. +Qed. + +End completed_algebra_caratheodory. + +Section elebesgue_measure. +Variable R : realType. + +Definition elebesgue_measure : set \bar R -> \bar R := + fun S => lebesgue_measure (fine @` (S `\` [set -oo; +oo]%E)). + +Lemma elebesgue_measure0 : elebesgue_measure set0 = 0%E. +Proof. by rewrite /elebesgue_measure set0D image_set0 measure0. Qed. + +Lemma elebesgue_measure_ge0 X : (0 <= elebesgue_measure X)%E. +Proof. exact/measure_ge0. Qed. + +Lemma semi_sigma_additive_elebesgue_measure : + semi_sigma_additive elebesgue_measure. +Proof. +move=> /= F mF tF mUF; rewrite /elebesgue_measure. +rewrite [X in lebesgue_measure X](_ : _ = + \bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first. + rewrite predeqE => r; split. + by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x. + by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n. +apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) + (fun n => fine @` (F n `\` [set -oo; +oo]%E))). +- move=> n; have := mF n. + move=> [X mX [X' mX']] XX'Fn. + apply: measurable_image_fine. + rewrite -XX'Fn. + apply: measurableU; first exact: measurable_image_EFin. + by case: mX' => //; exact: measurableU. +- move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. + move: tF => /(_ i j Logic.I Logic.I); apply. + suff ab : a = b by exists a; split => //; rewrite ab. + move: a b {Fia Fjb} aoo boo ax bx. + move=> [a| |] [b| |] /=. + + by move=> _ _ -> ->. + + by move=> _; rewrite not_orP => -[_]/(_ erefl). + + by move=> _; rewrite not_orP => -[]/(_ erefl). + + by rewrite not_orP => -[_]/(_ erefl). + + by rewrite not_orP => -[_]/(_ erefl). + + by rewrite not_orP => -[_]/(_ erefl). + + by rewrite not_orP => -[]/(_ erefl). + + by rewrite not_orP => -[]/(_ erefl). + + by rewrite not_orP => -[]/(_ erefl). +- move: mUF. + rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. + - rewrite setU0 => h. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + move=> -[n _ [x [Fnx xoo <-{r}]]]. + have : (\bigcup_n F n) x by exists n. + by rewrite -h => -[x' Xx' <-]. + have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r. + by exists n => //; exists r%:E => //; split => //; case. + - move=> h. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + move=> -[n _ [x [Fnx xoo <-]]]. + have : (\bigcup_n F n) x by exists n. + by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. + have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. + by exists n => //; exists r%:E => //; split => //; case. + - (* NB: almost the same as the previous one, factorize?*) + move=> h. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + move=> -[n _ [x [Fnx xoo <-]]]. + have : (\bigcup_n F n) x by exists n. + by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. + have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. + by exists n => //; exists r%:E => //; split => //; case. + - move=> h. + rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. + move=> -[n _ [x [Fnx xoo <-]]]. + have : (\bigcup_n F n) x by exists n. + by rewrite -h => -[[x' Xx' <-//]|]. + have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. + by exists n => //; exists r%:E => //; split => //; case. Qed. -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). +HB.instance Definition _ := isMeasure.Build _ _ _ elebesgue_measure + elebesgue_measure0 elebesgue_measure_ge0 + semi_sigma_additive_elebesgue_measure. -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. +End elebesgue_measure. -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. +Section lebesgue_measure_itv. +Variable R : realType. -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). +Let lebesgue_measure_itvoc (a b : R) : + (lebesgue_measure (`]a, b] : set R) = + wlength [the cumulative _ of idfun] `]a, b])%classic. Proof. -move=> mf. -exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). +rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=. +by rewrite measurable_mu_extE//; exact: is_ocitv. Qed. -Lemma measurable_powR (R : realType) p : - measurable_fun [set: R] (@powR R ^~ p). +Let lebesgue_measure_itvoo_subr1 (a : R) : + lebesgue_measure (`]a - 1, a[%classic : set R) = 1%E. 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. -#[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). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] -Notation measurable_fun_pow := measurable_funX (only parsing). - -Section standard_emeasurable_fun. -Variable R : realType. +rewrite itv_bnd_open_bigcup//; transitivity (limn (lebesgue_measure \o + (fun k => `]a - 1, a - k.+1%:R^-1]%classic : set R))). + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + - by move=> ?; exact: measurable_itv. + - by apply: bigcup_measurable => k _; exact: measurable_itv. + - move=> n m nm; apply/subsetPset => x /=; rewrite !in_itv/= => /andP[->/=]. + by move/le_trans; apply; rewrite lerB// ler_pV2 ?ler_nat//; + rewrite inE ltr0n andbT unitfE. +rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first. + apply/funext => n /=; rewrite lebesgue_measure_itvoc. + have [->|n0] := eqVneq n 0%N. + by rewrite invr1 subrr set_itvoc0 wlength0. + rewrite wlength_itv/= lte_fin ifT; last first. + by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n. + by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e. +apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW. +apply/(@cvgrPdist_lt _ [the pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e]. +near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//. +by near: n; exact: near_infty_natSinv_lt. +Unshelve. all: by end_near. Qed. -Lemma EFin_measurable (D : set R) : measurable_fun D EFin. +Lemma lebesgue_measure_set1 (a : R) : lebesgue_measure [set a] = 0%E. Proof. -move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. -move=> /= _ [_ [x ->]] <-; apply: measurableI => //. -by rewrite preimage_itv_o_infty EFin_itv; exact: measurable_itv. +suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) = + lebesgue_measure (`]a - 1, a[%classic%R : set R) + + lebesgue_measure [set a])%E. + rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP. + rewrite wlength_itv lte_fin ltrBlDr ltrDl ltr01. + rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e. + by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP. +rewrite -setUitv1// ?bnd_simp; last by rewrite ltrBlDr ltrDl. +rewrite measureU //; apply/seteqP; split => // x []/=. +by rewrite in_itv/= => + xa; rewrite xa ltxx andbF. Qed. -Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. +Let lebesgue_measure_itvoo (a b : R) : + (lebesgue_measure (`]a, b[ : set R) = + wlength [the cumulative _ of idfun] `]a, b[)%classic. 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. +have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. +have := lebesgue_measure_itvoc a b. +rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//. +- by have /= -> := lebesgue_measure_set1 b; rewrite adde0. +- by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF. Qed. -Lemma oppe_measurable (D : set (\bar R)) : - measurable_fun D (-%E : \bar R -> \bar R). +Let lebesgue_measure_itvcc (a b : R) : + (lebesgue_measure (`[a, b] : set R) = + wlength [the cumulative _ of idfun] `[a, b])%classic. 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. +have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt. +have := lebesgue_measure_itvoc a b. +rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//. +- by have /= -> := lebesgue_measure_set1 a; rewrite add0e. +- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. Qed. -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). - -(* NB: real-valued function *) -(* TODO: rename to measurable_EFin after notation measurable_EFin is removed? *) -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. +Let lebesgue_measure_itvco (a b : R) : + (lebesgue_measure (`[a, b[ : set R) = + wlength [the cumulative _ of idfun] `[a, b[)%classic. 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. +have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. +have := lebesgue_measure_itvoo a b. +rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//. +- by have /= -> := lebesgue_measure_set1 a; rewrite add0e. +- by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx. Qed. -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). +Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) : + lebesgue_measure ([set` Interval (BSide x a) (BSide y b)] : set R) = + wlength [the cumulative _ of idfun] [set` Interval (BSide x a) (BSide y b)]. Proof. -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/EFin_measurable_fun/measurableT_comp. +by move: x y => [|] [|]; [exact: lebesgue_measure_itvco | + exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo | + exact: lebesgue_measure_itvoc]. 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). +Let limnatR : lim (((k%:R)%:E : \bar R) @[k --> \oo]) = +oo%E. +Proof. by apply/cvg_lim => //; apply/cvgenyP. Qed. -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). +Let lebesgue_measure_itv_bnd_infty x (a : R) : + lebesgue_measure ([set` Interval (BSide x a) +oo%O] : set R) = +oo%E. 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. +rewrite itv_bnd_infty_bigcup; transitivity (limn (lebesgue_measure \o + (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))). + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + + by move=> k; exact: measurable_itv. + + by apply: bigcup_measurable => k _; exact: measurable_itv. + + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=]. + by move=> /le_trans; apply; rewrite lerD// ler_nat. +rewrite (_ : _ \o _ = (fun k => k%:R%:E))//. +apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/=. +rewrite lte_fin; have [->|n0] := eqVneq n 0%N; first by rewrite addr0 ltxx. +by rewrite ltrDl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e. 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). +Let lebesgue_measure_itv_infty_bnd y (b : R) : + lebesgue_measure ([set` Interval -oo%O (BSide y b)] : set R) = +oo%E. 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. +rewrite itv_infty_bnd_bigcup; transitivity (limn (lebesgue_measure \o + (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))). + apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + + by move=> k; exact: measurable_itv. + + by apply: bigcup_measurable => k _; exact: measurable_itv. + + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->]. + by rewrite andbT; apply: le_trans; rewrite lerB// ler_nat. +rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//. +apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/= lte_fin. +have [->|n0] := eqVneq n 0%N; first by rewrite subr0 ltxx. +rewrite ltrBlDr ltrDl ltr0n lt0n n0 EFinN EFinB fin_num_oppeB// addeA. +by rewrite subee// add0e. 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)). +Let lebesgue_measure_itv_infty_infty : + lebesgue_measure ([set` Interval -oo%O +oo%O] : set R) = +oo%E. 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]. +rewrite set_itv_infty_infty -(setUv (`]-oo, 0[)) setCitv. +rewrite [X in _ `|` (X `|` _) ]set_itvE set0U measureU//; last first. + apply/seteqP; split => //= x [] /= /[swap]. + by rewrite !in_itv/= andbT ltNge => ->//. +rewrite [X in (X + _)%E]lebesgue_measure_itv_infty_bnd. +by rewrite [X in (_ + X)%E]lebesgue_measure_itv_bnd_infty. Qed. -Lemma measurable_funepos D (f : T -> \bar R) : - measurable_fun D f -> measurable_fun D f^\+. -Proof. by move=> mf; exact: measurable_maxe. Qed. - -Lemma measurable_funeneg D (f : T -> \bar R) : - measurable_fun D f -> measurable_fun D f^\-. -Proof. by move=> mf; apply: measurable_maxe => //; exact: measurableT_comp. Qed. - -Lemma measurable_mine D (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => mine (f x) (g x)). +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. 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. +move: i => [[x a|[|]]] [y b|[|]]. + by rewrite lebesgue_measure_itv_bnd wlength_itv. +- by rewrite set_itvE ?measure0. +- by rewrite lebesgue_measure_itv_bnd_infty/= ltry. +- by rewrite lebesgue_measure_itv_infty_bnd/= ltNyr. +- by rewrite set_itvE ?measure0. +- by rewrite lebesgue_measure_itv_infty_infty. +- by rewrite set_itvE ?measure0. +- by rewrite set_itvE ?measure0. +- by rewrite set_itvE ?measure0. Qed. -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 lebesgue_measure_ball (x r : R) : (0 <= r)%R -> + lebesgue_measure (ball x r) = (r *+ 2)%:E. 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. +rewrite le_eqVlt => /predU1P[ <-|r0]. + by rewrite (ball0 _ _).2// measure0 mul0rn. +rewrite ball_itv lebesgue_measure_itv/= lte_fin ltrBlDr -addrA ltrDl. +by rewrite addr_gt0 // -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n. 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. +Lemma lebesgue_measure_closed_ball (x r : R) : 0 <= r -> + lebesgue_measure (closed_ball x r) = (r *+ 2)%:E. 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. +rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0// measure0. +rewrite closed_ball_itv// lebesgue_measure_itv/= lte_fin -ltrBlDl addrAC. +rewrite subrr add0r gtrN// ?mulr_gt0// -EFinD; congr (_%:E). +by rewrite opprB addrAC addrCA subrr addr0 -mulr2n. 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). +End lebesgue_measure_itv. + +Lemma lebesgue_measure_rat (R : realType) : + lebesgue_measure (range ratr : set R) = 0%E. +Proof. +have /pcard_eqP/bijPex[f bijf] := card_rat; set f1 := 'pinv_(fun=> 0) setT f. +rewrite (_ : range _ = \bigcup_n [set ratr (f1 n)]); last first. + apply/seteqP; split => [_ [q _ <-]|_ [n _ /= ->]]; last by exists (f1 n). + exists (f q) => //=; rewrite /f1 pinvKV// ?in_setE// => x y _ _. + by apply: bij_inj; rewrite -setTT_bijective. +rewrite measure_bigcup//; last first. + apply/trivIsetP => i j _ _ ij; apply/seteqP; split => //= _ [/= ->]. + move=> /fmorph_inj. + have /set_bij_inj /[apply] := bijpinv_bij (fun=> 0) bijf. + by rewrite in_setE => /(_ Logic.I Logic.I); exact/eqP. +by rewrite eseries0// => n _ _; exact: lebesgue_measure_set1. +Qed. Section negligible_outer_measure. Context {R : realType}. Implicit Types (A : set R). Local Open Scope ereal_scope. -Definition is_open_itv A := exists ab, A = `]ab.1, ab.2[%classic. - -Definition open_itv_cover A := [set F : (set R)^nat | - (forall i, is_open_itv (F i)) /\ A `<=` \bigcup_k (F k)]. - Let l := (@wlength R idfun). - -Lemma outer_measure_open_itv_cover A : (l^* A)%mu = - ereal_inf [set \sum_(k _ /= [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 /=; 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. - -Definition mu := (@lebesgue_measure R). +Let mu := (@lebesgue_measure R). Lemma outer_measure_open_le A (e : R) : (0 < e)%R -> exists U, [/\ open U, A `<=` U & mu U <= (l^* A)%mu + e%:E]. @@ -2186,11 +2292,10 @@ Qed. End negligible_outer_measure. Section lebesgue_regularity. +Local Open Scope ereal_scope. 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]. @@ -2375,101 +2480,6 @@ Qed. End lebesgue_regularity. -Section egorov. -Context d {R : realType} {T : measurableType d}. -Context (mu : {measure set T -> \bar R}). - -Local Open Scope ereal_scope. - -(*TODO : this generalizes to any metric space with a borel measure*) -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. - Definition vitali_cover {R : realType} (E : set R) I (B : I -> set R) (D : set I) := (forall i, is_ball (B i)) /\ diff --git a/theories/normedtype.v b/theories/normedtype.v index c078ab301..475d1aed3 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -15,7 +15,7 @@ Require Import ereal reals signed topology prodnormedzmodule function_spaces. (* We used these definitions to prove the intermediate value theorem and *) (* the Heine-Borel theorem, which states that the compact sets of *) (* $\mathbb{R}^n$ are the closed and bounded sets, Urysohn's lemma, Vitali's *) -(* covering lemmas (finite case), etc. *) +(* covering lemmas (finite case and infinite case), etc. *) (* *) (* * Limit superior and inferior: *) (* limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F *) diff --git a/theories/topology.v b/theories/topology.v index c6c50e8a7..ec080ab3c 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -6129,8 +6129,8 @@ split; first last. move=> ? ? _; exists V; last by rewrite -setIA setIid. by move: oV; rewrite openE /interior; apply. rewrite -open_subspaceIT => oUA. -have oxF : (forall (x : T), (U `&` A) x -> - exists V, (open_nbhs (x : T) V) /\ (V `&` A `<=` U `&` A)). +have oxF : forall x : T, (U `&` A) x -> + exists V, (open_nbhs (x : T) V) /\ (V `&` A `<=` U `&` A). move=> x /[dup] UAx /= [??]; move: (oUA _ UAx); case: nbhs_subspaceP => // ?. rewrite withinE /= => [[V nbhsV UV]]; rewrite -setIA setIid in UV. @@ -6248,12 +6248,12 @@ Qed. End Subspace. Global Instance subspace_filter {T : topologicalType} - (A : set T) (x : subspace A) : - Filter (nbhs_subspace x) := nbhs_subspace_filter x. + (A : set T) (x : subspace A) : + Filter (nbhs_subspace x) := nbhs_subspace_filter x. Global Instance subspace_proper_filter {T : topologicalType} - (A : set T) (x : subspace A) : - ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x. + (A : set T) (x : subspace A) : + ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x. Notation "{ 'within' A , 'continuous' f }" := (continuous (f : subspace A -> _)) : classical_set_scope.