From 95f619d652c64383ec6fee8b7f743ef1696fb6be Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 3 Jun 2022 20:13:36 +0900 Subject: [PATCH] tentative definition of lebesgue stieltjes measure --- theories/lebesgue_stieltjes_measure.v | 1617 ++----------------------- 1 file changed, 133 insertions(+), 1484 deletions(-) diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 56791e24d9..dead581881 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -9,35 +9,10 @@ Require Import sequences esum measure fsbigop cardinality set_interval. Require Import realfun. (******************************************************************************) -(* Lebesgue Measure *) +(* Lebesgue Stieltjes Measure *) (* *) -(* This file contains a formalization of the Lebesgue measure using the *) -(* Caratheodory's theorem available in measure.v and further develops the *) -(* theory of measurable functions. *) -(* *) -(* Main reference: *) -(* - Daniel Li, Intégration et applications, 2016 *) -(* - Achim Klenke, Probability Theory 2nd edition, 2014 *) -(* *) -(* hlength A == length of the hull of the set of real numbers A *) -(* ocitv == set of open-closed intervals ]x, y] where *) -(* x and y are real numbers *) -(* lebesgue_measure == the Lebesgue measure *) -(* *) -(* ps_infty == inductive definition of the powerset *) -(* {0, {-oo}, {+oo}, {-oo,+oo}} *) -(* emeasurable G == sigma-algebra over \bar R built out of the *) -(* measurables G of a sigma-algebra over R *) -(* elebesgue_measure == the Lebesgue measure extended to \bar R *) -(* *) -(* The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens provide proofs *) -(* of equivalence between the sigma-algebra generated by list of intervals *) -(* and the sigma-algebras generated by open rays, closed rays, and open *) -(* intervals. *) -(* *) -(* The modules ErealGenOInfty and ErealGenCInfty provide proofs of *) -(* equivalence between emeasurable and the sigmaa-algebras generated open *) -(* rays and closed rays. *) +(* This file contains a formalization of the Lebesgue-Stieltjes measure using *) +(* the Extension theorem available in measure.v. *) (* *) (******************************************************************************) @@ -50,33 +25,26 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Notation right_continuous f := (forall x, f%function @ at_right x --> f%function x). -(* ToDo : right_continuous + left_continuous = continuous *) +Notation right_continuous f := + (forall x, f%function @ at_right x --> f%function x). Section hlength. Local Open Scope ereal_scope. -Variable R : realType. -Variable f : R -> R. -Hypothesis f_monotone : {homo f : x y / (x <= y)%R}. -Hypothesis f_right_continuous : right_continuous f. +Variables (R : realType) (f : R -> R). +Hypothesis ndf : {homo f : x y / (x <= y)%R}. +Hypothesis rcf : right_continuous f. Let g x := if x is r%:E then (f r)%:E else x. Let g_monotone : {homo g : x y / (x <= y)%E}. Proof. -move=> [r||] [l||]//=. -rewrite !lee_fin. -apply f_monotone. - -by rewrite !leey. -by rewrite !leNye. +by move=> [r| |] [l| |]//=; rewrite ?leey ?leNye// !lee_fin; exact: ndf. Qed. Implicit Types i j : interval R. Definition itvs : Type := R. -Definition hlength (A : set itvs): \bar R := - let i := Rhull A in g i.2 - g i.1. +Definition hlength (A : set itvs): \bar R := let i := Rhull A in g i.2 - g i.1. Lemma hlength0 : hlength (set0 : set R) = 0. Proof. by rewrite /hlength Rhull0 /= subee. Qed. @@ -91,7 +59,7 @@ Lemma hlength_itv i : hlength [set` i] = if i.2 > i.1 then g i.2 - g i.1 else 0. Proof. case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK. rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first. - rewrite (_ : [set` i] = set0) ?hlength0//. + rewrite -hlength0; congr (hlength _). by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12). case: i => -[ba a|[|]] [bb b|[|]] //=. - rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try @@ -116,27 +84,14 @@ Qed. Lemma finite_hlengthE i : neitv i -> hlength [set` i] < +oo -> hlength [set` i] = (fine (g i.2))%:E - (fine (g i.1))%:E. Proof. -move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo. -rewrite hlength_itv. +move=> i0 ioo; have [i1f i2f] := hlength_finite_fin_num i0 ioo. rewrite fineK; last first. -rewrite /g. -move: ri2. -case:(ereal_of_itv_bound i.2) => //. - + by rewrite /g; move: i2f; case: (ereal_of_itv_bound i.2). rewrite fineK; last first. -rewrite /g. -move: ri1. -case:(ereal_of_itv_bound i.1) => //. - -case: ifPn => //. -rewrite -leNgt le_eqVlt => /predU1P[->|]. - rewrite subee//. -rewrite /g. -move: ri1. -case:(ereal_of_itv_bound i.1) => //. - + by rewrite /g; move: i1f; case: (ereal_of_itv_bound i.1). +rewrite hlength_itv; case: ifPn => //; rewrite -leNgt le_eqVlt => /predU1P[->|]. + by rewrite subee// /g; move: i1f; case: (ereal_of_itv_bound i.1). by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->. - Qed. Lemma hlength_infty_bnd b r : @@ -161,10 +116,7 @@ Qed. Lemma hlength_ge0 i : 0 <= hlength [set` i]. Proof. rewrite hlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |]. -- rewrite suber_ge0//. - move=> /ltW. - move=> /g_monotone. - done. +- by rewrite suber_ge0// => /ltW /g_monotone. - by rewrite ltNge leey. - by case: (i.2 : \bar _) => //= [r _]; rewrite leey. Qed. @@ -173,7 +125,18 @@ Local Hint Extern 0 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core. Lemma hlength_Rhull (A : set R) : hlength [set` Rhull A] = hlength A. Proof. by rewrite /hlength Rhull_involutive. Qed. -Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j]. +(* TODO: move, use in lebesgue_measure.v *) +Lemma le_inf (S1 S2 : set R) : + (-%R @` S2) `<=` down (-%R @` S1) -> nonempty S2 -> has_inf S1 + -> (inf S1 <= inf S2)%R. +Proof. +move=> S21 S12 S1i. +rewrite ler_oppl opprK le_sup// ?has_inf_supN//. +exact/nonemptyN. +Qed. + +Lemma le_hlength_itv i j : + {subset i <= j} -> hlength [set` i] <= hlength [set` j]. Proof. set I := [set` i]; set J := [set` j]. have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_ge0. @@ -182,16 +145,14 @@ have [J0|/set0P J0] := eqVneq J set0. move=> /subset_itvP ij; apply: lee_sub => /=. have [ui|ui] := asboolP (has_ubound I). have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey. - rewrite lee_fin. - apply f_monotone. - by rewrite le_sup// => r Ir; exists r; split => //; apply: ij. + rewrite lee_fin; apply: ndf; apply/le_sup => //. + by move=> r Ir; exists r; split => //; apply: ij. have [uj /=|//] := asboolP (has_ubound J). by move: ui; have := subset_has_ubound ij uj. have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye. have [li /=|li] := asboolP (has_lbound I); last first. by move: li; have := subset_has_lbound ij lj. -rewrite lee_fin. apply f_monotone. rewrite ler_oppl opprK le_sup// ?has_inf_supN//; last first. - by case: I0 => x Ix; exists (- x)%R, x. +rewrite lee_fin; apply/ndf/le_inf => //. move=> r [r' Ir' <-{r}]; exists (- r')%R. by split => //; exists r' => //; apply: ij. Qed. @@ -272,38 +233,6 @@ Lemma hlength_ge0' (f : R -> R) (f_monotone : {homo f : x y / (x <= y)%R}) (I : set itvs) : (0 <= hlength f I)%E. Proof. by rewrite -(hlength0 f) le_hlength. Qed. -(*Lemma hlength_semi_additive2 (f : R -> R) : - semi_additive2 (hlength f). -Proof. -move=> I J /ocitvP[|[a a12]] ->; first by rewrite set0U hlength0 add0e. -move=> /ocitvP[|[b b12]] ->; first by rewrite setU0 hlength0 adde0. -rewrite -subset0 => + ab0 => /ocitvP[|[x x12] abx]. - by rewrite setU_eq0 => -[-> ->]; rewrite setU0 hlength0 adde0. -rewrite abx !hlength_itv//= ?lte_fin a12 b12 x12/= -!EFinB -EFinD. -wlog ab1 : a a12 b b12 ab0 abx / a.1 <= b.1 => [hwlog|]. - have /orP[ab1|ba1] := le_total a.1 b.1; first by apply: hwlog. - by rewrite [in RHS]addrC; apply: hwlog => //; rewrite (setIC, setUC). -have := ab0; rewrite subset0. - -set_itvI/=. -rewrite /Order.join /Order.meet/= ?(andbF, orbF)/= ?(meetEtotal, joinEtotal). -rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _. -move=> /eqP/neitvP/=; rewrite bnd_simp/= /d/c (max_idPr _)// => /negP. -rewrite -leNgt le_minl orbC lt_geF//= => {c} {d} a2b1. -have ab i j : i \in `]a.1, a.2] -> j \in `]b.1, b.2] -> i <= j. - by move=> ia jb; rewrite (le_le_trans _ _ a2b1) ?(itvP ia) ?(itvP jb). -have /(congr1 sup) := abx; rewrite sup_setU// ?sup_itv_bounded// => bx. -have /(congr1 inf) := abx; rewrite inf_setU// ?inf_itv_bounded// => ax. -rewrite -{}ax -{x}bx in abx x12 *. -case: ltgtP a2b1 => // a2b1 _; last first. - by rewrite a2b1 [in RHS]addrC subrKA. -exfalso; pose c := (a.2 + b.1) / 2%:R. -have /predeqP/(_ c)[_ /(_ _)/Box[]] := abx. - apply: subset_itv_oo_oc; have := mid_in_itvoo a2b1. - by apply/subitvP; rewrite subitvE ?bnd_simp/= ?ltW. -apply/not_orP; rewrite /= !in_itv/=. -by rewrite lt_geF ?midf_lt//= andbF le_gtF ?midf_le//= ltW. -Qed.*) - Lemma hlength_semi_additive (f : R -> R) : semi_additive (hlength f). Proof. move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->. @@ -379,212 +308,120 @@ Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core. Lemma hlength_interval (F : R -> R) (a b : R) (x y : bool): a <= b -> hlength F [set` (Interval (BSide x a) (BSide y b))] = (F b - F a)%:E. Proof. -move=> ab. -rewrite hlength_itv/= lte_fin lt_neqAle ab andbT. -case: ifPn. - by rewrite EFinN EFinB. -rewrite negbK. -move/eqP ->. -by rewrite subrr. +move=> a_leq_b; rewrite hlength_itv/= lte_fin lt_neqAle a_leq_b andbT. +by have [-> /=|/= a_neq_b] := eqVneq a b; rewrite ?subrr// EFinN EFinB. Qed. -Lemma hlength_semi_additive_helper (F : R -> R) (n : nat) a0 b0 (a b : nat -> R) : - {homo F : x y / x <= y} -> - (forall i, (i < n)%nat -> (a i <= b i)) -> - `]a0, b0] `<=` \big[setU/set0]_(i < n) `] a i, b i]%classic -> - F b0 - F a0 <= \sum_(i < n) (F (b i) - F (a i)). -Proof. -move=> ndF ailtnbi h. -have H1 : (forall k, (k < n)%N -> @measurable itvs_semiRingOfSets `](a k), (b k)]%classic). - by move=> k kn. -have H2 : @measurable itvs_semiRingOfSets `]a0, b0]%classic. - apply is_ocitv. -move/(@content_sub_additive R itvs_semiRingOfSets (@hlength_measure F ndF) - `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) n H1 H2) : h. -rewrite /=. -move=> h. -case (leP a0 b0); last first. - move=> ba. - apply (@le_trans _ _ 0). - rewrite subr_le0. - apply ndF. - by apply ltW. - apply sumr_ge0. - move=> i _. - rewrite subr_ge0. - apply ndF. - by apply ailtnbi. -move=> ab. -move: h. -rewrite hlength_interval//. -move=> h. -rewrite -lee_fin (le_trans h)// -sumEFin. -apply:lee_sum. -move=> i _. -rewrite hlength_interval//. -by apply ailtnbi. -Qed. - -Lemma monotone_right_continuous (a : R) (e : R) (f : R -> R) (f_monotone : {homo f : x y / (x <= y)%R}) (f_right_continuous : (right_continuous f)) : +(* TODO: move? *) +Lemma nondecreasing_right_continuous (a : R) (e : R) (f : R -> R) + (ndf : {homo f : x y / x <= y}) (rcf : (right_continuous f)) : e > 0 -> exists Delta : {posnum R}, f (a + Delta%:num) <= f a + e. Proof. -move: e. -move=> _ /posnumP[ e ]. -move:f_right_continuous. -move=> /(_ a). -move/(@cvg_dist _ [normedModType R of R^o]). -move=> /(_ (e%:num)). -move=> /(_ [gt0 of (e%:num)]). -case. -rewrite /=. -move=> _ /posnumP[delta0 ]. -move=> /(_ (a + delta0%:num / 2)). -rewrite /=. -rewrite opprD. -rewrite addrA. -rewrite subrr. -rewrite distrC. -rewrite subr0. -rewrite ger0_norm //. -rewrite ltr_pdivr_mulr//. -rewrite ltr_pmulr//. -rewrite ltr1n. -move=> /(_ erefl). -rewrite ltr_addl. -rewrite divr_gt0//. -move=> /(_ erefl). -rewrite ler0_norm; last first. - rewrite subr_le0. - rewrite f_monotone//. - by rewrite ler_addl. -rewrite opprB. -rewrite ltr_subl_addl. -move=> H. -exists (PosNum [gt0 of (delta0%:num / 2)]). -rewrite /=. -by apply ltW. +move=> e0. +move: rcf => /(_ a)/(@cvg_dist _ [normedModType R of R^o]). +move=> /(_ _ e0)[] _ /posnumP[delta0] => h. +exists (PosNum [gt0 of (delta0%:num / 2)]) => //=. +move: h => /(_ (a + delta0%:num / 2)) /=. +rewrite opprD addrA subrr distrC subr0 ger0_norm //. +rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n => /(_ erefl). +rewrite ltr_addl divr_gt0// => /(_ erefl). +rewrite ler0_norm; last by rewrite subr_le0 ndf// ler_addl. +by rewrite opprB ltr_subl_addl => fa; exact: ltW. +Qed. + +(* TODO: rename *) +Lemma hlength_semi_additive_helper (f : R -> R) (D : {fset nat}) a0 b0 + (a b : nat -> R) : {homo f : x y / x <= y} -> + (forall i, i \in D -> a i <= b i) -> + `]a0, b0] `<=` \big[setU/set0]_(i <- D) `] a i, b i]%classic -> + f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)). +Proof. +move=> ndf Dab h; have [ab|ab] := leP a0 b0; last first. + apply (@le_trans _ _ 0); first by rewrite subr_le0 ndf// ltW. + by rewrite big_seq sumr_ge0// => i iD; rewrite subr_ge0 ndf// Dab. +have mab k : + [set` D] k -> @measurable itvs_semiRingOfSets `]a k, b k]%classic by []. +move: h; rewrite -bigcup_fset. +move/(@content_sub_fsum R _ (@hlength_measure f ndf) _ [set` D] + `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab + (is_ocitv _ _)) => /=. +rewrite hlength_interval// -lee_fin => /le_trans; apply. +rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq. +by apply: lee_sum => i iD; rewrite hlength_interval// Dab. Qed. -Lemma subset_interval' -(a1 a2 b1 b2: R) (xa ya xb yb: bool): b1 <= a1 -> a2 <= b2 -> (xa <= xb)%O -> (yb <= ya)%O -> -[set` (Interval (BSide xa a1) (BSide ya a2))] `<=` [set` (Interval (BSide xb b1) (BSide yb b2))]. -Proof. -Admitted. - -Lemma subset_interval -(a1 a2 b1 b2 : itv_bound R) : (b1 <= a1)%O -> (a2 <= b2)%O -> [set` (Interval a1 a2)] `<=` [set` (Interval b1 b2)]. -Proof. -Admitted. - Lemma hlength_sigma_sub_additive (f : R -> R) - (f_monotone : {homo f : x y / (x <= y)%R}) (f_right_continuous : right_continuous f) : + (ndf : {homo f : x y / (x <= y)%R}) (rcf : right_continuous f) : sigma_sub_additive (hlength f). Proof. move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE. move=> [a _ <-]; rewrite hlength_itv ?lte_fin/= -EFinB => lebig. case: ifPn => a12; last first. - rewrite nneseries_esum; last first. - by move=> ? _; exact: hlength_ge0'. + rewrite nneseries_esum; last by move=> ? _; exact: hlength_ge0'. by rewrite esum_ge0// => ? _; exact: hlength_ge0'. +wlog wlogh : b A AE lebig / forall n, (b n).1 <= (b n).2. + move=> /= h. + set A' := fun n => if (b n).1 >= (b n).2 then set0 else A n. + set b' := fun n => if (b n).1 >= (b n).2 then (0, 0) else b n. + rewrite [X in (_ <= X)%E](_ : _ = \sum_(n k. + rewrite /= /A' AE; case: ifPn => // bn. + by rewrite set_itv_ge//= bnd_simp -leNgt. + apply (h b'). + - move=> k; rewrite /A'; case: ifPn => // bk. + by rewrite set_itv_ge//= bnd_simp -leNgt /b' bk. + - by rewrite AE /b' (negbTE bk). + - apply: (subset_trans lebig); apply subset_bigcup => k _. + rewrite /A' AE; case: ifPn => bk //. + by rewrite subset0 set_itv_ge//= bnd_simp -leNgt. + - by move=> k; rewrite /b'; case: ifPn => //; rewrite -ltNge => /ltW. apply: lee_adde => e. rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//. apply: le_trans (epsilon_trick _ _ _) => //=; last first. by move=> ?; exact: hlength_ge0'. -have [Delta hDelta] : exists Delta : {posnum R}, f (a.1 + Delta%:num) <= f a.1 + e%:num / 2. - (* by continuity *) - by apply monotone_right_continuous. - -have [delta hdelta] : - exists delta : nat -> {posnum R}, forall i, f ((b i).2 + (delta i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. - suff : forall i, exists deltai : {posnum R}, f ((b i).2 + deltai%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. - by move/choice => -[f' hf']; exists f'. - (* by continuity *) - move=> i. - apply monotone_right_continuous => //. - rewrite divr_gt0 //. - rewrite exprn_gt0//. - -have H1 : `[ a.1 + Delta%:num , a.2] `<=` \bigcup_i `](b i).1, (b i).2 + (delta i)%:num[%classic. +have [c ce] := nondecreasing_right_continuous a.1 ndf rcf [gt0 of e%:num / 2]. +have [d de] : exists d : nat -> {posnum R}, forall i, + f ((b i).2 + (d i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. + suff : forall i, exists di : {posnum R}, + f ((b i).2 + di%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. + by move/choice => -[g hg]; exists g. + move=> k; apply nondecreasing_right_continuous => //. + by rewrite divr_gt0 // exprn_gt0. +have acbd : `[ a.1 + c%:num / 2, a.2] `<=` \bigcup_i `](b i).1, (b i).2 + (d i)%:num[%classic. apply (@subset_trans _ `]a.1, a.2]). - move=> r. - rewrite /=. - rewrite !in_itv/=. - move=> /andP [+ ->]. - rewrite andbT. - apply lt_le_trans. - by rewrite ltr_addl. - apply (subset_trans lebig). - move=> r. - rewrite /bigcup/=. - case. - move=> n _ Anr. - exists n => //. - move: Anr. - rewrite AE /=. - rewrite !in_itv/=. - move=> /andP [-> ]/=. - move/ le_lt_trans. - apply. - by rewrite ltr_addl. -have [n hn] : exists n, `] a.1 + Delta%:num / 2, a.2] `<=` \big[setU/set0]_(i < n) `](b i).1, (b i).2 + (delta i)%:num]%classic. -(* suff : exists n, `[ a.1 + Delta%:num, a.2] `<=` \big[setU/set0]_(i < n) `](b i).1, (b i).2 + (delta i)%:num[%classic. - case=> n hn. - exists n. - apply (@subset_trans _ `[(a.1 + Delta%:num / 4%:R), a.2]). - apply subset_interval => //=. - rewrite bnd_simp. - (*move=> r/=. - rewrite !in_itv/=. - move=> /andP [+ ->]. - rewrite andbT. - move/ ltW. - apply le_trans.*) - rewrite ler_add => //. - (*Unset Printing Notations.*) - rewrite ler_pmul //. - rewrite ler_pinv. - by rewrite ler_nat. - rewrite inE. - rewrite ltr0n. - rewrite andbT. - by rewrite unitf_gt0. - rewrite inE ltr0n andbT. - by rewrite unitf_gt0. - - apply:subset_trans. - apply:subset_trans hn. - apply subset_interval. - - - move=> r/=. -*) - (* by cover_compact *) - admit. - -have H0 : forall n, (b n).1 <= (b n).2. - admit. -have H2 : f a.2 - f (a.1 + Delta%:num) <= \sum_(i < n) (f ((b i).2 + (delta i)%:num) - f (b i).1). - apply: (@hlength_semi_additive_helper f n (a.1 + Delta%:num) a.2 - (fun x => (b x).1) (fun x => (b x).2 + (delta x)%:num)) =>//. - move => i iltnn. - apply (@le_trans _ _ (b i).2). - done. - by rewrite ler_addl. - admit. - -have H3 : (((f a.2 - f (a.1) - e%:num / 2))%:E <= - \sum_(i < n) ((hlength f) ( `](b i).1, (b i).2]%classic)) - + - \sum_(i < n) (f ((b i).2 + (delta i)%:num)%R - f (b i).2)%:E)%E. - admit. -have H4 : (((f a.2 - f (a.1) - e%:num / 2))%:E <= - \sum_(i < n) ((hlength f) ( `](b i).1, (b i).2]%classic)) - + - (e%:num / 2)%:E)%E. - admit. -Admitted. - -Lemma hlength_sigma_finite : sigma_finite [set: itvs] hlength. + move=> r; rewrite /= !in_itv/= => /andP [+ ->]. + by rewrite andbT; apply: lt_le_trans; rewrite ltr_addl. + apply (subset_trans lebig) => r [n _ Anr]; exists n => //. + move: Anr; rewrite AE /= !in_itv/= => /andP [->]/= /le_lt_trans. + by apply; rewrite ltr_addl. +have := @segment_compact _ (a.1 + c%:num / 2) a.2; rewrite compact_cover. +have obd k : [set: nat] k-> open `](b k).1, ((b k).2 + (d k)%:num)[%classic. + by move=> _; exact: interval_open. +move=> /(_ _ _ _ obd acbd){obd acbd}. +case=> X _ acXbd. +rewrite -EFinD. +apply: (@le_trans _ _ (\sum_(i <- X) (hlength f `](b i).1, (b i).2]%classic) + + \sum_(i <- X) (f ((b i).2 + (d i)%:num)%R - f (b i).2)%:E)%E). + apply: (@le_trans _ _ (f a.2 - f (a.1 + c%:num / 2))%:E). + rewrite lee_fin -addrA -opprD ler_sub// (le_trans _ ce)// ndf//. + by rewrite ler_add2l ler_pdivr_mulr// ler_pmulr// ler1n. + apply: (@le_trans _ _ (\sum_(i <- X) (f ((b i).2 + (d i)%:num) - f (b i).1)%:E)%E). + rewrite sumEFin lee_fin hlength_semi_additive_helper//. + by move=> k kX; rewrite (@le_trans _ _ (b k).2)// ler_addl. + apply: subset_trans. + exact/(subset_trans _ acXbd)/subset_itv_oc_cc. + move=> x [k kX] kx; rewrite -bigcup_fset; exists k => //. + by move: x kx; exact: subset_itv_oo_oc. + rewrite addeC -big_split/=; apply: lee_sum => k _. + by rewrite !(EFinB, hlength_interval)// addeA subeK. +rewrite -big_split/= nneseries_esum//; last first. + by move=> k _; rewrite adde_ge0// hlength_ge0'. +rewrite esum_ge//; exists X => //. +rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX. +by rewrite AE lee_add2l// lee_fin ler_subl_addl natrX de. +Qed. + +Lemma hlength_sigma_finite (f : R -> R) : sigma_finite [set: itvs] (hlength f). Proof. exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. @@ -599,1198 +436,10 @@ Qed. Let gitvs := g_measurableType ocitv. -Definition lebesgue_measure : {measure set gitvs -> \bar R} := - Hahn_ext_measure hlength_sigma_sub_additive. +Definition lebesgue_stieltjes_measure (f : R -> R) + (ndf : {homo f : x y / x <= y}) (rcf : right_continuous f) + : {measure set gitvs -> \bar R} := + @Hahn_ext_measure R _ (hlength_measure ndf) (hlength_sigma_sub_additive ndf rcf). End itv_semiRingOfSets. -Arguments lebesgue_measure {R}. -Section lebesgue_measure. -Variable R : realType. -Let gitvs := g_measurableType (@ocitv R). - -Lemma lebesgue_measure_unique (mu : {measure set gitvs -> \bar R}) : - (forall X, ocitv X -> hlength X = mu X) -> - forall X, measurable X -> lebesgue_measure X = mu X. -Proof. -move=> muE X mX; apply: Hahn_ext_unique => //=. -- exact: hlength_sigma_sub_additive. -- exact: hlength_sigma_finite. -Qed. - -End lebesgue_measure. - -Section ps_infty. -Context {T : Type}. -Local Open Scope ereal_scope. - -Inductive ps_infty : set \bar T -> Prop := -| ps_infty0 : ps_infty set0 -| ps_ninfty : ps_infty [set -oo] -| ps_pinfty : ps_infty [set +oo] -| ps_inftys : ps_infty [set -oo; +oo]. - -Lemma ps_inftyP (A : set \bar T) : ps_infty A <-> A `<=` [set -oo; +oo]. -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 measurableTypeR := g_measurableType G. -Let measurableR : set (set R) := @measurable measurableTypeR. - -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 (\bar R) := - isMeasurable.Build _ (Pointed.class _) - emeasurable0 emeasurableC bigcupT_emeasurable. - -End salgebra_ereal. - -Section puncture_ereal_itv. -Variable R : realDomainType. -Implicit Types (y : R) (b : bool). -Local Open Scope ereal_scope. - -Lemma punct_eitv_bnd_pinfty b y : [set` Interval (BSide b y%:E) +oo%O] = - EFin @` [set` Interval (BSide b y) +oo%O] `|` [set +oo]. -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 ?(ltey, leey). -Qed. - -Lemma punct_eitv_ninfty_bnd b y : [set` Interval -oo%O (BSide b y%:E)] = - [set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)]. -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 ?(ltNye, 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. - -Lemma set1_bigcap_oc (R : realType) (r : R) : - [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic. -Proof. -apply/seteqP; split=> [x ->|]. - by move=> i _/=; rewrite in_itv/= lexx ltr_subl_addr ltr_addl invr_gt0 ltr0n. -move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT. -apply/ler_addgt0Pl => e e_gt0; rewrite -ler_subl_addl ltW//. -have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. -rewrite ler_add2l ler_opp2 -lef_pinv ?invrK//; last by rewrite qualifE invr_gt0. -rewrite -addn1 natrD natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. -by rewrite -RfloorE lt_succ_Rfloor. -Qed. - -Section salgebra_R_ssets. -Variable R : realType. - -Definition measurableTypeR := - g_measurableType (@measurable (@itvs_semiRingOfSets R)). - -Definition measurableR : set (set R) := @measurable measurableTypeR. - -HB.instance Definition R_isMeasurable : isMeasurable R := - isMeasurable.Build measurableTypeR (Pointed.class R) - 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]%classic. - by apply: sub_sigma_algebra; apply: is_ocitv. -have pooE (x : R) : `]x, +oo[%classic = \bigcup_i `]x, x + i%:R]%classic. - apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. - by move=> [k _ /=] /itvP->. - move=> xy; exists `|ceil (y - x)|%N => //=. - rewrite in_itv/= xy/= -ler_subl_addl !natr_absz/=. - rewrite ger0_norm ?ceil_ge0 ?subr_ge0//; last exact: ltW. - by rewrite -RceilE Rceil_ge. -have mopoo (x : R) : measurable `]x, +oo[%classic. - by rewrite pooE; exact: bigcup_measurable. -have mnooc (x : R) : measurable `]-oo, x]%classic. - by rewrite -setCitvr; exact/measurableC. -have ooE (a b : R) : `]a, b[%classic = `]a, b]%classic `\ 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[%classic. - by rewrite ooE; exact: measurableD. -have mcc (a b : R) : measurable `[a, b]%classic. - case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU1itv//; apply/measurableU. -have mco (a b : R) : measurable `[a, b[%classic. - 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]%classic `\ 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. - -HB.instance Definition _ := - ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R)). -(* 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_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_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. - -Lemma itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R). -Proof. -rewrite set_itvE predeqE => t; split => /= [|<-//]. -by rewrite lee_pinfty_eq => /eqP. -Qed. - -Lemma itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R). -Proof. -by rewrite set_itvE predeqE => t; split => //=; apply/negP; rewrite -leNgt leey. -Qed. - -Lemma itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R). -Proof. by rewrite set_itvE predeqE => t; split => //= _; rewrite leNye. Qed. - -Lemma itv_oninfty_pinfty : - `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R). -Proof. -rewrite set_itvE predeqE => x; split => /=. -- by move: x => [x| |]; rewrite ?ltxx. -- by move: x => [x h|//|/(_ erefl)]; rewrite ?ltNye. -Qed. - -Lemma emeasurable_itv_bnd_pinfty 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_bnd_pinfty]. -- by case: b; rewrite ?itv_opinfty_pinfty ?itv_cpinfty_pinfty. -- case: b; first by rewrite itv_cninfty_pinfty. - by rewrite itv_oninfty_pinfty; exact/measurableC. -Qed. - -Lemma emeasurable_itv_ninfty_bnd b (y : \bar R) : - measurable [set` Interval -oo%O (BSide b y)]. -Proof. -by rewrite -setCitvr; exact/measurableC/emeasurable_itv_bnd_pinfty. -Qed. - -Definition elebesgue_measure' : set \bar R -> \bar R := - fun S => lebesgue_measure (fine @` (S `\` [set -oo; +oo]%E)). - -Lemma elebesgue_measure'0 : elebesgue_measure' set0 = 0%E. -Proof. by rewrite /elebesgue_measure' set0D image_set0 measure0. Qed. - -Lemma measurable_fine (X : set \bar R) : measurable X -> - measurable [set fine x | x in X `\` [set -oo; +oo]%E]. -Proof. -case => Y mY [X' [ | <-{X} | <-{X} | <-{X} ]]. -- rewrite setU0 => <-{X}. - rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - by move=> [x [[x' Yx' <-{x}/= _ <-//]]]. - by move=> Yr; exists r%:E; split => [|[]//]; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <- _ <-//]|]]]. - by move=> <-; rewrite not_orP => -[]/(_ erefl). - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - move=> [x [[[x' Yx' <-{x} _ <-//]|]]]. - by move=> ->; rewrite not_orP => -[_]/(_ erefl). - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -- rewrite [X in measurable X](_ : _ = Y) // predeqE => r; split. - by rewrite setDUl setDv setU0 => -[_ [[x' Yx' <-]] _ <-]. - by move=> Yr; exists r%:E => //; split => [|[]//]; left; exists r. -Qed. - -Lemma elebesgue_measure'_ge0 X : (0 <= elebesgue_measure' X)%E. -Proof. exact/measure_ge0. Qed. - -Lemma semi_sigma_additive_elebesgue_measure' : - semi_sigma_additive elebesgue_measure'. -Proof. -move=> /= F mF tF mUF; rewrite /elebesgue_measure'. -rewrite [X in lebesgue_measure X](_ : _ = - \bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first. - rewrite predeqE => r; split. - by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x. - by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n. -apply: (@measure_semi_sigma_additive _ _ (@lebesgue_measure R) - (fun n => fine @` (F n `\` [set -oo; +oo]%E))). -- move=> n; have := mF n. - move=> [X mX [X' mX']] XX'Fn. - apply: measurable_fine. - rewrite -XX'Fn. - apply: measurableU; first exact: measurable_EFin. - by case: mX' => //; exact: measurableU. -- move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. - move: tF => /(_ i j Logic.I Logic.I); apply. - suff ab : a = b by exists a; split => //; rewrite ab. - move: a b {Fia Fjb} aoo boo ax bx. - move=> [a| |] [b| |] /=. - + by move=> _ _ -> ->. - + by move=> _; rewrite not_orP => -[_]/(_ erefl). - + by move=> _; rewrite not_orP => -[]/(_ erefl). - + by rewrite not_orP => -[_]/(_ erefl). - + by rewrite not_orP => -[_]/(_ erefl). - + by rewrite not_orP => -[_]/(_ erefl). - + by rewrite not_orP => -[]/(_ erefl). - + by rewrite not_orP => -[]/(_ erefl). - + by rewrite not_orP => -[]/(_ erefl). -- move: mUF. - rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. - - rewrite setU0 => h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-{r}]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[x' Xx' <-]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r. - by exists n => //; exists r%:E => //; split => //; case. - - move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. - by exists n => //; exists r%:E => //; split => //; case. - - (* NB: almost the same as the previous one, factorize?*) - move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. - by exists n => //; exists r%:E => //; split => //; case. - - move=> h. - rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. - move=> -[n _ [x [Fnx xoo <-]]]. - have : (\bigcup_n F n) x by exists n. - by rewrite -h => -[[x' Xx' <-//]|]. - have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. - by exists n => //; exists r%:E => //; split => //; case. -Qed. - -Definition elebesgue_measure_isMeasure : is_measure elebesgue_measure' := - Measure.Axioms elebesgue_measure'0 elebesgue_measure'_ge0 - semi_sigma_additive_elebesgue_measure'. - -Definition elebesgue_measure : {measure set \bar R -> \bar R} := - Measure.Pack _ elebesgue_measure_isMeasure. - -End salgebra_R_ssets. -#[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| - apply: emeasurable_set1] : core. - -Section measurable_fun_measurable. -Local Open Scope ereal_scope. -Variables (T : measurableType) (R : realType) (D : set T) (f : T -> \bar R). -Hypotheses (mD : measurable D) (mf : measurable_fun D f). -Implicit Types y : \bar R. - -Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]). -Proof. -by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv_bnd_pinfty. -Qed. - -Lemma emeasurable_fun_o_infty y : measurable (D `&` [set x | y < f x]). -Proof. -by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv_bnd_pinfty. -Qed. - -Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]). -Proof. -by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv_ninfty_bnd. -Qed. - -Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]). -Proof. -by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv_ninfty_bnd. -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. - by apply: measurableI; [exact: emeasurable_fun_c_infty| - exact: emeasurable_fun_infty_c]. -rewrite predeqE => t; split => [/= [Dt ft]|]. - have [ft0|ft0] := leP 0%R (fine (f t)). - exists `|ceil (fine (f t))|%N => //=; split => //; split. - by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// ler_oppl oppr0. - by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge. - exists `|floor (fine (f t))|%N => //=; split => //; split. - rewrite natr_absz ltr0_norm ?floor_lt0// EFinN. - by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le. - by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). -move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. -by rewrite (lt_le_trans _ nft) ?ltNye//= (le_lt_trans fnt)// ltey. -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]. -Let T := g_measurableType G. - -Lemma measurable_itv_bnd_infty b x : - @measurable T [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 -> - @measurable T [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 : - @measurable (g_measurableType (measurable : set (set (itvs R)))) = - @measurable T. -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]. -Let T := g_measurableType G. - -Lemma measurable_itv_bnd_infty b x : - @measurable T [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 -> - @measurable T [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 : - @measurable (g_measurableType (measurable : set (set (itvs R)))) = - @measurable T. -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]. -Let T := g_measurableType G. - -Lemma measurable_itv_bnd_infty b x : - @measurable T [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 -> - @measurable T [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 : - @measurable (g_measurableType (measurable : set (set (itvs R)))) = - @measurable T. -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]. -Let T := g_measurableType G. - -Local Lemma measurable_itvoo x y : @measurable T `]x, y[%classic. -Proof. by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed. - -Local Lemma measurable_itv_o_infty x : @measurable T `]x, +oo[%classic. -Proof. -rewrite itv_bnd_inftyEbigcup; apply: bigcupT_measurable => i. -exact: measurable_itvoo. -Qed. - -Lemma measurable_itv_bnd_infty b x : - @measurable T [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 : - @measurable T [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 : - @measurable T [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 : - @measurable (g_measurableType (measurable : set (set (itvs R)))) = - @measurable T. -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?(ltNye, 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 /= ltNye. -Qed. - -Lemma eitv_c_infty r : `[r%:E, +oo[%classic = - \bigcap_k `](r - k.+1%:R^-1)%:E, +oo[%classic :> set _. -Proof. -rewrite predeqE => x; split=> [|]. -- move: x => [s /=| _ n _|//]. - + rewrite in_itv /= andbT lee_fin => rs n _ /=. - rewrite in_itv /= andbT lte_fin. - by rewrite ltr_subl_addl (le_lt_trans rs)// ltr_addr invr_gt0. - + by rewrite /= in_itv /= andbT ltey. -- move: x => [s| |/(_ 0%N Logic.I)] //=; last by rewrite in_itv /= leey. - move=> h; rewrite in_itv /= lee_fin leNgt andbT; apply/negP. - move=> /ltr_add_invr[k skr]; have {h} := h k Logic.I. - rewrite /= in_itv /= andbT lte_fin ltNge => /negP; apply. - by rewrite -ler_subl_addr opprK ltW. -Qed. - -Lemma eitv_infty_c r : `]-oo, r%:E]%classic = - \bigcap_k `]-oo, (r%:E + k.+1%:R^-1%:E)]%classic :> set _. -Proof. -rewrite predeqE => x; split=> [|]. -- move: x => [s /=|//|_ n _]. - + rewrite in_itv /= lee_fin => sr n _; rewrite /= in_itv /=. - by rewrite -EFinD lee_fin (le_trans sr)// ler_addl invr_ge0. - + by rewrite /= in_itv /= -EFinD leNye. -- move: x => [s|/(_ 0%N Logic.I)//|]/=; rewrite ?in_itv /= ?leNye//. - move=> h; rewrite lee_fin leNgt; apply/negP => /ltr_add_invr[k rks]. - have {h} := h k Logic.I; rewrite /= in_itv /=. - by rewrite -EFinD lee_fin leNgt => /negP; apply. -Qed. - -Lemma eset1_ninfty : - [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R). -Proof. -rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNye. -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) // ler_oppl oppr0 ler0n. -rewrite ler_oppl -abszN natr_absz gtr0_norm; last first. - by rewrite ltr_oppr oppr0 floor_lt0. -by rewrite mulrNz ler_oppl opprK floor_le. -Qed. - -Lemma eset1_pinfty : - [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). -Proof. -rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltey. -move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. -rewrite andbT lte_fin ltNge. -have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). -by rewrite natr_absz gtr0_norm // ?ceil_ge// ceil_gt0. -Qed. - -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 x, A = `]x, +oo[%classic]. -Let T := g_measurableType G. - -Lemma measurable_set1_ninfty : @measurable T [set -oo]. -Proof. -rewrite eset1_ninfty; apply: (@bigcapT_measurable T) => i. -rewrite -setCitvr; apply: measurableC; rewrite eitv_c_infty. -apply: bigcapT_measurable => j; apply: sub_sigma_algebra. -by exists (- (i%:R + j.+1%:R^-1))%:E; rewrite opprD. -Qed. - -Lemma measurable_set1_pinfty : @measurable T [set +oo]. -Proof. -rewrite eset1_pinfty; apply: bigcapT_measurable => i. -by apply: sub_sigma_algebra; exists i%:R%:E. -Qed. - -Lemma measurableE : emeasurable (measurable : set (set (itvs R))) = @measurable T. -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=> _ [x ->]; rewrite /emeasurable /=; move: x => [r| |]. - + exists `]r, +oo[%classic. - rewrite RGenOInfty.measurableE. - exact: RGenOInfty.measurable_itv_bnd_infty. - by exists [set +oo]; [constructor|rewrite -punct_eitv_bnd_pinfty]. - + exists set0 => //. - by exists set0; [constructor|rewrite setU0 itv_opinfty_pinfty image_set0]. - + exists setT => //; exists [set +oo]; first by constructor. - by rewrite itv_oninfty_pinfty punct_eitv_setTR. -move=> A [B mB [C mC]] <-; apply: measurableU; last first. - case: mC; [by []|exact: measurable_set1_ninfty - |exact: measurable_set1_pinfty|]. - - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. -rewrite RGenOInfty.measurableE in mB. -have smB := smallest_sub _ _ mB. -(* BUG: elim/smB : _. fails !! *) -apply: (smB (@measurable T \o (image^~ EFin))); last first. - move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. - by apply sub_sigma_algebra => /=; exists r%:E. - exact: measurable_set1_pinfty. -split=> /= [|D mD|F mF]; first by rewrite image_set0. -- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. -- by rewrite EFin_bigcup; apply: bigcupT_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 x, A = `[x, +oo[%classic]. -Let T := g_measurableType G. - -Lemma measurable_set1_ninfty : @measurable T [set -oo]. -Proof. -rewrite eset1_ninfty; apply: bigcapT_measurable=> i; rewrite -setCitvr. -by apply: measurableC; apply: sub_sigma_algebra; exists (- i%:R)%:E. -Qed. - -Lemma measurable_set1_pinfty : @measurable T [set +oo]. -Proof. -apply: sub_sigma_algebra; exists +oo; rewrite predeqE => x; split => [->//|/=]. -by rewrite in_itv /= andbT lee_pinfty_eq => /eqP ->. -Qed. - -Lemma measurableE : emeasurable (measurable : set (set (itvs R))) = @measurable T. -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_bnd_pinfty]. - - exists set0 => //; exists [set +oo]; first by constructor. - by rewrite image_set0 set0U itv_cpinfty_pinfty. - - exists setT => //; exists [set -oo; +oo]; first by constructor. - by rewrite itv_cninfty_pinfty setUA punct_eitv_setTL setUCl. -move=> _ [A' mA' [C mC]] <-; apply: measurableU; last first. - case: mC; [by []|exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty|]. - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. -rewrite RGenCInfty.measurableE in mA'. -have smA' := smallest_sub _ _ mA'. -(* BUG: elim/smA' : _. fails !! *) -apply: (smA' (@measurable T \o (image^~ EFin))); last first. - move=> _ [r ->]/=; rewrite EFin_itv_bnd_infty; apply: measurableD. - by apply sub_sigma_algebra => /=; exists r%:E. - exact: measurable_set1_pinfty. -split=> /= [|D mD|F mF]; first by rewrite image_set0. -- rewrite setTD EFin_setC; apply: measurableD; first exact: measurableC. - by apply: measurableU; [exact: measurable_set1_ninfty| - exact: measurable_set1_pinfty]. -- by rewrite EFin_bigcup; apply: bigcupT_measurable => i; exact: mF. -Qed. - -End erealgencinfty. -End ErealGenCInfty. - -Section trace. -Variable (T : Type). -Implicit Types (G : set (set T)) (A D : set T). - -(* intended as a trace sigma-algebra *) -Definition strace G D := [set x `&` D | x in G]. - -Lemma stracexx G D : G D -> strace G D D. -Proof. by rewrite /strace /=; exists D => //; rewrite setIid. Qed. - -Lemma sigma_algebra_strace G D : - sigma_algebra setT G -> sigma_algebra D (strace G D). -Proof. -move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I. -- move=> S [A mA ADS]; have mCA := GC _ mA. - have : strace G D (D `&` ~` A). - by rewrite setIC; exists (setT `\` A) => //; rewrite setTD. - rewrite -setDE => trDA. - have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0. - by rewrite DADS in trDA. -- move=> S mS; have /choice[M GM] : forall n, exists A, G A /\ S n = A `&` D. - by move=> n; have [A mA ADSn] := mS n; exists A. - exists (\bigcup_i (M i)); first by apply GU => i; exact: (GM i).1. - by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2. -Qed. - -End trace. - -Lemma strace_measurable (T : measurableType) (A : set T) : measurable A -> - strace measurable A `<=` measurable. -Proof. by move=> mA=> _ [C mC <-]; apply: measurableI. Qed. - -(* 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 (U : set R) : open U -> measurable U. -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 continuous_measurable_fun (f : R -> R) : continuous f -> - measurable_fun setT f. -Proof. -move=> /continuousP cf; apply: (measurability (RGenOpens.measurableE R)). -move=> _ [_ [a [b ->] <-]]; rewrite setTI. -by apply: open_measurable; exact/cf/interval_open. -Qed. - -End coutinuous_measurable. - -Section standard_measurable_fun. - -Lemma measurable_fun_normr (R : realType) (D : set R) : - 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 ltr_oppr. - - move=> rx /=. - by rewrite ler0_norm 1?ltr_oppr// (le_trans (ltW rx))// ler_oppl 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. - -End standard_measurable_fun. - -Section measurable_fun_realType. -Variables (T : measurableType) (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_itv_o_infty. -rewrite [X in measurable X](_ : _ = \bigcup_(q : rat) - ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))). - apply: bigcupT_measurable_rat => q; apply: measurableI. - - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv. - - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv. -rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]]. - rewrite -ltr_subl_addr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h. - exists r => //; rewrite setIACA setIid; split => //; split => /=. - by rewrite h. - by rewrite ltr_subl_addr addrC -ltr_subl_addr h. -by rewrite ltr_subl_addr=> afg; rewrite (lt_le_trans afg)// addrC ler_add2r ltW. -Qed. - -Lemma measurable_funrM D f (k : R) : measurable_fun D f -> - measurable_fun D (fun x => k * f x). -Proof. -apply: (@measurable_fun_comp _ _ _ ( *%R k)). -by apply: continuous_measurable_fun; apply: mulrl_continuous. -Qed. - -Lemma measurable_funN D f : measurable_fun D f -> measurable_fun D (-%R \o f). -Proof. -move=> mf mD; rewrite (_ : _ \o _ = (fun x => - 1 * f x)). - exact: measurable_funrM. -by under eq_fun do rewrite mulN1r. -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: measurable_funN. -Qed. - -Lemma measurable_fun_exprn D n f : - measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). -Proof. -apply: measurable_fun_comp ((@GRing.exp R)^~ n) _ _ _. -by apply: continuous_measurable_fun; apply: exprn_continuous. -Qed. - -Lemma measurable_fun_sqr D f : - measurable_fun D f -> measurable_fun D (fun x => f x ^+ 2). -Proof. exact: measurable_fun_exprn. Qed. - -Lemma measurable_funM D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g). -Proof. -move=> mf mg mD; 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 => //; last first. - by apply: measurable_funrM => //; exact: measurable_fun_sqr. - apply: measurable_funB => //; last first. - by apply: measurable_funrM => //; exact: measurable_fun_sqr. - apply: measurable_funrM => //. - by apply: measurable_fun_sqr => //; exact: measurable_funD. -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_max D f g : - measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g). -Proof. -move=> mf mg mD; apply (measurability (RGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ = - (D `&` f @^-1` `[x, +oo[) `|` (D `&` g @^-1` `[x, +oo[)); last first. - rewrite predeqE => t /=; split. - by rewrite /= !in_itv /= !andbT le_maxr => -[Dx /orP[|]]; tauto. - by move=> [|]; rewrite !in_itv/= !andbT le_maxr => -[Dx ->]//; rewrite orbT. -by apply: measurableU; [apply: mf|apply: mg] =>//; apply: measurable_itv. -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_lim_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 => lim_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 => lim_sup (h^~ x))}. - move=> t; rewrite inE => Dt; apply/esym/cvg_lim; first exact: Rhausdorff. - 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_ub; [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 --> f x) -> - measurable_fun D f. -Proof. -move=> mf_ f_f; have fE x : D x -> f x = lim_sup (h ^~ x). - move=> Dx; have /cvg_lim <-// := @cvg_sups _ (h ^~ x) (f x) (f_f _ Dx). - exact: Rhausdorff. -apply: (@eq_measurable_fun _ _ D (fun x => lim_sup (h ^~ x))). - by move=> x; rewrite inE => Dx; rewrite -fE. -apply: (@measurable_fun_lim_sup _ h) => // t Dt. -- apply/bounded_fun_has_ubound/(@cvg_seq_bounded _ [normedModType R of R^o]). - by apply/cvg_ex; eexists; exact: f_f. -- apply/bounded_fun_has_lbound/(@cvg_seq_bounded _ [normedModType R of R^o]). - by apply/cvg_ex; eexists; exact: f_f. -Qed. - -End measurable_fun_realType. - -Section standard_emeasurable_fun. -Variable R : realType. - -Lemma measurable_fun_EFin (D : set R) : measurable_fun D EFin. -Proof. -move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. -move=> /= _ [_ [x ->]] <-; move: x => [x| |]; apply: measurableI => //. -- by rewrite preimage_itv_o_infty EFin_itv; exact: measurable_itv. -- by rewrite [X in measurable X](_ : _ = set0)// predeqE. -- by rewrite preimage_EFin_setT. -Qed. - -Lemma measurable_fun_abse (D : set (\bar R)) : measurable_fun D abse. -Proof. -move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. -move=> /= _ [_ [x ->] <-]; move: x => [x| |]. -- rewrite [X in _ @^-1` X](punct_eitv_bnd_pinfty _ x) preimage_setU setIUr. - apply: measurableU; last first. - rewrite preimage_abse_pinfty. - by apply: measurableI => //; exact: measurableU. - apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). - rewrite -[X in measurable X]setTI. - by apply: measurable_fun_normr => //; exact: measurable_itv. - 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. -- by apply: measurableI => //; rewrite itv_opinfty_pinfty preimage_set0. -- apply: measurableI => //; rewrite itv_oninfty_pinfty -preimage_setC. - by apply: measurableC; rewrite preimage_abse_ninfty. -Qed. - -Lemma emeasurable_fun_minus (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_ninfty_bnd. -by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv lee_oppr. -Qed. - -End standard_emeasurable_fun. -#[global] Hint Extern 0 (measurable_fun _ abse) => - solve [exact: measurable_fun_abse] : core. -#[global] Hint Extern 0 (measurable_fun _ EFin) => - solve [exact: measurable_fun_EFin] : core. - -(* NB: real-valued function *) -Lemma EFin_measurable_fun (T : measurableType) (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: measurable_fun_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. - -Section emeasurable_fun. -Local Open Scope ereal_scope. -Variables (T : measurableType) (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_measurable => ? ?; exact/mf/emeasurable_itv_bnd_pinfty. -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_bnd_pinfty. -Qed. - -Lemma emeasurable_fun_max D (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => maxe (f x) (g x)). -Proof. -move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ = - (D `&` f @^-1` `[x, +oo[) `|` (D `&` g @^-1` `[x, +oo[)); last first. - rewrite predeqE => t /=; split. - by rewrite !/= /= !in_itv /= !andbT le_maxr => -[Dx /orP[|]]; - tauto. - by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_maxr; - move=> [Dx ->]//; rewrite orbT. -by apply: measurableU; [exact/mf/emeasurable_itv_bnd_pinfty| - exact/mg/emeasurable_itv_bnd_pinfty]. -Qed. - -Lemma emeasurable_fun_funenng D (f : T -> \bar R) : - measurable_fun D f -> measurable_fun D f^\+. -Proof. -by move=> mf; apply: emeasurable_fun_max => //; apply: measurable_fun_cst. -Qed. - -Lemma emeasurable_fun_funennp D (f : T -> \bar R) : - measurable_fun D f -> measurable_fun D f^\-. -Proof. -move=> mf; apply: emeasurable_fun_max => //; last exact: measurable_fun_cst. -by apply: measurable_fun_comp => //; apply: emeasurable_fun_minus. -Qed. - -Lemma emeasurable_fun_min D (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => mine (f x) (g x)). -Proof. -move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ = - (D `&` f @^-1` `[x, +oo[) `&` (D `&` g @^-1` `[x, +oo[)); last first. - rewrite predeqE => t /=; split. - rewrite !/= !in_itv /= !andbT le_minr => -[Dt /andP[xft xgt]]. - tauto. - move=> []; rewrite !/= !in_itv/= !andbT le_minr=> -[Dt xft [_ xgt]]. - by split => //; rewrite xft xgt. -by apply: measurableI; [exact/mf/emeasurable_itv_bnd_pinfty| - exact/mg/emeasurable_itv_bnd_pinfty]. -Qed. - -Lemma measurable_fun_elim_sup D (f : (T -> \bar R)^nat) : - (forall n, measurable_fun D (f n)) -> - measurable_fun D (fun x => elim_sup (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; 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 --> f x) -> measurable_fun D f. -Proof. -move=> mf_ f_f; have fE x : D x -> f x = elim_sup (f_^~ x). - by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx). -apply: (measurable_fun_ext (fun x => elim_sup (f_ ^~ x))) => //. - by move=> x; rewrite inE => Dx; rewrite fE. -exact: measurable_fun_elim_sup. -Qed. - -End emeasurable_fun. -Arguments emeasurable_fun_cvg {T R D} f_. +Arguments lebesgue_stieltjes_measure {R}.