diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5724ef64c..1aeb19d66 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -54,6 +54,27 @@ - in `normedtype.v`: + lemma `limf_esup_ge0` +- in `normedtype.v`: + + lemma `nbhs_left_ltBl` + + lemma `within_continuous_continuous` + +- in `measure.v`: + + lemma `measurable_fun_set0` + +- in `lebesgue_measure.v`: + + lemmas `measurable_fun_itv_co`, `measurable_fun_itv_oc`, `measurable_fun_itv_cc` + +- in `lebesgue_integral.v`: + + lemma `integral_itv_bndoo` + +- in `ftc.v`: + + lemmas `increasing_image_oo`, `decreasing_image_oo`, + `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, + `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, + + lemma `eq_integral_itv_bounded`. + + lemmas `integration_by_substitution_decreasing`, + `integration_by_substitution_oppr`, + `integration_by_substitution_increasing` ### Changed diff --git a/theories/ftc.v b/theories/ftc.v index 938408668..4e41c0198 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -51,7 +51,7 @@ apply: cvg_at_right_left_dnbhs. by rewrite -EFinD addrAC subrr add0r. have nice_E y : nicely_shrinking y (E y). split=> [n|]; first exact: measurable_itv. - exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n]. + exists (2, fun n => PosNum (d_gt0 n)); split => //= [n z|n]. rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->]. by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. @@ -679,3 +679,332 @@ exact: (derivable_oo_continuous_bnd_within Gab). Qed. End Rintegration_by_parts. + +(* TODO: move to realfun.v? *) +Section integration_by_substitution_preliminaries. +Context {R : realType}. +Notation mu := lebesgue_measure. +Implicit Types (F G f : R -> R) (a b : R). + +Lemma increasing_image_oo F (a b : R) : (a < b)%R -> + {in `[a, b] &, {homo F : x y / (x < y)%R}} -> + F @` `]a, b[ `<=` `]F a, F b[. +Proof. +move=> ab iF ? [x /= xab <-]. +move: xab; rewrite !in_itv/= => /andP[ax xb]. +by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW. +Qed. + +Lemma decreasing_image_oo F (a b : R) : (a < b)%R -> + {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> + F @` `]a, b[ `<=` `]F b, F a[. +Proof. +move=> ab iF ? [x /= xab <-]. +move: xab; rewrite !in_itv/= => /andP[ax xb]. +by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW. +Qed. + +Lemma increasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R -> + {in `[a, b[ &, {homo F : x y / (x < y)%R}} -> + F x @[x --> a^'+] --> F a -> + G x @[x --> (F a)^'+] --> l -> + (G \o F) x @[x --> a^'+] --> l. +Proof. +move=> ab incrF cFa GFa. +apply/cvgrPdist_le => /= e e0. +have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFa] := GFa. +have := cvg_at_right_within cFa. +move=> /cvgrPdist_lt/(_ _ d0)[d' /= d'0 {}cFa]. +near=> t. +apply: GFa; last by apply: incrF; rewrite //in_itv/= ?lexx//; apply/andP; split. +apply: cFa => //=. +rewrite ltr0_norm// ?subr_lt0// opprB. +by near: t; exact: nbhs_right_ltDr. +Unshelve. all: end_near. Qed. + +Lemma increasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R -> + {in `]a, b] &, {homo F : x y / (x < y)%R}} -> + F x @[x --> b^'-] --> F b -> + G x @[x --> (F b)^'-] --> l -> + (G \o F) x @[x --> b^'-] --> l. +Proof. +move=> ab incrF cFb GFb. +apply/cvgrPdist_le => /= e e0. +have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb. +have := cvg_at_left_within cFb. +move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. +near=> t. +apply: GFb; last by apply: incrF; rewrite //in_itv/= ?lexx//; apply/andP; split. +apply: cFb => //=. +rewrite gtr0_norm// ?subr_gt0//. +by near: t; exact: nbhs_left_ltBl. +Unshelve. all: end_near. Qed. + +Lemma decreasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R -> + {in `[a, b[ &, {homo F : x y /~ (x < y)%R}} -> + F x @[x --> a^'+] --> F a -> + G x @[x --> (F a)^'-] --> l -> + (G \o F) x @[x --> a^'+] --> l. +Proof. +move=> ab decrF cFa GFa. +apply/cvgrPdist_le => /= e e0. +have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa. +have := cvg_at_right_within cFa. +move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa]. +near=> t. +apply: GFa; last by apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split. +apply: cFa => //=. +rewrite ltr0_norm// ?subr_lt0// opprB. +by near: t; exact: nbhs_right_ltDr. +Unshelve. all: end_near. Qed. + +Lemma decreasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R -> + {in `]a, b] &, {homo F : x y /~ (x < y)%R}} -> + F x @[x --> b^'-] --> F b -> + G x @[x --> (F b)^'+] --> l -> + (G \o F) x @[x --> b^'-] --> l. +Proof. +move=> ab decrF cFb GFb. +apply/cvgrPdist_le => /= e e0. +have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb. +have := cvg_at_left_within cFb. (* different point from gt0 version *) +move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb]. +near=> t. +apply: GFb; last by apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split. +apply: cFb => //=. +rewrite gtr0_norm// ?subr_gt0//. +by near: t; exact: nbhs_left_ltBl. +Unshelve. all: end_near. Qed. + +End integration_by_substitution_preliminaries. + +Section integration_by_substitution. +Local Open Scope ereal_scope. +Context {R : realType}. +Notation mu := lebesgue_measure. +Implicit Types (F G f : R -> R) (a b : R). + +Lemma integration_by_substitution_decreasing F G a b : (a < b)%R -> + {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> + {in `]a, b[, continuous F^`()} -> + cvg (F^`() x @[x --> a^'+]) -> + cvg (F^`() x @[x --> b^'-]) -> + derivable_oo_continuous_bnd F a b -> + {within `[F b, F a], continuous G} -> + \int[mu]_(x in `[F b, F a]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * - F^`()) x)%:E. +Proof. +move=> ab decrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] Fab cG. +have cF := derivable_oo_continuous_bnd_within Fab. +have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx. +have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. + apply: measurable_funM. + - apply: (measurable_comp (measurable_itv `]F b, F a[)). + + exact: decreasing_image_oo. + + apply: subspace_continuous_measurable_fun => //. + by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. + + apply: subspace_continuous_measurable_fun => //. + by apply: continuous_subspaceW cF; exact/subset_itv_oo_cc. + - apply: subspace_continuous_measurable_fun => //. + by apply: continuous_in_subspaceT => x; rewrite inE/= => /cF'. +have {}mGFF' : measurable_fun `[a, b] ((G \o F) * F^`())%R. + exact: measurable_fun_itv_cc mGFF'. +have intG : mu.-integrable `[F b, F a] (EFin \o G). + by apply: continuous_compact_integrable => //; exact: segment_compact. +pose PG x := parameterized_integral mu (F b) x G. +have PGFbFa : derivable_oo_continuous_bnd PG (F b) (F a). + have [/= dF rF lF] := Fab; split => /=. + - move=> x xFbFa /=. + have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. + apply: (continuous_FTC1 xFa intG _ _).1 => /=. + by move: xFbFa; rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFbFa). + - have := parameterized_integral_continuous FbFa intG. + by move=> /(continuous_within_itvP _ FbFa)[]. + - exact: parameterized_integral_cvg_at_left. +rewrite (@continuous_FTC2 _ _ PG _ _ FbFa cG); last 2 first. +- split. + + move=> x /[dup]xFbFa; rewrite in_itv/= => /andP[Fbx xFa]. + apply: (continuous_FTC1 xFa intG Fbx _).1. + by move: cG => /(continuous_within_itvP _ FbFa)[+ _ _]; exact. + + have := parameterized_integral_continuous FbFa intG. + by move=> /(continuous_within_itvP _ FbFa)[]. + + exact: parameterized_integral_cvg_at_left. +- move=> x xFbFa. + have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. + apply: (continuous_FTC1 xFa _ _ _).2 => //=. + by move: xFbFa; rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFbFa). +set f := fun x => if x == a then r else if x == b then l else F^`() x. +have fE : {in `]a, b[, F^`() =1 f}. + by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF. +have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}. + move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp //; last first. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + by case: Fab => + _ _; exact. + by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo. + have /(@derive_val _ _ _ _ _ -%R) := @is_deriveNid _ _ (PG (F x)) 1%R. + rewrite fctE -derive1E => ->; rewrite mulN1r mulrN; congr -%R. + rewrite derive1_comp; last 2 first. + - by case: Fab => + _ _; exact. + - by case: PGFbFa => [+ _ _]; apply; exact: decreasing_image_oo. + rewrite fE//; congr *%R. + have /[dup]FxFbFa : F x \in `]F b, F a[ by exact: decreasing_image_oo. + rewrite in_itv/= => /andP[FbFx FxFa]. + apply: (continuous_FTC1 FxFa intG FbFx _).2 => //=. + exact: (within_continuous_continuous _ _ FxFbFa). +rewrite -[LHS]oppeK oppeB// addrC. +under eq_integral do rewrite mulrN EFinN. +rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. +- apply/(continuous_within_itvP _ ab); split. + + move=> x xab; apply: continuousM; first apply: continuous_comp. + * by move: cF => /(continuous_within_itvP _ ab)[+ _ _]; exact. + * move/(continuous_within_itvP _ FbFa) : cG => [+ _ _]; apply. + exact: decreasing_image_oo. + * have : -%R F^`() @ x --> (- f x)%R. + by rewrite -fE//; apply: cvgN; exact: cF'. + apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. + apply: (@open_in_nearW _ _ `]a, b[) ; last by rewrite inE. + exact: interval_open. + by move=> z; rewrite inE/= => zab; rewrite fctE fE. + + apply: cvgM. + apply: (decreasing_cvg_at_right_comp ab) => //. + * by move=> x y xab yab; apply: decrF; exact: subset_itv_co_cc. + * by move/continuous_within_itvP : cF => /(_ ab)[]. + * by move/continuous_within_itvP : cG => /(_ FbFa)[]. + rewrite fctE {2}/f eqxx; apply: cvgN. + apply: cvg_trans F'ar; apply: near_eq_cvg. + by near=> z; rewrite fE// in_itv/=; apply/andP; split. + + apply: cvgM. + apply: (decreasing_cvg_at_left_comp ab). + * by move=> //x y xab yab; apply: decrF; apply: subset_itv_oc_cc. + * by move/continuous_within_itvP : cF => /(_ ab)[]. + * by move/continuous_within_itvP : cG => /(_ FbFa)[]. + rewrite fctE {2}/f gt_eqF// eqxx. + apply: cvgN; apply: cvg_trans F'bl; apply: near_eq_cvg. + by near=> z; rewrite fE// in_itv/=; apply/andP; split. +- have [/= dF rF lF] := Fab. + have := derivable_oo_continuous_bnd_within PGFbFa. + move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]; split => /=. + - move=> x xab; apply/derivable1_diffP; apply: differentiable_comp => //. + apply: differentiable_comp; apply/derivable1_diffP. + by case: Fab => + _ _; exact. + by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo. + - apply: cvgN; apply/cvgrPdist_le => /= e e0. + have /cvgrPdist_le/(_ e e0)[d /= d0 {}PGFa] := PGFa. + have := cvg_at_right_within rF. + move/cvgrPdist_lt => /(_ _ d0)[d' /= d'0 {}cFa]. + near=> t. + apply: PGFa; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. + - apply: cvgN; apply/cvgrPdist_le => /= e e0. + have /cvgrPdist_le/(_ e e0)[d /= d0 {}PGFb] := PGFb. + have := cvg_at_left_within lF. + move/cvgrPdist_lt => /(_ _ d0)[d' /= d'0 {}cFb]. + near=> t. + apply: PGFb; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. + apply: cFb => //=. + rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +apply: eq_integral_itv_bounded. +- rewrite mulrN; apply: measurableT_comp => //. + apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. + by move=> x; rewrite inE/= => xab; rewrite !fctE fE. + by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc. +- apply: measurableT_comp => //; apply: measurable_funS mGFF' => //. + exact: subset_itv_oo_cc. +- by move=> x /[!inE] xab; rewrite mulrN !fctE fE. +Unshelve. all: end_near. Qed. + +Lemma integration_by_substitution_oppr G a b : (a < b)%R -> + {within `[(- b)%R, (- a)%R], continuous G} -> + \int[mu]_(x in `[(- b)%R, (- a)%R]) (G x)%:E = + \int[mu]_(x in `[a, b]) ((G \o -%R) x)%:E. +Proof. +move=> ab cG; have Dopp: (@GRing.opp R)^`() = cst (-1)%R. + by apply/funext => z; rewrite derive1E derive_val. +rewrite (@integration_by_substitution_decreasing -%R)//. +- apply: eq_integral => //= x /[!inE] xab; congr (EFin _). + by rewrite !fctE -[RHS]mulr1 derive1E deriveN// opprK derive_val. +- by move=> ? ? _ _; rewrite ltrN2. +- by rewrite Dopp => ? _; exact: cvg_cst. +- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. +- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. +- split => //. + + by rewrite -at_leftN; exact: cvg_at_left_filter. + + by rewrite -at_rightN; exact: cvg_at_right_filter. +Qed. + +Lemma integration_by_substitution_increasing F G a b : (a < b)%R -> + {in `[a, b] &, {homo F : x y / (x < y)%R}} -> + {in `]a, b[, continuous F^`()} -> + cvg (F^`() x @[x --> a^'+]) -> + cvg (F^`() x @[x --> b^'-]) -> + derivable_oo_continuous_bnd F a b -> + {within `[F a, F b], continuous G} -> + \int[mu]_(x in `[F a, F b]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. +Proof. +move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] Fab cG. +transitivity (\int[mu]_(x in `[F a, F b]) (((G \o -%R) \o -%R) x)%:E). + by apply/eq_integral => x ? /=; rewrite opprK. +have FaFb : (F a < F b)%R by rewrite incrF// in_itv/= lexx (ltW ab). +have cGN : {within `[- F b, - F a]%classic%R, continuous (G \o -%R)}. + apply/continuous_within_itvP; [by rewrite ltrN2|split]. + - move=> x /[dup]xab /[!in_itv]/= /andP[ax xb]. + apply: continuous_comp; first exact: continuousN. + - move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; apply. + by rewrite in_itv/= ltrNr xb ltrNl. + - move/(continuous_within_itvP _ FaFb) : cG => [_ _]. + by rewrite /= opprK => /cvg_at_leftNP. + - move/(continuous_within_itvP _ FaFb) : cG => [_ + _]. + by rewrite /= opprK => /cvg_at_rightNP. +rewrite -integration_by_substitution_oppr//. +rewrite (@integration_by_substitution_decreasing (- F)%R); first last. +- exact: cGN. +- split; [|by apply: cvgN; case: Fab..]. + by move=> x xab; apply: derivableN; case: Fab => + _ _; exact. +- apply/cvg_ex; exists (- l)%R. + move/cvgN : F'bl; apply: cvg_trans; apply: near_eq_cvg. + near=> z; rewrite fctE !derive1E deriveN//. + by case: Fab => + _ _; apply; rewrite in_itv/=; apply/andP; split. +- apply/cvg_ex; exists (- r)%R. + move/cvgN : F'ar; apply: cvg_trans; apply: near_eq_cvg. + near=> z; rewrite fctE !derive1E deriveN//. + by case: Fab => + _ _; apply; rewrite in_itv/=; apply/andP; split. +- move=> x xab; rewrite /continuous_at derive1E deriveN; last first. + by case: Fab => + _ _; exact. + rewrite -derive1E. + have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg. + rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//. + by case: Fab => + _ _; apply; near: y; exact: near_in_itv. +- by move=> x y xab yab yx; rewrite ltrN2 incrF. +- by []. +have mGF : measurable_fun `]a, b[ (G \o F). + apply: (@measurable_comp _ _ _ _ _ _ `]F a, F b[%classic) => //. + - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-. + by rewrite incrF ?incrF// in_itv/= ?lexx/= ?(ltW ab)//= ?(ltW ax) ?(ltW xb). + - apply: subspace_continuous_measurable_fun => //. + by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. + - apply: subspace_continuous_measurable_fun => //. + by apply: derivable_within_continuous => x xab; case: Fab => + _ _; exact. +have mF' : measurable_fun `]a, b[ F^`(). + apply: subspace_continuous_measurable_fun => //. + by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'. +rewrite integral_itv_bndoo//; last first. + rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first. + by apply/funext => y; rewrite /= opprK. + apply: measurable_funM => //; apply: measurableT_comp => //. + apply: (@eq_measurable_fun _ _ _ _ _ (- F^`())%R). + move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//. + by case: Fab => + _ _; apply. + exact: measurableT_comp. +rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM. +apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. +- by rewrite opprK -derive1E. +- by case: Fab => + _ _; exact. +Unshelve. all: end_near. Qed. + +End integration_by_substitution. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 2f38b1708..bb0fda01b 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6480,6 +6480,35 @@ move=> mf; have [rb|rb] := leP (BRight r) b. - by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. Qed. +Lemma integral_itv_bndoo (x y : R) (f : R -> R) (b0 b1 : bool) : + measurable_fun `]x, y[ f -> + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = + \int[mu]_(z in `]x, y[) (f z)%:E. +Proof. +have [xy|yx _|-> _] := ltgtP x y; last 2 first. +- rewrite !set_itv_ge ?integral_set0//=. + + by rewrite bnd_simp le_gtF// ltW. + + by move: b0 b1 => [|] [|]; rewrite bnd_simp ?lt_geF// le_gtF// ltW. +- by move: b0 b1 => [|] [|]; rewrite !set_itvE ?integral_set0 ?integral_set1. +move=> mf. +transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E). + case: b1 => //; rewrite -integral_itv_bndo_bndc//. + case: b0 => //. + exact: measurable_fun_itv_co mf. +by case: b0 => //; rewrite -integral_itv_obnd_cbnd. +Qed. + +Lemma eq_integral_itv_bounded (x y : R) (g f : R -> R) (b0 b1 : bool) : + measurable_fun `]x, y[ f -> measurable_fun `]x, y[ g -> + {in `]x, y[, f =1 g} -> + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (g z)%:E. +Proof. +move=> mf mg fg. +rewrite integral_itv_bndoo// (@integral_itv_bndoo _ _ g)//. +by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg. +Qed. + End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 7c79837ee..8689a2529 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -243,6 +243,52 @@ case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. 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)) diff --git a/theories/measure.v b/theories/measure.v index c9238f6ee..a00237c84 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1582,8 +1582,10 @@ apply/seteqP; split=> [t /=| t /= [] [] ->//]. by case: ifPn => ft; [left|right]. Qed. -Lemma measurable_fun_set1 a (f : T1 -> T2) : -measurable_fun (set1 a) f. +Lemma measurable_fun_set0 (f : T1 -> T2) : measurable_fun set0 f. +Proof. by move=> A B _; rewrite set0I. Qed. + +Lemma measurable_fun_set1 a (f : T1 -> T2) : measurable_fun [set a] f. Proof. by move=> ? ? ?; rewrite set1I; case: ifP. Qed. End measurable_fun. diff --git a/theories/normedtype.v b/theories/normedtype.v index 238c5d0a7..e34d9ec5b 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1361,6 +1361,12 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y. Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt. Unshelve. all: by end_near. Qed. +Lemma nbhs_left_ltBl x e : 0 < e -> \forall y \near x^'-, x - y < e. +Proof. +move=> e0; near=> y; rewrite -ltrBrDl ltrNl opprB; near: y. +by apply: nbhs_left_gt; rewrite ltrBlDr ltrDl. +Unshelve. all: by end_near. Qed. + Lemma withinN (A : set R) a : within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)]. Proof. @@ -2181,6 +2187,12 @@ rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|]. by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. Qed. +Lemma within_continuous_continuous {R : realType} a b (f : R -> R) x : (a < b)%R -> + {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}. +Proof. +by move=> ab /continuous_within_itvP-/(_ ab)[+ _] /[swap] xab cf; exact. +Qed. + (* TODO: generalize to R : numFieldType *) Section hausdorff.