From caae62323fb99beed78f866218588183486864c0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Feb 2025 18:42:56 +0900 Subject: [PATCH] fixes #1315 --- CHANGELOG_UNRELEASED.md | 22 + _CoqProject | 1 + theories/Make | 1 + theories/derive.v | 25 - theories/lebesgue_measure.v | 1681 +------------------------------- theories/measurable_realfun.v | 1704 +++++++++++++++++++++++++++++++++ theories/normedtype.v | 45 - 7 files changed, 1731 insertions(+), 1748 deletions(-) create mode 100644 theories/measurable_realfun.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b7c04b703d..e4e90cfb1b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -100,6 +100,9 @@ - in `normedtype.v`: + lemmas `ninfty`, `cvgy_compNP` +- new file `measurable_realfun.v` + + with as contents the first half of the file `lebesgue_measure.v` + ### Changed - in `lebesgue_integral.v` @@ -126,6 +129,9 @@ - in `normedtype.v`: + lemma `cvgyNP` renamed to `cvgNy_compN` and generalized +- file `lebesgue_measure.v` + + first half moved to a new file `measurable_realfun.v` + ### Renamed - in `measure.v` @@ -229,6 +235,22 @@ `__deprecated__dvg_ereal_cvg`, `__deprecated__ereal_cvg_real` (were deprecated since 0.6.0) +- in `derive.v`: + + notations `le0r_cvg_map`, `ler0_cvg_map`, `ler_cvg_map` + (deprecated since 0.6.0) + + lemmas `__deprecated__le0r_cvg_map`, `__deprecated__ler0_cvg_map`, + `__deprecated__ler_cvg_map` + (deprecated since 0.6.0) + +- in `normedtype.v` + + notations `cvg_distP`, `cvg_distW`, `continuous_cvg_dist`, `cvg_dist2P`, + `cvg_gt_ge`, `cvg_lt_le_`, `linear_bounded0` + (deprecated since 0.6.0) + + lemmas `__deprecated__cvg_distW`, `__deprecated__continuous_cvg_dist`, + `__deprecated__cvg_gt_ge`, `__deprecated__cvg_lt_le`, + `__deprecated__linear_bounded0 ` + (deprecated since 0.6.0) + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index b5e4a8169c..74ddd750a8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -77,6 +77,7 @@ theories/sequences.v theories/exp.v theories/trigo.v theories/esum.v +theories/measurable_realfun.v theories/lebesgue_measure.v theories/lebesgue_stieltjes_measure.v theories/forms.v diff --git a/theories/Make b/theories/Make index e3a8d9799a..aac6828d70 100644 --- a/theories/Make +++ b/theories/Make @@ -44,6 +44,7 @@ sequences.v exp.v trigo.v esum.v +measurable_realfun.v lebesgue_measure.v forms.v derive.v diff --git a/theories/derive.v b/theories/derive.v index 743ce282ab..9bbfe99c26 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1463,31 +1463,6 @@ by apply: xe_A => //; rewrite eq_sym. Qed. Arguments cvg_at_leftE {R V} f x. -Lemma __deprecated__le0r_cvg_map (R : realFieldType) (T : topologicalType) - (F : set_system T) (FF : ProperFilter F) (f : T -> R) : - (\forall x \near F, 0 <= f x) -> cvg (f @ F) -> 0 <= lim (f @ F). -Proof. by move=> ? ?; rewrite limr_ge. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="generalized by `limr_ge`")] -Notation le0r_cvg_map := __deprecated__le0r_cvg_map (only parsing). - -Lemma __deprecated__ler0_cvg_map (R : realFieldType) (T : topologicalType) - (F : set_system T) (FF : ProperFilter F) (f : T -> R) : - (\forall x \near F, f x <= 0) -> cvg (f @ F) -> lim (f @ F) <= 0. -Proof. by move=> ? ?; rewrite limr_le. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="generalized by `limr_le`")] -Notation ler0_cvg_map := __deprecated__ler0_cvg_map (only parsing). - -Lemma __deprecated__ler_cvg_map (R : realFieldType) (T : topologicalType) - (F : set_system T) (FF : ProperFilter F) (f g : T -> R) : - (\forall x \near F, f x <= g x) -> cvg (f @ F) -> cvg (g @ F) -> - lim (f @ F) <= lim (g @ F). -Proof. by move=> ? ? ?; rewrite ler_lim. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="subsumed by `ler_lim`")] -Notation ler_cvg_map := __deprecated__ler_cvg_map (only parsing). - Lemma derive1_at_max (R : realFieldType) (f : R -> R) (a b c : R) : a <= b -> (forall t, t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R -> (forall t, t \in `]a, b[%R -> f t <= f c) -> is_derive c 1 f 0. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 802b4b3655..7d2a444f62 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -6,14 +6,13 @@ From mathcomp Require Import cardinality fsbigop reals ereal signed. From mathcomp Require Import topology numfun tvs normedtype function_spaces. From HB Require Import structures. From mathcomp Require Import sequences esum measure real_interval realfun exp. -From mathcomp Require Export lebesgue_stieltjes_measure. +From mathcomp Require Export measurable_realfun lebesgue_stieltjes_measure. (**md**************************************************************************) (* # Lebesgue Measure *) (* *) -(* 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 *) +(* This file 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$. *) @@ -23,28 +22,6 @@ From mathcomp Require Export lebesgue_stieltjes_measure. (* - Achim Klenke, Probability Theory 2nd edition, 2014 *) (* *) (* ``` *) -(* completed_algebra_gen == generator of the completed Lebesgue *) -(* sigma-algebra *) -(* ps_infty == inductive definition of the powerset *) -(* {0, {-oo}, {+oo}, {-oo,+oo}} *) -(* emeasurable G == sigma-algebra over \bar R built out of the *) -(* measurables G of a sigma-algebra over R *) -(* ``` *) -(* *) -(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) -(* of equivalence between the sigma-algebra generated by open-closed *) -(* intervals and the sigma-algebras generated by open rays, closed rays, and *) -(* open intervals. *) -(* *) -(* The module NGenCInfty provides a proof of equivalence between the *) -(* sigma-algebra for natural numbers and the sigma-algebra generated by *) -(* closed rays. *) -(* *) -(* The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs *) -(* of equivalence between emeasurable and the sigma-algebras generated by *) -(* open rays and closed rays. *) -(* *) -(* ``` *) (* lebesgue_measure == the Lebesgue measure *) (* completed_lebesgue_measure == the completed Lebesgue measure *) (* elebesgue_measure == the Lebesgue measure extended to \bar R *) @@ -66,1658 +43,6 @@ Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Definition completed_algebra_gen d {T : semiRingOfSetsType d} {R : realType} - (mu : set T -> \bar R) : set _ := - [set A `|` N | A in d.-measurable & N in mu.-negligible]. - -Section ps_infty. -Context {T : Type}. -Local Open Scope ereal_scope. - -Inductive ps_infty : set \bar T -> Prop := -| ps_infty0 : ps_infty set0 -| ps_ninfty : ps_infty [set -oo] -| ps_pinfty : ps_infty [set +oo] -| ps_inftys : ps_infty [set -oo; +oo]. - -Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo]. -Proof. -split => [[]//|Aoo]. -by have [] := subset_set2 Aoo; move=> ->; constructor. -Qed. - -Lemma setCU_Efin (A : set T) (B : set \bar T) : ps_infty B -> - ~` (EFin @` A) `&` ~` B = (EFin @` ~` A) `|` ([set -oo%E; +oo%E] `&` ~` B). -Proof. -move=> ps_inftyB. -have -> : ~` (EFin @` A) = EFin @` (~` A) `|` [set -oo; +oo]%E. - by rewrite EFin_setC setDKU // => x [|] -> -[]. -rewrite setIUl; congr (_ `|` _); rewrite predeqE => -[x| |]; split; try by case. -by move=> [] x' Ax' [] <-{x}; split; [exists x'|case: ps_inftyB => // -[]]. -Qed. - -End ps_infty. - -Section salgebra_ereal. -Variables (R : realType) (G : set (set R)). -Let measurableR : set (set R) := G.-sigma.-measurable. - -Definition emeasurable : set (set \bar R) := - [set EFin @` A `|` B | A in measurableR & B in ps_infty]. - -Lemma emeasurable0 : emeasurable set0. -Proof. -exists set0; first exact: measurable0. -by exists set0; rewrite ?setU0// ?image_set0//; constructor. -Qed. - -Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X). -Proof. -move => -[A mA] [B PooB <-]; rewrite setCU setCU_Efin //. -exists (~` A); [exact: measurableC | exists ([set -oo%E; +oo%E] `&` ~` B) => //]. -case: PooB. -- by rewrite setC0 setIT; constructor. -- rewrite setIUl setICr set0U -setDE. - have [_ ->] := @setDidPl (\bar R) [set +oo%E] [set -oo%E]; first by constructor. - by rewrite predeqE => x; split => // -[->]. -- rewrite setIUl setICr setU0 -setDE. - have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor. - by rewrite predeqE => x; split => // -[->]. -- by rewrite setICr; constructor. -Qed. - -Lemma bigcupT_emeasurable (F : (set \bar R)^nat) : - (forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)). -Proof. -move=> mF; pose P := fun i j => measurableR j.1 /\ ps_infty j.2 /\ - F i = [set x%:E | x in j.1] `|` j.2. -have [f fi] : {f : nat -> (set R) * (set \bar R) & forall i, P i (f i) }. - by apply: choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x, y). -exists (\bigcup_i (f i).1). - by apply: bigcupT_measurable => i; exact: (fi i).1. -exists (\bigcup_i (f i).2). - apply/ps_inftyP => x [n _] fn2x. - have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n. - exact. -rewrite [RHS](@eq_bigcupr _ _ _ _ - (fun i => [set x%:E | x in (f i).1] `|` (f i).2)); last first. - by move=> i; have [_ []] := fi i. -rewrite bigcupU; congr (_ `|` _). -rewrite predeqE => i /=; split=> [[r [n _ fn1r <-{i}]]|[n _ [r fn1r <-{i}]]]; - by [exists n => //; exists r | exists r => //; exists n]. -Qed. - -Definition ereal_isMeasurable : isMeasurable default_measure_display (\bar R) := - isMeasurable.Build _ _ - emeasurable0 emeasurableC bigcupT_emeasurable. - -End salgebra_ereal. - -Section puncture_ereal_itv. -Variable R : realDomainType. -Implicit Types (y : R) (b : bool). -Local Open Scope ereal_scope. - -Lemma punct_eitv_bndy b y : [set` Interval (BSide b y%:E) +oo%O] = - EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo]. -Proof. -rewrite predeqE => x; split; rewrite /= in_itv andbT. -- move: x => [x| |] yxb; [|by right|by case: b yxb]. - by left; exists x => //; rewrite in_itv /= andbT; case: b yxb. -- move=> [[r]|->]. - + by rewrite in_itv /= andbT => yxb <-; case: b yxb. - + by case: b => /=; rewrite ?(ltry, leey). -Qed. - -Lemma punct_eitv_Nybnd b y : [set` Interval -oo%O (BSide b y%:E)] = - [set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)]. -Proof. -rewrite predeqE => x; split; rewrite /= in_itv. -- move: x => [x| |] yxb; [|by case: b yxb|by left]. - by right; exists x => //; rewrite in_itv /= andbT; case: b yxb. -- move=> [->|[r]]. - + by case: b => /=; rewrite ?(ltNyr, leNye). - + by rewrite in_itv /= => yxb <-; case: b yxb. -Qed. - -Lemma punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set~ -oo]. -Proof. -rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. -by move=> [x| |] //= _; [left; exists x|right]. -Qed. - -Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo]. -Proof. -rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. -by move=> [x| |] //= _; [left; exists x|right]. -Qed. - -End puncture_ereal_itv. - -Section salgebra_R_ssets. -Variable R : realType. - -Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). -Definition measurableR : set (set R) := - (R.-ocitv.-measurable).-sigma.-measurable. - -HB.instance Definition _ := Pointed.on R. -HB.instance Definition R_isMeasurable : - isMeasurable default_measure_display R := - @isMeasurable.Build _ measurableTypeR measurableR - measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). -(*HB.instance (Real.sort R) R_isMeasurable.*) - -Lemma measurable_set1 (r : R) : measurable [set r]. -Proof. -rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. -by apply: sub_sigma_algebra; exact/is_ocitv. -Qed. -#[local] Hint Resolve measurable_set1 : core. - -Lemma measurable_itv (i : interval R) : measurable [set` i]. -Proof. -have moc (a b : R) : measurable `]a, b]. - by apply: sub_sigma_algebra; apply: is_ocitv. -have mopoo (x : R) : measurable `]x, +oo[. - by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable. -have mnooc (x : R) : measurable `]-oo, x]. - by rewrite -setCitvr; exact/measurableC. -have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. - case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D. - by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF. -have moo (a b : R) : measurable `]a, b[. - by rewrite ooE; exact: measurableD. -have mcc (a b : R) : measurable `[a, b]. - case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU1itv//; apply/measurableU. -have mco (a b : R) : measurable `[a, b[. - case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU1itv//; apply/measurableU. -have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. - by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx. -case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. -- by rewrite -setU1itv//; exact/measurableU. -- by rewrite oooE; exact/measurableD. -- by rewrite set_itv_infty_infty. -Qed. -#[local] Hint Resolve measurable_itv : core. - -Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) : - measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> - measurable_fun `[x, y[ f. -Proof. -have [xy|yx _] := ltP x y; last first. - by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0. -move: b0 b1 => [|] [|] // mf. -- apply: measurable_funS mf => //; exact: subset_itv_co_cc. -- rewrite -setU1itv//= measurable_funU//; split => //. - exact: measurable_fun_set1. -- rewrite -setU1itv//= measurable_funU//; split. - exact: measurable_fun_set1. - by apply: measurable_funS mf => //; exact: subset_itv_oo_oc. -Qed. - -Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) : - measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> - measurable_fun `]x, y] f. -Proof. -have [xy|yx _] := ltP x y; last first. - by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0. -move: b0 b1 => [|] [|] // mf. -- rewrite -setUitv1//= measurable_funU//; split. - by apply: measurable_funS mf => //; exact: subset_itv_oo_co. - exact: measurable_fun_set1. -- by apply: measurable_funS mf => //; exact: subset_itv_oc_cc. -- rewrite -setUitv1//= measurable_funU//; split => //. - exact: measurable_fun_set1. -Qed. - -Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) : - measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> - measurable_fun `[x, y] f. -Proof. -move=> mf. -have [xy|] := ltP x y; last first. - rewrite le_eqVlt => /predU1P[->|ba]. - by rewrite set_itv1; exact: measurable_fun_set1. - rewrite set_itv_ge//; first exact: measurable_fun_set0. - by rewrite -leNgt bnd_simp. -rewrite -setUitv1//=; last by rewrite bnd_simp ltW. - rewrite measurable_funU//; split => //. - exact: measurable_fun_itv_co mf. -exact: measurable_fun_set1. -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). -Proof. -by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0]. -Qed. - -Lemma emeasurable_set1 (x : \bar R) : measurable [set x]. -Proof. -case: x => [r| |]. -- by rewrite -image_set1; apply: measurable_image_EFin; apply: measurable_set1. -- exists set0 => //; [exists [set +oo%E]; [by constructor|]]. - by rewrite image_set0 set0U. -- exists set0 => //; [exists [set -oo%E]; [by constructor|]]. - by rewrite image_set0 set0U. -Qed. -#[local] Hint Resolve emeasurable_set1 : core. - -Let emeasurable_itv_bndy b (y : \bar R) : - measurable [set` Interval (BSide b y) +oo%O]. -Proof. -move: y => [y| |]. -- exists [set` Interval (BSide b y) +oo%O]; first exact: measurable_itv. - by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy]. -- by case: b; rewrite ?itv_oyy ?itv_cyy. -- case: b; first by rewrite itv_cNyy. - by rewrite itv_oNyy; exact/measurableC. -Qed. - -Let emeasurable_itv_Nybnd b (y : \bar R) : - measurable [set` Interval -oo%O (BSide b y)]. -Proof. by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bndy. Qed. - -Lemma emeasurable_itv (i : interval (\bar R)) : - measurable ([set` i]%classic : set \bar R). -Proof. -rewrite -[X in measurable X]setCK; apply: measurableC. -rewrite set_interval.setCitv /=; apply: measurableU => [|]. -- by move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE. -- by move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE. -Qed. - -Lemma measurable_image_fine (X : set \bar R) : measurable X -> - measurable [set fine x | x in X `\` [set -oo; +oo]%E]. -Proof. -case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. -- rewrite setU0 => <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. - by move=> Yr; exists r%:E; split => [|[]//]; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <- _ <-//]|]]]. - by move=> <-; rewrite not_orP => -[]/(_ erefl). - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. - by move=> ->; rewrite not_orP => -[_]/(_ erefl). - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -Qed. - -Lemma measurable_ball (x : R) e : measurable (ball x e). -Proof. by rewrite ball_itv; exact: measurable_itv. Qed. - -Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). -Proof. -have [r0|r0] := leP r 0; first by rewrite closed_ball0. -rewrite closed_ball_itv//. -Qed. - -End salgebra_R_ssets. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| - apply: emeasurable_set1] : core. -#[global] -Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. -#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_bnd_pinfty := emeasurable_itv (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing). - -Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D -> - measurable_fun D fine. -Proof. -move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then - D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first. - apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]]. - - by case: ifPn => _; split => //; left; exists r. - - by rewrite mem_set//; split => //; right; right. - - by rewrite mem_set//; split => //; right; left. - - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr. - - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. - - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. -case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin. -by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU]. -Qed. -#[global] Hint Extern 0 (measurable_fun _ fine) => - solve [exact: fine_measurable] : core. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `fine_measurable` instead")] -Notation measurable_fine := fine_measurable (only parsing). - -Section measurable_fun_measurable. -Local Open Scope ereal_scope. -Context d (T : sigmaRingType d) (R : realType). -Variables (D : set T) (f : T -> \bar R). -Hypotheses (mD : measurable D) (mf : measurable_fun D f). -Implicit Types y : \bar R. - -Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]). -Proof. by rewrite -preimage_itvcy; exact/mf/emeasurable_itv. Qed. - -Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]). -Proof. by rewrite -preimage_itvoy; exact/mf/emeasurable_itv. Qed. - -Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]). -Proof. by rewrite -preimage_itvNyo; exact/mf/emeasurable_itv. Qed. - -Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]). -Proof. by rewrite -preimage_itvNyc; exact/mf/emeasurable_itv. Qed. - -Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]). -Proof. -rewrite [X in measurable X](_ : _ = - \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))). - apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA. - exact/measurableI/emeasurable_fun_infty_c/emeasurable_fun_c_infty. -rewrite predeqE => t; split => [/= [Dt ft]|]. - exists `|ceil `|fine (f t)| |%N => //=; split=> //; split. - rewrite -[leRHS](fineK ft) lee_fin lerNl pmulrn abszE ceil_ge_int ger0_norm. - by rewrite ceil_le// -normrN ler_norm. - by rewrite -(ceil0 R) ceil_le. - rewrite -[leLHS](fineK ft) lee_fin pmulrn abszE ceil_ge_int ger0_norm. - by rewrite ceil_le// ler_norm. - by rewrite -(ceil0 R) ceil_le. -move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. -by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. -Qed. - -Lemma emeasurable_neq y : measurable (D `&` [set x | f x != y]). -Proof. -rewrite (_ : [set x | f x != y] = f @^-1` (setT `\ y)). - exact/mf/measurableD. -rewrite predeqE => t; split; last by rewrite /preimage /= => -[_ /eqP]. -by rewrite /= => ft0; rewrite /preimage /=; split => //; exact/eqP. -Qed. - -End measurable_fun_measurable. - -Module RGenOInfty. -Section rgenoinfty. -Variable R : realType. -Implicit Types x y z : R. - -Definition G := [set A | exists x, A = `]x, +oo[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; last by apply: sub_sigma_algebra; eexists; reflexivity. -rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k. -by apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b x : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b x)]. -Proof. -case: a => [a r _|[_|//]]. - by rewrite set_itv_splitD; apply: measurableD => //; - exact: measurable_itv_bnd_infty. -by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; exact: measurable_itv_bounded. -apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> A' /= [x ->]; exact: measurable_itv. -Qed. - -End rgenoinfty. -End RGenOInfty. - -Module RGenInftyO. -Section rgeninftyo. -Variable R : realType. -Implicit Types x y z : R. - -Definition G := [set A | exists x, A = `]-oo, x[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. -Proof. -case: b; first by apply sub_sigma_algebra; eexists; reflexivity. -rewrite -setCitvr itv_o_inftyEbigcup; apply/measurableC/bigcupT_measurable => n. -rewrite -setCitvl; apply: measurableC. -by apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b x : a != -oo%O -> - G.-sigma.-measurable [set` Interval (BSide b x) a]. -Proof. -case: a => [a r _|[//|_]]. - by rewrite set_itv_splitD; apply/measurableD => //; - rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty. -by rewrite -setCitvl; apply: measurableC; apply: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; apply: measurable_itv_bounded. -apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> A' /= [x ->]; apply: measurable_itv. -Qed. - -End rgeninftyo. -End RGenInftyO. - -Module RGenCInfty. -Section rgencinfty. -Variable R : realType. -Implicit Types x y z : R. - -Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty. -rewrite itv_o_inftyEbigcup; apply: bigcupT_measurable => k. -by apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b y : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b y)]. -Proof. -case: a => [a r _|[_|//]]. - rewrite set_itv_splitD. - by apply: measurableD; apply: measurable_itv_bnd_infty. -by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; apply: measurable_itv_bounded. -apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> A' /= [x ->]; apply: measurable_itv. -Qed. - -End rgencinfty. -End RGenCInfty. - -Module RGenOpens. -Section rgenopens. -Variable R : realType. -Implicit Types x y z : R. - -Definition G := [set A | exists x y, A = `]x, y[%classic]. - -Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic. -Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. - -Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic. -Proof. -rewrite itv_bnd_inftyEbigcup; apply: bigcupT_measurable => i. -exact: measurable_itvoo. -Qed. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; last exact: measurable_itv_o_infty. -rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k. -exact: measurable_itv_o_infty. -Qed. - -Lemma measurable_itv_infty_bnd b x : - G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. -Proof. -by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. -Qed. - -Lemma measurable_itv_bounded a x b y : - G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)]. -Proof. -move: a b => [] []; rewrite -[X in measurable X]setCK setCitv; - apply: measurableC; apply: measurableU; try solve[ - exact: measurable_itv_infty_bnd|exact: measurable_itv_bnd_infty]. -Qed. - -Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - by move=> I [x _ <-]; apply: measurable_itv_bounded. -apply: smallest_sub; first exact: smallest_sigma_algebra. -by move=> A' /= [x [y ->]]; apply: measurable_itv. -Qed. - -End rgenopens. -End RGenOpens. - -Section erealwithrays. -Variable R : realType. -Implicit Types (x y z : \bar R) (r s : R). -Local Open Scope ereal_scope. - -Lemma EFin_itv_bnd_infty b r : EFin @` [set` Interval (BSide b r) +oo%O] = - [set` Interval (BSide b r%:E) +oo%O] `\ +oo. -Proof. -rewrite eqEsubset; split => [x [s /itvP rs <-]|x []]. - split => //=; rewrite in_itv /=. - by case: b in rs *; rewrite /= ?(lee_fin, lte_fin) rs. -move: x => [s|_ /(_ erefl)|] //=; rewrite in_itv /= andbT; last first. - by case: b => /=; rewrite 1?(leNgt,ltNge) 1?(ltNyr, leNye). -by case: b => /=; rewrite 1?(lte_fin,lee_fin) => rs _; - exists s => //; rewrite in_itv /= rs. -Qed. - -Lemma EFin_itv r : [set s | r%:E < s%:E] = `]r, +oo[%classic. -Proof. -by rewrite predeqE => s; split => [|]; rewrite /= lte_fin in_itv/= andbT. -Qed. - -Lemma preimage_EFin_setT : @EFin R @^-1` [set x | x \in `]-oo%E, +oo[] = setT. -Proof. -by rewrite set_itvE predeqE => r; split=> // _; rewrite /preimage /= ltNyr. -Qed. - -Lemma eitv_bnd_infty b r : `[r%:E, +oo[%classic = - \bigcap_k [set` Interval (BSide b (r - k.+1%:R^-1)%:E) +oo%O] :> set _. -Proof. -rewrite predeqE => x; split=> [|]. -- move: x => [s /=| _ n _|//]. - + rewrite in_itv /= andbT lee_fin => rs n _ /=; rewrite in_itv/= andbT. - case: b => /=. - * by rewrite lee_fin lerBlDl (le_trans rs)// lerDr. - * by rewrite lte_fin ltrBlDl (le_lt_trans rs)// ltrDr. - + by rewrite /= in_itv /= andbT; case: b => /=; rewrite lteey. -- move: x => [s| |/(_ 0%N Logic.I)] /=; rewrite ?in_itv/= ?leey//; last first. - by case: b. - move=> h; rewrite lee_fin leNgt andbT; apply/negP => /ltr_add_invr[k skr]. - have {h} := h k Logic.I; rewrite /= in_itv /= andbT; case: b => /=. - + by rewrite lee_fin lerBlDr leNgt skr. - + by rewrite lte_fin ltrBlDr ltNge (ltW skr). -Qed. - -Lemma eitv_infty_bnd b r : `]-oo, r%:E]%classic = - \bigcap_k [set` Interval -oo%O (BSide b (r%:E + k.+1%:R^-1%:E))] :> set _. -Proof. -rewrite predeqE => x; split=> [|]. -- move: x => [s /=|//|_ n _]. - + rewrite in_itv /= lee_fin => sr n _; rewrite /= in_itv /= -EFinD. - case: b => /=. - * by rewrite lte_fin (le_lt_trans sr)// ltrDl. - * by rewrite lee_fin (le_trans sr)// lerDl. - + by rewrite /= in_itv /= -EFinD; case: b => //=; rewrite lteNye. -- move: x => [s|/(_ 0%N Logic.I)|]/=; rewrite !in_itv/= ?leNye//; last first. - by case: b. - move=> h; rewrite lee_fin leNgt; apply/negP => /ltr_add_invr[k rks]. - have {h} := h k Logic.I; rewrite /= in_itv /= -EFinD; case: b => /=. - + by rewrite lte_fin ltNge (ltW rks). - + by rewrite lee_fin leNgt rks. -Qed. - -Lemma eset1Ny : - [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R). -Proof. -rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr. -move=> [r|/(_ O Logic.I)|]//. -move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge. -rewrite lee_fin; have [r0|r0] := leP 0%R r. - by rewrite (le_trans _ r0) // lerNl oppr0 ler0n. -rewrite lerNl -abszN natr_absz gtr0_norm; last first. - by rewrite ltrNr oppr0 -floor_lt0. -by rewrite mulrNz lerNl opprK ge_floor. -Qed. - -Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). -Proof. -rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. -move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. -rewrite andbT lte_fin ltNge. -have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). -by rewrite natr_absz gtr0_norm// ?le_ceil// -ceil_gt0. -Qed. - -End erealwithrays. - -Module ErealGenOInfty. -Section erealgenoinfty. -Variable R : realType. -Implicit Types (x y z : \bar R) (r s : R). - -Local Open Scope ereal_scope. - -Definition G := [set A : set \bar R | exists r, A = `]r%:E, +oo[%classic]. - -Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. -Proof. -rewrite eset1Ny; apply: bigcap_measurable => // i _. -rewrite -setCitvr; apply: measurableC; rewrite (eitv_bnd_infty false). -apply: bigcap_measurable => // j _; apply: sub_sigma_algebra. -by exists (- (i%:R + j.+1%:R^-1))%R; rewrite opprD. -Qed. - -Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. -Proof. -rewrite eset1y; apply: bigcapT_measurable => i. -by apply: sub_sigma_algebra; exists i%:R. -Qed. - -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. -Proof. -apply/seteqP; split; last first. - apply: smallest_sub. - split; first exact: emeasurable0. - by move=> *; rewrite setTD; exact: emeasurableC. - by move=> *; exact: bigcupT_emeasurable. - move=> _ [r ->]; rewrite /emeasurable /=. - exists `]r, +oo[%classic. - rewrite RGenOInfty.measurableE. - exact: RGenOInfty.measurable_itv_bnd_infty. - by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. -move=> A [B mB [C mC]] <-; apply: measurableU; last first. - case: mC; [by []|exact: measurable_set1Ny|exact: measurable_set1y|]. - - by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. -rewrite RGenOInfty.measurableE in mB. -have smB := smallest_sub _ _ mB. -(* BUG: elim/smB : _. fails !! *) -apply: (smB (G.-sigma.-measurable \o (image^~ EFin))); last first. - move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. - by apply: sub_sigma_algebra => /=; exists r. - exact: measurable_set1y. -split=> /= [|D mD|F mF]; first by rewrite image_set0. -- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. - by apply: measurableU; [exact: measurable_set1Ny| exact: measurable_set1y]. -- by rewrite EFin_bigcup; apply: bigcup_measurable => i _ ; exact: mF. -Qed. - -End erealgenoinfty. -End ErealGenOInfty. - -Module ErealGenCInfty. -Section erealgencinfty. -Variable R : realType. -Implicit Types (x y z : \bar R) (r s : R). -Local Open Scope ereal_scope. - -Definition G := [set A : set \bar R | exists r, A = `[r%:E, +oo[%classic]. - -Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. -Proof. -rewrite eset1Ny; apply: bigcapT_measurable=> i; rewrite -setCitvr. -by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%R. -Qed. - -Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. -Proof. -rewrite eset1y; apply: bigcap_measurable => // i _. -rewrite -setCitvl; apply: measurableC; rewrite (eitv_infty_bnd true). -apply: bigcap_measurable => // j _; rewrite -setCitvr; apply: measurableC. -by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R. -Qed. - -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. -Proof. -apply/seteqP; split; last first. - apply: smallest_sub. - split; first exact: emeasurable0. - by move=> *; rewrite setTD; exact: emeasurableC. - by move=> *; exact: bigcupT_emeasurable. - move=> _ [r ->]/=; exists `[r, +oo[%classic. - rewrite RGenOInfty.measurableE. - exact: RGenOInfty.measurable_itv_bnd_infty. - by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. -move=> _ [A' mA' [C mC]] <-; apply: measurableU; last first. - case: mC; [by []|exact: measurable_set1Ny| exact: measurable_set1y|]. - by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. -rewrite RGenCInfty.measurableE in mA'. -have smA' := smallest_sub _ _ mA'. -(* BUG: elim/smA' : _. fails !! *) -apply: (smA' (G.-sigma.-measurable \o (image^~ EFin))); last first. - move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. - by apply: sub_sigma_algebra => /=; exists r. - exact: measurable_set1y. -split=> /= [|D mD|F mF]; first by rewrite image_set0. -- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. - by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. -- by rewrite EFin_bigcup; apply: bigcup_measurable => i _; exact: mF. -Qed. - -End erealgencinfty. -End ErealGenCInfty. - -Module ErealGenInftyO. -Section erealgeninftyo. -Variable R : realType. - -Definition G := [set A : set \bar R | exists r, A = `]-oo, r%:E[%classic]. - -Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. -Proof. -rewrite ErealGenCInfty.measurableE eqEsubset; split => A. - apply: smallest_sub; first exact: smallest_sigma_algebra. - move=> _ [x ->]; rewrite -[X in _.-measurable X]setCK; apply: measurableC. - by apply: sub_sigma_algebra; exists x; rewrite setCitvr. -apply: smallest_sub; first exact: smallest_sigma_algebra. -move=> x Gx; rewrite -(setCK x); apply: measurableC; apply: sub_sigma_algebra. -by case: Gx => y ->; exists y; rewrite setCitvl. -Qed. - -End erealgeninftyo. -End ErealGenInftyO. - -(* 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). -Proof. -move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. -by apply: measurableI => //; exact: open_measurable. -Qed. - -Lemma closed_measurable (A : set R) : closed A -> measurable A. -Proof. by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed. - -Lemma compact_measurable (A : set R) : compact A -> measurable A. -Proof. -by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable. -Qed. - -Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : - measurable D -> continuous f -> measurable_fun D f. -Proof. -move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)). -move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //. -exact/cf/interval_open. -Qed. - -Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) : - open D -> {in D, continuous f} -> measurable_fun D f. -Proof. -move=> oD; rewrite -(continuous_open_subspace f oD). -by apply: subspace_continuous_measurable_fun; exact: open_measurable. -Qed. - -Lemma continuous_measurable_fun (f : R -> R) : - continuous f -> measurable_fun setT f. -Proof. -by move=> cf; apply: open_continuous_measurable_fun => //; exact: openT. -Qed. - -End coutinuous_measurable. - -Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : - lower_semicontinuous f -> measurable_fun setT f. -Proof. -move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)). -move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. -by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact. -Qed. - -Section standard_measurable_fun. -Variable R : realType. -Implicit Types D : set R. - -Lemma oppr_measurable D : measurable_fun D -%R. -Proof. -apply: measurable_funTS => /=; apply: continuous_measurable_fun. -exact: opp_continuous. -Qed. - -Lemma normr_measurable D : measurable_fun D (@normr _ R). -Proof. -move=> mD; apply: (measurability (RGenOInfty.measurableE R)) => //. -move=> /= _ [_ [x ->] <-]; apply: measurableI => //. -have [x0|x0] := leP 0 x. - rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic. - by apply: measurableU; apply: measurable_itv. - rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=. - - have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm] => // xr; - rewrite 2!in_itv/=. - + by right; rewrite xr. - + by left; rewrite ltrNr. - - move=> rx /=. - by rewrite ler0_norm 1?ltrNr// (le_trans (ltW rx))// lerNl oppr0. - - by rewrite in_itv /= andbT => xr; rewrite (lt_le_trans _ (ler_norm _)). -rewrite [X in measurable X](_ : _ = setT)// predeqE => r. -by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). -Qed. - -Lemma mulrl_measurable D (k : R) : measurable_fun D ( *%R k). -Proof. -apply: measurable_funTS => /=. -by apply: continuous_measurable_fun; exact: mulrl_continuous. -Qed. - -Lemma mulrr_measurable D (k : R) : measurable_fun D (fun x => x * k). -Proof. -apply: measurable_funTS => /=. -by apply: continuous_measurable_fun; exact: mulrr_continuous. -Qed. - -Lemma exprn_measurable D n : measurable_fun D (fun x => x ^+ n). -Proof. -apply measurable_funTS => /=. -by apply continuous_measurable_fun; exact: exprn_continuous. -Qed. - -End standard_measurable_fun. -#[global] Hint Extern 0 (measurable_fun _ -%R) => - solve [exact: oppr_measurable] : core. -#[global] Hint Extern 0 (measurable_fun _ normr) => - solve [exact: normr_measurable] : core. -#[global] Hint Extern 0 (measurable_fun _ ( *%R _)) => - solve [exact: mulrl_measurable] : core. -#[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) => - solve [exact: exprn_measurable] : core. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `exprn_measurable` instead")] -Notation measurable_exprn := exprn_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrl_measurable` instead")] -Notation measurable_mulrl := mulrl_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrr_measurable` instead")] -Notation measurable_mulrr := mulrr_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppr_measurable` instead")] -Notation measurable_oppr := oppr_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `normr_measurable` instead")] -Notation measurable_normr := normr_measurable (only parsing). - -Section measurable_fun_realType. -Context d (T : measurableType d) (R : realType). -Implicit Types (D : set T) (f g : T -> R). - -Lemma measurable_funD D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). -Proof. -move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //. -move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy. -rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) - ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))). - apply: bigcupT_measurable_rat => q; apply: measurableI. - - by rewrite -preimage_itvoy; apply: mf => //; exact: measurable_itv. - - by rewrite -preimage_itvoy; apply: mg => //; exact: measurable_itv. -rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. - rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h. - exists r => //; rewrite setIACA setIid; split => //; split => /=. - by rewrite h. - by rewrite ltrBlDr addrC -ltrBlDr h. -by rewrite ltrBlDr=> afg; rewrite (lt_le_trans afg)// addrC lerD2r ltW. -Qed. - -Lemma measurable_funB D f g : measurable_fun D f -> - measurable_fun D g -> measurable_fun D (f \- g). -Proof. by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. Qed. - -Lemma measurable_funM D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g). -Proof. -move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2) - \- (fun x => 2%:R^-1 * (f x ^+ 2)) \- (fun x => 2%:R^-1 * (g x ^+ 2))). - apply: measurable_funB; first apply: measurable_funB. - - apply: measurableT_comp => //. - by apply: measurableT_comp (exprn_measurable _) _; exact: measurable_funD. - - apply: measurableT_comp => //. - exact: measurableT_comp (exprn_measurable _) _. - - apply: measurableT_comp => //. - exact: measurableT_comp (exprn_measurable _) _. -rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA. -rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK. -by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE. -Qed. - -Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x < g x). -Proof. -move=> mf mg mD; apply: (measurable_fun_bool true) => //. -under eq_fun do rewrite -subr_gt0. -by rewrite preimage_true -preimage_itvoy; exact: measurable_funB. -Qed. - -Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x <= g x). -Proof. -move=> mf mg mD; apply: (measurable_fun_bool true) => //. -under eq_fun do rewrite -subr_ge0. -by rewrite preimage_true -preimage_itvcy; exact: measurable_funB. -Qed. - -Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x == g x). -Proof. -move=> mf mg. -rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))). - by apply: measurable_and; exact: measurable_fun_ler. -by under eq_fun do rewrite eq_le. -Qed. - -Lemma measurable_maxr D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g). -Proof. -by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; - [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. -Qed. - -Lemma measurable_minr D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). -Proof. -by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; - [exact: measurable_fun_ltr|exact: measurable_funS mf|exact: measurable_funS mg]. -Qed. - -Lemma measurable_fun_sups D (h : (T -> R)^nat) n : - (forall t, D t -> has_ubound (range (h ^~ t))) -> - (forall m, measurable_fun D (h m)) -> - measurable_fun D (fun x => sups (h ^~ x) n). -Proof. -move=> f_ub mf mD; apply: (measurability (RGenOInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr. -by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. -Qed. - -Lemma measurable_fun_infs D (h : (T -> R)^nat) n : - (forall t, D t -> has_lbound (range (h ^~ t))) -> - (forall n, measurable_fun D (h n)) -> - measurable_fun D (fun x => infs (h ^~ x) n). -Proof. -move=> lb_f mf mD; apply: (measurability (RGenInftyO.measurableE R)) =>//. -move=> _ [_ [x ->] <-]; rewrite infs_preimage // setI_bigcupr. -by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. -Qed. - -Lemma measurable_fun_limn_sup D (h : (T -> R)^nat) : - (forall t, D t -> has_ubound (range (h ^~ t))) -> - (forall t, D t -> has_lbound (range (h ^~ t))) -> - (forall n, measurable_fun D (h n)) -> - measurable_fun D (fun x => limn_sup (h ^~ x)). -Proof. -move=> f_ub f_lb mf. -have : {in D, (fun x => inf [set sups (h ^~ x) n | n in [set n | 0 <= n]%N]) - =1 (fun x => limn_sup (h^~ x))}. - move=> t; rewrite inE => Dt; apply/esym/cvg_lim => //. - rewrite [X in _ --> X](_ : _ = inf (range (sups (h^~t)))). - by apply: cvg_sups_inf; [exact: f_ub|exact: f_lb]. - by congr (inf [set _ | _ in _]); rewrite predeqE. -move/eq_measurable_fun; apply; apply: measurable_fun_infs => //. - move=> t Dt; have [M hM] := f_lb _ Dt; exists M => _ [m /= nm <-]. - rewrite (@le_trans _ _ (h m t)) //; first by apply hM => /=; exists m. - by apply: sup_ubound; [exact/has_ubound_sdrop/f_ub|exists m => /=]. -by move=> k; exact: measurable_fun_sups. -Qed. - -Lemma measurable_fun_cvg D (h : (T -> R)^nat) f : - (forall m, measurable_fun D (h m)) -> (forall x, D x -> h ^~ x @ \oo --> f x) -> - measurable_fun D f. -Proof. -move=> mf_ f_f; have fE x : D x -> f x = limn_sup (h ^~ x). - move=> Dx; have /cvg_lim <-// := @cvg_sups _ (h ^~ x) (f x) (f_f _ Dx). -apply: (@eq_measurable_fun _ _ _ _ D (fun x => limn_sup (h ^~ x))). - by move=> x; rewrite inE => Dx; rewrite -fE. -apply: (@measurable_fun_limn_sup _ h) => // t Dt. -- by apply/bounded_fun_has_ubound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. -- by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. -Qed. - -Lemma measurable_indic D (U : set T) : measurable U -> - measurable_fun D (\1_U : _ -> R). -Proof. -move=> mU mD /= Y mY. -have [Y0|Y0] := pselect (Y 0%R); have [Y1|Y1] := pselect (Y 1%R). -- rewrite [X in measurable X](_ : _ = D)//. - by apply/seteqP; split => //= r Dr /=; rewrite indicE; case: (_ \in _). -- rewrite [X in measurable (_ `&` X)](_ : _ = ~` U)//. - by apply: measurableI => //; exact: measurableC. - apply/seteqP; split => [//= r /= + Ur|r Ur]; rewrite /= indicE. - by rewrite mem_set. - by rewrite memNset. -- rewrite [X in measurable (_ `&` X)](_ : _ = U); first exact: measurableI. - apply/seteqP; split => [//= r /=|r Ur]; rewrite /= indicE. - by have [//|Ur] := pselect (U r); rewrite memNset. - by rewrite mem_set. -- rewrite [X in measurable X](_ : _ = set0)//. - by apply/seteqP; split => // r /= -[_]; rewrite indicE; case: (_ \in _). -Qed. - -Lemma measurable_indicP D : measurable D <-> measurable_fun setT (\1_D : _ -> R). -Proof. -split=> [|m1]; first exact: measurable_indic. -have -> : D = (\1_D : _ -> R) @^-1` `]0, +oo[. - apply/seteqP; split => t/=. - by rewrite indicE => /mem_set ->; rewrite in_itv/= ltr01. - by rewrite in_itv/= andbT indicE ltr0n; have [/set_mem|//] := boolP (t \in D). -by rewrite -[_ @^-1` _]setTI; exact: m1. -Qed. - -End measurable_fun_realType. -#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")] -Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing). - -Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R). -Proof. -rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. - by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=; - rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. -apply/measurable_funU => //; split. -- apply/measurable_restrictT => //=. - rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE. - by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. -- have : {in `]0, +oo[%classic, continuous (@ln R)}. - by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. - rewrite -continuous_open_subspace; last exact: interval_open. - by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv. -Qed. -#[global] Hint Extern 0 (measurable_fun _ (@ln _)) => - solve [apply: measurable_ln] : core. -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_ln` instead")] -Notation measurable_fun_ln := measurable_ln (only parsing). - -Lemma measurable_expR (R : realType) : measurable_fun [set: R] expR. -Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. -#[global] Hint Extern 0 (measurable_fun _ expR) => - solve [apply: measurable_expR] : core. - -Lemma natmul_measurable {R : realType} D n : - measurable_fun D (fun x : R => x *+ n). -Proof. -under eq_fun do rewrite -mulr_natr. -by do 2 apply: measurable_funM => //. -Qed. - -Lemma measurable_funX d (T : measurableType d) {R : realType} D (f : T -> R) n : - measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). -Proof. -move=> mf. -exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). -Qed. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] -Notation measurable_fun_pow := measurable_funX (only parsing). - -Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). -Proof. -apply: measurable_fun_if => //. -- apply: (measurable_fun_bool true). - rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//. - by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. -- rewrite setTI; apply: measurableT_comp => //. - rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp. - by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP. -Qed. -#[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) => - solve [apply: measurable_powR] : core. - -Lemma measurable_powRr {R : realType} b : measurable_fun [set: R] (@powR R b). -Proof. -rewrite /powR; apply: measurable_fun_if => //. -- rewrite preimage_true setTI/=. - case: (b == 0); rewrite ?set_true ?set_false. - + by apply: measurableT_comp => //; exact: measurable_fun_eqr. - + exact: measurable_fun_set0. -- rewrite preimage_false setTI; apply: measurableT_comp => //. - exact: mulrr_measurable. -Qed. - -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")] -Notation measurable_fun_max := measurable_maxr (only parsing). - -Module NGenCInfty. -Section ngencinfty. -Implicit Types x y z : nat. - -Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic]. - -Lemma measurable_itv_bnd_infty b x : - G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. -Proof. -case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty. -rewrite [X in measurable X](_ : _ = - \bigcup_(k in [set k | k >= x]%N) `[k.+1, +oo[%classic); last first. - apply/seteqP; split => [z /=|/= z [t/= xt]]. - rewrite in_itv/= andbT => xz; exists z.-1 => /=. - by rewrite -ltnS//=; case: z xz. - by case: z xz => //= z xz; rewrite in_itv/= lexx andbT. - by rewrite !in_itv/= !andbT; apply: lt_le_trans; rewrite ltEnat/= ltnS. -rewrite bigcup_mkcond; apply: bigcupT_measurable => k. -by case: ifPn => //= _; apply: sub_sigma_algebra; eexists; reflexivity. -Qed. - -Lemma measurable_itv_bounded a b y : a != +oo%O -> - G.-sigma.-measurable [set` Interval a (BSide b y)]. -Proof. -case: a => [a r _|[_|//]]. - by rewrite set_itv_splitD; apply: measurableD; apply: measurable_itv_bnd_infty. -by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. -Qed. - -Lemma measurableE : @measurable _ nat = G.-sigma.-measurable. -Proof. -rewrite eqEsubset; split => [A mA|A]; last exact: smallest_sub. -rewrite (_ : A = \bigcup_(i in A) `[i, i.+1[%classic). - by apply: bigcup_measurable => k Ak; exact: measurable_itv_bounded. -apply/seteqP; split => [x Ax|x [k Ak]]. - by exists x => //=; rewrite in_itv/= lexx/= ltEnat /= ltnS. -by rewrite /= in_itv/= leEnat ltEnat /= ltnS -eqn_leq => /eqP <-. -Qed. - -End ngencinfty. -End NGenCInfty. - -Section measurable_fun_nat. -Context d (T : measurableType d). -Implicit Types (D : set T) (f g : T -> nat). - -Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x + g x)%N. -Proof. -move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. -move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy. -rewrite [X in measurable X](_ : _ = \bigcup_q - ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))). - apply: bigcupT_measurable => q; apply: measurableI. - - by rewrite -preimage_itvcy; exact: mf. - - by rewrite -preimage_itvcy; exact: mg. -rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[?]]. -- move=> afxgx; exists (a - g x)%N => //=; split; split => //. - by rewrite leEnat leq_subLR// addnC -leEnat. - have [gxa|gxa] := leqP (g x) a; first by rewrite subKn. - by move/ltnW : (gxa); rewrite -subn_eq0 => /eqP ->; rewrite subn0 ltW. -- rewrite leEnat leq_subLR => arg; split => //. - by rewrite (leq_trans arg)// leq_add2r. -Qed. - -Lemma measurable_fun_maxn D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => maxn (f x) (g x)). -Proof. -move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. -move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ = - ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))). - apply: measurableU. - - by rewrite -preimage_itvcy; exact: mf. - - by rewrite -preimage_itvcy; exact: mg. -rewrite predeqE => x; split => [[Dx /=]|]. -- by rewrite in_itv/= andbT; have [fg agx|gf afx] := leqP (f x) (g x); tauto. -- move=> [[Dx /= afx]|[Dx /= agx]]. - + rewrite in_itv/= andbT; split => //. - by rewrite (le_trans afx)// leEnat leq_maxl. - + rewrite in_itv/= andbT; split => //. - by rewrite (le_trans agx)// leEnat leq_maxr. -Qed. - -Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N -> - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x - g x)%N. -Proof. -move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. -move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy. -rewrite [X in measurable X](_ : _ = \bigcup_q - ((D `&` [set x | maxn a q <= f x]%O) `&` - (D `&` [set x | g x <= (q - a)%N]%O))). - apply: bigcupT_measurable => q; apply: measurableI. - - by rewrite -preimage_itvcy; exact: mf. - - by rewrite -preimage_itvNyc; exact: mg. -rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[_]]. -- move=> afxgx; exists (g x + a)%N => //; split; split => //=. - rewrite leEnat; have /maxn_idPr -> := leq_addl (g x) a. - by rewrite -leq_subRL. - by rewrite leEnat addnK. -- rewrite leEnat => gxra; split => //; rewrite -(leq_add2r (g x)) subnK//. - have [afx|afx] := leqP a (f x). - rewrite -(@leq_sub2rE a)// addnC addnK (leq_trans gxra)// leq_sub2r//. - by rewrite (leq_trans _ rfx)//; exact: leq_maxr. - move: gxra; rewrite -(leq_add2l a) subnKC//; last first. - by have := leq_ltn_trans rfx afx; rewrite ltnNge leq_maxl. - by move=> /leq_trans; apply; rewrite (leq_trans _ rfx)//; exact: leq_maxr. -Qed. - -Lemma measurable_fun_subn D f g : measurable_fun D f -> - measurable_fun D g -> measurable_fun D (fun x => f x - g x)%N. -Proof. -move=> mf mg. -rewrite [X in measurable_fun _ X](_ : _ = fun x => (maxn (f x) (g x) - g x)%N). - apply: measurable_fun_subn' => //; last exact: measurable_fun_maxn. - by move=> t; rewrite leq_maxr. -apply/funext => x; have [//|gf] := leqP (g x) (f x). -by apply/eqP; rewrite subnn subn_eq0// ltnW. -Qed. - -Lemma measurable_fun_ltn D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x < g x)%N. -Proof. -move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. -- have -> : (fun x => f x < g x)%O = (fun x => 0%N < (g x - f x)%N)%O. - apply/funext => n; apply/idP/idP. - by rewrite !ltEnat /ltn/= => fg; rewrite subn_gt0. - by rewrite !ltEnat /ltn/= => fg; rewrite -subn_gt0. - by rewrite preimage_true -preimage_itvoy; exact: measurable_fun_subn. -- under eq_fun do rewrite ltnNge. - rewrite preimage_false set_predC setCK. - rewrite [X in _ `&` X](_ : _ = \bigcup_(i in range f) - ([set y | g y <= i]%O `&` [set t | i <= f t]%O)). - rewrite setI_bigcupr; apply: bigcup_measurable => k fk. - rewrite setIIr; apply: measurableI => //. - + by rewrite -preimage_itvNyc; exact: mg. - + by rewrite -preimage_itvcy; exact: mf. - apply/funext => n/=. - suff : (g n <= f n)%N <-> - (\bigcup_(i in range f) ([set y | g y <= i]%O `&` [set t | i <= f t]%O)) n. - by move/propext. - split=> [gfn|[k [t _ <- []]] /=]. - by exists (f n) => //; split => /=. - by move=> /leq_trans; apply. -- by rewrite preimage_set0 setI0. -- by rewrite preimage_setT setIT. -Qed. - -Lemma measurable_fun_leq D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x <= g x)%N. -Proof. -move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. -- rewrite preimage_true [X in _ `&` X](_ : _ = - \bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)). - rewrite setI_bigcupr; apply: bigcup_measurable => k fk. - rewrite setIIr; apply: measurableI => //. - + by rewrite -preimage_itvNyc; exact: mf. - + by rewrite -preimage_itvcy; exact: mg. - apply/funext => n/=. - suff : (f n <= g n)%N <-> - (\bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)) n. - by move/propext. - split=> [gfn|[k [t _ <- []]] /=]. - by exists (g n) => //; split => /=. - by move=> /leq_trans; apply. -- under eq_fun do rewrite leqNgt. - by rewrite preimage_false set_predC setCK; exact: measurable_fun_ltn. -- by rewrite preimage_set0 setI0. -- by rewrite preimage_setT setIT. -Qed. - -Lemma measurable_fun_eqn D f g : measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x == g x). -Proof. -move=> mf mg. -rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))%N). - by apply: measurable_and; exact: measurable_fun_leq. -by under eq_fun do rewrite eq_le. -Qed. - -End measurable_fun_nat. - -Section standard_emeasurable_fun. -Variable R : realType. - -Lemma EFin_measurable (D : set R) : measurable_fun D EFin. -Proof. -move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. -move=> /= _ [_ [x ->]] <-; apply: measurableI => //. -by rewrite preimage_itvoy EFin_itv; exact: measurable_itv. -Qed. - -Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. -Proof. -move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. -move=> /= _ [_ [x ->] <-]. -rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. -apply: measurableU; last first. - by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. -apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). - by rewrite -[X in measurable X]setTI; exact: normr_measurable. -exists set0; first by constructor. -rewrite setU0 predeqE => -[y| |]; split => /= => -[r]; - rewrite ?/= /= ?in_itv /= ?andbT => xr//. - + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry. - + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry. -Qed. - -Lemma oppe_measurable (D : set (\bar R)) : - measurable_fun D (-%E : \bar R -> \bar R). -Proof. -move=> mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite (_ : _ @^-1` _ = `]-oo, (- x)%:E]%classic). - by apply: measurableI => //; exact: emeasurable_itv. -by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv leeNr. -Qed. - -End standard_emeasurable_fun. -#[global] Hint Extern 0 (measurable_fun _ abse) => - solve [exact: abse_measurable] : core. -#[global] Hint Extern 0 (measurable_fun _ EFin) => - solve [exact: EFin_measurable] : core. -#[global] Hint Extern 0 (measurable_fun _ -%E) => - solve [exact: oppe_measurable] : core. -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppe_measurable` instead")] -Notation measurable_oppe := oppe_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `abse_measurable` instead")] -Notation measurable_abse := abse_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `EFin_measurable` instead")] -Notation measurable_EFin := EFin_measurable (only parsing). -#[deprecated(since="mathcomp-analysis 1.4.0", note="use `natmul_measurable` instead")] -Notation measurable_natmul := natmul_measurable (only parsing). - -(* NB: real-valued function *) -Lemma measurable_EFinP d (T : measurableType d) (R : realType) (D : set T) - (g : T -> R) : - measurable_fun D (EFin \o g) <-> measurable_fun D g. -Proof. -split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp. -rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)). - by apply: mf => //; exists A => //; exists set0; [constructor|rewrite setU0]. -congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. -by move=> ? ?; exact: preimage_image. -Qed. -#[deprecated(since="mathcomp-analysis 1.6.0", note="use `measurable_EFinP` instead")] -Notation EFin_measurable_fun := measurable_EFinP (only parsing). - -Lemma measurable_fun_dirac - d {T : measurableType d} {R : realType} D (U : set T) : - measurable U -> measurable_fun D (fun x => \d_x U : \bar R). -Proof. by move=> /measurable_indic/measurable_EFinP. Qed. - -Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) : - measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f). -Proof. -move=> mf;rewrite (_ : er_map _ = - fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. - by apply: funext=> -[]. -apply: measurable_fun_ifT => //=. -+ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num. -+ exact/measurable_EFinP/measurableT_comp. -Qed. -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] -Notation measurable_fun_er_map := measurable_er_map (only parsing). - -Section emeasurable_fun. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Implicit Types (D : set T). - -Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) : - (forall n, measurable_fun D (f n)) -> - forall n, measurable_fun D (fun x => einfs (f ^~ x) n). -Proof. -move=> mf n mD. -apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=. -by apply: bigcap_measurableType => ? ?; exact/mf/emeasurable_itv. -Qed. - -Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) : - (forall n, measurable_fun D (f n)) -> - forall n, measurable_fun D (fun x => esups (f ^~ x) n). -Proof. -move=> mf n mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr. -by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv. -Qed. - -Lemma measurable_maxe D (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => maxe (f x) (g x)). -Proof. -move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ = - (D `&` f @^-1` `[x%:E, +oo[) `|` (D `&` g @^-1` `[x%:E, +oo[)); last first. - rewrite predeqE => t /=; split. - by rewrite !/= /= !in_itv /= !andbT le_max => -[Dx /orP[|]]; - tauto. - by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_max; - move=> [Dx ->]//; rewrite orbT. -by apply: measurableU; [exact/mf/emeasurable_itv| exact/mg/emeasurable_itv]. -Qed. - -Lemma measurable_funepos D (f : T -> \bar R) : - measurable_fun D f -> measurable_fun D f^\+. -Proof. by move=> mf; rewrite unlock; exact: measurable_maxe. Qed. - -Lemma measurable_funeneg D (f : T -> \bar R) : - measurable_fun D f -> measurable_fun D f^\-. -Proof. -move=> mf; rewrite unlock; apply: measurable_maxe => //. -exact: measurableT_comp. -Qed. - -Lemma measurable_mine D (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => mine (f x) (g x)). -Proof. -move=> mf mg; rewrite (_ : (fun _ => _) = (fun x => - maxe (- f x) (- g x))). - apply: measurableT_comp => //. - by apply: measurable_maxe; exact: measurableT_comp. -by rewrite funeqE => x; rewrite oppe_max !oppeK. -Qed. - -Lemma measurable_fun_limn_esup D (f : (T -> \bar R)^nat) : - (forall n, measurable_fun D (f n)) -> - measurable_fun D (fun x => limn_esup (f ^~ x)). -Proof. -move=> mf mD; rewrite (_ : (fun _ => _) = - (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])). - by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups. -rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //. -rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))). - exact: cvg_esups_inf. -by congr (ereal_inf [set _ | _ in _]); rewrite predeqE. -Qed. - -Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) : - (forall m, measurable_fun D (f_ m)) -> - (forall x, D x -> f_ ^~ x @ \oo --> f x) -> measurable_fun D f. -Proof. -move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x). - rewrite limn_esup_lim. - by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx). -apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //. - by move=> x; rewrite inE => Dx; rewrite fE. -exact: measurable_fun_limn_esup. -Qed. -End emeasurable_fun. -Arguments emeasurable_fun_cvg {d T R D} f_. - -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurableT_comp` instead")] -Notation emeasurable_funN := measurableT_comp (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")] -Notation emeasurable_fun_max := measurable_maxe (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mine` instead")] -Notation emeasurable_fun_min := measurable_mine (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")] -Notation emeasurable_fun_funepos := measurable_funepos (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funeneg` instead")] -Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")] -Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing). - -Section open_itv_cover. -Context {R : realType}. -Implicit Types (A : set R). -Local Open Scope ereal_scope. - -Let l := (@wlength R idfun). - -Lemma outer_measure_open_itv_cover A : (l^* A)%mu = - ereal_inf [set \sum_(k _ /= [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. - -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 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. - (* 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. *) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v new file mode 100644 index 0000000000..8e9fb289f1 --- /dev/null +++ b/theories/measurable_realfun.v @@ -0,0 +1,1704 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import finmap fingroup perm rat archimedean. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals ereal signed. +From mathcomp Require Import topology numfun tvs normedtype function_spaces. +From HB Require Import structures. +From mathcomp Require Import sequences esum measure real_interval realfun exp. +From mathcomp Require Export lebesgue_stieltjes_measure. + +(**md**************************************************************************) +(* # Measurable Functions over $\mathbb{R}$ and $\overline{\mathbb{R}}$ *) +(* *) +(* This file further develops the theory of measurable functions (including *) +(* Egorov's theorem). *) +(* *) +(* Main references: *) +(* - Daniel Li, Intégration et applications, 2016 *) +(* - Achim Klenke, Probability Theory 2nd edition, 2014 *) +(* *) +(* ``` *) +(* completed_algebra_gen == generator of the completed Lebesgue *) +(* sigma-algebra *) +(* ps_infty == inductive definition of the powerset *) +(* {0, {-oo}, {+oo}, {-oo,+oo}} *) +(* emeasurable G == sigma-algebra over \bar R built out of the *) +(* measurables G of a sigma-algebra over R *) +(* ``` *) +(* *) +(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) +(* of equivalence between the sigma-algebra generated by open-closed *) +(* intervals and the sigma-algebras generated by open rays, closed rays, and *) +(* open intervals. *) +(* *) +(* The module NGenCInfty provides a proof of equivalence between the *) +(* sigma-algebra for natural numbers and the sigma-algebra generated by *) +(* closed rays. *) +(* *) +(* The modules ErealGenOInfty, ErealGenCInfty, ErealGenInftyO provide proofs *) +(* of equivalence between emeasurable and the sigma-algebras generated by *) +(* open rays and closed rays. *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Definition completed_algebra_gen d {T : semiRingOfSetsType d} {R : realType} + (mu : set T -> \bar R) : set _ := + [set A `|` N | A in d.-measurable & N in mu.-negligible]. + +Section ps_infty. +Context {T : Type}. +Local Open Scope ereal_scope. + +Inductive ps_infty : set \bar T -> Prop := +| ps_infty0 : ps_infty set0 +| ps_ninfty : ps_infty [set -oo] +| ps_pinfty : ps_infty [set +oo] +| ps_inftys : ps_infty [set -oo; +oo]. + +Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo]. +Proof. +split => [[]//|Aoo]. +by have [] := subset_set2 Aoo; move=> ->; constructor. +Qed. + +Lemma setCU_Efin (A : set T) (B : set \bar T) : ps_infty B -> + ~` (EFin @` A) `&` ~` B = (EFin @` ~` A) `|` ([set -oo%E; +oo%E] `&` ~` B). +Proof. +move=> ps_inftyB. +have -> : ~` (EFin @` A) = EFin @` (~` A) `|` [set -oo; +oo]%E. + by rewrite EFin_setC setDKU // => x [|] -> -[]. +rewrite setIUl; congr (_ `|` _); rewrite predeqE => -[x| |]; split; try by case. +by move=> [] x' Ax' [] <-{x}; split; [exists x'|case: ps_inftyB => // -[]]. +Qed. + +End ps_infty. + +Section salgebra_ereal. +Variables (R : realType) (G : set (set R)). +Let measurableR : set (set R) := G.-sigma.-measurable. + +Definition emeasurable : set (set \bar R) := + [set EFin @` A `|` B | A in measurableR & B in ps_infty]. + +Lemma emeasurable0 : emeasurable set0. +Proof. +exists set0; first exact: measurable0. +by exists set0; rewrite ?setU0// ?image_set0//; constructor. +Qed. + +Lemma emeasurableC (X : set \bar R) : emeasurable X -> emeasurable (~` X). +Proof. +move => -[A mA] [B PooB <-]; rewrite setCU setCU_Efin //. +exists (~` A); [exact: measurableC | exists ([set -oo%E; +oo%E] `&` ~` B) => //]. +case: PooB. +- by rewrite setC0 setIT; constructor. +- rewrite setIUl setICr set0U -setDE. + have [_ ->] := @setDidPl (\bar R) [set +oo%E] [set -oo%E]; first by constructor. + by rewrite predeqE => x; split => // -[->]. +- rewrite setIUl setICr setU0 -setDE. + have [_ ->] := @setDidPl (\bar R) [set -oo%E] [set +oo%E]; first by constructor. + by rewrite predeqE => x; split => // -[->]. +- by rewrite setICr; constructor. +Qed. + +Lemma bigcupT_emeasurable (F : (set \bar R)^nat) : + (forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)). +Proof. +move=> mF; pose P := fun i j => measurableR j.1 /\ ps_infty j.2 /\ + F i = [set x%:E | x in j.1] `|` j.2. +have [f fi] : {f : nat -> (set R) * (set \bar R) & forall i, P i (f i) }. + by apply: choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x, y). +exists (\bigcup_i (f i).1). + by apply: bigcupT_measurable => i; exact: (fi i).1. +exists (\bigcup_i (f i).2). + apply/ps_inftyP => x [n _] fn2x. + have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n. + exact. +rewrite [RHS](@eq_bigcupr _ _ _ _ + (fun i => [set x%:E | x in (f i).1] `|` (f i).2)); last first. + by move=> i; have [_ []] := fi i. +rewrite bigcupU; congr (_ `|` _). +rewrite predeqE => i /=; split=> [[r [n _ fn1r <-{i}]]|[n _ [r fn1r <-{i}]]]; + by [exists n => //; exists r | exists r => //; exists n]. +Qed. + +Definition ereal_isMeasurable : isMeasurable default_measure_display (\bar R) := + isMeasurable.Build _ _ + emeasurable0 emeasurableC bigcupT_emeasurable. + +End salgebra_ereal. + +Section puncture_ereal_itv. +Variable R : realDomainType. +Implicit Types (y : R) (b : bool). +Local Open Scope ereal_scope. + +Lemma punct_eitv_bndy b y : [set` Interval (BSide b y%:E) +oo%O] = + EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo]. +Proof. +rewrite predeqE => x; split; rewrite /= in_itv andbT. +- move: x => [x| |] yxb; [|by right|by case: b yxb]. + by left; exists x => //; rewrite in_itv /= andbT; case: b yxb. +- move=> [[r]|->]. + + by rewrite in_itv /= andbT => yxb <-; case: b yxb. + + by case: b => /=; rewrite ?(ltry, leey). +Qed. + +Lemma punct_eitv_Nybnd b y : [set` Interval -oo%O (BSide b y%:E)] = + [set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)]. +Proof. +rewrite predeqE => x; split; rewrite /= in_itv. +- move: x => [x| |] yxb; [|by case: b yxb|by left]. + by right; exists x => //; rewrite in_itv /= andbT; case: b yxb. +- move=> [->|[r]]. + + by case: b => /=; rewrite ?(ltNyr, leNye). + + by rewrite in_itv /= => yxb <-; case: b yxb. +Qed. + +Lemma punct_eitv_setTR : range (@EFin R) `|` [set +oo] = [set~ -oo]. +Proof. +rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. +by move=> [x| |] //= _; [left; exists x|right]. +Qed. + +Lemma punct_eitv_setTL : range (@EFin R) `|` [set -oo] = [set~ +oo]. +Proof. +rewrite eqEsubset; split => [a [[a' _ <-]|->]|] //. +by move=> [x| |] //= _; [left; exists x|right]. +Qed. + +End puncture_ereal_itv. + +Section salgebra_R_ssets. +Variable R : realType. + +Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). +Definition measurableR : set (set R) := + (R.-ocitv.-measurable).-sigma.-measurable. + +HB.instance Definition _ := Pointed.on R. +HB.instance Definition R_isMeasurable : + isMeasurable default_measure_display R := + @isMeasurable.Build _ measurableTypeR measurableR + measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +(*HB.instance (Real.sort R) R_isMeasurable.*) + +Lemma measurable_set1 (r : R) : measurable [set r]. +Proof. +rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact/is_ocitv. +Qed. +#[local] Hint Resolve measurable_set1 : core. + +Lemma measurable_itv (i : interval R) : measurable [set` i]. +Proof. +have moc (a b : R) : measurable `]a, b]. + by apply: sub_sigma_algebra; apply: is_ocitv. +have mopoo (x : R) : measurable `]x, +oo[. + by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable. +have mnooc (x : R) : measurable `]-oo, x]. + by rewrite -setCitvr; exact/measurableC. +have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. + case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D. + by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF. +have moo (a b : R) : measurable `]a, b[. + by rewrite ooE; exact: measurableD. +have mcc (a b : R) : measurable `[a, b]. + case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU1itv//; apply/measurableU. +have mco (a b : R) : measurable `[a, b[. + case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU1itv//; apply/measurableU. +have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. + by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx. +case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. +- by rewrite -setU1itv//; exact/measurableU. +- by rewrite oooE; exact/measurableD. +- by rewrite set_itv_infty_infty. +Qed. +#[local] Hint Resolve measurable_itv : core. + +Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `[x, y[ f. +Proof. +have [xy|yx _] := ltP x y; last first. + by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0. +move: b0 b1 => [|] [|] // mf. +- apply: measurable_funS mf => //; exact: subset_itv_co_cc. +- rewrite -setU1itv//= measurable_funU//; split => //. + exact: measurable_fun_set1. +- rewrite -setU1itv//= measurable_funU//; split. + exact: measurable_fun_set1. + by apply: measurable_funS mf => //; exact: subset_itv_oo_oc. +Qed. + +Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `]x, y] f. +Proof. +have [xy|yx _] := ltP x y; last first. + by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0. +move: b0 b1 => [|] [|] // mf. +- rewrite -setUitv1//= measurable_funU//; split. + by apply: measurable_funS mf => //; exact: subset_itv_oo_co. + exact: measurable_fun_set1. +- by apply: measurable_funS mf => //; exact: subset_itv_oc_cc. +- rewrite -setUitv1//= measurable_funU//; split => //. + exact: measurable_fun_set1. +Qed. + +Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `[x, y] f. +Proof. +move=> mf. +have [xy|] := ltP x y; last first. + rewrite le_eqVlt => /predU1P[->|ba]. + by rewrite set_itv1; exact: measurable_fun_set1. + rewrite set_itv_ge//; first exact: measurable_fun_set0. + by rewrite -leNgt bnd_simp. +rewrite -setUitv1//=; last by rewrite bnd_simp ltW. + rewrite measurable_funU//; split => //. + exact: measurable_fun_itv_co mf. +exact: measurable_fun_set1. +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). +Proof. +by move=> mA; exists A => //; exists set0; [constructor|rewrite setU0]. +Qed. + +Lemma emeasurable_set1 (x : \bar R) : measurable [set x]. +Proof. +case: x => [r| |]. +- by rewrite -image_set1; apply: measurable_image_EFin; apply: measurable_set1. +- exists set0 => //; [exists [set +oo%E]; [by constructor|]]. + by rewrite image_set0 set0U. +- exists set0 => //; [exists [set -oo%E]; [by constructor|]]. + by rewrite image_set0 set0U. +Qed. +#[local] Hint Resolve emeasurable_set1 : core. + +Let emeasurable_itv_bndy b (y : \bar R) : + measurable [set` Interval (BSide b y) +oo%O]. +Proof. +move: y => [y| |]. +- exists [set` Interval (BSide b y) +oo%O]; first exact: measurable_itv. + by exists [set +oo%E]; [constructor|rewrite -punct_eitv_bndy]. +- by case: b; rewrite ?itv_oyy ?itv_cyy. +- case: b; first by rewrite itv_cNyy. + by rewrite itv_oNyy; exact/measurableC. +Qed. + +Let emeasurable_itv_Nybnd b (y : \bar R) : + measurable [set` Interval -oo%O (BSide b y)]. +Proof. by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bndy. Qed. + +Lemma emeasurable_itv (i : interval (\bar R)) : + measurable ([set` i]%classic : set \bar R). +Proof. +rewrite -[X in measurable X]setCK; apply: measurableC. +rewrite set_interval.setCitv /=; apply: measurableU => [|]. +- by move: i => [[b1 i1|[|]] i2] /=; rewrite ?set_interval.set_itvE. +- by move: i => [i1 [b2 i2|[|]]] /=; rewrite ?set_interval.set_itvE. +Qed. + +Lemma measurable_image_fine (X : set \bar R) : measurable X -> + measurable [set fine x | x in X `\` [set -oo; +oo]%E]. +Proof. +case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. +- rewrite setU0 => <-{X}. + rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. + by move=> Yr; exists r%:E; split => [|[]//]; exists r. +- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + move=> [x [[[x' Yx' <- _ <-//]|]]]. + by move=> <-; rewrite not_orP => -[]/(_ erefl). + by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. +- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. + by move=> ->; rewrite not_orP => -[_]/(_ erefl). + by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. +- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. + by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. + by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. +Qed. + +Lemma measurable_ball (x : R) e : measurable (ball x e). +Proof. by rewrite ball_itv; exact: measurable_itv. Qed. + +Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r). +Proof. +have [r0|r0] := leP r 0; first by rewrite closed_ball0. +rewrite closed_ball_itv//. +Qed. + +End salgebra_R_ssets. +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| + apply: emeasurable_set1] : core. +#[global] +Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. +#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] +Notation emeasurable_itv_bnd_pinfty := emeasurable_itv (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] +Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing). + +Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D -> + measurable_fun D fine. +Proof. +move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then + D `&` ((EFin @` B) `|` [set -oo; +oo]%E) else D `&` EFin @` B); last first. + apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]]. + - by case: ifPn => _; split => //; left; exists r. + - by rewrite mem_set//; split => //; right; right. + - by rewrite mem_set//; split => //; right; left. + - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr. + - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. + - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. +case: ifPn => B0; apply/measurableI => //; last exact: measurable_image_EFin. +by apply: measurableU; [exact: measurable_image_EFin|exact: measurableU]. +Qed. +#[global] Hint Extern 0 (measurable_fun _ fine) => + solve [exact: fine_measurable] : core. +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `fine_measurable` instead")] +Notation measurable_fine := fine_measurable (only parsing). + +Section measurable_fun_measurable. +Local Open Scope ereal_scope. +Context d (T : sigmaRingType d) (R : realType). +Variables (D : set T) (f : T -> \bar R). +Hypotheses (mD : measurable D) (mf : measurable_fun D f). +Implicit Types y : \bar R. + +Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]). +Proof. by rewrite -preimage_itvcy; exact/mf/emeasurable_itv. Qed. + +Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]). +Proof. by rewrite -preimage_itvoy; exact/mf/emeasurable_itv. Qed. + +Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]). +Proof. by rewrite -preimage_itvNyo; exact/mf/emeasurable_itv. Qed. + +Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]). +Proof. by rewrite -preimage_itvNyc; exact/mf/emeasurable_itv. Qed. + +Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]). +Proof. +rewrite [X in measurable X](_ : _ = + \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))). + apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA. + exact/measurableI/emeasurable_fun_infty_c/emeasurable_fun_c_infty. +rewrite predeqE => t; split => [/= [Dt ft]|]. + exists `|ceil `|fine (f t)| |%N => //=; split=> //; split. + rewrite -[leRHS](fineK ft) lee_fin lerNl pmulrn abszE ceil_ge_int ger0_norm. + by rewrite ceil_le// -normrN ler_norm. + by rewrite -(ceil0 R) ceil_le. + rewrite -[leLHS](fineK ft) lee_fin pmulrn abszE ceil_ge_int ger0_norm. + by rewrite ceil_le// ler_norm. + by rewrite -(ceil0 R) ceil_le. +move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. +by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. +Qed. + +Lemma emeasurable_neq y : measurable (D `&` [set x | f x != y]). +Proof. +rewrite (_ : [set x | f x != y] = f @^-1` (setT `\ y)). + exact/mf/measurableD. +rewrite predeqE => t; split; last by rewrite /preimage /= => -[_ /eqP]. +by rewrite /= => ft0; rewrite /preimage /=; split => //; exact/eqP. +Qed. + +End measurable_fun_measurable. + +Module RGenOInfty. +Section rgenoinfty. +Variable R : realType. +Implicit Types x y z : R. + +Definition G := [set A | exists x, A = `]x, +oo[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; last by apply: sub_sigma_algebra; eexists; reflexivity. +rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k. +by apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b x : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b x)]. +Proof. +case: a => [a r _|[_|//]]. + by rewrite set_itv_splitD; apply: measurableD => //; + exact: measurable_itv_bnd_infty. +by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; exact: measurable_itv_bounded. +apply: smallest_sub; first exact: smallest_sigma_algebra. +by move=> A' /= [x ->]; exact: measurable_itv. +Qed. + +End rgenoinfty. +End RGenOInfty. + +Module RGenInftyO. +Section rgeninftyo. +Variable R : realType. +Implicit Types x y z : R. + +Definition G := [set A | exists x, A = `]-oo, x[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. +Proof. +case: b; first by apply sub_sigma_algebra; eexists; reflexivity. +rewrite -setCitvr itv_o_inftyEbigcup; apply/measurableC/bigcupT_measurable => n. +rewrite -setCitvl; apply: measurableC. +by apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b x : a != -oo%O -> + G.-sigma.-measurable [set` Interval (BSide b x) a]. +Proof. +case: a => [a r _|[//|_]]. + by rewrite set_itv_splitD; apply/measurableD => //; + rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty. +by rewrite -setCitvl; apply: measurableC; apply: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; apply: measurable_itv_bounded. +apply: smallest_sub; first exact: smallest_sigma_algebra. +by move=> A' /= [x ->]; apply: measurable_itv. +Qed. + +End rgeninftyo. +End RGenInftyO. + +Module RGenCInfty. +Section rgencinfty. +Variable R : realType. +Implicit Types x y z : R. + +Definition G : set (set R) := [set A | exists x, A = `[x, +oo[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty. +rewrite itv_o_inftyEbigcup; apply: bigcupT_measurable => k. +by apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b y : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b y)]. +Proof. +case: a => [a r _|[_|//]]. + rewrite set_itv_splitD. + by apply: measurableD; apply: measurable_itv_bnd_infty. +by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; apply: measurable_itv_bounded. +apply: smallest_sub; first exact: smallest_sigma_algebra. +by move=> A' /= [x ->]; apply: measurable_itv. +Qed. + +End rgencinfty. +End RGenCInfty. + +Module RGenOpens. +Section rgenopens. +Variable R : realType. +Implicit Types x y z : R. + +Definition G := [set A | exists x y, A = `]x, y[%classic]. + +Local Lemma measurable_itvoo x y : G.-sigma.-measurable `]x, y[%classic. +Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. + +Local Lemma measurable_itv_o_infty x : G.-sigma.-measurable `]x, +oo[%classic. +Proof. +rewrite itv_bnd_inftyEbigcup; apply: bigcupT_measurable => i. +exact: measurable_itvoo. +Qed. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; last exact: measurable_itv_o_infty. +rewrite itv_c_inftyEbigcap; apply: bigcapT_measurable => k. +exact: measurable_itv_o_infty. +Qed. + +Lemma measurable_itv_infty_bnd b x : + G.-sigma.-measurable [set` Interval -oo%O (BSide b x)]. +Proof. +by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty. +Qed. + +Lemma measurable_itv_bounded a x b y : + G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)]. +Proof. +move: a b => [] []; rewrite -[X in measurable X]setCK setCitv; + apply: measurableC; apply: measurableU; try solve[ + exact: measurable_itv_infty_bnd|exact: measurable_itv_bnd_infty]. +Qed. + +Lemma measurableE : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + by move=> I [x _ <-]; apply: measurable_itv_bounded. +apply: smallest_sub; first exact: smallest_sigma_algebra. +by move=> A' /= [x [y ->]]; apply: measurable_itv. +Qed. + +End rgenopens. +End RGenOpens. + +Section erealwithrays. +Variable R : realType. +Implicit Types (x y z : \bar R) (r s : R). +Local Open Scope ereal_scope. + +Lemma EFin_itv_bnd_infty b r : EFin @` [set` Interval (BSide b r) +oo%O] = + [set` Interval (BSide b r%:E) +oo%O] `\ +oo. +Proof. +rewrite eqEsubset; split => [x [s /itvP rs <-]|x []]. + split => //=; rewrite in_itv /=. + by case: b in rs *; rewrite /= ?(lee_fin, lte_fin) rs. +move: x => [s|_ /(_ erefl)|] //=; rewrite in_itv /= andbT; last first. + by case: b => /=; rewrite 1?(leNgt,ltNge) 1?(ltNyr, leNye). +by case: b => /=; rewrite 1?(lte_fin,lee_fin) => rs _; + exists s => //; rewrite in_itv /= rs. +Qed. + +Lemma EFin_itv r : [set s | r%:E < s%:E] = `]r, +oo[%classic. +Proof. +by rewrite predeqE => s; split => [|]; rewrite /= lte_fin in_itv/= andbT. +Qed. + +Lemma preimage_EFin_setT : @EFin R @^-1` [set x | x \in `]-oo%E, +oo[] = setT. +Proof. +by rewrite set_itvE predeqE => r; split=> // _; rewrite /preimage /= ltNyr. +Qed. + +Lemma eitv_bnd_infty b r : `[r%:E, +oo[%classic = + \bigcap_k [set` Interval (BSide b (r - k.+1%:R^-1)%:E) +oo%O] :> set _. +Proof. +rewrite predeqE => x; split=> [|]. +- move: x => [s /=| _ n _|//]. + + rewrite in_itv /= andbT lee_fin => rs n _ /=; rewrite in_itv/= andbT. + case: b => /=. + * by rewrite lee_fin lerBlDl (le_trans rs)// lerDr. + * by rewrite lte_fin ltrBlDl (le_lt_trans rs)// ltrDr. + + by rewrite /= in_itv /= andbT; case: b => /=; rewrite lteey. +- move: x => [s| |/(_ 0%N Logic.I)] /=; rewrite ?in_itv/= ?leey//; last first. + by case: b. + move=> h; rewrite lee_fin leNgt andbT; apply/negP => /ltr_add_invr[k skr]. + have {h} := h k Logic.I; rewrite /= in_itv /= andbT; case: b => /=. + + by rewrite lee_fin lerBlDr leNgt skr. + + by rewrite lte_fin ltrBlDr ltNge (ltW skr). +Qed. + +Lemma eitv_infty_bnd b r : `]-oo, r%:E]%classic = + \bigcap_k [set` Interval -oo%O (BSide b (r%:E + k.+1%:R^-1%:E))] :> set _. +Proof. +rewrite predeqE => x; split=> [|]. +- move: x => [s /=|//|_ n _]. + + rewrite in_itv /= lee_fin => sr n _; rewrite /= in_itv /= -EFinD. + case: b => /=. + * by rewrite lte_fin (le_lt_trans sr)// ltrDl. + * by rewrite lee_fin (le_trans sr)// lerDl. + + by rewrite /= in_itv /= -EFinD; case: b => //=; rewrite lteNye. +- move: x => [s|/(_ 0%N Logic.I)|]/=; rewrite !in_itv/= ?leNye//; last first. + by case: b. + move=> h; rewrite lee_fin leNgt; apply/negP => /ltr_add_invr[k rks]. + have {h} := h k Logic.I; rewrite /= in_itv /= -EFinD; case: b => /=. + + by rewrite lte_fin ltNge (ltW rks). + + by rewrite lee_fin leNgt rks. +Qed. + +Lemma eset1Ny : + [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R). +Proof. +rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr. +move=> [r|/(_ O Logic.I)|]//. +move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge. +rewrite lee_fin; have [r0|r0] := leP 0%R r. + by rewrite (le_trans _ r0) // lerNl oppr0 ler0n. +rewrite lerNl -abszN natr_absz gtr0_norm; last first. + by rewrite ltrNr oppr0 -floor_lt0. +by rewrite mulrNz lerNl opprK ge_floor. +Qed. + +Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). +Proof. +rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. +move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. +rewrite andbT lte_fin ltNge. +have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). +by rewrite natr_absz gtr0_norm// ?le_ceil// -ceil_gt0. +Qed. + +End erealwithrays. + +Module ErealGenOInfty. +Section erealgenoinfty. +Variable R : realType. +Implicit Types (x y z : \bar R) (r s : R). + +Local Open Scope ereal_scope. + +Definition G := [set A : set \bar R | exists r, A = `]r%:E, +oo[%classic]. + +Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. +Proof. +rewrite eset1Ny; apply: bigcap_measurable => // i _. +rewrite -setCitvr; apply: measurableC; rewrite (eitv_bnd_infty false). +apply: bigcap_measurable => // j _; apply: sub_sigma_algebra. +by exists (- (i%:R + j.+1%:R^-1))%R; rewrite opprD. +Qed. + +Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. +Proof. +rewrite eset1y; apply: bigcapT_measurable => i. +by apply: sub_sigma_algebra; exists i%:R. +Qed. + +Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Proof. +apply/seteqP; split; last first. + apply: smallest_sub. + split; first exact: emeasurable0. + by move=> *; rewrite setTD; exact: emeasurableC. + by move=> *; exact: bigcupT_emeasurable. + move=> _ [r ->]; rewrite /emeasurable /=. + exists `]r, +oo[%classic. + rewrite RGenOInfty.measurableE. + exact: RGenOInfty.measurable_itv_bnd_infty. + by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. +move=> A [B mB [C mC]] <-; apply: measurableU; last first. + case: mC; [by []|exact: measurable_set1Ny|exact: measurable_set1y|]. + - by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. +rewrite RGenOInfty.measurableE in mB. +have smB := smallest_sub _ _ mB. +(* BUG: elim/smB : _. fails !! *) +apply: (smB (G.-sigma.-measurable \o (image^~ EFin))); last first. + move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. + by apply: sub_sigma_algebra => /=; exists r. + exact: measurable_set1y. +split=> /= [|D mD|F mF]; first by rewrite image_set0. +- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. + by apply: measurableU; [exact: measurable_set1Ny| exact: measurable_set1y]. +- by rewrite EFin_bigcup; apply: bigcup_measurable => i _ ; exact: mF. +Qed. + +End erealgenoinfty. +End ErealGenOInfty. + +Module ErealGenCInfty. +Section erealgencinfty. +Variable R : realType. +Implicit Types (x y z : \bar R) (r s : R). +Local Open Scope ereal_scope. + +Definition G := [set A : set \bar R | exists r, A = `[r%:E, +oo[%classic]. + +Lemma measurable_set1Ny : G.-sigma.-measurable [set -oo]. +Proof. +rewrite eset1Ny; apply: bigcapT_measurable=> i; rewrite -setCitvr. +by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%R. +Qed. + +Lemma measurable_set1y : G.-sigma.-measurable [set +oo]. +Proof. +rewrite eset1y; apply: bigcap_measurable => // i _. +rewrite -setCitvl; apply: measurableC; rewrite (eitv_infty_bnd true). +apply: bigcap_measurable => // j _; rewrite -setCitvr; apply: measurableC. +by apply: sub_sigma_algebra; exists (i%:R + j.+1%:R^-1)%R. +Qed. + +Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Proof. +apply/seteqP; split; last first. + apply: smallest_sub. + split; first exact: emeasurable0. + by move=> *; rewrite setTD; exact: emeasurableC. + by move=> *; exact: bigcupT_emeasurable. + move=> _ [r ->]/=; exists `[r, +oo[%classic. + rewrite RGenOInfty.measurableE. + exact: RGenOInfty.measurable_itv_bnd_infty. + by exists [set +oo]; [constructor|rewrite -punct_eitv_bndy]. +move=> _ [A' mA' [C mC]] <-; apply: measurableU; last first. + case: mC; [by []|exact: measurable_set1Ny| exact: measurable_set1y|]. + by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. +rewrite RGenCInfty.measurableE in mA'. +have smA' := smallest_sub _ _ mA'. +(* BUG: elim/smA' : _. fails !! *) +apply: (smA' (G.-sigma.-measurable \o (image^~ EFin))); last first. + move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. + by apply: sub_sigma_algebra => /=; exists r. + exact: measurable_set1y. +split=> /= [|D mD|F mF]; first by rewrite image_set0. +- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. + by apply: measurableU; [exact: measurable_set1Ny|exact: measurable_set1y]. +- by rewrite EFin_bigcup; apply: bigcup_measurable => i _; exact: mF. +Qed. + +End erealgencinfty. +End ErealGenCInfty. + +Module ErealGenInftyO. +Section erealgeninftyo. +Variable R : realType. + +Definition G := [set A : set \bar R | exists r, A = `]-oo, r%:E[%classic]. + +Lemma measurableE : emeasurable (@ocitv R) = G.-sigma.-measurable. +Proof. +rewrite ErealGenCInfty.measurableE eqEsubset; split => A. + apply: smallest_sub; first exact: smallest_sigma_algebra. + move=> _ [x ->]; rewrite -[X in _.-measurable X]setCK; apply: measurableC. + by apply: sub_sigma_algebra; exists x; rewrite setCitvr. +apply: smallest_sub; first exact: smallest_sigma_algebra. +move=> x Gx; rewrite -(setCK x); apply: measurableC; apply: sub_sigma_algebra. +by case: Gx => y ->; exists y; rewrite setCitvl. +Qed. + +End erealgeninftyo. +End ErealGenInftyO. + +(* 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). +Proof. +move=> mD /open_subspaceP [V [oV] VD]; rewrite setIC -VD. +by apply: measurableI => //; exact: open_measurable. +Qed. + +Lemma closed_measurable (A : set R) : closed A -> measurable A. +Proof. by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed. + +Lemma compact_measurable (A : set R) : compact A -> measurable A. +Proof. +by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable. +Qed. + +Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : + measurable D -> continuous f -> measurable_fun D f. +Proof. +move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)). +move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //. +exact/cf/interval_open. +Qed. + +Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) : + open D -> {in D, continuous f} -> measurable_fun D f. +Proof. +move=> oD; rewrite -(continuous_open_subspace f oD). +by apply: subspace_continuous_measurable_fun; exact: open_measurable. +Qed. + +Lemma continuous_measurable_fun (f : R -> R) : + continuous f -> measurable_fun setT f. +Proof. +by move=> cf; apply: open_continuous_measurable_fun => //; exact: openT. +Qed. + +End coutinuous_measurable. + +Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) : + lower_semicontinuous f -> measurable_fun setT f. +Proof. +move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)). +move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable. +by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact. +Qed. + +Section standard_measurable_fun. +Variable R : realType. +Implicit Types D : set R. + +Lemma oppr_measurable D : measurable_fun D -%R. +Proof. +apply: measurable_funTS => /=; apply: continuous_measurable_fun. +exact: opp_continuous. +Qed. + +Lemma normr_measurable D : measurable_fun D (@normr _ R). +Proof. +move=> mD; apply: (measurability (RGenOInfty.measurableE R)) => //. +move=> /= _ [_ [x ->] <-]; apply: measurableI => //. +have [x0|x0] := leP 0 x. + rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic. + by apply: measurableU; apply: measurable_itv. + rewrite predeqE => r; split => [|[|]]; rewrite preimage_itv ?in_itv ?andbT/=. + - have [r0|r0] := leP 0 r; [rewrite ger0_norm|rewrite ltr0_norm] => // xr; + rewrite 2!in_itv/=. + + by right; rewrite xr. + + by left; rewrite ltrNr. + - move=> rx /=. + by rewrite ler0_norm 1?ltrNr// (le_trans (ltW rx))// lerNl oppr0. + - by rewrite in_itv /= andbT => xr; rewrite (lt_le_trans _ (ler_norm _)). +rewrite [X in measurable X](_ : _ = setT)// predeqE => r. +by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). +Qed. + +Lemma mulrl_measurable D (k : R) : measurable_fun D ( *%R k). +Proof. +apply: measurable_funTS => /=. +by apply: continuous_measurable_fun; exact: mulrl_continuous. +Qed. + +Lemma mulrr_measurable D (k : R) : measurable_fun D (fun x => x * k). +Proof. +apply: measurable_funTS => /=. +by apply: continuous_measurable_fun; exact: mulrr_continuous. +Qed. + +Lemma exprn_measurable D n : measurable_fun D (fun x => x ^+ n). +Proof. +apply measurable_funTS => /=. +by apply continuous_measurable_fun; exact: exprn_continuous. +Qed. + +End standard_measurable_fun. +#[global] Hint Extern 0 (measurable_fun _ -%R) => + solve [exact: oppr_measurable] : core. +#[global] Hint Extern 0 (measurable_fun _ normr) => + solve [exact: normr_measurable] : core. +#[global] Hint Extern 0 (measurable_fun _ ( *%R _)) => + solve [exact: mulrl_measurable] : core. +#[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) => + solve [exact: exprn_measurable] : core. +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `exprn_measurable` instead")] +Notation measurable_exprn := exprn_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrl_measurable` instead")] +Notation measurable_mulrl := mulrl_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrr_measurable` instead")] +Notation measurable_mulrr := mulrr_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppr_measurable` instead")] +Notation measurable_oppr := oppr_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `normr_measurable` instead")] +Notation measurable_normr := normr_measurable (only parsing). + +Section measurable_fun_realType. +Context d (T : measurableType d) (R : realType). +Implicit Types (D : set T) (f g : T -> R). + +Lemma measurable_funD D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). +Proof. +move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //. +move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy. +rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) + ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))). + apply: bigcupT_measurable_rat => q; apply: measurableI. + - by rewrite -preimage_itvoy; apply: mf => //; exact: measurable_itv. + - by rewrite -preimage_itvoy; apply: mg => //; exact: measurable_itv. +rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. + rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h. + exists r => //; rewrite setIACA setIid; split => //; split => /=. + by rewrite h. + by rewrite ltrBlDr addrC -ltrBlDr h. +by rewrite ltrBlDr=> afg; rewrite (lt_le_trans afg)// addrC lerD2r ltW. +Qed. + +Lemma measurable_funB D f g : measurable_fun D f -> + measurable_fun D g -> measurable_fun D (f \- g). +Proof. by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. Qed. + +Lemma measurable_funM D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g). +Proof. +move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2) + \- (fun x => 2%:R^-1 * (f x ^+ 2)) \- (fun x => 2%:R^-1 * (g x ^+ 2))). + apply: measurable_funB; first apply: measurable_funB. + - apply: measurableT_comp => //. + by apply: measurableT_comp (exprn_measurable _) _; exact: measurable_funD. + - apply: measurableT_comp => //. + exact: measurableT_comp (exprn_measurable _) _. + - apply: measurableT_comp => //. + exact: measurableT_comp (exprn_measurable _) _. +rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA. +rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK. +by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE. +Qed. + +Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x < g x). +Proof. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_gt0. +by rewrite preimage_true -preimage_itvoy; exact: measurable_funB. +Qed. + +Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x <= g x). +Proof. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_ge0. +by rewrite preimage_true -preimage_itvcy; exact: measurable_funB. +Qed. + +Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x == g x). +Proof. +move=> mf mg. +rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))). + by apply: measurable_and; exact: measurable_fun_ler. +by under eq_fun do rewrite eq_le. +Qed. + +Lemma measurable_maxr D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g). +Proof. +by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; + [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. +Qed. + +Lemma measurable_minr D f g : + measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). +Proof. +by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; + [exact: measurable_fun_ltr|exact: measurable_funS mf|exact: measurable_funS mg]. +Qed. + +Lemma measurable_fun_sups D (h : (T -> R)^nat) n : + (forall t, D t -> has_ubound (range (h ^~ t))) -> + (forall m, measurable_fun D (h m)) -> + measurable_fun D (fun x => sups (h ^~ x) n). +Proof. +move=> f_ub mf mD; apply: (measurability (RGenOInfty.measurableE R)) => //. +move=> _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr. +by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. +Qed. + +Lemma measurable_fun_infs D (h : (T -> R)^nat) n : + (forall t, D t -> has_lbound (range (h ^~ t))) -> + (forall n, measurable_fun D (h n)) -> + measurable_fun D (fun x => infs (h ^~ x) n). +Proof. +move=> lb_f mf mD; apply: (measurability (RGenInftyO.measurableE R)) =>//. +move=> _ [_ [x ->] <-]; rewrite infs_preimage // setI_bigcupr. +by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv. +Qed. + +Lemma measurable_fun_limn_sup D (h : (T -> R)^nat) : + (forall t, D t -> has_ubound (range (h ^~ t))) -> + (forall t, D t -> has_lbound (range (h ^~ t))) -> + (forall n, measurable_fun D (h n)) -> + measurable_fun D (fun x => limn_sup (h ^~ x)). +Proof. +move=> f_ub f_lb mf. +have : {in D, (fun x => inf [set sups (h ^~ x) n | n in [set n | 0 <= n]%N]) + =1 (fun x => limn_sup (h^~ x))}. + move=> t; rewrite inE => Dt; apply/esym/cvg_lim => //. + rewrite [X in _ --> X](_ : _ = inf (range (sups (h^~t)))). + by apply: cvg_sups_inf; [exact: f_ub|exact: f_lb]. + by congr (inf [set _ | _ in _]); rewrite predeqE. +move/eq_measurable_fun; apply; apply: measurable_fun_infs => //. + move=> t Dt; have [M hM] := f_lb _ Dt; exists M => _ [m /= nm <-]. + rewrite (@le_trans _ _ (h m t)) //; first by apply hM => /=; exists m. + by apply: sup_ubound; [exact/has_ubound_sdrop/f_ub|exists m => /=]. +by move=> k; exact: measurable_fun_sups. +Qed. + +Lemma measurable_fun_cvg D (h : (T -> R)^nat) f : + (forall m, measurable_fun D (h m)) -> (forall x, D x -> h ^~ x @ \oo --> f x) -> + measurable_fun D f. +Proof. +move=> mf_ f_f; have fE x : D x -> f x = limn_sup (h ^~ x). + move=> Dx; have /cvg_lim <-// := @cvg_sups _ (h ^~ x) (f x) (f_f _ Dx). +apply: (@eq_measurable_fun _ _ _ _ D (fun x => limn_sup (h ^~ x))). + by move=> x; rewrite inE => Dx; rewrite -fE. +apply: (@measurable_fun_limn_sup _ h) => // t Dt. +- by apply/bounded_fun_has_ubound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. +- by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. +Qed. + +Lemma measurable_indic D (U : set T) : measurable U -> + measurable_fun D (\1_U : _ -> R). +Proof. +move=> mU mD /= Y mY. +have [Y0|Y0] := pselect (Y 0%R); have [Y1|Y1] := pselect (Y 1%R). +- rewrite [X in measurable X](_ : _ = D)//. + by apply/seteqP; split => //= r Dr /=; rewrite indicE; case: (_ \in _). +- rewrite [X in measurable (_ `&` X)](_ : _ = ~` U)//. + by apply: measurableI => //; exact: measurableC. + apply/seteqP; split => [//= r /= + Ur|r Ur]; rewrite /= indicE. + by rewrite mem_set. + by rewrite memNset. +- rewrite [X in measurable (_ `&` X)](_ : _ = U); first exact: measurableI. + apply/seteqP; split => [//= r /=|r Ur]; rewrite /= indicE. + by have [//|Ur] := pselect (U r); rewrite memNset. + by rewrite mem_set. +- rewrite [X in measurable X](_ : _ = set0)//. + by apply/seteqP; split => // r /= -[_]; rewrite indicE; case: (_ \in _). +Qed. + +Lemma measurable_indicP D : measurable D <-> measurable_fun setT (\1_D : _ -> R). +Proof. +split=> [|m1]; first exact: measurable_indic. +have -> : D = (\1_D : _ -> R) @^-1` `]0, +oo[. + apply/seteqP; split => t/=. + by rewrite indicE => /mem_set ->; rewrite in_itv/= ltr01. + by rewrite in_itv/= andbT indicE ltr0n; have [/set_mem|//] := boolP (t \in D). +by rewrite -[_ @^-1` _]setTI; exact: m1. +Qed. + +End measurable_fun_realType. +#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")] +Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing). + +Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R). +Proof. +rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. + by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=; + rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. +apply/measurable_funU => //; split. +- apply/measurable_restrictT => //=. + rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE. + by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. +- have : {in `]0, +oo[%classic, continuous (@ln R)}. + by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. + rewrite -continuous_open_subspace; last exact: interval_open. + by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv. +Qed. +#[global] Hint Extern 0 (measurable_fun _ (@ln _)) => + solve [apply: measurable_ln] : core. +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_ln` instead")] +Notation measurable_fun_ln := measurable_ln (only parsing). + +Lemma measurable_expR (R : realType) : measurable_fun [set: R] expR. +Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. +#[global] Hint Extern 0 (measurable_fun _ expR) => + solve [apply: measurable_expR] : core. + +Lemma natmul_measurable {R : realType} D n : + measurable_fun D (fun x : R => x *+ n). +Proof. +under eq_fun do rewrite -mulr_natr. +by do 2 apply: measurable_funM => //. +Qed. + +Lemma measurable_funX d (T : measurableType d) {R : realType} D (f : T -> R) n : + measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). +Proof. +move=> mf. +exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). +Qed. +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] +Notation measurable_fun_pow := measurable_funX (only parsing). + +Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). +Proof. +apply: measurable_fun_if => //. +- apply: (measurable_fun_bool true). + rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//. + by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. +- rewrite setTI; apply: measurableT_comp => //. + rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp. + by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP. +Qed. +#[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) => + solve [apply: measurable_powR] : core. + +Lemma measurable_powRr {R : realType} b : measurable_fun [set: R] (@powR R b). +Proof. +rewrite /powR; apply: measurable_fun_if => //. +- rewrite preimage_true setTI/=. + case: (b == 0); rewrite ?set_true ?set_false. + + by apply: measurableT_comp => //; exact: measurable_fun_eqr. + + exact: measurable_fun_set0. +- rewrite preimage_false setTI; apply: measurableT_comp => //. + exact: mulrr_measurable. +Qed. + +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")] +Notation measurable_fun_max := measurable_maxr (only parsing). + +Module NGenCInfty. +Section ngencinfty. +Implicit Types x y z : nat. + +Definition G : set (set nat) := [set A | exists x, A = `[x, +oo[%classic]. + +Lemma measurable_itv_bnd_infty b x : + G.-sigma.-measurable [set` Interval (BSide b x) +oo%O]. +Proof. +case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itv_c_infty. +rewrite [X in measurable X](_ : _ = + \bigcup_(k in [set k | k >= x]%N) `[k.+1, +oo[%classic); last first. + apply/seteqP; split => [z /=|/= z [t/= xt]]. + rewrite in_itv/= andbT => xz; exists z.-1 => /=. + by rewrite -ltnS//=; case: z xz. + by case: z xz => //= z xz; rewrite in_itv/= lexx andbT. + by rewrite !in_itv/= !andbT; apply: lt_le_trans; rewrite ltEnat/= ltnS. +rewrite bigcup_mkcond; apply: bigcupT_measurable => k. +by case: ifPn => //= _; apply: sub_sigma_algebra; eexists; reflexivity. +Qed. + +Lemma measurable_itv_bounded a b y : a != +oo%O -> + G.-sigma.-measurable [set` Interval a (BSide b y)]. +Proof. +case: a => [a r _|[_|//]]. + by rewrite set_itv_splitD; apply: measurableD; apply: measurable_itv_bnd_infty. +by rewrite -setCitvr; apply: measurableC; apply: measurable_itv_bnd_infty. +Qed. + +Lemma measurableE : @measurable _ nat = G.-sigma.-measurable. +Proof. +rewrite eqEsubset; split => [A mA|A]; last exact: smallest_sub. +rewrite (_ : A = \bigcup_(i in A) `[i, i.+1[%classic). + by apply: bigcup_measurable => k Ak; exact: measurable_itv_bounded. +apply/seteqP; split => [x Ax|x [k Ak]]. + by exists x => //=; rewrite in_itv/= lexx/= ltEnat /= ltnS. +by rewrite /= in_itv/= leEnat ltEnat /= ltnS -eqn_leq => /eqP <-. +Qed. + +End ngencinfty. +End NGenCInfty. + +Section measurable_fun_nat. +Context d (T : measurableType d). +Implicit Types (D : set T) (f g : T -> nat). + +Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x + g x)%N. +Proof. +move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. +move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy. +rewrite [X in measurable X](_ : _ = \bigcup_q + ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))). + apply: bigcupT_measurable => q; apply: measurableI. + - by rewrite -preimage_itvcy; exact: mf. + - by rewrite -preimage_itvcy; exact: mg. +rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[?]]. +- move=> afxgx; exists (a - g x)%N => //=; split; split => //. + by rewrite leEnat leq_subLR// addnC -leEnat. + have [gxa|gxa] := leqP (g x) a; first by rewrite subKn. + by move/ltnW : (gxa); rewrite -subn_eq0 => /eqP ->; rewrite subn0 ltW. +- rewrite leEnat leq_subLR => arg; split => //. + by rewrite (leq_trans arg)// leq_add2r. +Qed. + +Lemma measurable_fun_maxn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => maxn (f x) (g x)). +Proof. +move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. +move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ = + ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))). + apply: measurableU. + - by rewrite -preimage_itvcy; exact: mf. + - by rewrite -preimage_itvcy; exact: mg. +rewrite predeqE => x; split => [[Dx /=]|]. +- by rewrite in_itv/= andbT; have [fg agx|gf afx] := leqP (f x) (g x); tauto. +- move=> [[Dx /= afx]|[Dx /= agx]]. + + rewrite in_itv/= andbT; split => //. + by rewrite (le_trans afx)// leEnat leq_maxl. + + rewrite in_itv/= andbT; split => //. + by rewrite (le_trans agx)// leEnat leq_maxr. +Qed. + +Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N -> + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x - g x)%N. +Proof. +move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //. +move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy. +rewrite [X in measurable X](_ : _ = \bigcup_q + ((D `&` [set x | maxn a q <= f x]%O) `&` + (D `&` [set x | g x <= (q - a)%N]%O))). + apply: bigcupT_measurable => q; apply: measurableI. + - by rewrite -preimage_itvcy; exact: mf. + - by rewrite -preimage_itvNyc; exact: mg. +rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[_]]. +- move=> afxgx; exists (g x + a)%N => //; split; split => //=. + rewrite leEnat; have /maxn_idPr -> := leq_addl (g x) a. + by rewrite -leq_subRL. + by rewrite leEnat addnK. +- rewrite leEnat => gxra; split => //; rewrite -(leq_add2r (g x)) subnK//. + have [afx|afx] := leqP a (f x). + rewrite -(@leq_sub2rE a)// addnC addnK (leq_trans gxra)// leq_sub2r//. + by rewrite (leq_trans _ rfx)//; exact: leq_maxr. + move: gxra; rewrite -(leq_add2l a) subnKC//; last first. + by have := leq_ltn_trans rfx afx; rewrite ltnNge leq_maxl. + by move=> /leq_trans; apply; rewrite (leq_trans _ rfx)//; exact: leq_maxr. +Qed. + +Lemma measurable_fun_subn D f g : measurable_fun D f -> + measurable_fun D g -> measurable_fun D (fun x => f x - g x)%N. +Proof. +move=> mf mg. +rewrite [X in measurable_fun _ X](_ : _ = fun x => (maxn (f x) (g x) - g x)%N). + apply: measurable_fun_subn' => //; last exact: measurable_fun_maxn. + by move=> t; rewrite leq_maxr. +apply/funext => x; have [//|gf] := leqP (g x) (f x). +by apply/eqP; rewrite subnn subn_eq0// ltnW. +Qed. + +Lemma measurable_fun_ltn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x < g x)%N. +Proof. +move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. +- have -> : (fun x => f x < g x)%O = (fun x => 0%N < (g x - f x)%N)%O. + apply/funext => n; apply/idP/idP. + by rewrite !ltEnat /ltn/= => fg; rewrite subn_gt0. + by rewrite !ltEnat /ltn/= => fg; rewrite -subn_gt0. + by rewrite preimage_true -preimage_itvoy; exact: measurable_fun_subn. +- under eq_fun do rewrite ltnNge. + rewrite preimage_false set_predC setCK. + rewrite [X in _ `&` X](_ : _ = \bigcup_(i in range f) + ([set y | g y <= i]%O `&` [set t | i <= f t]%O)). + rewrite setI_bigcupr; apply: bigcup_measurable => k fk. + rewrite setIIr; apply: measurableI => //. + + by rewrite -preimage_itvNyc; exact: mg. + + by rewrite -preimage_itvcy; exact: mf. + apply/funext => n/=. + suff : (g n <= f n)%N <-> + (\bigcup_(i in range f) ([set y | g y <= i]%O `&` [set t | i <= f t]%O)) n. + by move/propext. + split=> [gfn|[k [t _ <- []]] /=]. + by exists (f n) => //; split => /=. + by move=> /leq_trans; apply. +- by rewrite preimage_set0 setI0. +- by rewrite preimage_setT setIT. +Qed. + +Lemma measurable_fun_leq D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x <= g x)%N. +Proof. +move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. +- rewrite preimage_true [X in _ `&` X](_ : _ = + \bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)). + rewrite setI_bigcupr; apply: bigcup_measurable => k fk. + rewrite setIIr; apply: measurableI => //. + + by rewrite -preimage_itvNyc; exact: mf. + + by rewrite -preimage_itvcy; exact: mg. + apply/funext => n/=. + suff : (f n <= g n)%N <-> + (\bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)) n. + by move/propext. + split=> [gfn|[k [t _ <- []]] /=]. + by exists (g n) => //; split => /=. + by move=> /leq_trans; apply. +- under eq_fun do rewrite leqNgt. + by rewrite preimage_false set_predC setCK; exact: measurable_fun_ltn. +- by rewrite preimage_set0 setI0. +- by rewrite preimage_setT setIT. +Qed. + +Lemma measurable_fun_eqn D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x == g x). +Proof. +move=> mf mg. +rewrite (_ : (fun x => f x == g x) = (fun x => (f x <= g x) && (g x <= f x))%N). + by apply: measurable_and; exact: measurable_fun_leq. +by under eq_fun do rewrite eq_le. +Qed. + +End measurable_fun_nat. + +Section standard_emeasurable_fun. +Variable R : realType. + +Lemma EFin_measurable (D : set R) : measurable_fun D EFin. +Proof. +move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. +move=> /= _ [_ [x ->]] <-; apply: measurableI => //. +by rewrite preimage_itvoy EFin_itv; exact: measurable_itv. +Qed. + +Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse. +Proof. +move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. +move=> /= _ [_ [x ->] <-]. +rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. +apply: measurableU; last first. + by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. +apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). + by rewrite -[X in measurable X]setTI; exact: normr_measurable. +exists set0; first by constructor. +rewrite setU0 predeqE => -[y| |]; split => /= => -[r]; + rewrite ?/= /= ?in_itv /= ?andbT => xr//. + + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry. + + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry. +Qed. + +Lemma oppe_measurable (D : set (\bar R)) : + measurable_fun D (-%E : \bar R -> \bar R). +Proof. +move=> mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. +move=> _ [_ [x ->] <-]; rewrite (_ : _ @^-1` _ = `]-oo, (- x)%:E]%classic). + by apply: measurableI => //; exact: emeasurable_itv. +by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv leeNr. +Qed. + +End standard_emeasurable_fun. +#[global] Hint Extern 0 (measurable_fun _ abse) => + solve [exact: abse_measurable] : core. +#[global] Hint Extern 0 (measurable_fun _ EFin) => + solve [exact: EFin_measurable] : core. +#[global] Hint Extern 0 (measurable_fun _ -%E) => + solve [exact: oppe_measurable] : core. +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `oppe_measurable` instead")] +Notation measurable_oppe := oppe_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `abse_measurable` instead")] +Notation measurable_abse := abse_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `EFin_measurable` instead")] +Notation measurable_EFin := EFin_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `natmul_measurable` instead")] +Notation measurable_natmul := natmul_measurable (only parsing). + +(* NB: real-valued function *) +Lemma measurable_EFinP d (T : measurableType d) (R : realType) (D : set T) + (g : T -> R) : + measurable_fun D (EFin \o g) <-> measurable_fun D g. +Proof. +split=> [mf mD A mA|]; last by move=> mg; exact: measurableT_comp. +rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)). + by apply: mf => //; exists A => //; exists set0; [constructor|rewrite setU0]. +congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. +by move=> ? ?; exact: preimage_image. +Qed. +#[deprecated(since="mathcomp-analysis 1.6.0", note="use `measurable_EFinP` instead")] +Notation EFin_measurable_fun := measurable_EFinP (only parsing). + +Lemma measurable_fun_dirac + d {T : measurableType d} {R : realType} D (U : set T) : + measurable U -> measurable_fun D (fun x => \d_x U : \bar R). +Proof. by move=> /measurable_indic/measurable_EFinP. Qed. + +Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) : + measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f). +Proof. +move=> mf;rewrite (_ : er_map _ = + fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. + by apply: funext=> -[]. +apply: measurable_fun_ifT => //=. ++ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num. ++ exact/measurable_EFinP/measurableT_comp. +Qed. +#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] +Notation measurable_fun_er_map := measurable_er_map (only parsing). + +Section emeasurable_fun. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). +Implicit Types (D : set T). + +Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) : + (forall n, measurable_fun D (f n)) -> + forall n, measurable_fun D (fun x => einfs (f ^~ x) n). +Proof. +move=> mf n mD. +apply: (measurability (ErealGenCInfty.measurableE R)) => //. +move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=. +by apply: bigcap_measurableType => ? ?; exact/mf/emeasurable_itv. +Qed. + +Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) : + (forall n, measurable_fun D (f n)) -> + forall n, measurable_fun D (fun x => esups (f ^~ x) n). +Proof. +move=> mf n mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. +move=> _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr. +by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv. +Qed. + +Lemma measurable_maxe D (f g : T -> \bar R) : + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => maxe (f x) (g x)). +Proof. +move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. +move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ = + (D `&` f @^-1` `[x%:E, +oo[) `|` (D `&` g @^-1` `[x%:E, +oo[)); last first. + rewrite predeqE => t /=; split. + by rewrite !/= /= !in_itv /= !andbT le_max => -[Dx /orP[|]]; + tauto. + by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_max; + move=> [Dx ->]//; rewrite orbT. +by apply: measurableU; [exact/mf/emeasurable_itv| exact/mg/emeasurable_itv]. +Qed. + +Lemma measurable_funepos D (f : T -> \bar R) : + measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; rewrite unlock; exact: measurable_maxe. Qed. + +Lemma measurable_funeneg D (f : T -> \bar R) : + measurable_fun D f -> measurable_fun D f^\-. +Proof. +move=> mf; rewrite unlock; apply: measurable_maxe => //. +exact: measurableT_comp. +Qed. + +Lemma measurable_mine D (f g : T -> \bar R) : + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => mine (f x) (g x)). +Proof. +move=> mf mg; rewrite (_ : (fun _ => _) = (fun x => - maxe (- f x) (- g x))). + apply: measurableT_comp => //. + by apply: measurable_maxe; exact: measurableT_comp. +by rewrite funeqE => x; rewrite oppe_max !oppeK. +Qed. + +Lemma measurable_fun_limn_esup D (f : (T -> \bar R)^nat) : + (forall n, measurable_fun D (f n)) -> + measurable_fun D (fun x => limn_esup (f ^~ x)). +Proof. +move=> mf mD; rewrite (_ : (fun _ => _) = + (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])). + by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups. +rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //. +rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))). + exact: cvg_esups_inf. +by congr (ereal_inf [set _ | _ in _]); rewrite predeqE. +Qed. + +Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) : + (forall m, measurable_fun D (f_ m)) -> + (forall x, D x -> f_ ^~ x @ \oo --> f x) -> measurable_fun D f. +Proof. +move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x). + rewrite limn_esup_lim. + by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx). +apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //. + by move=> x; rewrite inE => Dx; rewrite fE. +exact: measurable_fun_limn_esup. +Qed. +End emeasurable_fun. +Arguments emeasurable_fun_cvg {d T R D} f_. + +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurableT_comp` instead")] +Notation emeasurable_funN := measurableT_comp (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")] +Notation emeasurable_fun_max := measurable_maxe (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mine` instead")] +Notation emeasurable_fun_min := measurable_mine (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")] +Notation emeasurable_fun_funepos := measurable_funepos (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funeneg` instead")] +Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing). +#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")] +Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing). + +Section open_itv_cover. +Context {R : realType}. +Implicit Types (A : set R). +Local Open Scope ereal_scope. + +Let l := (@wlength R idfun). + +Lemma outer_measure_open_itv_cover A : (l^* A)%mu = + ereal_inf [set \sum_(k _ /= [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. + +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 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. diff --git a/theories/normedtype.v b/theories/normedtype.v index a36ac85f25..dbc0e3d4d0 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1192,10 +1192,6 @@ Arguments cvgr0_norm_le {_ _ _ F FF}. #[global] Hint Extern 0 (is_true (`|?x| <= _)) => match goal with H : x \is_near _ |- _ => near: x; exact: cvgr0_norm_le end : core. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgrPdist_lt` or a variation instead")] -Notation cvg_distP := fcvgrPdist_lt (only parsing). - Section nbhs_lt_le. Context {R : realType}. Implicit Types x z : R. @@ -2131,15 +2127,7 @@ Proof. by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r. Qed. -Lemma __deprecated__cvg_distW {F : set_system V} {FF : Filter F} (y : V) : - (forall eps, 0 < eps -> \forall y' \near F, `|y - y'| <= eps) -> - F --> y. -Proof. by move=> /cvgrPdist_le. Qed. - End PseudoNormedZMod_numFieldType. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="use `cvgrPdist_le` or a variation instead")] -Notation cvg_distW := __deprecated__cvg_distW (only parsing). Section NormedModule_numFieldType. Variables (R : numFieldType) (V : normedModType R). @@ -2357,14 +2345,6 @@ Definition near_simpl := (@near_simpl, @nbhs_normE, @filter_from_normE, Ltac near_simpl := rewrite ?near_simpl. End NearNorm. -Lemma __deprecated__continuous_cvg_dist {R : numFieldType} - (V W : pseudoMetricNormedZmodType R) (f : V -> W) x l : - continuous f -> x --> l -> forall e : {posnum R}, `|f l - f x| < e%:num. -Proof. by move=> cf /cvg_eq->// e; rewrite subrr normr0. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="simply use the fact that `(x --> l) -> (x = l)`")] -Notation continuous_cvg_dist := __deprecated__continuous_cvg_dist (only parsing). - (** Matrices *) Section mx_norm. Variables (K : numDomainType) (m n : nat). @@ -2555,10 +2535,6 @@ End prod_NormedModule_lemmas. Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}. Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}. -#[deprecated(since="mathcomp-analysis 0.6.0", -note="use `fcvgr2dist_ltP` or a variant instead")] -Notation cvg_dist2P := fcvgr2dist_ltP (only parsing). - (** Normed vector spaces have some continuous functions that are in fact continuous on pseudoMetricNormedZmodType *) Section NVS_continuity_pseudoMetricNormedZmodType. @@ -2907,21 +2883,7 @@ Proof. exact: cvgr_to_ge. Qed. Lemma limr_le x f : cvg (f @ F) -> (\near F, x >= f F) -> x >= lim (f @ F). Proof. exact: cvgr_to_le. Qed. -Lemma __deprecated__cvg_gt_ge (u : T -> R) a b : - u @ F --> b -> a < b -> \forall n \near F, a <= u n. -Proof. by move=> ?; apply: cvgr_ge. Qed. - -Lemma __deprecated__cvg_lt_le (u : T -> R) c b : - u @ F --> b -> b < c -> \forall n \near F, u n <= c. -Proof. by move=> ?; apply: cvgr_le. Qed. - End ProperFilterRealType. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgr_ge` and generalized to a `Filter`")] -Notation cvg_gt_ge := __deprecated__cvg_gt_ge (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgr_le` and generalized to a `Filter`")] -Notation cvg_lt_le_:= __deprecated__cvg_lt_le (only parsing). Section local_continuity. @@ -5772,10 +5734,6 @@ rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//. by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0. Unshelve. all: by end_near. Qed. -Lemma __deprecated__linear_bounded0 (f : {linear V -> W}) : - bounded_near f (nbhs (0 : V)) -> {for 0, continuous f}. -Proof. by move=> ? ?; exact: bounded_linear_continuous. Qed. - Lemma continuousfor0_continuous (f : {linear V -> W}) : {for 0, continuous f} -> continuous f. Proof. by move=> /continuous_linear_bounded/bounded_linear_continuous. Qed. @@ -5800,9 +5758,6 @@ by rewrite ler_pM. Unshelve. all: by end_near. Qed. End LinearContinuousBounded. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="generalized to `bounded_linear_continuous`")] -Notation linear_bounded0 := __deprecated__linear_bounded0 (only parsing). Section center_radius. Context {R : numDomainType} {M : pseudoPMetricType R}.